AddCommute.neg : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute a b → -(a + b) = -a + -b
AddCommute.add_neg : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute a b → -(a + b) = -a + -b

Commute.inv : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute a b → (a * b)⁻¹ = a⁻¹ * b⁻¹
Commute.mul_inv : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute a b → (a * b)⁻¹ = a⁻¹ * b⁻¹

Exists₂.imp : ∀ {α : Sort u_1} {β : α → Sort u_2} {p q : (a : α) → β a → Prop},
  (∀ (a : α) (b : β a), p a b → q a b) → (∃ a b, p a b) → ∃ a b, q a b
BEx.imp_right : ∀ {α : Sort u_1} {p : α → Prop} {P Q : (x : α) → p x → Prop},
  (∀ (x : α) (h : p x), P x h → Q x h) → (∃ x, ∃ (h : p x), P x h) → ∃ x, ∃ (h : p x), Q x h

imp_or : ∀ {a b c : Prop}, a → b ∨ c ↔ (a → b) ∨ (a → c)
imp_or' : ∀ {a : Sort u_1} {b c : Prop}, (∀ (a : a), b ∨ c) ↔ (∀ (a : a), b) ∨ ∀ (a : a), c

forall₂_imp : ∀ {α : Sort u_1} {β : α → Sort u_2} {p q : (a : α) → β a → Prop},
  (∀ (a : α) (b : β a), p a b → q a b) → (∀ (a : α) (b : β a), p a b) → ∀ (a : α) (b : β a), q a b
BAll.imp_right : ∀ {α : Sort u_1} {p : α → Prop} {P Q : (x : α) → p x → Prop},
  (∀ (x : α) (h : p x), P x h → Q x h) → (∀ (x : α) (h : p x), P x h) → ∀ (x : α) (h : p x), Q x h

max_def : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), max a b = if a ≤ b then b else a
LinearOrder.max_def : ∀ {α : Type u_2} [self : LinearOrder α] (a b : α), max a b = if a ≤ b then b else a

min_def : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), min a b = if a ≤ b then a else b
LinearOrder.min_def : ∀ {α : Type u_2} [self : LinearOrder α] (a b : α), min a b = if a ≤ b then a else b

Bool.coe_false : (false = true) = False
Bool.coe_sort_false : (false = true) = False

Bool.coe_sort_true : (true = true) = True
Bool.coe_true : (true = true) = True

Bool.bool_eq_false : ∀ {b : Bool}, ¬b = true → b = false
Bool.eq_false_of_not_eq_true : ∀ {b : Bool}, ¬b = true → b = false

Function.LeftInverse.rightInverse_of_injective : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α},
  Function.LeftInverse f g → Function.Injective f → Function.RightInverse f g
Function.rightInverse_of_injective_of_leftInverse : ∀ {α : Sort u₁} {β : Sort u₂} {f : α → β} {g : β → α},
  Function.Injective f → Function.LeftInverse f g → Function.RightInverse f g

Quotient.ind₂' : ∀ {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} {p : Quotient s₁ → Quotient s₂ → Prop},
  (∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)) → ∀ (q₁ : Quotient s₁) (q₂ : Quotient s₂), p q₁ q₂
Quotient.inductionOn₂' : ∀ {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β}
  {p : Quotient s₁ → Quotient s₂ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂),
  (∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)) → p q₁ q₂

Subtype.val_prop : ∀ {α : Type u_1} {S : Set α} (a : { a // a ∈ S }), ↑a ∈ S
Subtype.coe_prop : ∀ {α : Type u_1} {S : Set α} (a : { a // a ∈ S }), ↑a ∈ S

Option.casesOn'_some : ∀ {α : Type u_1} {β : Type u_2} (x : β) (f : α → β) (a : α), (some a).casesOn' x f = f a
Option.casesOn'_coe : ∀ {α : Type u_1} {β : Type u_2} (x : β) (f : α → β) (a : α), (some a).casesOn' x f = f a

lt_of_le_of_lt' : ∀ {α : Type u_2} [inst : Preorder α] {a b c : α}, b ≤ c → a < b → a < c
lt_of_lt_of_le : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a < b → b ≤ c → a < c

Ne.lt_of_le : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≠ b → a ≤ b → a < b
lt_of_le_of_ne : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → a ≠ b → a < b

lt_of_lt_of_le' : ∀ {α : Type u_2} [inst : Preorder α] {a b c : α}, b < c → a ≤ b → a < c
lt_of_le_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a ≤ b → b < c → a < c

Ne.lt_of_le' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, b ≠ a → a ≤ b → a < b
lt_of_le_of_ne' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≠ a → a < b

lt_trans' : ∀ {α : Type u_2} [inst : Preorder α] {a b c : α}, b < c → a < b → a < c
lt_trans : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a < b → b < c → a < c

left_or_right_lt_sup : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ≠ b → a < a ⊔ b ∨ b < a ⊔ b
Ne.lt_sup_or_lt_sup : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ≠ b → a < a ⊔ b ∨ b < a ⊔ b

Ne.inf_lt_or_inf_lt : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ≠ b → a ⊓ b < a ∨ a ⊓ b < b
inf_lt_left_or_right : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ≠ b → a ⊓ b < a ∨ a ⊓ b < b

sdiff_eq_left : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x \ y = x ↔ Disjoint x y
sdiff_eq_self_iff_disjoint' : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x \ y = x ↔ Disjoint x y

Set.not_subset_iff_exists_mem_not_mem : ∀ {α : Type u_1} {s t : Set α}, ¬s ⊆ t ↔ ∃ x ∈ s, x ∉ t
Set.not_subset : ∀ {α : Type u} {s t : Set α}, ¬s ⊆ t ↔ ∃ a ∈ s, a ∉ t

Set.inter_nonempty_iff_exists_left : ∀ {α : Type u} {s t : Set α}, (s ∩ t).Nonempty ↔ ∃ x ∈ s, x ∈ t
Set.inter_nonempty : ∀ {α : Type u} {s t : Set α}, (s ∩ t).Nonempty ↔ ∃ x ∈ s, x ∈ t

Set.mem_of_mem_of_subset : ∀ {α : Type u} {x : α} {s t : Set α}, x ∈ s → s ⊆ t → x ∈ t
Set.mem_of_subset_of_mem : ∀ {α : Type u} {s₁ s₂ : Set α} {a : α}, s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂

Set.Nonempty.eq_univ : ∀ {α : Type u} {s : Set α} [Subsingleton α], s.Nonempty → s = Set.univ
Subsingleton.eq_univ_of_nonempty : ∀ {α : Type u_1} [Subsingleton α] {s : Set α}, s.Nonempty → s = Set.univ

Set.setOf_eq_eq_singleton : ∀ {α : Type u} {a : α}, {n | n = a} = {a}
Set.set_compr_eq_eq_singleton : ∀ {α : Type u} {a : α}, {b | b = a} = {a}

Equiv.optionEquivSumPUnit_coe : ∀ {α : Type u_4} (a : α), (Equiv.optionEquivSumPUnit α) (some a) = Sum.inl a
Equiv.optionEquivSumPUnit_some : ∀ {α : Type u_4} (a : α), (Equiv.optionEquivSumPUnit α) (some a) = Sum.inl a

Equiv.optionSubtype_symm_apply_apply_some : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (x : β)
  (e : α ≃ { y // y ≠ x }) (a : α), ↑((Equiv.optionSubtype x).symm e) (some a) = ↑(e a)
Equiv.optionSubtype_symm_apply_apply_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (x : β)
  (e : α ≃ { y // y ≠ x }) (a : α), ↑((Equiv.optionSubtype x).symm e) (some a) = ↑(e a)

Set.pi_univ_ite : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Set ι) [inst : DecidablePred fun x => x ∈ s]
  (t : (i : ι) → Set (α i)), (Set.univ.pi fun i => if i ∈ s then t i else Set.univ) = s.pi t
Set.univ_pi_ite : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Set ι) [inst : DecidablePred fun x => x ∈ s]
  (t : (i : ι) → Set (α i)), (Set.univ.pi fun i => if i ∈ s then t i else Set.univ) = s.pi t

Set.subset_prod : ∀ {α : Type u_1} {β : Type u_2} {s : Set (α × β)}, s ⊆ (Prod.fst '' s) ×ˢ (Prod.snd '' s)
Set.subset_fst_image_prod_snd_image : ∀ {α : Type u_1} {β : Type u_2} {s : Set (α × β)},
  s ⊆ (Prod.fst '' s) ×ˢ (Prod.snd '' s)

Set.Nontrivial.offDiag_nonempty : ∀ {α : Type u_1} {s : Set α}, s.Nontrivial → s.offDiag.Nonempty
Set.Subsingleton.offDiag_eq_empty : ∀ {α : Type u_1} {s : Set α}, s.Nontrivial → s.offDiag.Nonempty

mul_div : ∀ {G : Type u_3} [inst : DivInvMonoid G] (a b c : G), a * (b / c) = a * b / c
mul_div_assoc' : ∀ {G : Type u_3} [inst : DivInvMonoid G] (a b c : G), a * (b / c) = a * b / c

add_sub : ∀ {G : Type u_3} [inst : SubNegMonoid G] (a b c : G), a + (b - c) = a + b - c
add_sub_assoc' : ∀ {G : Type u_3} [inst : SubNegMonoid G] (a b c : G), a + (b - c) = a + b - c

Nat.not_even_two_mul_add_one : ∀ (n : ℕ), ¬Even (2 * n + 1)
Nat.not_even_bit1 : ∀ (n : ℕ), ¬Even (2 * n + 1)

Function.Involutive.iterate_bit0 : ∀ {α : Type u_4} {f : α → α}, Function.Involutive f → ∀ (n : ℕ), f^[2 * n] = id
Function.Involutive.iterate_two_mul : ∀ {α : Type u_4} {f : α → α}, Function.Involutive f → ∀ (n : ℕ), f^[2 * n] = id

invertible_unique : ∀ {α : Type u} [inst : Monoid α] (a b : α) [inst_1 : Invertible a] [inst_2 : Invertible b],
  a = b → ⅟ a = ⅟ b
Invertible.congr : ∀ {α : Type u} [inst : Monoid α] (a b : α) [inst_1 : Invertible a] [inst_2 : Invertible b],
  a = b → ⅟ a = ⅟ b

mul_le_mul_of_nonneg_of_nonpos' : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b c d : R}
  [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R],
  c ≤ a → b ≤ d → 0 ≤ a → d ≤ 0 → a * b ≤ c * d
mul_le_mul_of_nonpos_of_nonneg' : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b c d : R}
  [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R],
  c ≤ a → b ≤ d → 0 ≤ a → d ≤ 0 → a * b ≤ c * d

RelIso.eq_iff_eq : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) {a b : α},
  f a = f b ↔ a = b
RelIso.apply_eq_iff_eq : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) {x y : α},
  f x = f y ↔ x = y

OrderHomClass.monotone : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : FunLike F α β] [OrderHomClass F α β] (f : F), Monotone ⇑f
OrderHomClass.mono : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : FunLike F α β] [OrderHomClass F α β] (f : F), Monotone ⇑f

Option.map₂_some_some : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β),
  Option.map₂ f (some a) (some b) = some (f a b)
Option.map₂_coe_coe : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β),
  Option.map₂ f (some a) (some b) = some (f a b)

Mathlib.Meta.Positivity.lt_of_le_of_ne' : ∀ {A : Type u_1} {a b : A} [inst : PartialOrder A], a ≤ b → b ≠ a → a < b
lt_of_le_of_ne' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≠ a → a < b

Int.IsUnit.natAbs_eq : ∀ {u : ℤ}, IsUnit u → u.natAbs = 1
Int.natAbs_of_isUnit : ∀ {u : ℤ}, IsUnit u → u.natAbs = 1

Nonneg.pow_nonneg : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : Preorder α] [ZeroLEOneClass α] [PosMulMono α]
  {a : α}, 0 ≤ a → ∀ (n : ℕ), 0 ≤ a ^ n
pow_nonneg : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [ZeroLEOneClass M₀]
  [PosMulMono M₀], 0 ≤ a → ∀ (n : ℕ), 0 ≤ a ^ n

Nonneg.coe_nsmul : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddLeftMono α] (n : ℕ)
  (a : { x // 0 ≤ x }), ↑(n • a) = n • ↑a
Nonneg.nsmul_coe : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddLeftMono α] (n : ℕ)
  (r : { x // 0 ≤ x }), ↑(n • r) = n • ↑r

Mathlib.Tactic.Ring.natCast_add : ∀ {R : Type u_1} [inst : CommSemiring R] {b₁ b₂ : R} {a₁ a₂ : ℕ},
  ↑a₁ = b₁ → ↑a₂ = b₂ → ↑(a₁ + a₂) = b₁ + b₂
Mathlib.Tactic.Ring.inv_add : ∀ {R : Type u_1} [inst : CommSemiring R] {b₁ b₂ : R} {a₁ a₂ : ℕ},
  ↑a₁ = b₁ → ↑a₂ = b₂ → ↑(a₁ + a₂) = b₁ + b₂

Set.union_iInter : ∀ {β : Type u_2} {ι : Sort u_5} (s : Set β) (t : ι → Set β), s ∪ ⋂ i, t i = ⋂ i, s ∪ t i
Set.union_distrib_iInter_left : ∀ {α : Type u_1} {ι : Sort u_5} (s : ι → Set α) (t : Set α), t ∪ ⋂ i, s i = ⋂ i, t ∪ s i

Set.union_distrib_iInter₂_right : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} (s : (i : ι) → κ i → Set α)
  (t : Set α), (⋂ i, ⋂ j, s i j) ∪ t = ⋂ i, ⋂ j, s i j ∪ t
Set.iInter₂_union : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} (s : (i : ι) → κ i → Set α) (t : Set α),
  (⋂ i, ⋂ j, s i j) ∪ t = ⋂ i, ⋂ j, s i j ∪ t

Set.iInter_union : ∀ {β : Type u_2} {ι : Sort u_5} (s : ι → Set β) (t : Set β), (⋂ i, s i) ∪ t = ⋂ i, s i ∪ t
Set.union_distrib_iInter_right : ∀ {α : Type u_1} {ι : Sort u_5} (s : ι → Set α) (t : Set α),
  (⋂ i, s i) ∪ t = ⋂ i, s i ∪ t

Set.union_distrib_iInter₂_left : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} (s : Set α)
  (t : (i : ι) → κ i → Set α), s ∪ ⋂ i, ⋂ j, t i j = ⋂ i, ⋂ j, s ∪ t i j
Set.union_iInter₂ : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} (s : Set α) (t : (i : ι) → κ i → Set α),
  s ∪ ⋂ i, ⋂ j, t i j = ⋂ i, ⋂ j, s ∪ t i j

Set.dual_ordConnected_iff : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α},
  (⇑OrderDual.ofDual ⁻¹' s).OrdConnected ↔ s.OrdConnected
Set.ordConnected_dual : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α},
  (⇑OrderDual.ofDual ⁻¹' s).OrdConnected ↔ s.OrdConnected

leOnePart_le_one' : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a : α}, a⁻ᵐ ≤ 1 ↔ a⁻¹ ≤ 1
leOnePart_le_one : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a : α}, a⁻ᵐ ≤ 1 ↔ a⁻¹ ≤ 1

