Loogle!

Result

Found 8326 declarations mentioning Equiv. Of these, only the first 200 are shown.

• Equiv 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u_1) (β : Sort u_2) : Sort (max (max 1 u_1) u_2)
• Equiv.propEquivBool 📋 Mathlib.Logic.Equiv.Defs
  : Prop ≃ Bool
• Equiv.punitEquivPUnit 📋 Mathlib.Logic.Equiv.Defs
  : PUnit.{v} ≃ PUnit.{w}
• Equiv.refl 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u_1) : α ≃ α
• Equiv.arrowPUnitEquivPUnit 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u_1) : (α → PUnit.{v}) ≃ PUnit.{w}
• Equiv.emptyArrowEquivPUnit 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u_1) : (Empty → α) ≃ PUnit.{u}
• Equiv.falseArrowEquivPUnit 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u_1) : (False → α) ≃ PUnit.{u}
• Equiv.inhabited' 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} : Inhabited (α ≃ α)
• Equiv.pemptyArrowEquivPUnit 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u_1) : (PEmpty.{u_2} → α) ≃ PUnit.{u}
• Equiv.plift 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} : PLift α ≃ α
• Equiv.propEquivPUnit 📋 Mathlib.Logic.Equiv.Defs
  {p : Prop} (h : p) : p ≃ PUnit.{0}
• Equiv.punitArrowEquiv 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u_1) : (PUnit.{u} → α) ≃ α
• Equiv.trueArrowEquiv 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u_1) : (True → α) ≃ α
• Equiv.ulift 📋 Mathlib.Logic.Equiv.Defs
  {α : Type v} : ULift.{u, v} α ≃ α
• Equiv.equivEmpty 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u) [IsEmpty α] : α ≃ Empty
• Equiv.equivPEmpty 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort v) [IsEmpty α] : α ≃ PEmpty.{u}
• Equiv.equivPUnit 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u) [Unique α] : α ≃ PUnit.{v}
• Equiv.propEquivPEmpty 📋 Mathlib.Logic.Equiv.Defs
  {p : Prop} (h : ¬p) : p ≃ PEmpty.{u_1}
• Equiv.equivEmptyEquiv 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u) : α ≃ Empty ≃ IsEmpty α
• Equiv.instTrans 📋 Mathlib.Logic.Equiv.Defs
  : Trans Equiv Equiv Equiv
• Equiv.invFun 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} (self : α ≃ β) : β → α
• Equiv.toFun 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} (self : α ≃ β) : α → β
• Equiv.Simps.symm_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : β → α
• finOneEquiv 📋 Mathlib.Logic.Equiv.Defs
  : Fin 1 ≃ Unit
• finTwoEquiv 📋 Mathlib.Logic.Equiv.Defs
  : Fin 2 ≃ Bool
• finZeroEquiv 📋 Mathlib.Logic.Equiv.Defs
  : Fin 0 ≃ Empty
• finZeroEquiv' 📋 Mathlib.Logic.Equiv.Defs
  : Fin 0 ≃ PEmpty.{u}
• Equiv.arrowPUnitOfIsEmpty 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u_1) (β : Sort u_2) [IsEmpty α] : (α → β) ≃ PUnit.{u}
• Equiv.equiv_subsingleton_cod 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} [Subsingleton β] : Subsingleton (α ≃ β)
• Equiv.equiv_subsingleton_dom 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} [Subsingleton α] : Subsingleton (α ≃ β)
• Equiv.funUnique 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u) (β : Sort u_1) [Unique α] : (α → β) ≃ β
• Equiv.instEquivLike 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} : EquivLike (α ≃ β) α β
• Equiv.instFunLike 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} : FunLike (α ≃ β) α β
• Equiv.ofIff 📋 Mathlib.Logic.Equiv.Defs
  {P Q : Prop} (h : P ↔ Q) : P ≃ Q
• Equiv.symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : β ≃ α
• Equiv.cast 📋 Mathlib.Logic.Equiv.Defs
  {α β : Sort u_1} (h : α = β) : α ≃ β