negPart_nonpos : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α}, a⁻ ≤ 0 ↔ -a ≤ 0
negPart_nonpos' : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α}, a⁻ ≤ 0 ↔ -a ≤ 0

LinearEquiv.coe_toLinearMap : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_6} {M₂ : Type u_8} [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : _root_.Module R M}
  {module_S_M₂ : _root_.Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'}
  {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂), ⇑↑e = ⇑e
LinearEquiv.coe_coe : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_6} {M₂ : Type u_8} [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : _root_.Module R M}
  {module_S_M₂ : _root_.Module S M₂} {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'}
  {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂), ⇑↑e = ⇑e

Set.image2_sInter_left_subset : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (S : Set (Set α)) (t : Set β)
  (f : α → β → γ), Set.image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, Set.image2 f s t
Set.image2_sInter_subset_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (S : Set (Set α))
  (t : Set β), Set.image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, Set.image2 f s t

Set.image2_sInter_subset_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : Set α)
  (T : Set (Set β)), Set.image2 f s (⋂₀ T) ⊆ ⋂ t ∈ T, Set.image2 f s t
Set.image2_sInter_right_subset : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Set α) (S : Set (Set β))
  (f : α → β → γ), Set.image2 f t (⋂₀ S) ⊆ ⋂ s ∈ S, Set.image2 f t s

Subgroup.map_inf_eq : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H K : Subgroup G)
  (f : G →* N), Function.Injective ⇑f → Subgroup.map f (H ⊓ K) = Subgroup.map f H ⊓ Subgroup.map f K
Subgroup.map_inf : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H K : Subgroup G) (f : G →* N),
  Function.Injective ⇑f → Subgroup.map f (H ⊓ K) = Subgroup.map f H ⊓ Subgroup.map f K

AddSubgroup.map_inf : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H K : AddSubgroup G)
  (f : G →+ N), Function.Injective ⇑f → AddSubgroup.map f (H ⊓ K) = AddSubgroup.map f H ⊓ AddSubgroup.map f K
AddSubgroup.map_inf_eq : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H K : AddSubgroup G)
  (f : G →+ N), Function.Injective ⇑f → AddSubgroup.map f (H ⊓ K) = AddSubgroup.map f H ⊓ AddSubgroup.map f K

Multiset.induction_on : ∀ {α : Type u_1} {p : Multiset α → Prop} (s : Multiset α),
  p 0 → (∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)) → p s
Multiset.induction : ∀ {α : Type u_1} {p : Multiset α → Prop},
  p 0 → (∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)) → ∀ (s : Multiset α), p s

Multiset.strongDownwardInduction_eq : ∀ {α : Type u_1} {p : Multiset α → Sort u_3} {n : ℕ}
  (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁) (s : Multiset α),
  Multiset.strongDownwardInduction H s = H s fun {t₂} ht _hst => Multiset.strongDownwardInduction H t₂ ht
Multiset.strongDownwardInduction.eq_def : ∀ {α : Type u_1} {p : Multiset α → Sort u_3} {n : ℕ}
  (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁) (s : Multiset α),
  Multiset.strongDownwardInduction H s = H s fun {t} ht _h => Multiset.strongDownwardInduction H t ht

Multiset.strongInductionOn.eq_def : ∀ {α : Type u_1} {p : Multiset α → Sort u_3} (s : Multiset α)
  (ih : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s),
  s.strongInductionOn ih = ih s fun t _h => t.strongInductionOn ih
Multiset.strongInductionOn_eq : ∀ {α : Type u_1} {p : Multiset α → Sort u_3} (s : Multiset α)
  (H : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s),
  s.strongInductionOn H = H s fun t _h => t.strongInductionOn H

Multiset.ext'_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α},
  s = t ↔ ∀ (a : α), Multiset.count a s = Multiset.count a t
Multiset.ext : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α},
  s = t ↔ ∀ (a : α), Multiset.count a s = Multiset.count a t

Multiset.sub_add_cancel : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, t ≤ s → s - t + t = s
Multiset.add_sub_cancel : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, t ≤ s → s - t + t = s

List.take_one_drop_eq_of_lt_length : ∀ {α : Type u} {l : List α} {n : ℕ} (h : n < l.length),
  List.take 1 (List.drop n l) = [l.get ⟨n, h⟩]
List.take_one_drop_eq_of_lt_length : ∀ {α : Type u} {l : List α} {n : ℕ} (h : n < l.length),
  List.take 1 (List.drop n l) = [l.get ⟨n, h⟩]

Multiset.Nodup.inter : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α} (t : Multiset α),
  s.Nodup → (s ∩ t).Nodup
Multiset.Nodup.inter_left : ∀ {α : Type u_1} {s : Multiset α} [inst : DecidableEq α] (t : Multiset α),
  s.Nodup → (s ∩ t).Nodup

Finset.cons_induction : ∀ {α : Type u_3} {motive : Finset α → Prop},
  motive ∅ → (∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)) → ∀ (s : Finset α), motive s
Finset.cons_induction_on : ∀ {α : Type u_3} {motive : Finset α → Prop} (s : Finset α),
  motive ∅ → (∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)) → motive s

Finset.induction_on : ∀ {α : Type u_3} {motive : Finset α → Prop} [inst : DecidableEq α] (s : Finset α),
  motive ∅ → (∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s)) → motive s
Finset.induction : ∀ {α : Type u_3} {motive : Finset α → Prop} [inst : DecidableEq α],
  motive ∅ → (∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s)) → ∀ (s : Finset α), motive s

Finset.union_sdiff_self : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∪ t) \ t = s \ t
Finset.union_sdiff_right : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∪ t) \ t = s \ t

Finset.exists_mem_ne : ∀ {α : Type u_1} {s : Finset α}, 1 < s.card → ∀ (a : α), ∃ b ∈ s, b ≠ a
Finset.exists_ne_of_one_lt_card : ∀ {α : Type u_1} {s : Finset α}, 1 < s.card → ∀ (a : α), ∃ b ∈ s, b ≠ a

Finset.biUnion_subset : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [inst : DecidableEq β]
  {s' : Finset β}, s.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s'
Finset.biUnion_subset_iff_forall_subset : ∀ {α : Type u_4} {β : Type u_5} [inst : DecidableEq β] {s : Finset α}
  {t : Finset β} {f : α → Finset β}, s.biUnion f ⊆ t ↔ ∀ x ∈ s, f x ⊆ t

Fin.succAbove_zero_apply : ∀ {n : ℕ} (i : Fin n), Fin.succAbove 0 i = i.succ
Fin.zero_succAbove : ∀ {n : ℕ} (i : Fin n), Fin.succAbove 0 i = i.succ

Fin.succAbove_inj : ∀ {n : ℕ} {p : Fin (n + 1)} {i j : Fin n}, p.succAbove i = p.succAbove j ↔ i = j
Fin.succAbove_right_inj : ∀ {n : ℕ} {p : Fin (n + 1)} {i j : Fin n}, p.succAbove i = p.succAbove j ↔ i = j

Submodule.subtype_injective : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  {module_M : _root_.Module R M} (p : Submodule R M), Function.Injective ⇑p.subtype
Submodule.injective_subtype : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  {module_M : _root_.Module R M} (p : Submodule R M), Function.Injective ⇑p.subtype

NonUnitalSubring.mem_carrier : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : NonUnitalSubring R} {x : R},
  x ∈ s.toNonUnitalSubsemiring ↔ x ∈ s
NonUnitalSubring.mem_toNonUnitalSubsemiring : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : NonUnitalSubring R}
  {x : R}, x ∈ s.toNonUnitalSubsemiring ↔ x ∈ s

Finset.exists_not_mem : ∀ {α : Type u} [Infinite α] (s : Finset α), ∃ a, a ∉ s
Infinite.exists_not_mem_finset : ∀ {α : Type u_1} [Infinite α] (s : Finset α), ∃ x, x ∉ s

RingHom.closure_preimage_le : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) (s : Set S),
  Subring.closure (⇑f ⁻¹' s) ≤ Subring.comap f (Subring.closure s)
Subring.closure_preimage_le : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) (s : Set S),
  Subring.closure (⇑f ⁻¹' s) ≤ Subring.comap f (Subring.closure s)

NonUnitalAlgHom.prod_toFun : ∀ {R : Type u} [inst : Monoid R] {A : Type v} {B : Type w} {C : Type w₁}
  [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B]
  [inst_4 : NonUnitalNonAssocSemiring C] [inst_5 : DistribMulAction R B] [inst_6 : DistribMulAction R C]
  (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) (i : A), (f.prod g) i = Pi.prod (⇑f) (⇑g) i
NonUnitalAlgHom.prod_apply : ∀ {R : Type u} [inst : Monoid R] {A : Type v} {B : Type w} {C : Type w₁}
  [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B]
  [inst_4 : NonUnitalNonAssocSemiring C] [inst_5 : DistribMulAction R B] [inst_6 : DistribMulAction R C]
  (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) (i : A), (f.prod g) i = Pi.prod (⇑f) (⇑g) i

NonUnitalAlgHom.snd_apply : ∀ (R : Type u) [inst : Monoid R] (A : Type v) (B : Type w)
  [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B]
  [inst_4 : DistribMulAction R B] (self : A × B), (NonUnitalAlgHom.snd R A B) self = self.2
NonUnitalAlgHom.snd_toFun : ∀ (R : Type u) [inst : Monoid R] (A : Type v) (B : Type w)
  [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B]
  [inst_4 : DistribMulAction R B] (self : A × B), (NonUnitalAlgHom.snd R A B) self = self.2

NonUnitalAlgHom.fst_toFun : ∀ (R : Type u) [inst : Monoid R] (A : Type v) (B : Type w)
  [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B]
  [inst_4 : DistribMulAction R B] (self : A × B), (NonUnitalAlgHom.fst R A B) self = self.1
NonUnitalAlgHom.fst_apply : ∀ (R : Type u) [inst : Monoid R] (A : Type v) (B : Type w)
  [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B]
  [inst_4 : DistribMulAction R B] (self : A × B), (NonUnitalAlgHom.fst R A B) self = self.1

Submodule.map_comap_eq_of_le : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : _root_.Module R M]
  [inst_5 : _root_.Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_10} [inst_6 : FunLike F M M₂]
  [inst_7 : SemilinearMapClass F τ₁₂ M M₂] [inst_8 : RingHomSurjective τ₁₂] {f : F} {p : Submodule R₂ M₂},
  p ≤ LinearMap.range f → Submodule.map f (Submodule.comap f p) = p
Submodule.map_comap_eq_self : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : _root_.Module R M]
  [inst_5 : _root_.Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_10} [inst_6 : FunLike F M M₂]
  [inst_7 : SemilinearMapClass F τ₁₂ M M₂] [inst_8 : RingHomSurjective τ₁₂] {f : F} {q : Submodule R₂ M₂},
  q ≤ LinearMap.range f → Submodule.map f (Submodule.comap f q) = q

Antisymmetrization.ind : ∀ {α : Type u_1} (r : α → α → Prop) [inst : IsPreorder α r]
  {p : Antisymmetrization α r → Prop}, (∀ (a : α), p (toAntisymmetrization r a)) → ∀ (q : Antisymmetrization α r), p q
Antisymmetrization.induction_on : ∀ {α : Type u_1} (r : α → α → Prop) [inst : IsPreorder α r]
  {p : Antisymmetrization α r → Prop} (a : Antisymmetrization α r), (∀ (a : α), p (toAntisymmetrization r a)) → p a

WCovBy.of_image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a b : α} (f : α ↪o β),
  f a ⩿ f b → a ⩿ b
OrderEmbedding.wcovBy_of_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β)
  {x y : α}, f x ⩿ f y → x ⩿ y

CovBy.of_image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a b : α} (f : α ↪o β),
  f a ⋖ f b → a ⋖ b
OrderEmbedding.covBy_of_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β)
  {x y : α}, f x ⋖ f y → x ⋖ y

Set.Ico_succ_right_eq_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Set.Ico a (Order.succ b) = Set.Icc a b
Order.Ico_succ_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Set.Ico a (Order.succ b) = Set.Icc a b

Set.Iio_succ_eq_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (b : α),
  Set.Iio (Order.succ b) = Set.Iic b
Order.Iio_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a : α),
  Set.Iio (Order.succ a) = Set.Iic a

Set.Ioi_pred_eq_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α] (a : α),
  Set.Ioi (Order.pred a) = Set.Ici a
Order.Ioi_pred : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α] (a : α),
  Set.Ioi (Order.pred a) = Set.Ici a

Set.Ioo_succ_right_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Set.Ioo a (Order.succ b) = Set.Ioc a b
Order.Ioo_succ_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Set.Ioo a (Order.succ b) = Set.Ioc a b

Set.Ioo_pred_left_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α] (a b : α),
  Set.Ioo (Order.pred a) b = Set.Ico a b
Order.Ioo_pred_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α] (a b : α),
  Set.Ioo (Order.pred a) b = Set.Ico a b

Set.Ioi_pred_eq_Ici_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a : α},
  ¬IsMin a → Set.Ioi (Order.pred a) = Set.Ici a
Order.Ioi_pred_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a : α},
  ¬IsMin a → Set.Ioi (Order.pred a) = Set.Ici a

Set.Iio_succ_eq_Iic_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {b : α},
  ¬IsMax b → Set.Iio (Order.succ b) = Set.Iic b
Order.Iio_succ_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a : α},
  ¬IsMax a → Set.Iio (Order.succ a) = Set.Iic a

Set.Ioc_pred_left_eq_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α] (a b : α),
  Set.Ioc (Order.pred a) b = Set.Icc a b
Order.Ioc_pred_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α] (a b : α),
  Set.Ioc (Order.pred a) b = Set.Icc a b

Finset.nonempty_Ioi : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α],
  (Finset.Ioi a).Nonempty ↔ ¬IsMax a
Finset.Ioi_nonempty : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α],
  (Finset.Ioi a).Nonempty ↔ ¬IsMax a

Finset.nonempty_Iio : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α],
  (Finset.Iio a).Nonempty ↔ ¬IsMin a
Finset.Iio_nonempty : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α],
  (Finset.Iio a).Nonempty ↔ ¬IsMin a

Encodable.encodek₂ : ∀ {α : Type u_1} [inst : Encodable α] (a : α), Encodable.decode₂ α (Encodable.encode a) = some a
Encodable.decode₂_encode : ∀ {α : Type u_1} [inst : Encodable α] (a : α),
  Encodable.decode₂ α (Encodable.encode a) = some a

Part.pure_eq_some : ∀ {α : Type u_1} (a : α), pure a = Part.some a
Part.ret_eq_some : ∀ {α : Type u_1} (a : α), pure a = Part.some a

AddSubgroup.zmultiples_one_eq_top : AddSubgroup.zmultiples 1 = ⊤
Int.zmultiples_one : AddSubgroup.zmultiples 1 = ⊤

finprod_eq_prod_of_mulSupport_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) {s : Finset α},
  Function.mulSupport f ⊆ ↑s → ∏ᶠ (i : α), f i = ∏ i ∈ s, f i
finprod_eq_finset_prod_of_mulSupport_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M)
  {s : Finset α}, Function.mulSupport f ⊆ ↑s → ∏ᶠ (i : α), f i = ∏ i ∈ s, f i

finsum_eq_sum_of_support_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) {s : Finset α},
  Function.support f ⊆ ↑s → ∑ᶠ (i : α), f i = ∑ i ∈ s, f i
finsum_eq_finset_sum_of_support_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M)
  {s : Finset α}, Function.support f ⊆ ↑s → ∑ᶠ (i : α), f i = ∑ i ∈ s, f i

Nat.cast_prod : ∀ {α : Type u_3} {β : Type u_4} [inst : CommSemiring β] (f : α → ℕ) (s : Finset α),
  ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
Finset.prod_natCast : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommSemiring α] (s : Finset ι) (f : ι → ℕ),
  ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)

Sym.eq_replicate_iff : ∀ {α : Type u_1} {n : ℕ} {s : Sym α n} {a : α}, s = Sym.replicate n a ↔ ∀ b ∈ s, b = a
Sym.eq_replicate : ∀ {α : Type u_1} {a : α} {n : ℕ} {s : Sym α n}, s = Sym.replicate n a ↔ ∀ b ∈ s, b = a

LinearMap.coprod_map_prod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : _root_.Module R M]
  [inst_5 : _root_.Module R M₂] [inst_6 : _root_.Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (S : Submodule R M)
  (S' : Submodule R M₂), Submodule.map (f.coprod g) (S.prod S') = Submodule.map f S ⊔ Submodule.map g S'
LinearMap.map_coprod_prod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : _root_.Module R M]
  [inst_5 : _root_.Module R M₂] [inst_6 : _root_.Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (p : Submodule R M)
  (q : Submodule R M₂), Submodule.map (f.coprod g) (p.prod q) = Submodule.map f p ⊔ Submodule.map g q

Unitization.inrNonUnitalAlgHom_toFun : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R]
  [inst_1 : NonUnitalSemiring A] [inst_2 : _root_.Module R A] (a : A), (Unitization.inrNonUnitalAlgHom R A) a = ↑a
Unitization.inrNonUnitalAlgHom_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R]
  [inst_1 : NonUnitalSemiring A] [inst_2 : _root_.Module R A] (a : A), (Unitization.inrNonUnitalAlgHom R A) a = ↑a

finFunctionFinEquiv_apply_val : ∀ {m n : ℕ} (f : Fin n → Fin m), ↑(finFunctionFinEquiv f) = ∑ i, ↑(f i) * m ^ ↑i
finFunctionFinEquiv_apply : ∀ {m n : ℕ} (f : Fin n → Fin m), ↑(finFunctionFinEquiv f) = ∑ i, ↑(f i) * m ^ ↑i

Quotient.ind_fintype_pi : ∀ {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)}
  {C : ((i : ι) → Quotient (S i)) → Prop},
  (∀ (a : (i : ι) → α i), C fun x => ⟦a x⟧) → ∀ (q : (i : ι) → Quotient (S i)), C q
Quotient.induction_on_fintype_pi : ∀ {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Sort u_2}
  {S : (i : ι) → Setoid (α i)} {C : ((i : ι) → Quotient (S i)) → Prop} (q : (i : ι) → Quotient (S i)),
  (∀ (a : (i : ι) → α i), C fun x => ⟦a x⟧) → C q

AddLocalization.ind : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → Prop},
  (∀ (y : M × ↥S), p (AddLocalization.mk y.1 y.2)) → ∀ (x : AddLocalization S), p x
AddLocalization.induction_on : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M}
  {p : AddLocalization S → Prop} (x : AddLocalization S), (∀ (y : M × ↥S), p (AddLocalization.mk y.1 y.2)) → p x

Localization.ind : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization S → Prop},
  (∀ (y : M × ↥S), p (Localization.mk y.1 y.2)) → ∀ (x : Localization S), p x
Localization.induction_on : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization S → Prop}
  (x : Localization S), (∀ (y : M × ↥S), p (Localization.mk y.1 y.2)) → p x

Cardinal.mk_sigma_congr : ∀ {ι ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι'),
  (∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g (e i))) → Cardinal.mk ((i : ι) × f i) = Cardinal.mk ((i : ι') × g i)
Cardinal.mk_sigma_congr' : ∀ {ι : Type u} {ι' : Type v} {f : ι → Type (max w u v)} {g : ι' → Type (max w u v)}
  (e : ι ≃ ι'),
  (∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g (e i))) → Cardinal.mk ((i : ι) × f i) = Cardinal.mk ((i : ι') × g i)

Cardinal.mk_pi_congr : ∀ {ι ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι'),
  (∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g (e i))) → Cardinal.mk ((i : ι) → f i) = Cardinal.mk ((i : ι') → g i)
Cardinal.mk_pi_congr' : ∀ {ι : Type u} {ι' : Type v} {f : ι → Type (max w u v)} {g : ι' → Type (max w u v)}
  (e : ι ≃ ι'),
  (∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g (e i))) → Cardinal.mk ((i : ι) → f i) = Cardinal.mk ((i : ι') → g i)

Cardinal.mk_range_eq_lift : ∀ {α : Type u} {β : Type v} {f : α → β},
  Function.Injective f →
    Cardinal.lift.{max u w, v} (Cardinal.mk ↑(Set.range f)) = Cardinal.lift.{max v w, u} (Cardinal.mk α)
Cardinal.mk_range_eq_of_injective : ∀ {α : Type u} {β : Type v} {f : α → β},
  Function.Injective f → Cardinal.lift.{u, v} (Cardinal.mk ↑(Set.range f)) = Cardinal.lift.{v, u} (Cardinal.mk α)

Cardinal.lt_aleph0_iff_finite : ∀ {α : Type u}, Cardinal.mk α < Cardinal.aleph0 ↔ Finite α
Cardinal.mk_lt_aleph0_iff : ∀ {α : Type u}, Cardinal.mk α < Cardinal.aleph0 ↔ Finite α

Set.Infinite.encard_eq : ∀ {α : Type u_1} {s : Set α}, s.Infinite → s.encard = ⊤
Set.encard_eq_top : ∀ {α : Type u_1} {s : Set α}, s.Infinite → s.encard = ⊤

Finite.card_le_of_injective : ∀ {α : Type u_1} {β : Type u_2} [Finite β] (f : α → β),
  Function.Injective f → Nat.card α ≤ Nat.card β
Nat.card_le_card_of_injective : ∀ {α : Type u} {β : Type v} [Finite β] (f : α → β),
  Function.Injective f → Nat.card α ≤ Nat.card β

Finite.card_le_of_surjective : ∀ {α : Type u_1} {β : Type u_2} [Finite α] (f : α → β),
  Function.Surjective f → Nat.card β ≤ Nat.card α
Nat.card_le_card_of_surjective : ∀ {α : Type u} {β : Type v} [Finite α] (f : α → β),
  Function.Surjective f → Nat.card β ≤ Nat.card α

Finite.card_sum : ∀ {α : Type u_1} {β : Type u_2} [Finite α] [Finite β], Nat.card (α ⊕ β) = Nat.card α + Nat.card β
Nat.card_sum : ∀ {α : Type u_1} {β : Type u_2} [Finite α] [Finite β], Nat.card (α ⊕ β) = Nat.card α + Nat.card β

Finite.card_pos : ∀ {α : Type u_1} [Finite α] [h : Nonempty α], 0 < Nat.card α
Nat.card_pos : ∀ {α : Type u_1} [Nonempty α] [Finite α], 0 < Nat.card α

QuotientGroup.lift_mk' : ∀ {G : Type u} [inst : Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x}
  [inst_1 : Monoid M] {φ : G →* M} (HN : N ≤ φ.ker) (g : G), (QuotientGroup.lift N φ HN) ↑g = φ g
QuotientGroup.lift_mk : ∀ {G : Type u} [inst : Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x}
  [inst_1 : Monoid M] {φ : G →* M} (HN : N ≤ φ.ker) (g : G), (QuotientGroup.lift N φ HN) ↑g = φ g

QuotientAddGroup.lift_mk : ∀ {G : Type u} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x}
  [inst_1 : AddMonoid M] {φ : G →+ M} (HN : N ≤ φ.ker) (g : G), (QuotientAddGroup.lift N φ HN) ↑g = φ g
QuotientAddGroup.lift_mk' : ∀ {G : Type u} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x}
  [inst_1 : AddMonoid M] {φ : G →+ M} (HN : N ≤ φ.ker) (g : G), (QuotientAddGroup.lift N φ HN) ↑g = φ g

QuotientAddGroup.kerLift_mk' : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (φ : G →+ H)
  (g : G), (QuotientAddGroup.kerLift φ) ↑g = φ g
QuotientAddGroup.kerLift_mk : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (φ : G →+ H)
  (g : G), (QuotientAddGroup.kerLift φ) ↑g = φ g

QuotientGroup.kerLift_mk' : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (φ : G →* H) (g : G),
  (QuotientGroup.kerLift φ) ↑g = φ g
QuotientGroup.kerLift_mk : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (φ : G →* H) (g : G),
  (QuotientGroup.kerLift φ) ↑g = φ g

Set.EqOn.eventuallyEq_of_mem : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {l : Filter α} {f g : α → β},
  Set.EqOn f g s → s ∈ l → f =ᶠ[l] g
Filter.eventuallyEq_of_mem : ∀ {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} {s : Set α},
  s ∈ l → Set.EqOn f g s → f =ᶠ[l] g

Filter.map_comap_setCoe_val : ∀ {β : Type u_2} (f : Filter β) (s : Set β),
  Filter.map Subtype.val (Filter.comap Subtype.val f) = f ⊓ Filter.principal s
Filter.subtype_coe_map_comap : ∀ {α : Type u_1} (s : Set α) (f : Filter α),
  Filter.map Subtype.val (Filter.comap Subtype.val f) = f ⊓ Filter.principal s

Ordinal.IsLimit.nat_lt : ∀ {o : Ordinal.{u_4}}, o.IsLimit → ∀ (n : ℕ), ↑n < o
Ordinal.nat_lt_limit : ∀ {o : Ordinal.{u_4}}, o.IsLimit → ∀ (n : ℕ), ↑n < o

Ordinal.deriv_id_of_nfp_id : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Ordinal.nfp f = id → Ordinal.deriv f = id
Ordinal.deriv_eq_id_of_nfp_eq_id : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Ordinal.nfp f = id → Ordinal.deriv f = id

Basis.mk_eq_rank' : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : _root_.Module R M] {ι : Type w} [StrongRankCondition R] (v : Basis ι R M),
  Cardinal.lift.{max v m, w} (Cardinal.mk ι) = Cardinal.lift.{max w m, v} (Module.rank R M)
Basis.mk_eq_rank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : _root_.Module R M] {ι : Type w} [StrongRankCondition R] (v : Basis ι R M),
  Cardinal.lift.{v, w} (Cardinal.mk ι) = Cardinal.lift.{w, v} (Module.rank R M)

Finsupp.coe_mono : ∀ {ι : Type u_1} {α : Type u_3} [inst : Zero α] [inst_1 : Preorder α], Monotone Finsupp.toFun
Finsupp.coe_strictMono : ∀ {ι : Type u_1} {α : Type u_3} [inst : Zero α] [inst_1 : Preorder α], Monotone Finsupp.toFun

Module.finrank_pi : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] {ι : Type v} [inst_2 : Fintype ι],
  Module.finrank R (ι → R) = Fintype.card ι
Module.finrank_fintype_fun_eq_card : ∀ (R : Type u) {η : Type u₁'} [inst : Semiring R] [StrongRankCondition R]
  [inst_2 : Fintype η], Module.finrank R (η → R) = Fintype.card η

Polynomial.natDegree_eq_natDegree : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S]
  {p : Polynomial R} {q : Polynomial S}, p.degree = q.degree → p.natDegree = q.natDegree
Polynomial.natDegree_eq_of_degree_eq : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R}
  [inst_1 : Semiring S] {q : Polynomial S}, p.degree = q.degree → p.natDegree = q.natDegree

Polynomial.nonempty_support_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.support.Nonempty ↔ p ≠ 0
Polynomial.support_nonempty : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.support.Nonempty ↔ p ≠ 0

Polynomial.eval₂_hom : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S]
  (f : R →+* S) (x : R), Polynomial.eval₂ f (f x) p = f (Polynomial.eval x p)
Polynomial.eval₂_at_apply : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {S : Type u_1} [inst_1 : Semiring S]
  (f : R →+* S) (r : R), Polynomial.eval₂ f (f r) p = f (Polynomial.eval r p)

DFinsupp.coe_mono : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)]
  [inst_1 : (i : ι) → Preorder (α i)], Monotone DFunLike.coe
DFinsupp.coe_strictMono : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)]
  [inst_1 : (i : ι) → Preorder (α i)], Monotone DFunLike.coe

Polynomial.coeff_mul_of_natDegree_le : ∀ {R : Type u} {m n : ℕ} [inst : Semiring R] {p q : Polynomial R},
  p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n
Polynomial.coeff_mul_add_eq_of_natDegree_le : ∀ {R : Type u} [inst : Semiring R] {df dg : ℕ} {f g : Polynomial R},
  f.natDegree ≤ df → g.natDegree ≤ dg → (f * g).coeff (df + dg) = f.coeff df * g.coeff dg

MvPolynomial.support_coeff_finSuccEquiv : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ}
  {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {m : Fin n →₀ ℕ},
  m ∈ (((MvPolynomial.finSuccEquiv R n) f).coeff i).support ↔ Finsupp.cons i m ∈ f.support
MvPolynomial.mem_support_coeff_finSuccEquiv : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ}
  {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x : Fin n →₀ ℕ},
  x ∈ (((MvPolynomial.finSuccEquiv R n) f).coeff i).support ↔ Finsupp.cons i x ∈ f.support

Polynomial.monic_of_degree_le : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} (n : ℕ),
  p.degree ≤ ↑n → p.coeff n = 1 → p.Monic
Polynomial.monic_of_degree_le_of_coeff_eq_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} (n : ℕ),
  p.degree ≤ ↑n → p.coeff n = 1 → p.Monic

Polynomial.Monic.natDegree_eq_zero_iff_eq_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.Monic → (p.natDegree = 0 ↔ p = 1)
Polynomial.Monic.natDegree_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.Monic → (p.natDegree = 0 ↔ p = 1)

Polynomial.leadingCoeff_map' : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S},
  Function.Injective ⇑f → ∀ (p : Polynomial R), (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
Polynomial.leadingCoeff_of_injective : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S]
  {f : R →+* S}, Function.Injective ⇑f → ∀ (p : Polynomial R), (Polynomial.map f p).leadingCoeff = f p.leadingCoeff

Polynomial.coeff_restriction' : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} {n : ℕ},
  ↑(p.restriction.coeff n) = p.coeff n
Polynomial.coeff_restriction : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} {n : ℕ},
  ↑(p.restriction.coeff n) = p.coeff n

Polynomial.coeff_toSubring : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T)
  {n : ℕ}, ↑((p.toSubring T hp).coeff n) = p.coeff n
Polynomial.coeff_toSubring' : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T)
  {n : ℕ}, ↑((p.toSubring T hp).coeff n) = p.coeff n

RingHom.Finite.finiteType : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] {f : A →+* B},
  f.Finite → f.FiniteType
RingHom.FiniteType.of_finite : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] {f : A →+* B},
  f.Finite → f.FiniteType