• Equiv.decidableEq 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) [DecidableEq β] : DecidableEq α
• Equiv.equivOfIsEmpty 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u_1) (β : Sort u_2) [IsEmpty α] [IsEmpty β] : α ≃ β
• Equiv.equivOfUnique 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u) (β : Sort v) [Unique α] [Unique β] : α ≃ β
• Equiv.inhabited 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} [Inhabited β] (e : α ≃ β) : Inhabited α
• Equiv.nonempty 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) [Nonempty β] : Nonempty α
• Equiv.nontrivial 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_1} {β : Type u_2} (e : α ≃ β) [Nontrivial β] : Nontrivial α
• Equiv.ofUnique 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u) (β : Sort v) [Unique α] [Unique β] : α ≃ β
• Equiv.subsingleton 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) [Subsingleton β] : Subsingleton α
• Equiv.unique 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} [Unique β] (e : α ≃ β) : Unique α
• Equiv.subsingleton.symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) [Subsingleton α] : Subsingleton β
• Equiv.conj 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : (α → α) ≃ (β → β)
• Equiv.nonempty_congr 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : Nonempty α ↔ Nonempty β
• Equiv.nontrivial_congr 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_1} {β : Type u_2} (e : α ≃ β) : Nontrivial α ↔ Nontrivial β
• Equiv.permCongr 📋 Mathlib.Logic.Equiv.Defs
  {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') : Equiv.Perm α' ≃ Equiv.Perm β'
• Equiv.sigmaEquivProd 📋 Mathlib.Logic.Equiv.Defs
  (α : Type u_1) (β : Type u_2) : (_ : α) × β ≃ α × β
• Equiv.subsingleton_congr 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : Subsingleton α ↔ Subsingleton β
• Equiv.ofBijective 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f) : α ≃ β
• EquivLike.toEquiv 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (f : F) : α ≃ β
• instCoeTCEquivOfEquivLike 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] : CoeTC F (α ≃ β)
• Equiv.psigmaEquivSubtype 📋 Mathlib.Logic.Equiv.Defs
  {α : Type v} (P : α → Prop) : (i : α) ×' P i ≃ Subtype P
• Equiv.refl_symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} : (Equiv.refl α).symm = Equiv.refl α
• Equiv.symm_bijective 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} : Function.Bijective Equiv.symm
• Equiv.trans 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ
• Equiv.sigmaPLiftEquivSubtype 📋 Mathlib.Logic.Equiv.Defs
  {α : Type v} (P : α → Prop) : (i : α) × PLift (P i) ≃ Subtype P
• Equiv.psigmaEquivSigma 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_2} (β : α → Type u_1) : (i : α) ×' β i ≃ (i : α) × β i
• Equiv.sigmaULiftPLiftEquivSubtype 📋 Mathlib.Logic.Equiv.Defs
  {α : Type v} (P : α → Prop) : (i : α) × ULift.{u_1, 0} (PLift (P i)) ≃ Subtype P