AddAction.Quotient.mk_vadd_out : ∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddMonoid β]
  [inst_2 : AddAction β α] (H : AddSubgroup α) [inst_3 : AddAction.QuotientAction β H] (b : β) (q : α ⧸ H),
  ↑(b +ᵥ Quotient.out q) = b +ᵥ q
AddAction.Quotient.coe_vadd_out : ∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddMonoid β]
  [inst_2 : AddAction β α] (H : AddSubgroup α) [inst_3 : AddAction.QuotientAction β H] (b : β) (q : α ⧸ H),
  ↑(b +ᵥ Quotient.out q) = b +ᵥ q

MulAction.Quotient.smul_mk : ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Monoid β] [inst_2 : MulAction β α]
  (H : Subgroup α) [inst_3 : MulAction.QuotientAction β H] (b : β) (a : α), b • ↑a = ↑(b • a)
MulAction.Quotient.smul_coe : ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Monoid β] [inst_2 : MulAction β α]
  (H : Subgroup α) [inst_3 : MulAction.QuotientAction β H] (b : β) (a : α), b • ↑a = ↑(b • a)

AddAction.Quotient.vadd_mk : ∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddMonoid β]
  [inst_2 : AddAction β α] (H : AddSubgroup α) [inst_3 : AddAction.QuotientAction β H] (b : β) (a : α),
  b +ᵥ ↑a = ↑(b +ᵥ a)
AddAction.Quotient.vadd_coe : ∀ {α : Type u} {β : Type v} [inst : AddGroup α] [inst_1 : AddMonoid β]
  [inst_2 : AddAction β α] (H : AddSubgroup α) [inst_3 : AddAction.QuotientAction β H] (b : β) (a : α),
  b +ᵥ ↑a = ↑(b +ᵥ a)

MulAction.Quotient.mk_smul_out : ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Monoid β]
  [inst_2 : MulAction β α] (H : Subgroup α) [inst_3 : MulAction.QuotientAction β H] (b : β) (q : α ⧸ H),
  ↑(b • Quotient.out q) = b • q
MulAction.Quotient.coe_smul_out : ∀ {α : Type u} {β : Type v} [inst : Group α] [inst_1 : Monoid β]
  [inst_2 : MulAction β α] (H : Subgroup α) [inst_3 : MulAction.QuotientAction β H] (b : β) (q : α ⧸ H),
  ↑(b • Quotient.out q) = b • q

ZMod.val_cast_of_lt : ∀ {n a : ℕ}, a < n → (↑a).val = a
ZMod.val_natCast_of_lt : ∀ {n a : ℕ}, a < n → (↑a).val = a

multiplicity_pos_of_dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a ∣ b → 0 < multiplicity a b
Dvd.multiplicity_pos : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a ∣ b → 0 < multiplicity a b

Subfield.closure_preimage_le : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L]
  (f : K →+* L) (s : Set L), Subfield.closure (⇑f ⁻¹' s) ≤ Subfield.comap f (Subfield.closure s)
RingHom.field_closure_preimage_le : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L]
  (f : K →+* L) (s : Set L), Subfield.closure (⇑f ⁻¹' s) ≤ Subfield.comap f (Subfield.closure s)

Sym2.forall_mem_pair : ∀ {α : Type u_1} {P : α → Prop} {a b : α}, (∀ x ∈ s(a, b), P x) ↔ P a ∧ P b
Sym2.ball : ∀ {α : Type u_1} {p : α → Prop} {a b : α}, (∀ c ∈ s(a, b), p c) ↔ p a ∧ p b

Sym2.inductionOn : ∀ {α : Type u_1} {f : Sym2 α → Prop} (i : Sym2 α), (∀ (x y : α), f s(x, y)) → f i
Sym2.ind : ∀ {α : Type u_1} {f : Sym2 α → Prop}, (∀ (x y : α), f s(x, y)) → ∀ (i : Sym2 α), f i

CategoryTheory.eq_whisker' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X Y : C} {f g : X ⟶ Y},
  f = g → ∀ {Z : C} (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h
CategoryTheory.eq_whisker : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f g : X ⟶ Y},
  f = g → ∀ (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h

CategoryTheory.NatTrans.comp_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) (X : C),
  (CategoryTheory.CategoryStruct.comp α β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)
CategoryTheory.NatTrans.vcomp_app' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) (X : C),
  (CategoryTheory.CategoryStruct.comp α β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)

CategoryTheory.ConcreteCategory.congr_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.HasForget C] {X Y : C} {f g : X ⟶ Y},
  f = g → ∀ (x : (CategoryTheory.forget C).obj X), f x = g x
CategoryTheory.congr_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.HasForget C] {X Y : C} {f g : X ⟶ Y},
  f = g → ∀ (x : (CategoryTheory.forget C).obj X), f x = g x

Tactic.Elementwise.hom_elementwise : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  [inst_1 : CategoryTheory.HasForget C] {X Y : C} {f g : X ⟶ Y},
  f = g → ∀ (x : (CategoryTheory.forget C).obj X), f x = g x
CategoryTheory.congr_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.HasForget C] {X Y : C} {f g : X ⟶ Y},
  f = g → ∀ (x : (CategoryTheory.forget C).obj X), f x = g x

CategoryTheory.CostructuredArrow.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D}
  {X Y : CategoryTheory.CostructuredArrow S T} (f g : X ⟶ Y), f.left = g.left → f = g
CategoryTheory.CostructuredArrow.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D}
  {A B : CategoryTheory.CostructuredArrow S T} (f g : A ⟶ B), f.left = g.left → f = g

CategoryTheory.CostructuredArrow.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D}
  {A B : CategoryTheory.CostructuredArrow S T} (f g : A ⟶ B), f = g ↔ f.left = g.left
CategoryTheory.CostructuredArrow.hom_eq_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {T : D} {S : CategoryTheory.Functor C D}
  {X Y : CategoryTheory.CostructuredArrow S T} (f g : X ⟶ Y), f = g ↔ f.left = g.left

CategoryTheory.StructuredArrow.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D}
  {A B : CategoryTheory.StructuredArrow S T} (f g : A ⟶ B), f = g ↔ f.right = g.right
CategoryTheory.StructuredArrow.hom_eq_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D}
  {X Y : CategoryTheory.StructuredArrow S T} (f g : X ⟶ Y), f = g ↔ f.right = g.right

CategoryTheory.StructuredArrow.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D}
  {X Y : CategoryTheory.StructuredArrow S T} (f g : X ⟶ Y), f.right = g.right → f = g
CategoryTheory.StructuredArrow.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {S : D} {T : CategoryTheory.Functor C D}
  {A B : CategoryTheory.StructuredArrow S T} (f g : A ⟶ B), f.right = g.right → f = g

AddCommGrp.hom_nsmul : ∀ {M N : AddCommGrp} (n : ℕ) (f : M ⟶ N), AddCommGrp.Hom.hom (n • f) = n • AddCommGrp.Hom.hom f
AddCommGrp.hom_zsmul : ∀ {M N : AddCommGrp} (n : ℕ) (f : M ⟶ N), AddCommGrp.Hom.hom (n • f) = n • AddCommGrp.Hom.hom f

ModuleCat.hom_zsmul : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (n : ℕ) (f : M ⟶ N),
  ModuleCat.Hom.hom (n • f) = n • ModuleCat.Hom.hom f
ModuleCat.hom_nsmul : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (n : ℕ) (f : M ⟶ N),
  ModuleCat.Hom.hom (n • f) = n • ModuleCat.Hom.hom f

Equiv.Perm.Disjoint.cycleType_mul : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {f g : Equiv.Perm α},
  f.Disjoint g → (f * g).cycleType = f.cycleType + g.cycleType
Equiv.Perm.Disjoint.cycleType : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ τ : Equiv.Perm α},
  σ.Disjoint τ → (σ * τ).cycleType = σ.cycleType + τ.cycleType

CoalgEquiv.coe_coe : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : _root_.Module R A] [inst_4 : _root_.Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₗc[R] B), ⇑↑e = ⇑e
CoalgEquiv.coe_toCoalgHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : AddCommMonoid B] [inst_3 : _root_.Module R A] [inst_4 : _root_.Module R B]
  [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B] (e : A ≃ₗc[R] B), ⇑↑e = ⇑e

BialgEquiv.coe_toCoalgEquiv : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₐc[R] B), ⇑↑e = ⇑e
BialgEquiv.coe_toAlgEquiv : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₐc[R] B), ⇑↑e = ⇑e

BialgEquiv.coe_coe : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₐc[R] B), ⇑↑e = ⇑e
BialgEquiv.coe_toBialgHom : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] (e : A ≃ₐc[R] B), ⇑↑e = ⇑e

Mon_.tensorObj_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.BraidedCategory C] (X Y : Mon_ C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X.X Y.X X.X Y.X)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom X.mul Y.mul)
Mon_.tensor_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.BraidedCategory C] (M N : Mon_ C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj M N).mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M.X N.X M.X N.X)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom M.mul N.mul)

Mon_.tensorObj_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.BraidedCategory C] (X Y : Mon_ C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).one =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom X.one Y.one)
Mon_.tensor_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.BraidedCategory C] (M N : Mon_ C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj M N).one =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom M.one N.one)

Comon_.tensorObj_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.BraidedCategory C] (A B : Comon_ C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj A B).X = CategoryTheory.MonoidalCategoryStruct.tensorObj A.X B.X
Comon_.monoidal_tensorObj_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.BraidedCategory C] (X Y : Comon_ C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).X = CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X

BddLat.hom_comp : ∀ {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z),
  Lat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Lat.Hom.hom g).comp (Lat.Hom.hom f)
Lat.hom_comp : ∀ {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z),
  Lat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Lat.Hom.hom g).comp (Lat.Hom.hom f)

BddLat.comp_apply : ∀ {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
Lat.comp_apply : ∀ {X Y Z : Lat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

BddLat.id_apply : ∀ (X : Lat) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
Lat.id_apply : ∀ (X : Lat) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

BddLat.hom_id : ∀ {X : Lat}, Lat.Hom.hom (CategoryTheory.CategoryStruct.id X) = LatticeHom.id ↑X
Lat.hom_id : ∀ {X : Lat}, Lat.Hom.hom (CategoryTheory.CategoryStruct.id X) = LatticeHom.id ↑X

CategoryTheory.ObjectProperty.ι_ε : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal],
  CategoryTheory.Functor.LaxMonoidal.ε P.ι =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
CategoryTheory.ObjectProperty.ι_η : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal],
  CategoryTheory.Functor.LaxMonoidal.ε P.ι =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

Function.Exact.of_comp_eq_zero_of_ker_in_range : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P}
  [inst : Zero P], g ∘ f = 0 → (∀ (y : N), g y = 0 → y ∈ Set.range f) → Function.Exact f g
Function.Exact.of_comp_of_mem_range : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P}
  [inst : Zero P], g ∘ f = 0 → (∀ (x : N), g x = 0 → x ∈ Set.range f) → Function.Exact f g

CategoryTheory.ShortComplex.ShortExact.ab_exact_iff_function_exact : ∀ (S : CategoryTheory.ShortComplex Ab),
  S.Exact ↔ Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom S.f) ⇑(CategoryTheory.ConcreteCategory.hom S.g)
CategoryTheory.ShortComplex.ab_exact_iff_function_exact : ∀ (S : CategoryTheory.ShortComplex Ab),
  S.Exact ↔ Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom S.f) ⇑(CategoryTheory.ConcreteCategory.hom S.g)

CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_hom : ∀ {C : Type u_1} {D : Type u_2}
  [inst : CategoryTheory.Category.{u_4, u_1} C] [inst_1 : CategoryTheory.Category.{u_5, u_2} D]
  (L : CategoryTheory.Functor C D) {H : Type u_3} [inst_2 : CategoryTheory.Category.{u_6, u_3} H]
  (F : CategoryTheory.Functor C H) [inst_3 : L.HasPointwiseLeftKanExtension F] (X : D)
  (f : CategoryTheory.CostructuredArrow L X),
  CategoryTheory.CategoryStruct.comp ((L.leftKanExtensionUnit F).app f.left)
      (CategoryTheory.CategoryStruct.comp ((L.leftKanExtension F).map f.hom)
        (L.leftKanExtensionObjIsoColimit F X).hom) =
    CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L X).comp F) f
CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom : ∀ {C : Type u_1}
  {D : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C] [inst_1 : CategoryTheory.Category.{u_5, u_2} D]
  (L : CategoryTheory.Functor C D) {H : Type u_3} [inst_2 : CategoryTheory.Category.{u_6, u_3} H]
  (F : CategoryTheory.Functor C H) [inst_3 : L.HasPointwiseLeftKanExtension F] (X : D)
  (f : CategoryTheory.CostructuredArrow L X),
  CategoryTheory.CategoryStruct.comp ((L.leftKanExtensionUnit F).app f.left)
      (CategoryTheory.CategoryStruct.comp ((L.leftKanExtension F).map f.hom)
        (L.leftKanExtensionObjIsoColimit F X).hom) =
    CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L X).comp F) f

Finset.range_add : ∀ (a b : ℕ), Finset.range (a + b) = Finset.range a ∪ Finset.map (addLeftEmbedding a) (Finset.range b)
Finset.range_add_eq_union : ∀ (a b : ℕ),
  Finset.range (a + b) = Finset.range a ∪ Finset.map (addLeftEmbedding a) (Finset.range b)

RootableBy.surjective_pow : ∀ (A : Type u_4) (α : Type u_5) [inst : Monoid A] [inst_1 : Pow A α] [inst_2 : Zero α]
  [RootableBy A α] {n : α}, n ≠ 0 → Function.Surjective fun a => a ^ n
pow_left_surj_of_rootableBy : ∀ (A : Type u_1) (α : Type u_2) [inst : Monoid A] [inst_1 : Pow A α] [inst_2 : Zero α]
  [RootableBy A α] {n : α}, n ≠ 0 → Function.Surjective fun a => a ^ n

smul_right_surj_of_divisibleBy : ∀ (A : Type u_1) (α : Type u_2) [inst : AddMonoid A] [inst_1 : SMul α A]
  [inst_2 : Zero α] [DivisibleBy A α] {n : α}, n ≠ 0 → Function.Surjective fun a => n • a
DivisibleBy.surjective_smul : ∀ (A : Type u_4) (α : Type u_5) [inst : AddMonoid A] [inst_1 : SMul α A] [inst_2 : Zero α]
  [DivisibleBy A α] {n : α}, n ≠ 0 → Function.Surjective fun a => n • a

ContinuousOn.coeFun : ∀ {F : Type u_1} {α : Type u_2} {X : Type u_3} {Z : Type u_4} [inst : FunLike F α X]
  [inst_1 : TopologicalSpace F] [inst_2 : TopologicalSpace X] [ContinuousEvalConst F α X] [inst_4 : TopologicalSpace Z]
  {f : Z → F} {s : Set Z}, ContinuousOn f s → ∀ (x : α), ContinuousOn (fun x_1 => (f x_1) x) s
ContinuousOn.eval_const : ∀ {F : Type u_1} {α : Type u_2} {X : Type u_3} {Z : Type u_4} [inst : FunLike F α X]
  [inst_1 : TopologicalSpace F] [inst_2 : TopologicalSpace X] [ContinuousEvalConst F α X] [inst_4 : TopologicalSpace Z]
  {f : Z → F} {s : Set Z}, ContinuousOn f s → ∀ (x : α), ContinuousOn (fun x_1 => (f x_1) x) s