• Equiv.arrowCongr 📋 Mathlib.Logic.Equiv.Defs
  {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : (α₁ → β₁) ≃ (α₂ → β₂)
• Equiv.arrowCongr' 📋 Mathlib.Logic.Equiv.Defs
  {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (hα : α₁ ≃ α₂) (hβ : β₁ ≃ β₂) : (α₁ → β₁) ≃ (α₂ → β₂)
• Equiv.conj_refl 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} : (Equiv.refl α).conj = Equiv.refl (α → α)
• Equiv.piUnique 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} [Unique α] (β : α → Sort u_1) : ((i : α) → β i) ≃ β default
• Equiv.functionSwap 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u_1) (β : Sort u_2) (γ : α → β → Sort u_3) : ((a : α) → (b : β) → γ a b) ≃ ((b : β) → (a : α) → γ a b)
• Equiv.left_inv 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} (self : α ≃ β) : Function.LeftInverse self.invFun self.toFun
• Equiv.right_inv 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} (self : α ≃ β) : Function.RightInverse self.invFun self.toFun
• Equiv.sigmaEquivProdOfEquiv 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_1} {β : Type u_2} {β₁ : α → Type u_3} (F : (a : α) → β₁ a ≃ β) : Sigma β₁ ≃ α × β
• Equiv.equivCongr 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α ≃ β) (cd : γ ≃ δ) : α ≃ γ ≃ (β ≃ δ)
• Equiv.refl_trans 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : (Equiv.refl α).trans e = e
• Equiv.symm_symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : e.symm.symm = e
• Equiv.trans_refl 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : e.trans (Equiv.refl β) = e
• Equiv.coe_refl 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} : ⇑(Equiv.refl α) = id
• Equiv.refl_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} (x : α) : (Equiv.refl α) x = x
• Equiv.sumIsLeft 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_1} {β : Type u_2} : { x // x.isLeft = true } ≃ α
• Equiv.sumIsRight 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_1} {β : Type u_2} : { x // x.isRight = true } ≃ β
• Equiv.bijective 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : Function.Bijective ⇑e
• Equiv.cast_refl 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} (h : α = α := ⋯) : Equiv.cast h = Equiv.refl α
• Equiv.injective 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : Function.Injective ⇑e
• Equiv.mk 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} (toFun : α → β) (invFun : β → α) (left_inv : Function.LeftInverse invFun toFun) (right_inv : Function.RightInverse invFun toFun) : α ≃ β
• Equiv.psigmaEquivSigmaPLift 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_2} (β : α → Sort u_1) : (i : α) ×' β i ≃ (i : PLift α) × PLift (β i.down)
• Equiv.surjective 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : Function.Surjective ⇑e
• Equiv.arrowCongr'_refl 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_1} {β : Type u_2} : (Equiv.refl α).arrowCongr' (Equiv.refl β) = Equiv.refl (α → β)
• Equiv.arrowCongr_refl 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} : (Equiv.refl α).arrowCongr (Equiv.refl β) = Equiv.refl (α → β)
• Equiv.self_trans_symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : e.trans e.symm = Equiv.refl α
• Equiv.symm_trans_self 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : e.symm.trans e = Equiv.refl β
• Equiv.equivPUnit_apply 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u) [Unique α] (a✝ : α) : (Equiv.equivPUnit α) a✝ = PUnit.unit
• Equiv.coe_fn_injective 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} : Function.Injective fun e => ⇑e
• Equiv.psigmaCongrRight 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β₁ : α → Sort u_1} {β₂ : α → Sort u_2} (F : (a : α) → β₁ a ≃ β₂ a) : (a : α) ×' β₁ a ≃ (a : α) ×' β₂ a
• Equiv.sigmaCongrRight 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_3} {β₁ : α → Type u_1} {β₂ : α → Type u_2} (F : (a : α) → β₁ a ≃ β₂ a) : (a : α) × β₁ a ≃ (a : α) × β₂ a
• Equiv.equivCongr_refl 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} : (Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α ≃ β)
• Equiv.plift_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} : ⇑Equiv.plift = PLift.down
• Equiv.toFun_as_coe 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : e.toFun = ⇑e
• Equiv.ulift_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Type v} : ⇑Equiv.ulift = ULift.down
• Quot.congrRight 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {r r' : α → α → Prop} (eq : ∀ (a₁ a₂ : α), r a₁ a₂ ↔ r' a₁ a₂) : Quot r ≃ Quot r'
• Equiv.cast_symm 📋 Mathlib.Logic.Equiv.Defs
  {α β : Sort u_1} (h : α = β) : (Equiv.cast h).symm = Equiv.cast ⋯
• Equiv.forall_congr_right 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {q : β → Prop} (e : α ≃ β) : (∀ (a : α), q (e a)) ↔ ∀ (b : β), q b
• Quotient.congrRight 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {r r' : Setoid α} (eq : ∀ (a₁ a₂ : α), r a₁ a₂ ↔ r' a₁ a₂) : Quotient r ≃ Quotient r'
• Equiv.invFun_as_coe 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : e.invFun = ⇑e.symm
• Equiv.conj_symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : e.conj.symm = e.symm.conj
• Equiv.permCongr_symm 📋 Mathlib.Logic.Equiv.Defs
  {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') : e.permCongr.symm = e.symm.permCongr
• Equiv.equivPUnit_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u) [Unique α] (a✝ : PUnit.{v}) : (Equiv.equivPUnit α).symm a✝ = default
• Equiv.forall_congr_left 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {p : α → Prop} (e : α ≃ β) : (∀ (a : α), p a) ↔ ∀ (b : β), p (e.symm b)
• Equiv.cast_apply 📋 Mathlib.Logic.Equiv.Defs
  {α β : Sort u_1} (h : α = β) (x : α) : (Equiv.cast h) x = cast h x
• Equiv.existsUnique_congr_right 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {q : β → Prop} (e : α ≃ β) : (∃! a, q (e a)) ↔ ∃! b, q b
• Equiv.exists_congr_right 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {q : β → Prop} (e : α ≃ β) : (∃ a, q (e a)) ↔ ∃ b, q b
• Equiv.ofBijective_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f) (a✝ : α) : (Equiv.ofBijective f hf) a✝ = f a✝
• Equiv.psigmaCongrRight_refl 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_2} {β : α → Sort u_1} : (Equiv.psigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl ((a : α) ×' β a)
• Equiv.sigmaCongrLeft 📋 Mathlib.Logic.Equiv.Defs
  {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ → Type u_3} (e : α₁ ≃ α₂) : (a : α₁) × β (e a) ≃ (a : α₂) × β a
• Equiv.sigmaCongrRight_refl 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_2} {β : α → Type u_1} : (Equiv.sigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl ((a : α) × β a)
• Equiv.eq_symm_iff_trans_eq_refl 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {f : α ≃ β} {g : β ≃ α} : f = g.symm ↔ f.trans g = Equiv.refl α
• Equiv.symm_eq_iff_trans_eq_refl 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {f : α ≃ β} {g : β ≃ α} : f.symm = g ↔ f.trans g = Equiv.refl α
• Equiv.trans_eq_refl_iff_eq_symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {f : α ≃ β} {g : β ≃ α} : f.trans g = Equiv.refl α ↔ f = g.symm
• Equiv.trans_eq_refl_iff_symm_eq 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {f : α ≃ β} {g : β ≃ α} : f.trans g = Equiv.refl α ↔ f.symm = g
• Equiv.bijective_comp 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ) : Function.Bijective (f ∘ ⇑e) ↔ Function.Bijective f
• Equiv.cast_eq_iff_heq 📋 Mathlib.Logic.Equiv.Defs
  {α β : Sort u_1} (h : α = β) {a : α} {b : β} : (Equiv.cast h) a = b ↔ HEq a b
• Equiv.comp_bijective 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ) : Function.Bijective (⇑e ∘ f) ↔ Function.Bijective f
• Equiv.comp_injective 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ) : Function.Injective (⇑e ∘ f) ↔ Function.Injective f
• Equiv.comp_surjective 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ) : Function.Surjective (⇑e ∘ f) ↔ Function.Surjective f
• Equiv.existsUnique_congr_left 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {p : α → Prop} (e : α ≃ β) : (∃! a, p a) ↔ ∃! b, p (e.symm b)
• Equiv.exists_congr_left 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {p : α → Prop} (e : α ≃ β) : (∃ a, p a) ↔ ∃ b, p (e.symm b)
• Equiv.injective_comp 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ) : Function.Injective (f ∘ ⇑e) ↔ Function.Injective f
• Equiv.instTrans_trans 📋 Mathlib.Logic.Equiv.Defs
  {a✝ : Sort u_2} {b✝ : Sort u_1} {c✝ : Sort u_3} (e₁ : a✝ ≃ b✝) (e₂ : b✝ ≃ c✝) : Trans.trans e₁ e₂ = e₁.trans e₂
• Equiv.ofBijective_apply_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f) (x : β) : f ((Equiv.ofBijective f hf).symm x) = x
• Equiv.ofBijective_symm_apply_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f) (x : α) : (Equiv.ofBijective f hf).symm (f x) = x
• Equiv.sigmaCongrLeft' 📋 Mathlib.Logic.Equiv.Defs
  {α₁ : Type u_1} {α₂ : Type u_2} {β : α₁ → Type u_3} (f : α₁ ≃ α₂) : (a : α₁) × β a ≃ (a : α₂) × β (f.symm a)