ENNReal.sup_eq_zero : ∀ {a b : ENNReal}, max a b = 0 ↔ a = 0 ∧ b = 0
ENNReal.max_eq_zero_iff : ∀ {a b : ENNReal}, max a b = 0 ↔ a = 0 ∧ b = 0

ENNReal.toReal_eq_toReal : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → (a.toReal = b.toReal ↔ a = b)
ENNReal.toReal_eq_toReal_iff' : ∀ {x y : ENNReal}, x ≠ ⊤ → y ≠ ⊤ → (x.toReal = y.toReal ↔ x = y)

EReal.add_ne_top_iff_ne_top_left : ∀ {x y : EReal}, y ≠ ⊥ → y ≠ ⊤ → (x + y ≠ ⊤ ↔ x ≠ ⊤)
EReal.add_ne_top_iff_of_ne_bot_of_ne_top : ∀ {x y : EReal}, y ≠ ⊥ → y ≠ ⊤ → (x + y ≠ ⊤ ↔ x ≠ ⊤)

EReal.add_ne_top_iff_ne_top₂ : ∀ {x y : EReal}, x ≠ ⊥ → y ≠ ⊥ → (x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤)
EReal.add_ne_top_iff_of_ne_bot : ∀ {x y : EReal}, x ≠ ⊥ → y ≠ ⊥ → (x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤)

IsUniformInducing.of_comp_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α]
  [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ] {g : β → γ},
  IsUniformInducing g → ∀ {f : α → β}, IsUniformInducing (g ∘ f) ↔ IsUniformInducing f
IsUniformInducing.isUniformInducing_comp_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α]
  [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ] {f : α → β} {g : β → γ},
  IsUniformInducing g → (IsUniformInducing (g ∘ f) ↔ IsUniformInducing f)

Metric.emetric_ball_top : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), EMetric.ball x ⊤ = Set.univ
Metric.eball_top_eq_univ : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), EMetric.ball x ⊤ = Set.univ

BddBelow.isBounded : ∀ {α : Type u_1} {s : Set α} [inst : Bornology α] [inst_1 : Preorder α] [IsOrderBornology α],
  BddBelow s → BddAbove s → Bornology.IsBounded s
BddAbove.isBounded : ∀ {α : Type u_1} {s : Set α} [inst : Bornology α] [inst_1 : Preorder α] [IsOrderBornology α],
  BddAbove s → BddBelow s → Bornology.IsBounded s

PartialHomeomorph.toFun_eq_coe : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y), ↑e.toPartialEquiv = ↑e
PartialHomeomorph.coe_coe : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : PartialHomeomorph X Y), ↑e.toPartialEquiv = ↑e

Homeomorph.isLocalHomeomorph : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (f : X ≃ₜ Y), IsLocalHomeomorph ⇑f
IsLocalHomeomorph.Homeomorph.isLocalHomeomorph : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y), IsLocalHomeomorph ⇑h

CommGrp_.id_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (A : Grp_ C),
  (CategoryTheory.CategoryStruct.id A).hom = CategoryTheory.CategoryStruct.id A.X
Grp_.id_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (A : Grp_ C),
  (CategoryTheory.CategoryStruct.id A).hom = CategoryTheory.CategoryStruct.id A.X

Matrix.Nondegenerate.of_det_ne_zero : ∀ {n : Type u_1} [inst : Fintype n] {A : Type u_4} [inst_1 : DecidableEq n]
  [inst_2 : CommRing A] [IsDomain A] {M : Matrix n n A}, M.det ≠ 0 → M.Nondegenerate
Matrix.nondegenerate_of_det_ne_zero : ∀ {m : Type u_1} {A : Type u_3} [inst : Fintype m] [inst_1 : CommRing A]
  [IsDomain A] [inst_3 : DecidableEq m] {M : Matrix m m A}, M.det ≠ 0 → M.Nondegenerate

Subtype.ext_val_iff : ∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, a1 = a2 ↔ ↑a1 = ↑a2
Subtype.ext_val_iff : ∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : { x // p x }}, a1 = a2 ↔ ↑a1 = ↑a2

UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow : ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α]
  [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α] {p : α},
  Irreducible p → ∀ (k : ℕ), UniqueFactorizationMonoid.normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)
Irreducible.normalizedFactors_pow : ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α]
  [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α] {p : α},
  Irreducible p → ∀ (k : ℕ), UniqueFactorizationMonoid.normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)

Ne.eq_def : ∀ {α : Sort u} (a b : α), (a ≠ b) = ¬a = b
Ne.eq_def : ∀ {α : Sort u} (a b : α), (a ≠ b) = ¬a = b

MonoidHom.compAddChar_apply : ∀ {A : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddMonoid A] [inst_1 : Monoid M]
  [inst_2 : Monoid N] (f : M →* N) (φ : AddChar A M), ⇑(f.compAddChar φ) = ⇑f ∘ ⇑φ
MonoidHom.coe_compAddChar : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] {N : Type u_5}
  [inst_2 : Monoid N] (f : M →* N) (φ : AddChar A M), ⇑(f.compAddChar φ) = ⇑f ∘ ⇑φ

QuaternionAlgebra.coe_commutes : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂ c₃)
  [inst : CommRing R], ↑r * a = a * ↑r
QuaternionAlgebra.comm : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : CommRing R] (r : R) (x : QuaternionAlgebra R c₁ c₂ c₃),
  ↑r * x = x * ↑r

FreeGroup.reduce.rev : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeGroup.Red L₁ L₂ → FreeGroup.Red L₂ (FreeGroup.reduce L₁)
FreeGroup.Red.reduce_left : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeGroup.Red L₁ L₂ → FreeGroup.Red L₂ (FreeGroup.reduce L₁)

FreeAddGroup.Red.reduce_left : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₂ (FreeAddGroup.reduce L₁)
FreeAddGroup.reduce.rev : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.Red L₁ L₂ → FreeAddGroup.Red L₂ (FreeAddGroup.reduce L₁)

ComplexShape.boundaryLE_embeddingUpIntLE_iff : ∀ (p : ℤ) (n : ℕ), (ComplexShape.embeddingUpIntGE p).BoundaryGE n ↔ n = 0
ComplexShape.boundaryGE_embeddingUpIntGE_iff : ∀ (p : ℤ) (n : ℕ), (ComplexShape.embeddingUpIntGE p).BoundaryGE n ↔ n = 0

LieModuleEquiv.coe_toLieModuleHom : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R]
  [inst_1 : LieRing L] [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : _root_.Module R M]
  [inst_5 : _root_.Module R N] [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N),
  ⇑e.toLieModuleHom = ⇑e
LieModuleEquiv.coe_coe : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : _root_.Module R M] [inst_5 : _root_.Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N), ⇑e.toLieModuleHom = ⇑e

MvPolynomial.sum_weightedHomogeneousComponent : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3}
  [inst_1 : AddCommMonoid M] (w : σ → M) (φ : MvPolynomial σ R),
  ∑ᶠ (m : M), (MvPolynomial.weightedHomogeneousComponent w m) φ = φ
MvPolynomial.finsum_weightedHomogeneousComponent : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R]
  {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M) (φ : MvPolynomial σ R),
  ∑ᶠ (m : M), (MvPolynomial.weightedHomogeneousComponent w m) φ = φ

MvPolynomial.weightedHomogeneousComponent_of_isWeightedHomogeneous_same : ∀ {R : Type u_1} {M : Type u_2}
  [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M} {m : M} {p : MvPolynomial σ R},
  MvPolynomial.IsWeightedHomogeneous w p m → (MvPolynomial.weightedHomogeneousComponent w m) p = p
MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_same : ∀ {R : Type u_1} {M : Type u_2}
  [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M} {m : M} {p : MvPolynomial σ R},
  MvPolynomial.IsWeightedHomogeneous w p m → (MvPolynomial.weightedHomogeneousComponent w m) p = p

LieHom.toNonUnitalAlgHom_toFun : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] {L₂ : Type w} [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (a : L),
  f.toNonUnitalAlgHom a = f a
LieHom.toNonUnitalAlgHom_apply : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] {L₂ : Type w} [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (a : L),
  f.toNonUnitalAlgHom a = f a

Associates.eq_of_prod_eq_prod : ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α]
  [Nontrivial α] {a b : Associates.FactorSet α}, a.prod = b.prod → a = b
Associates.FactorSet.unique : ∀ {α : Type u_1} [inst : CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α]
  [Nontrivial α] {p q : Associates.FactorSet α}, p.prod = q.prod → p = q

squarefree_iff_no_irreducibles : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [WfDvdMonoid R] {x : R},
  x ≠ 0 → (Squarefree x ↔ ∀ (p : R), Irreducible p → ¬p * p ∣ x)
squarefree_iff_irreducible_sq_not_dvd_of_ne_zero : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [WfDvdMonoid R]
  {r : R}, r ≠ 0 → (Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r)

PerfectPairing.restrict_apply_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R]
  [inst_1 : AddCommGroup M] [inst_2 : _root_.Module R M] [inst_3 : AddCommGroup N] [inst_4 : _root_.Module R N]
  (p : PerfectPairing R M N) {M' : Type u_4} {N' : Type u_5} [inst_5 : AddCommGroup M'] [inst_6 : _root_.Module R M']
  [inst_7 : AddCommGroup N'] [inst_8 : _root_.Module R N'] (i : M' →ₗ[R] M) (j : N' →ₗ[R] N)
  (hi : Function.Injective ⇑i) (hj : Function.Injective ⇑j)
  (hij : p.IsPerfectCompl (LinearMap.range i) (LinearMap.range j)) (x : M') (y : N'),
  ((p.restrict i j hi hj hij) x) y = (p (i x)) (j y)
PerfectPairing.restrict_toFun_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R]
  [inst_1 : AddCommGroup M] [inst_2 : _root_.Module R M] [inst_3 : AddCommGroup N] [inst_4 : _root_.Module R N]
  (p : PerfectPairing R M N) {M' : Type u_4} {N' : Type u_5} [inst_5 : AddCommGroup M'] [inst_6 : _root_.Module R M']
  [inst_7 : AddCommGroup N'] [inst_8 : _root_.Module R N'] (i : M' →ₗ[R] M) (j : N' →ₗ[R] N)
  (hi : Function.Injective ⇑i) (hj : Function.Injective ⇑j)
  (hij : p.IsPerfectCompl (LinearMap.range i) (LinearMap.range j)) (a : M') (m : N'),
  ((p.restrict i j hi hj hij) a) m = (p (i a)) (j m)

smul_pi₀ : ∀ {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [inst : GroupWithZero K]
  [inst_1 : (i : ι) → MulAction K (R i)] {r : K} (S : Set ι) (t : (i : ι) → Set (R i)),
  r ≠ 0 → r • S.pi t = S.pi (r • t)
Set.smul_set_pi₀ : ∀ {M : Type u_3} {ι : Type u_4} {α : ι → Type u_5} [inst : GroupWithZero M]
  [inst_1 : (i : ι) → MulAction M (α i)] {c : M},
  c ≠ 0 → ∀ (I : Set ι) (s : (i : ι) → Set (α i)), c • I.pi s = I.pi (c • s)

smul_pi : ∀ {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [inst : Group K] [inst_1 : (i : ι) → MulAction K (R i)]
  (r : K) (S : Set ι) (t : (i : ι) → Set (R i)), r • S.pi t = S.pi (r • t)
Set.smul_set_pi : ∀ {G : Type u_5} {ι : Type u_6} {α : ι → Type u_7} [inst : Group G]
  [inst_1 : (i : ι) → MulAction G (α i)] (c : G) (I : Set ι) (s : (i : ι) → Set (α i)), c • I.pi s = I.pi (c • s)

smul_univ_pi : ∀ {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [inst : (i : ι) → SMul K (R i)] (r : K)
  (t : (i : ι) → Set (R i)), r • Set.univ.pi t = Set.univ.pi (r • t)
Set.smul_set_univ_pi : ∀ {M : Type u_5} {ι : Type u_6} {π : ι → Type u_7} [inst : (i : ι) → SMul M (π i)] (c : M)
  (s : (i : ι) → Set (π i)), c • Set.univ.pi s = Set.univ.pi (c • s)

vadd_univ_pi : ∀ {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [inst : (i : ι) → VAdd K (R i)] (r : K)
  (t : (i : ι) → Set (R i)), r +ᵥ Set.univ.pi t = Set.univ.pi (r +ᵥ t)
Set.vadd_set_univ_pi : ∀ {M : Type u_5} {ι : Type u_6} {π : ι → Type u_7} [inst : (i : ι) → VAdd M (π i)] (c : M)
  (s : (i : ι) → Set (π i)), c +ᵥ Set.univ.pi s = Set.univ.pi (c +ᵥ s)

vadd_pi : ∀ {K : Type u_1} {ι : Type u_2} {R : ι → Type u_3} [inst : AddGroup K] [inst_1 : (i : ι) → AddAction K (R i)]
  (r : K) (S : Set ι) (t : (i : ι) → Set (R i)), r +ᵥ S.pi t = S.pi (r +ᵥ t)
Set.vadd_set_pi : ∀ {G : Type u_5} {ι : Type u_6} {α : ι → Type u_7} [inst : AddGroup G]
  [inst_1 : (i : ι) → AddAction G (α i)] (c : G) (I : Set ι) (s : (i : ι) → Set (α i)), c +ᵥ I.pi s = I.pi (c +ᵥ s)

measurableSet_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β}
  {t : Set β}, Measurable f → MeasurableSet t → MeasurableSet (f ⁻¹' t)
MeasurableSet.preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β}
  {t : Set β}, MeasurableSet t → Measurable f → MeasurableSet (f ⁻¹' t)

Summable.compl_add : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  [ContinuousAdd α] {s : Set β}, Summable (f ∘ Subtype.val) → Summable (f ∘ Subtype.val) → Summable f
Summable.add_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  [ContinuousAdd α] {s : Set β}, Summable (f ∘ Subtype.val) → Summable (f ∘ Subtype.val) → Summable f

Multipliable.compl_add : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  [ContinuousMul α] {s : Set β}, Multipliable (f ∘ Subtype.val) → Multipliable (f ∘ Subtype.val) → Multipliable f
Multipliable.mul_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  [ContinuousMul α] {s : Set β}, Multipliable (f ∘ Subtype.val) → Multipliable (f ∘ Subtype.val) → Multipliable f

tendsto_real_toNNReal_atTop : Filter.Tendsto Real.toNNReal Filter.atTop Filter.atTop
Real.tendsto_toNNReal_atTop : Filter.Tendsto Real.toNNReal Filter.atTop Filter.atTop

uniformity_basis_dist_pow_of_lt_one : ∀ {α : Type u_4} [inst : PseudoMetricSpace α] {r : ℝ},
  0 < r → r < 1 → (uniformity α).HasBasis (fun x => True) fun k => {p | dist p.1 p.2 < r ^ k}
Metric.uniformity_basis_dist_pow : ∀ {α : Type u} [inst : PseudoMetricSpace α] {r : ℝ},
  0 < r → r < 1 → (uniformity α).HasBasis (fun x => True) fun n => {p | dist p.1 p.2 < r ^ n}

edist_zero_right : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E), edist a 0 = ‖a‖ₑ
edist_zero_eq_enorm : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (x : E), edist x 0 = ‖x‖ₑ

ofReal_norm : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (x : E), ENNReal.ofReal ‖x‖ = ‖x‖ₑ
ofReal_norm_eq_enorm : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E), ENNReal.ofReal ‖a‖ = ‖a‖ₑ

Real.enorm_eq_ofReal : ∀ {r : ℝ}, 0 ≤ r → ‖r‖ₑ = ENNReal.ofReal r
Real.enorm_of_nonneg : ∀ {r : ℝ}, 0 ≤ r → ‖r‖ₑ = ENNReal.ofReal r

ofReal_norm_eq_enorm' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E), ENNReal.ofReal ‖a‖ = ‖a‖ₑ
ofReal_norm' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (x : E), ENNReal.ofReal ‖x‖ = ‖x‖ₑ

edist_one_eq_enorm : ∀ {E : Type u_5} [inst : SeminormedGroup E] (x : E), edist x 1 = ‖x‖ₑ
edist_one_right : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E), edist a 1 = ‖a‖ₑ

Inseparable.enorm_eq_enorm : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ContinuousENorm E] {u v : E},
  Inseparable u v → ‖u‖ₑ = ‖v‖ₑ