• Equiv.surjective_comp 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ) : Function.Surjective (f ∘ ⇑e) ↔ Function.Surjective f
• Equiv.forall_congr 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (e a)) : (∀ (a : α), p a) ↔ ∀ (b : β), q b
• Equiv.leftInverse_symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (f : α ≃ β) : Function.LeftInverse ⇑f.symm ⇑f
• Equiv.left_inv' 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : Function.LeftInverse ⇑e.symm ⇑e
• Equiv.permCongr_refl 📋 Mathlib.Logic.Equiv.Defs
  {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') : e.permCongr (Equiv.refl α') = Equiv.refl β'
• Equiv.rightInverse_symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (f : α ≃ β) : Function.RightInverse ⇑f.symm ⇑f
• Equiv.right_inv' 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : Function.RightInverse ⇑e.symm ⇑e
• Equiv.sigmaCongr 📋 Mathlib.Logic.Equiv.Defs
  {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : α₁ → Type u_3} {β₂ : α₂ → Type u_4} (f : α₁ ≃ α₂) (F : (a : α₁) → β₁ a ≃ β₂ (f a)) : Sigma β₁ ≃ Sigma β₂
• Equiv.funUnique_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u) (β : Sort u_1) [Unique α] : ⇑(Equiv.funUnique α β).symm = uniqueElim
• Equiv.apply_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) (x : β) : e (e.symm x) = x
• Equiv.symm_apply_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) (x : α) : e.symm (e x) = x
• Equiv.forall_congr' 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (b : β), p (e.symm b) ↔ q b) : (∀ (a : α), p a) ↔ ∀ (b : β), q b
• Equiv.cast_trans 📋 Mathlib.Logic.Equiv.Defs
  {α β γ : Sort u_1} (h : α = β) (h2 : β = γ) : (Equiv.cast h).trans (Equiv.cast h2) = Equiv.cast ⋯
• Equiv.coe_fn_mk 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (f : α → β) (g : β → α) (l : Function.LeftInverse g f) (r : Function.RightInverse g f) : ⇑{ toFun := f, invFun := g, left_inv := l, right_inv := r } = f
• Equiv.congr_arg 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {f : α ≃ β} {x x' : α} : x = x' → f x = f x'
• Equiv.existsUnique_congr 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (e a)) : (∃! a, p a) ↔ ∃! b, q b
• Equiv.exists_congr 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (a : α), p a ↔ q (e a)) : (∃ a, p a) ↔ ∃ b, q b
• Equiv.ofUnique_apply 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u) (β : Sort v) [Unique α] [Unique β] (a✝ : α) : (Equiv.ofUnique α β) a✝ = default a✝
• Equiv.apply_eq_iff_eq 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (f : α ≃ β) {x y : α} : f x = f y ↔ x = y
• Equiv.symm_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (f : α ≃ β) (b : α) : f.symm.symm b = f b
• EquivLike.coe_coe 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) : ⇑↑e = ⇑e
• Equiv.conj_trans 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α ≃ β) (e₂ : β ≃ γ) : (e₁.trans e₂).conj = e₁.conj.trans e₂.conj
• Equiv.self_comp_symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : ⇑e ∘ ⇑e.symm = id
• Equiv.symm_comp_self 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) : ⇑e.symm ∘ ⇑e = id
• Equiv.trans_assoc 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α ≃ β) (bc : β ≃ γ) (cd : γ ≃ δ) : (ab.trans bc).trans cd = ab.trans (bc.trans cd)
• Equiv.coe_fn_symm_mk 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (f : α → β) (g : β → α) (l : Function.LeftInverse g f) (r : Function.RightInverse g f) : ⇑{ toFun := f, invFun := g, left_inv := l, right_inv := r }.symm = g
• Equiv.coe_inj 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {e₁ e₂ : α ≃ β} : ⇑e₁ = ⇑e₂ ↔ e₁ = e₂
• Equiv.existsUnique_congr' 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (b : β), p (e.symm b) ↔ q b) : (∃! a, p a) ↔ ∃! b, q b
• Equiv.exists_congr' 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ (b : β), p (e.symm b) ↔ q b) : (∃ a, p a) ↔ ∃ b, q b
• Equiv.ofUnique_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u) (β : Sort v) [Unique α] [Unique β] (a✝ : β) : (Equiv.ofUnique α β).symm a✝ = default a✝
• Equiv.apply_eq_iff_eq_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {x : α} {y : β} (f : α ≃ β) : f x = y ↔ x = f.symm y
• Equiv.arrowCongr'_symm 📋 Mathlib.Logic.Equiv.Defs
  {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : (e₁.arrowCongr' e₂).symm = e₁.symm.arrowCongr' e₂.symm
• Equiv.arrowCongr_symm 📋 Mathlib.Logic.Equiv.Defs
  {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : (e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm
• Equiv.congr_fun 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {f g : α ≃ β} (h : f = g) (x : α) : f x = g x
• Equiv.eq_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {x : β} {y : α} : y = e.symm x ↔ e y = x
• Equiv.ext 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {f g : α ≃ β} (H : ∀ (x : α), f x = g x) : f = g
• Equiv.symm_apply_eq 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {x : β} {y : α} : e.symm x = y ↔ x = e y
• Equiv.ext_iff 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {f g : α ≃ β} : f = g ↔ ∀ (x : α), f x = g x
• Equiv.funUnique_apply 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u) (β : Sort u_1) [Unique α] : ⇑(Equiv.funUnique α β) = fun f => f default
• Equiv.pSigmaAssoc 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : α → Sort u_2} (γ : (a : α) → β a → Sort u_3) : (ab : (a : α) ×' β a) ×' γ ab.fst ab.snd ≃ (a : α) ×' (b : β a) ×' γ a b
• Equiv.sigmaAssoc 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_1} {β : α → Type u_2} (γ : (a : α) → β a → Type u_3) : (ab : (a : α) × β a) × γ ab.fst ab.snd ≃ (a : α) × (b : β a) × γ a b
• EquivLike.apply_coe_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) (x : β) : e ((↑e).symm x) = x
• EquivLike.coe_symm_apply_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) (x : α) : (↑e).symm (e x) = x
• Equiv.mk.sizeOf_spec 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} [SizeOf α] [SizeOf β] (toFun : α → β) (invFun : β → α) (left_inv : Function.LeftInverse invFun toFun) (right_inv : Function.RightInverse invFun toFun) : sizeOf { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } = 1
• Equiv.equivCongr_symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α ≃ β) (cd : γ ≃ δ) : (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm
• Equiv.Perm.sigmaCongrRight_symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_1} {β : α → Type u_2} (F : (a : α) → Equiv.Perm (β a)) : Equiv.symm (Equiv.Perm.sigmaCongrRight F) = Equiv.Perm.sigmaCongrRight fun a => Equiv.symm (F a)
• Equiv.permCongr_def 📋 Mathlib.Logic.Equiv.Defs
  {α' : Type u_1} {β' : Type u_2} (e : α' ≃ β') (p : Equiv.Perm α') : e.permCongr p = (e.symm.trans p).trans e
• EquivLike.coe_symm_comp_self 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) : ⇑(↑e).symm ∘ ⇑e = id
• EquivLike.self_comp_coe_symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {F : Sort u_1} [EquivLike F α β] (e : F) : ⇑e ∘ ⇑(↑e).symm = id
• Quot.congrLeft 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {r : α → α → Prop} (e : α ≃ β) : Quot r ≃ Quot fun b b' => r (e.symm b) (e.symm b')
• Quot.congr 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {ra : α → α → Prop} {rb : β → β → Prop} (e : α ≃ β) (eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)) : Quot ra ≃ Quot rb
• Equiv.psigmaCongrRight_symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_3} {β₁ : α → Sort u_1} {β₂ : α → Sort u_2} (F : (a : α) → β₁ a ≃ β₂ a) : (Equiv.psigmaCongrRight F).symm = Equiv.psigmaCongrRight fun a => (F a).symm
• Equiv.sigmaCongrRight_symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Type u_3} {β₁ : α → Type u_1} {β₂ : α → Type u_2} (F : (a : α) → β₁ a ≃ β₂ a) : (Equiv.sigmaCongrRight F).symm = Equiv.sigmaCongrRight fun a => (F a).symm
• Quotient.congr 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {ra : Setoid α} {rb : Setoid β} (e : α ≃ β) (eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)) : Quotient ra ≃ Quotient rb
• Equiv.equivCongr_refl_left 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (bg : β ≃ γ) (e : α ≃ β) : ((Equiv.refl α).equivCongr bg) e = e.trans bg
• Equiv.trans_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ) (a : α) : (f.trans g) a = g (f a)
• Equiv.coe_trans 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ) : ⇑(f.trans g) = ⇑g ∘ ⇑f
• Equiv.comp_symm_eq 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : β → γ) (g : α → γ) : g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e
• Equiv.eq_comp_symm 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : β → γ) (g : α → γ) : f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g
• Equiv.eq_symm_comp 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : γ → α) (g : γ → β) : f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g
• Equiv.equivCongr_refl_right 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} (ab e : α ≃ β) : (ab.equivCongr (Equiv.refl β)) e = ab.symm.trans e
• Equiv.symm_comp_eq 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : γ → α) (g : γ → β) : ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f
• Equiv.sigmaEquivProd_apply 📋 Mathlib.Logic.Equiv.Defs
  (α : Type u_1) (β : Type u_2) (a : (_ : α) × β) : (Equiv.sigmaEquivProd α β) a = (a.fst, a.snd)