Inseparable.enorm_eq_enorm' : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ContinuousENorm E] {u v : E},
  Inseparable u v → ‖u‖ₑ = ‖v‖ₑ

IsCompact.closedBall_mul : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → ∀ (x : E), Metric.closedBall x δ * s = x • Metric.cthickening δ s
IsCompact.closedBall_div : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → ∀ (x : E), Metric.closedBall x δ * s = x • Metric.cthickening δ s

IsCompact.closedBall_sub : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → ∀ (x : E), Metric.closedBall x δ + s = x +ᵥ Metric.cthickening δ s
IsCompact.closedBall_add : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → ∀ (x : E), Metric.closedBall x δ + s = x +ᵥ Metric.cthickening δ s

Real.pow_lt_of_lt_log : ∀ {x y : ℝ} {n : ℕ}, 0 < y → Real.log x < ↑n * Real.log y → x < y ^ n
Real.lt_pow_of_log_lt : ∀ {x y : ℝ} {n : ℕ}, 0 < y → Real.log x < ↑n * Real.log y → x < y ^ n

Real.rpow_lt_of_lt_log : ∀ {x y z : ℝ}, 0 < y → Real.log x < z * Real.log y → x < y ^ z
Real.lt_rpow_of_log_lt : ∀ {x y z : ℝ}, 0 < y → Real.log x < z * Real.log y → x < y ^ z

Real.zpow_lt_of_lt_log : ∀ {x y : ℝ} {n : ℤ}, 0 < y → Real.log x < ↑n * Real.log y → x < y ^ n
Real.lt_zpow_of_log_lt : ∀ {x y : ℝ} {n : ℤ}, 0 < y → Real.log x < ↑n * Real.log y → x < y ^ n

Real.rpow_le_of_le_log : ∀ {x y z : ℝ}, 0 < y → Real.log x ≤ z * Real.log y → x ≤ y ^ z
Real.le_rpow_of_log_le : ∀ {x y z : ℝ}, 0 < y → Real.log x ≤ z * Real.log y → x ≤ y ^ z

Real.le_pow_of_log_le : ∀ {x y : ℝ} {n : ℕ}, 0 < y → Real.log x ≤ ↑n * Real.log y → x ≤ y ^ n
Real.pow_le_of_le_log : ∀ {x y : ℝ} {n : ℕ}, 0 < y → Real.log x ≤ ↑n * Real.log y → x ≤ y ^ n

Real.zpow_le_of_le_log : ∀ {x y : ℝ} {n : ℤ}, 0 < y → Real.log x ≤ ↑n * Real.log y → x ≤ y ^ n
Real.le_zpow_of_log_le : ∀ {x y : ℝ} {n : ℤ}, 0 < y → Real.log x ≤ ↑n * Real.log y → x ≤ y ^ n

NNReal.rpow_sub_natCast : ∀ {x : NNReal}, x ≠ 0 → ∀ (y : ℝ) (n : ℕ), x ^ (y - ↑n) = x ^ y / x ^ n
NNReal.rpow_sub_intCast : ∀ {x : NNReal}, x ≠ 0 → ∀ (y : ℝ) (n : ℕ), x ^ (y - ↑n) = x ^ y / x ^ n

tendsto_rpow_atTop_of_base_gt_one : ∀ (b : ℝ), 1 < b → Filter.Tendsto (fun x => b ^ x) Filter.atBot (nhds 0)
tendsto_rpow_atBot_of_base_gt_one : ∀ (b : ℝ), 1 < b → Filter.Tendsto (fun x => b ^ x) Filter.atBot (nhds 0)

AffineEquiv.coe_linear : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : _root_.Module k V₁]
  [inst_4 : _root_.Module k V₂] [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂),
  (↑e).linear = ↑e.linear
AffineEquiv.linear_toAffineMap : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : _root_.Module k V₁]
  [inst_4 : _root_.Module k V₂] [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂),
  (↑e).linear = ↑e.linear

AffineEquiv.equivUnitsAffineMap_symm_apply_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : _root_.Module k V₁] [inst_3 : AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁),
  (AffineEquiv.equivUnitsAffineMap.symm u) a = ↑u a
AffineEquiv.equivUnitsAffineMap_symm_apply_toFun : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : _root_.Module k V₁] [inst_3 : AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (a : P₁),
  (AffineEquiv.equivUnitsAffineMap.symm u) a = ↑u a

AffineEquiv.coe_toAffineMap : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : _root_.Module k V₁]
  [inst_4 : _root_.Module k V₂] [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), ⇑↑e = ⇑e
AffineEquiv.coe_coe : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : _root_.Module k V₁] [inst_4 : _root_.Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), ⇑↑e = ⇑e

Monotone.convex_gt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β]
  [inst_6 : _root_.Module 𝕜 E] [OrderedSMul 𝕜 E] {f : E → β}, Monotone f → ∀ (r : β), Convex 𝕜 {x | f x ≤ r}
Monotone.convex_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β]
  [inst_6 : _root_.Module 𝕜 E] [OrderedSMul 𝕜 E] {f : E → β}, Monotone f → ∀ (r : β), Convex 𝕜 {x | f x ≤ r}

Monotone.convex_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β]
  [inst_6 : _root_.Module 𝕜 E] [OrderedSMul 𝕜 E] {f : E → β}, Monotone f → ∀ (r : β), Convex 𝕜 {x | f x ≤ r}
Monotone.convex_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β]
  [inst_6 : _root_.Module 𝕜 E] [OrderedSMul 𝕜 E] {f : E → β}, Monotone f → ∀ (r : β), Convex 𝕜 {x | f x ≤ r}

ContinuousLinearMap.le_opENorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜]
  [inst_3 : NontriviallyNormedField 𝕜₂] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂}
  [inst_6 : RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) (x : E), ‖f x‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ
ContinuousLinearMap.le_opNorm_enorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜]
  [inst_3 : NontriviallyNormedField 𝕜₂] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂}
  [inst_6 : RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) (x : E), ‖f x‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ

Filter.Germ.const_nsmul : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [inst : SMul M G] (a : G)
  (n : M), ↑(n • a) = n • ↑a
Filter.Germ.const_smul : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [inst : SMul M G] (n : M)
  (a : G), ↑(n • a) = n • ↑a

MeasureTheory.MemLp.of_le_mul' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  {ε : Type u_7} {ε' : Type u_8} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [inst_2 : TopologicalSpace ε']
  [inst_3 : ContinuousENorm ε'] {f : α → ε} {g : α → ε'} {c : NNReal},
  MeasureTheory.MemLp g p μ →
    MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ) → MeasureTheory.MemLp f p μ
MeasureTheory.MemLp.of_enorm_le_mul : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal}
  {μ : MeasureTheory.Measure α} {ε : Type u_7} {ε' : Type u_8} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  [inst_2 : TopologicalSpace ε'] [inst_3 : ContinuousENorm ε'] {f : α → ε} {g : α → ε'} {c : NNReal},
  MeasureTheory.MemLp g p μ →
    MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ) → MeasureTheory.MemLp f p μ

MeasureTheory.measureReal_restrict_apply₀' : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s t : Set α}, MeasureTheory.NullMeasurableSet s μ → (μ.restrict s) t = μ (t ∩ s)
MeasureTheory.Measure.restrict_apply₀' : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s t : Set α}, MeasureTheory.NullMeasurableSet s μ → (μ.restrict s) t = μ (t ∩ s)

MeasureTheory.Content.innerContent_mono' : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G)
  ⦃U V : Set G⦄ (hU : IsOpen U) (hV : IsOpen V),
  U ⊆ V → μ.innerContent { carrier := U, is_open' := hU } ≤ μ.innerContent { carrier := V, is_open' := hV }
MeasureTheory.Content.innerContent_mono : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G)
  ⦃U V : Set G⦄ (hU : IsOpen U) (hV : IsOpen V),
  U ⊆ V → μ.innerContent { carrier := U, is_open' := hU } ≤ μ.innerContent { carrier := V, is_open' := hV }

Asymptotics.IsEquivalent.congr_right : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v w : α → β}
  {l : Filter α}, Asymptotics.IsEquivalent l u v → v =ᶠ[l] w → Asymptotics.IsEquivalent l u w
Asymptotics.IsEquivalent.trans_eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β]
  {l : Filter α} {f g₁ g₂ : α → β}, Asymptotics.IsEquivalent l f g₁ → g₁ =ᶠ[l] g₂ → Asymptotics.IsEquivalent l f g₂

Matrix.UnitaryGroup.inv_val : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v}
  [inst_2 : CommRing α] [inst_3 : StarRing α] (A : ↥(Matrix.unitaryGroup n α)), ↑A⁻¹ = star ↑A
Matrix.UnitaryGroup.inv_apply : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v}
  [inst_2 : CommRing α] [inst_3 : StarRing α] (A : ↥(Matrix.unitaryGroup n α)), ↑A⁻¹ = star ↑A

Matrix.UnitaryGroup.one_val : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v}
  [inst_2 : CommRing α] [inst_3 : StarRing α], ↑1 = 1
Matrix.UnitaryGroup.one_apply : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v}
  [inst_2 : CommRing α] [inst_3 : StarRing α], ↑1 = 1

Matrix.UnitaryGroup.mul_val : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v}
  [inst_2 : CommRing α] [inst_3 : StarRing α] (A B : ↥(Matrix.unitaryGroup n α)), ↑(A * B) = ↑A * ↑B
Matrix.UnitaryGroup.mul_apply : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v}
  [inst_2 : CommRing α] [inst_3 : StarRing α] (A B : ↥(Matrix.unitaryGroup n α)), ↑(A * B) = ↑A * ↑B

finSuccAboveOrderIso_symm_apply_ne_last : ∀ {n : ℕ} {p : Fin (n + 1)} (h : p ≠ Fin.last n) (x : { x // x ≠ p }),
  (finSuccAboveEquiv p).symm x = (p.castLT ⋯).predAbove ↑x
finSuccAboveEquiv_symm_apply_ne_last : ∀ {n : ℕ} {p : Fin (n + 1)} (h : p ≠ Fin.last n) (x : { x // x ≠ p }),
  (finSuccAboveEquiv p).symm x = (p.castLT ⋯).predAbove ↑x

Finset.prod_eq_prod_Ico_succ_bot : ∀ {M : Type u_2} [inst : CommMonoid M] {a b : ℕ},
  a < b → ∀ (f : ℕ → M), ∏ k ∈ Finset.Ico a b, f k = f a * ∏ k ∈ Finset.Ico (a + 1) b, f k
Finset.prod_eq_prod_Ico_succ_bot : ∀ {M : Type u_2} [inst : CommMonoid M] {a b : ℕ},
  a < b → ∀ (f : ℕ → M), ∏ k ∈ Finset.Ico a b, f k = f a * ∏ k ∈ Finset.Ico (a + 1) b, f k

Finset.sum_eq_sum_Ico_succ_bot : ∀ {M : Type u_2} [inst : AddCommMonoid M] {a b : ℕ},
  a < b → ∀ (f : ℕ → M), ∑ k ∈ Finset.Ico a b, f k = f a + ∑ k ∈ Finset.Ico (a + 1) b, f k
Finset.sum_eq_sum_Ico_succ_bot : ∀ {M : Type u_2} [inst : AddCommMonoid M] {a b : ℕ},
  a < b → ∀ (f : ℕ → M), ∑ k ∈ Finset.Ico a b, f k = f a + ∑ k ∈ Finset.Ico (a + 1) b, f k

Polynomial.smeval_def : ∀ {R : Type u_3} [inst : Semiring R] (p : Polynomial R) {S : Type u_4}
  [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ] [inst_3 : MulActionWithZero R S] (x : S),
  p.smeval x = p.sum (Polynomial.smul_pow x)
Polynomial.smeval_eq_sum : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) {S : Type u_2}
  [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ] [inst_3 : MulActionWithZero R S] (x : S),
  p.smeval x = p.sum (Polynomial.smul_pow x)

SkewMonoidAlgebra.single_zero_right : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] (a : G),
  SkewMonoidAlgebra.single a 0 = 0
SkewMonoidAlgebra.single_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] (a : G),
  SkewMonoidAlgebra.single a 0 = 0

Tropical.injective_trop : ∀ {R : Type u}, Function.Injective Tropical.trop
Tropical.trop_injective : ∀ {R : Type u}, Function.Injective Tropical.trop

Tropical.untrop_max : ∀ {R : Type u} [inst : LinearOrder R] (x y : Tropical R),
  Tropical.untrop (max x y) = max (Tropical.untrop x) (Tropical.untrop y)
Tropical.untrop_sup : ∀ {R : Type u} [inst : LinearOrder R] (x y : Tropical R),
  Tropical.untrop (max x y) = max (Tropical.untrop x) (Tropical.untrop y)

Tropical.trop_inf : ∀ {R : Type u} [inst : LinearOrder R] (x y : R),
  Tropical.trop (min x y) = Tropical.trop x + Tropical.trop y
Tropical.trop_min : ∀ {R : Type u} [inst : LinearOrder R] (x y : R),
  Tropical.trop (min x y) = Tropical.trop x + Tropical.trop y

Tropical.trop_max_def : ∀ {R : Type u} [inst : LinearOrder R] (x y : Tropical R),
  max x y = Tropical.trop (max (Tropical.untrop x) (Tropical.untrop y))
Tropical.trop_sup_def : ∀ {R : Type u} [inst : LinearOrder R] (x y : Tropical R),
  max x y = Tropical.trop (max (Tropical.untrop x) (Tropical.untrop y))

Tropical.injective_untrop : ∀ {R : Type u}, Function.Injective Tropical.untrop
Tropical.untrop_injective : ∀ {R : Type u}, Function.Injective Tropical.untrop

HahnSeries.orderTop_add_le_mul : ∀ {R : Type u_3} {Γ : Type u_6} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R},
  x.orderTop + y.orderTop ≤ (x * y).orderTop
HahnSeries.orderTop_add_orderTop_le_orderTop_mul : ∀ {R : Type u_3} {Γ : Type u_6} [inst : AddCommMonoid Γ]
  [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : NonUnitalNonAssocSemiring R]
  {x y : HahnSeries Γ R}, x.orderTop + y.orderTop ≤ (x * y).orderTop

AlgebraicGeometry.Scheme.comp_base : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base
AlgebraicGeometry.Scheme.comp_coeBase : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base

AlgebraicGeometry.Scheme.comp_coeBase_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  {Z_1 : TopCat} (h : ↑Z.toPresheafedSpace ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).base h =
    CategoryTheory.CategoryStruct.comp f.base (CategoryTheory.CategoryStruct.comp g.base h)
AlgebraicGeometry.Scheme.comp_base_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : TopCat}
  (h : ↑Z.toPresheafedSpace ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).base h =
    CategoryTheory.CategoryStruct.comp f.base (CategoryTheory.CategoryStruct.comp g.base h)

CategoryTheory.Functor.Final.exists_coeq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C]
  [F.Final] {d : D} {c : C} (s s' : d ⟶ F.obj c),
  ∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)
CategoryTheory.Functor.Final.exists_coeq_of_locally_small : ∀ {C : Type v₁} [inst : CategoryTheory.Category.{v₁, v₁} C]
  {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₁, u₂} D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.IsFilteredOrEmpty C] [F.Final] {d : D} {c : C} (s s' : d ⟶ F.obj c),
  ∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)

WeierstrassCurve.Projective.fin3_def : ∀ {R : Type r} (P : Fin 3 → R), ![P 0, P 1, P 2] = P
WeierstrassCurve.Jacobian.fin3_def : ∀ {R : Type r} (P : Fin 3 → R), ![P 0, P 1, P 2] = P

WeierstrassCurve.Projective.comp_fin3 : ∀ {R : Type r} {S : Type s} (f : R → S) (X Y Z : R),
  f ∘ ![X, Y, Z] = ![f X, f Y, f Z]
WeierstrassCurve.Jacobian.comp_fin3 : ∀ {R : Type r} {S : Type s} (f : R → S) (X Y Z : R),
  f ∘ ![X, Y, Z] = ![f X, f Y, f Z]

WeierstrassCurve.Projective.fin3_def_ext : ∀ {R : Type r} (X Y Z : R),
  ![X, Y, Z] 0 = X ∧ ![X, Y, Z] 1 = Y ∧ ![X, Y, Z] 2 = Z
WeierstrassCurve.Jacobian.fin3_def_ext : ∀ {R : Type r} (X Y Z : R),
  ![X, Y, Z] 0 = X ∧ ![X, Y, Z] 1 = Y ∧ ![X, Y, Z] 2 = Z

Fin.orderSucc_eq : ∀ {n : ℕ}, Order.succ = fun i => Fin.lastCases (Fin.last n) Fin.succ i
Fin.orderPred_eq : ∀ {n : ℕ}, Order.succ = fun i => Fin.lastCases (Fin.last n) Fin.succ i

CategoryTheory.ReflPrefunctor.congr_map : ∀ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V]
  (F : U ⥤q V) {X Y : U} {f g : X ⟶ Y}, f = g → F.map f = F.map g
Prefunctor.congr_map : ∀ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] (F : U ⥤q V) {X Y : U}
  {f g : X ⟶ Y}, f = g → F.map f = F.map g

FormalMultilinearSeries.le_radius_of_summable : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal},
  (Summable fun n => ‖p n‖ * ↑r ^ n) → ↑r ≤ p.radius
FormalMultilinearSeries.le_radius_of_summable_norm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {r : NNReal} (p : FormalMultilinearSeries 𝕜 E F),
  (Summable fun n => ‖p n‖ * ↑r ^ n) → ↑r ≤ p.radius

ContinuousLinearMap.analyticWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) (x : E), AnalyticWithinAt 𝕜 (⇑f) s x
ContinuousLinearEquiv.analyticWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) (x : E), AnalyticWithinAt 𝕜 (⇑f) s x

LinearIsometryEquiv.analyticWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) (x : E), AnalyticWithinAt 𝕜 (⇑f) s x
ContinuousLinearEquiv.analyticWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] (f : E →L[𝕜] F) (s : Set E) (x : E), AnalyticWithinAt 𝕜 (⇑f) s x

DifferentiableAt.fderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E},
  DifferentiableAt 𝕜 f x → UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 f s x = fderiv 𝕜 f x
fderivWithin_eq_fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E},
  UniqueDiffWithinAt 𝕜 s x → DifferentiableAt 𝕜 f x → fderivWithin 𝕜 f s x = fderiv 𝕜 f x

CStarMatrix.map_map : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} {B : Type u_6} {C : Type u_7} {M : Matrix m n A}
  {f : A → B} {g : B → C}, (M.map f).map g = M.map (g ∘ f)
Matrix.map_map : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {β : Type u_10} {γ : Type u_11}
  {f : α → β} {g : β → γ}, (M.map f).map g = M.map (g ∘ f)

exists_hasDerivWithinAt_eq_of_ge_of_le : ∀ {a b : ℝ} {f f' : ℝ → ℝ},
  a ≤ b →
    (∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) →
      ∀ {m : ℝ}, f' a ≤ m → m ≤ f' b → m ∈ f' '' Set.Icc a b
exists_hasDerivWithinAt_eq_of_le_of_ge : ∀ {a b : ℝ} {f f' : ℝ → ℝ},
  a ≤ b →
    (∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) →
      ∀ {m : ℝ}, f' a ≤ m → m ≤ f' b → m ∈ f' '' Set.Icc a b

achart_val : ∀ (H : Type u) {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
  [inst_2 : ChartedSpace H M] (x : M), ↑(achart H x) = chartAt H x
coe_achart : ∀ (H : Type u) {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
  [inst_2 : ChartedSpace H M] (x : M), ↑(achart H x) = chartAt H x

MDifferentiable.mfderivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H]
  {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5}
  [inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
  {f : M → M'} {x : M} {s : Set M},
  MDifferentiableAt I I' f x → UniqueMDiffWithinAt I s x → mfderivWithin I I' f s x = mfderiv I I' f x
mfderivWithin_eq_mfderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H]
  {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5}
  [inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M']
  {f : M → M'} {x : M} {s : Set M},
  UniqueMDiffWithinAt I s x → MDifferentiableAt I I' f x → mfderivWithin I I' f s x = mfderiv I I' f x

contMDiffAt_finset_sum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
  {H : Type u_3} [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x : M} {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiffAt I' I n (f i) x) → ContMDiffAt I' I n (fun x => ∑ i ∈ t, f i x) x
ContMDiffAt.sum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x₀ : M} {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiffAt I' I n (f i) x₀) → ContMDiffAt I' I n (fun x => ∑ i ∈ t, f i x) x₀

ContMDiffWithinAt.sum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
  {H : Type u_3} [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {x₀ : M} {t : Finset ι}
  {f : ι → M → G},
  (∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x₀) → ContMDiffWithinAt I' I n (fun x => ∑ i ∈ t, f i x) s x₀
contMDiffWithinAt_finset_sum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
  {H : Type u_3} [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι}
  {f : ι → M → G},
  (∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) → ContMDiffWithinAt I' I n (fun x => ∑ i ∈ t, f i x) s x

contMDiff_finset_prod : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
  {H : Type u_3} [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiff I' I n (f i)) → ContMDiff I' I n fun x => ∏ i ∈ t, f i x
ContMDiff.prod : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiff I' I n (f i)) → ContMDiff I' I n fun x => ∏ i ∈ t, f i x

contMDiffWithinAt_finset_prod : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
  {H : Type u_3} [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι}
  {f : ι → M → G},
  (∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) → ContMDiffWithinAt I' I n (fun x => ∏ i ∈ t, f i x) s x
ContMDiffWithinAt.prod : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
  {H : Type u_3} [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {x₀ : M} {t : Finset ι}
  {f : ι → M → G},
  (∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x₀) → ContMDiffWithinAt I' I n (fun x => ∏ i ∈ t, f i x) s x₀

ContMDiffAt.prod : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x₀ : M} {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiffAt I' I n (f i) x₀) → ContMDiffAt I' I n (fun x => ∏ i ∈ t, f i x) x₀
contMDiffAt_finset_prod : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
  {H : Type u_3} [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x : M} {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiffAt I' I n (f i) x) → ContMDiffAt I' I n (fun x => ∏ i ∈ t, f i x) x

contMDiff_finset_sum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
  {H : Type u_3} [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiff I' I n (f i)) → ContMDiff I' I n fun x => ∑ i ∈ t, f i x
ContMDiff.sum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiff I' I n (f i)) → ContMDiff I' I n fun x => ∑ i ∈ t, f i x

UpperHalfPlane.lt_dist_iff_lt_dist_coe_center : ∀ {z w : UpperHalfPlane} {r : ℝ},
  r < dist z w ↔ w.im * Real.sinh r < dist ↑z ↑(w.center r)
UpperHalfPlane.le_dist_iff_le_dist_coe_center : ∀ {z w : UpperHalfPlane} {r : ℝ},
  r < dist z w ↔ w.im * Real.sinh r < dist ↑z ↑(w.center r)

Cardinal.mk_subtype_le_of_countable_eventually_mem_aux : ∀ {α ι : Type u} {a : Cardinal.{u}} [Countable ι]
  {f : ι → Set α} {l : Filter ι} [l.NeBot] {t : Set α},
  (∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i) → (∀ (i : ι), Cardinal.mk ↑(f i) ≤ a) → Cardinal.mk ↑t ≤ a
Cardinal.mk_subtype_le_of_countable_eventually_mem : ∀ {α : Type u} {ι : Type v} {a : Cardinal.{u}} [Countable ι]
  {f : ι → Set α} {l : Filter ι} [l.NeBot] {t : Set α},
  (∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i) → (∀ (i : ι), Cardinal.mk ↑(f i) ≤ a) → Cardinal.mk ↑t ≤ a

ContinuousAffineEquiv.coe_injective : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : _root_.Module k V₁] [inst_3 : AddTorsor V₁ P₁]
  [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : _root_.Module k V₂] [inst_7 : AddTorsor V₂ P₂]
  [inst_8 : TopologicalSpace P₂], Function.Injective ContinuousAffineEquiv.toAffineEquiv
ContinuousAffineEquiv.toAffineEquiv_injective : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6}
  {V₂ : Type u_7} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : _root_.Module k V₁] [inst_3 : AddTorsor V₁ P₁]
  [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : _root_.Module k V₂] [inst_7 : AddTorsor V₂ P₂]
  [inst_8 : TopologicalSpace P₂], Function.Injective ContinuousAffineEquiv.toAffineEquiv

ContinuousAffineEquiv.image_symm_eq_preimage : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6}
  {V₂ : Type u_7} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : _root_.Module k V₁] [inst_3 : AddTorsor V₁ P₁]
  [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : _root_.Module k V₂] [inst_7 : AddTorsor V₂ P₂]
  [inst_8 : TopologicalSpace P₂] (e : P₁ ≃ᴬ[k] P₂) (s : Set P₂), ⇑e.symm '' s = ⇑e ⁻¹' s
ContinuousAffineEquiv.image_symm : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : _root_.Module k V₁] [inst_3 : AddTorsor V₁ P₁]
  [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : _root_.Module k V₂] [inst_7 : AddTorsor V₂ P₂]
  [inst_8 : TopologicalSpace P₂] (f : P₁ ≃ᴬ[k] P₂) (s : Set P₂), ⇑f.symm '' s = ⇑f ⁻¹' s

ContinuousAffineEquiv.symm_refl : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : _root_.Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁],
  (ContinuousAffineEquiv.refl k P₁).symm = ContinuousAffineEquiv.refl k P₁
ContinuousAffineEquiv.refl_symm : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : _root_.Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁],
  (ContinuousAffineEquiv.refl k P₁).symm = ContinuousAffineEquiv.refl k P₁

SchwartzMap.coeFn_zero : ∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F], ⇑0 = 0
SchwartzMap.coe_zero : ∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F], ⇑0 = 0

mem_pairSelfAdjointMatricesSubmodule' : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {n : Type u_5} [inst_1 : Fintype n]
  (J J₃ A : Matrix n n R₂) [inst_2 : DecidableEq n], A ∈ pairSelfAdjointMatricesSubmodule J J₃ ↔ J.IsAdjointPair J₃ A A
mem_pairSelfAdjointMatricesSubmodule : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : Fintype n]
  (J J₂ A₁ : Matrix n n R) [inst_2 : DecidableEq n],
  A₁ ∈ pairSelfAdjointMatricesSubmodule J J₂ ↔ J.IsAdjointPair J₂ A₁ A₁

mem_skewAdjointMatricesSubmodule' : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {n : Type u_5} [inst_1 : Fintype n]
  (J A : Matrix n n R₂) [inst_2 : DecidableEq n], A ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A
mem_skewAdjointMatricesSubmodule : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : Fintype n]
  (J A₁ : Matrix n n R) [inst_2 : DecidableEq n], A₁ ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A₁

mem_selfAdjointMatricesSubmodule' : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {n : Type u_5} [inst_1 : Fintype n]
  (J A : Matrix n n R₂) [inst_2 : DecidableEq n], A ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A
mem_selfAdjointMatricesSubmodule : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : Fintype n]
  (J A₁ : Matrix n n R) [inst_2 : DecidableEq n], A₁ ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A₁

IsDedekindDomain.HeightOneSpectrum.intValuationDef_zero : ∀ {R : Type u_1} [inst : CommRing R]
  [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R), v.intValuationDef 0 = 0
IsDedekindDomain.HeightOneSpectrum.intValuation.map_zero' : ∀ {R : Type u_1} [inst : CommRing R]
  [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R), v.intValuationDef 0 = 0