• Equiv.forall₂_congr 📋 Mathlib.Logic.Equiv.Defs
  {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} {p : α₁ → β₁ → Prop} {q : α₂ → β₂ → Prop} (eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂) (h : ∀ {x : α₁} {y : β₁}, p x y ↔ q (eα x) (eβ y)) : (∀ (x : α₁) (y : β₁), p x y) ↔ ∀ (x : α₂) (y : β₂), q x y
• Equiv.conj_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} (e : α ≃ β) (f : α → α) (a✝ : β) : e.conj f a✝ = e (f (e.symm a✝))
• Equiv.piUnique_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} [Unique α] (β : α → Sort u_1) : ⇑(Equiv.piUnique β) = fun f => f default
• Equiv.sigmaEquivProd_symm_apply 📋 Mathlib.Logic.Equiv.Defs
  (α : Type u_1) (β : Type u_2) (a : α × β) : (Equiv.sigmaEquivProd α β).symm a = ⟨a.1, a.2⟩
• Equiv.symm_trans_apply 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ) (a : γ) : (f.trans g).symm a = f.symm (g.symm a)
• Equiv.mk.injEq 📋 Mathlib.Logic.Equiv.Defs
  {α : Sort u_1} {β : Sort u_2} (toFun : α → β) (invFun : β → α) (left_inv : Function.LeftInverse invFun toFun) (right_inv : Function.RightInverse invFun toFun) (toFun✝ : α → β) (invFun✝ : β → α) (left_inv✝ : Function.LeftInverse invFun✝ toFun✝) (right_inv✝ : Function.RightInverse invFun✝ toFun✝) : ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } = { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }) = (toFun = toFun✝ ∧ invFun = invFun✝)
• Equiv.arrowCongr'_trans 📋 Mathlib.Logic.Equiv.Defs
  {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α₃ : Type u_5} {β₃ : Type u_6} (e₁ : α₁ ≃ α₂) (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃) : (e₁.trans e₂).arrowCongr' (e₁'.trans e₂') = (e₁.arrowCongr' e₁').trans (e₂.arrowCongr' e₂')
• Equiv.arrowCongr_trans 📋 Mathlib.Logic.Equiv.Defs
  {α₁ : Sort u_1} {α₂ : Sort u_2} {α₃ : Sort u_3} {β₁ : Sort u_4} {β₂ : Sort u_5} {β₃ : Sort u_6} (e₁ : α₁ ≃ α₂) (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃) : (e₁.trans e₂).arrowCongr (e₁'.trans e₂') = (e₁.arrowCongr e₁').trans (e₂.arrowCongr e₂')
• Equiv.functionSwap_apply 📋 Mathlib.Logic.Equiv.Defs
  (α : Sort u_1) (β : Sort u_2) (γ : α → β → Sort u_3) : ⇑(Equiv.functionSwap α β γ) = Function.swap

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision 40fea08