PiTensorProduct.tprodL_apply : ∀ {ι : Type uι} [inst : Fintype ι] (𝕜 : Type u𝕜) [inst_1 : NontriviallyNormedField 𝕜]
  {E : ι → Type uE} [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  (a : (i : ι) → E i), (PiTensorProduct.tprodL 𝕜) a = (PiTensorProduct.tprod 𝕜) a
PiTensorProduct.tprodL_toFun : ∀ {ι : Type uι} [inst : Fintype ι] (𝕜 : Type u𝕜) [inst_1 : NontriviallyNormedField 𝕜]
  {E : ι → Type uE} [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  (a : (i : ι) → E i), (PiTensorProduct.tprodL 𝕜) a = (PiTensorProduct.tprod 𝕜) a

PiTensorProduct.mapLMultilinear_apply_apply : ∀ {ι : Type uι} [inst : Fintype ι] (𝕜 : Type u𝕜)
  [inst_1 : NontriviallyNormedField 𝕜] (E : ι → Type uE) [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (E' : ι → Type u_1) [inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)]
  [inst_5 : (i : ι) → NormedSpace 𝕜 (E' i)] (f : (i : ι) → E i →L[𝕜] E' i) (a : PiTensorProduct 𝕜 fun i => E i),
  ((PiTensorProduct.mapLMultilinear 𝕜 E E') f) a =
    (PiTensorProduct.liftAux ((PiTensorProduct.tprodL 𝕜).compContinuousLinearMap f).toMultilinearMap) a
PiTensorProduct.mapLMultilinear_toFun_apply : ∀ {ι : Type uι} [inst : Fintype ι] (𝕜 : Type u𝕜)
  [inst_1 : NontriviallyNormedField 𝕜] (E : ι → Type uE) [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (E' : ι → Type u_1) [inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)]
  [inst_5 : (i : ι) → NormedSpace 𝕜 (E' i)] (f : (i : ι) → E i →L[𝕜] E' i) (a : PiTensorProduct 𝕜 fun i => E i),
  ((PiTensorProduct.mapLMultilinear 𝕜 E E') f) a =
    (PiTensorProduct.liftAux ((PiTensorProduct.tprodL 𝕜).compContinuousLinearMap f).toMultilinearMap) a

Subgroup.IsComplement.card_mul_card : ∀ {G : Type u_1} [inst : Group G] {S T : Set G},
  Subgroup.IsComplement S T → Nat.card ↑S * Nat.card ↑T = Nat.card G
Subgroup.IsComplement.card_mul : ∀ {G : Type u_1} [inst : Group G] {S T : Set G},
  Subgroup.IsComplement S T → Nat.card ↑S * Nat.card ↑T = Nat.card G

Action.forget_ε : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V],
  CategoryTheory.Functor.LaxMonoidal.ε (Action.forget V G) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)
Action.forget_η : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{u_3, u_1} V] (G : Type u_2) [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V],
  CategoryTheory.Functor.LaxMonoidal.ε (Action.forget V G) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)

Mathlib.Tactic.Bicategory.eval_bicategoricalComp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B}
  {f g h i : a ⟶ b} {η η' : f ⟶ g} {α : g ≅ h} {θ θ' : h ⟶ i} {αθ : g ⟶ i} {ηαθ : f ⟶ i},
  η = η' →
    θ = θ' →
      CategoryTheory.CategoryStruct.comp α.hom θ' = αθ →
        CategoryTheory.CategoryStruct.comp η' αθ = ηαθ →
          CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp α.hom θ) = ηαθ
Mathlib.Tactic.Bicategory.eval_monoidalComp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B}
  {f g h i : a ⟶ b} {η η' : f ⟶ g} {α : g ≅ h} {θ θ' : h ⟶ i} {αθ : g ⟶ i} {ηαθ : f ⟶ i},
  η = η' →
    θ = θ' →
      CategoryTheory.CategoryStruct.comp α.hom θ' = αθ →
        CategoryTheory.CategoryStruct.comp η' αθ = ηαθ →
          CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp α.hom θ) = ηαθ

SimpleGraph.Walk.tail_cons_eq : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (SimpleGraph.Walk.cons h p).tail = p.copy ⋯ ⋯
SimpleGraph.Walk.tail_cons : ∀ {V : Type u} {G : SimpleGraph V} {t u v : V} (p : G.Walk u v) (h : G.Adj t u),
  (SimpleGraph.Walk.cons h p).tail = p.copy ⋯ ⋯

IncidenceAlgebra.zeta_mul_kappa : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : NonAssocSemiring 𝕜] [inst_1 : Preorder α]
  [inst_2 : LocallyFiniteOrder α] [inst_3 : DecidableLE α] (a b : α),
  (IncidenceAlgebra.zeta 𝕜 * IncidenceAlgebra.zeta 𝕜) a b = ↑(Finset.Icc a b).card
IncidenceAlgebra.zeta_mul_zeta : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : NonAssocSemiring 𝕜] [inst_1 : Preorder α]
  [inst_2 : LocallyFiniteOrder α] [inst_3 : DecidableLE α] (a b : α),
  (IncidenceAlgebra.zeta 𝕜 * IncidenceAlgebra.zeta 𝕜) a b = ↑(Finset.Icc a b).card

Combinatorics.Subspace.coe_apply : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} (l : Combinatorics.Subspace η α ι)
  (x : η → α) (i : ι), ↑l x i = Sum.elim id x (l.idxFun i)
Combinatorics.Subspace.apply_def : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} (l : Combinatorics.Subspace η α ι)
  (x : η → α) (i : ι), ↑l x i = Sum.elim id x (l.idxFun i)

ultrafilter_pure_injective : ∀ {α : Type u}, Function.Injective pure
Ultrafilter.pure_injective : ∀ {α : Type u}, Function.Injective pure

TypeVec.subtypeVal_diagSub : ∀ {n : ℕ} {α : TypeVec.{u_1} n},
  TypeVec.comp (TypeVec.subtypeVal α.repeatEq) TypeVec.diagSub = TypeVec.prod.diag
TypeVec.diag_sub_val : ∀ {n : ℕ} {α : TypeVec.{u} n},
  TypeVec.comp (TypeVec.subtypeVal α.repeatEq) TypeVec.diagSub = TypeVec.prod.diag

TypeVec.prod_id : ∀ {n : ℕ} {α β : TypeVec.{u} n}, TypeVec.prod.map TypeVec.id TypeVec.id = TypeVec.id
TypeVec.prod_map_id : ∀ {n : ℕ} {α β : TypeVec.{u_1} n}, TypeVec.prod.map TypeVec.id TypeVec.id = TypeVec.id

Matroid.ext_iff_indep : ∀ {α : Type u_1} {M₁ M₂ : Matroid α},
  M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
Matroid.ext_indep_iff : ∀ {α : Type u_1} {M₁ M₂ : Matroid α},
  M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)

Matroid.IsBasis.restrict_isBase : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  M.IsBasis I X → (M.restrict X).IsBase I
Matroid.IsBasis.isBase_restrict : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  M.IsBasis I X → (M.restrict X).IsBase I

Matroid.eq_loopyOn_iff_loops_eq : ∀ {α : Type u_1} {M : Matroid α} {E : Set α},
  M = Matroid.loopyOn E ↔ M.loops = E ∧ M.E = E
Matroid.eq_loopyOn_iff_loops : ∀ {α : Type u_1} {M : Matroid α} {E : Set α},
  M = Matroid.loopyOn E ↔ M.loops = E ∧ M.E = E

Matroid.IsBase.mem_of_isColoop : ∀ {α : Type u_1} {M : Matroid α} {e : α} {B : Set α}, M.IsBase B → M.IsColoop e → e ∈ B
Matroid.IsColoop.mem_of_isBase : ∀ {α : Type u_1} {M : Matroid α} {e : α} {B : Set α}, M.IsColoop e → M.IsBase B → e ∈ B

Matroid.IsBasis'.finite_of_isRkFinite : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α},
  M.IsBasis' I X → M.IsRkFinite X → I.Finite
Matroid.IsRkFinite.finite_of_isBasis' : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α},
  M.IsRkFinite X → M.IsBasis' I X → I.Finite

Matroid.IsRkFinite.finite_of_isBasis : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α},
  M.IsRkFinite X → M.IsBasis I X → I.Finite
Matroid.IsBasis.finite_of_isRkFinite : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α},
  M.IsBasis I X → M.IsRkFinite X → I.Finite

PartENat.toWithTop_natCast : ∀ (n : ℕ) {x : Decidable (↑n).Dom}, (↑n).toWithTop = ↑n
PartENat.toWithTop_natCast' : ∀ (n : ℕ) {x : Decidable (↑n).Dom}, (↑n).toWithTop = ↑n

PFunctor.M.bisim : ∀ {P : PFunctor.{u}} (R : P.M → P.M → Prop),
  (∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)) →
    ∀ (x y : P.M), R x y → x = y
PFunctor.M.bisim_equiv : ∀ {P : PFunctor.{u}} (R : P.M → P.M → Prop),
  (∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)) →
    ∀ (x y : P.M), R x y → x = y

AlgebraicIndependent.to_subtype_range : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R]
  [inst_1 : CommRing A] [inst_2 : Algebra R A], AlgebraicIndependent R x → AlgebraicIndependent R Subtype.val
AlgebraicIndependent.coe_range : ∀ {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [inst : CommRing R]
  [inst_1 : CommRing A] [inst_2 : Algebra R A], AlgebraicIndependent R x → AlgebraicIndependent R Subtype.val

Pretrivialization.linearMapAt_eq_zero : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4}
  [inst : Semiring R] [inst_1 : TopologicalSpace F] [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F]
  [inst_4 : _root_.Module R F] [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → _root_.Module R (E x)]
  (e : Pretrivialization F Bundle.TotalSpace.proj) [inst_7 : Pretrivialization.IsLinear R e] {b : B},
  b ∉ e.baseSet → Pretrivialization.linearMapAt R e b = 0
Pretrivialization.linearMapAt_def_of_not_mem : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4}
  [inst : Semiring R] [inst_1 : TopologicalSpace F] [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F]
  [inst_4 : _root_.Module R F] [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → _root_.Module R (E x)]
  (e : Pretrivialization F Bundle.TotalSpace.proj) [inst_7 : Pretrivialization.IsLinear R e] {b : B},
  b ∉ e.baseSet → Pretrivialization.linearMapAt R e b = 0

IsLocalDiffeomorphAt.localInverse_contMDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] {H : Type u_4} [inst_5 : TopologicalSpace H] {G : Type u_5} [inst_6 : TopologicalSpace G]
  {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞}
  {f : M → N} {x : M} (hf : IsLocalDiffeomorphAt I J n f x),
  ContMDiffOn J I n (↑hf.localInverse.toPartialEquiv) hf.localInverse.source
IsLocalDiffeomorphAt.contmdiffOn_localInverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] {H : Type u_4} [inst_5 : TopologicalSpace H] {G : Type u_5} [inst_6 : TopologicalSpace G]
  {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞}
  {f : M → N} {x : M} (hf : IsLocalDiffeomorphAt I J n f x),
  ContMDiffOn J I n (↑hf.localInverse.toPartialEquiv) hf.localInverse.source

MeasureTheory.measurable_uniqueElim_cylinderEvents : ∀ {ι : Type u_2} {X : ι → Type u_3}
  [m : (i : ι) → MeasurableSpace (X i)] [inst : Unique ι], Measurable uniqueElim
measurable_uniqueElim : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)]
  [inst_1 : Unique δ], Measurable uniqueElim

MeasureTheory.ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω]
  (ν : MeasureTheory.ProbabilityMeasure Ω), ⇑ν.toFiniteMeasure = ⇑ν
MeasureTheory.ProbabilityMeasure.coeFn_toFiniteMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω]
  (μ : MeasureTheory.ProbabilityMeasure Ω), ⇑μ.toFiniteMeasure = ⇑μ

MeasureTheory.ProbabilityMeasure.toFiniteMeasure_apply : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω]
  (μ : MeasureTheory.ProbabilityMeasure Ω) (s : Set Ω), μ.toFiniteMeasure s = μ s
MeasureTheory.ProbabilityMeasure.toFiniteMeasure_apply_eq_apply : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω]
  (ν : MeasureTheory.ProbabilityMeasure Ω) (s : Set Ω), ν.toFiniteMeasure s = ν s

MvPowerSeries.eq_zero_iff_forall_coeff_eq_zero_and : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R]
  {f : MvPowerSeries σ R}, f = 0 ↔ ∀ (d : σ →₀ ℕ), (MvPowerSeries.coeff R d) f = 0
MvPowerSeries.eq_zero_iff_forall_coeff_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R]
  {f : MvPowerSeries σ R}, f = 0 ↔ ∀ (d : σ →₀ ℕ), (MvPowerSeries.coeff R d) f = 0

Ring.choose_eq_nat_choose : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R]
  [NatPowAssoc R] (n k : ℕ), Ring.choose (↑n) k = ↑(n.choose k)
Ring.choose_natCast : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R]
  [NatPowAssoc R] (n k : ℕ), Ring.choose (↑n) k = ↑(n.choose k)

HahnSeries.SummableFamily.coeff_def : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ]
  [inst_1 : AddCommMonoid R] (s : HahnSeries.SummableFamily Γ R α) (a : α) (g : Γ), (s.coeff g) a = (s a).coeff g
HahnSeries.SummableFamily.coeff_toFun : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ]
  [inst_1 : AddCommMonoid R] (s : HahnSeries.SummableFamily Γ R α) (g : Γ) (a : α), (s.coeff g) a = (s a).coeff g

AlgebraicGeometry.Polynomial.isOpenMap_comap_C : ∀ {R : Type u_1} [inst : CommRing R],
  IsOpenMap ⇑(PrimeSpectrum.comap Polynomial.C)
Polynomial.isOpenMap_comap_C : ∀ {R : Type u_1} [inst : CommRing R], IsOpenMap ⇑(PrimeSpectrum.comap Polynomial.C)

Nimber.bot_eq_zero : ⊥ = 0
Nat.bot_eq_zero : ⊥ = 0

Mathlib.Tactic.LinearCombination'.pf_div_c : ∀ {α : Type u_1} {a b : α} [inst : Div α], a = b → ∀ (c : α), a / c = b / c
Mathlib.Tactic.LinearCombination.div_eq_const : ∀ {α : Type u_1} {a b : α} [inst : Div α],
  a = b → ∀ (c : α), a / c = b / c

Mathlib.Tactic.LinearCombination'.c_mul_pf : ∀ {α : Type u_1} {b c : α} [inst : Mul α], b = c → ∀ (a : α), a * b = a * c
Mathlib.Tactic.LinearCombination.mul_const_eq : ∀ {α : Type u_1} {b c : α} [inst : Mul α],
  b = c → ∀ (a : α), a * b = a * c

Mathlib.Tactic.LinearCombination'.pf_mul_c : ∀ {α : Type u_1} {a b : α} [inst : Mul α], a = b → ∀ (c : α), a * c = b * c
Mathlib.Tactic.LinearCombination.mul_eq_const : ∀ {α : Type u_1} {a b : α} [inst : Mul α],
  a = b → ∀ (c : α), a * c = b * c

Mathlib.Tactic.LinearCombination'.add_pf : ∀ {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [inst : Add α],
  a₁ = b₁ → a₂ = b₂ → a₁ + a₂ = b₁ + b₂
Mathlib.Tactic.LinearCombination.add_eq_eq : ∀ {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [inst : Add α],
  a₁ = b₁ → a₂ = b₂ → a₁ + a₂ = b₁ + b₂

Mathlib.Tactic.LinearCombination'.eq_of_add_pow : ∀ {α : Type u_1} {a a' b b' : α} [inst : Ring α] [NoZeroDivisors α]
  (n : ℕ), a = b → (a' - b') ^ n - (a - b) = 0 → a' = b'
Mathlib.Tactic.LinearCombination.eq_of_add_pow : ∀ {α : Type u_1} {a a' b b' : α} [inst : Ring α] [NoZeroDivisors α]
  (n : ℕ), a = b → (a' - b') ^ n - (a - b) = 0 → a' = b'

Mathlib.Meta.Multiset.insert_eq_cons : ∀ {α : Type u_1} (a : α) (s : Multiset α), insert a s = a ::ₘ s
Multiset.insert_eq_cons : ∀ {α : Type u_1} (a : α) (s : Multiset α), insert a s = a ::ₘ s

CpltSepUniformSpace.hom_ofHom : ∀ {X Y : Type u} [inst : UniformSpace X] [inst_1 : UniformSpace Y]
  (f : { f // UniformContinuous f }), UniformSpaceCat.Hom.hom (UniformSpaceCat.ofHom f) = f
UniformSpaceCat.hom_ofHom : ∀ {X Y : Type u} [inst : UniformSpace X] [inst_1 : UniformSpace Y]
  (f : { f // UniformContinuous f }), UniformSpaceCat.Hom.hom (UniformSpaceCat.ofHom f) = f