mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Rep.Iso
Rep.unit_iso_comm : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] (V : Rep.{w, u, v} k G) (g : G) (x : ↑V),
  Rep.unitIsoAddEquiv ((V.ρ g).toFun x) =
    ((Rep.ofModuleMonoidAlgebra.obj (Rep.toModuleMonoidAlgebra.obj V)).ρ g).toFun (Rep.unitIsoAddEquiv x)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ ∩ t₂).contains k = (t₁.contains k && t₂.contains k)
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.inducedFunctor_comp_obj : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮} {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor C 𝒳} (hF : F.comp p = (CategoryTheory.Functor.const C).obj S) (X : C),
  CategoryTheory.Functor.Fiber.fiberInclusion.obj ((CategoryTheory.Functor.Fiber.inducedFunctor hF).obj X) = F.obj X
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Iso.mk_inv : ∀ {α β : PartOrdEmb} (e : ↑α ≃o ↑β), (PartOrdEmb.Iso.mk e).inv = PartOrdEmb.ofHom (RelIso.toRelEmbedding e.symm)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomain_one : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Zero M] [inst_2 : Zero N] {F : Type u_9}
  [inst_3 : FunLike F M N] [ZeroHomClass F M N] (f : F), AddMonoidAlgebra.mapDomain (⇑f) 1 = 1
-- Mathlib.Algebra.Group.Units.Equiv
/-- Right addition in an `AddGroup` is a permutation of the underlying type.  -/
Equiv.addRight : {G : Type u_5} → [AddGroup G] → G → Equiv.Perm G
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.ext_iff : ∀ {X Y : PartOrdEmb} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.associator_obj_inl_inr : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (X : D),
  (CategoryTheory.sum.associator C D E).obj (Sum.inl (Sum.inr X)) = Sum.inr (Sum.inl X)
-- Mathlib.Algebra.Module.Equiv.Basic
/-- Any two modules that are subsingletons are isomorphic.  -/
LinearEquiv.ofSubsingleton : {R : Type u_1} →
  (M : Type u_5) →
    (M₂ : Type u_7) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M] → [inst_4 : Module R M₂] → [Subsingleton M] → [Subsingleton M₂] → M ≃ₗ[R] M₂
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_le_of_nonpos_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α] [AddLeftMono α] {a b : α}, b ≤ 0 → a + b ≤ a
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.typein_le_typein : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] {a b : α},
  (Ordinal.typein r).toRelEmbedding a ≤ (Ordinal.typein r).toRelEmbedding b ↔ ¬r b a
-- Mathlib.Analysis.Normed.Module.Basic
NormedSpace.discreteTopology_zmultiples : ∀ {E : Type u_6} [inst : NormedAddCommGroup E] [NormedSpace ℚ E] (e : E), DiscreteTopology ↥(AddSubgroup.zmultiples e)
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.optionEquivalence_unitIso : ∀ {J : Type w₁} (C' : Option J → Type u₁) [inst : (i : Option J) → CategoryTheory.Category.{v₁, u₁} (C' i)],
  (CategoryTheory.Pi.optionEquivalence C').unitIso =
    CategoryTheory.NatIso.pi' fun i =>
      match i with
      | none =>
        CategoryTheory.Iso.refl
          ((CategoryTheory.Functor.id ((i : Option J) → C' i)).comp (CategoryTheory.Pi.eval C' none))
      | some val =>
        CategoryTheory.Iso.refl
          ((CategoryTheory.Functor.id ((i : Option J) → C' i)).comp (CategoryTheory.Pi.eval C' (some val)))
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor_obj_right_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.toArrowArrowFunctor.obj sq).right.right = sq.X₄
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ \ t₂).getKey! k = default
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_insert_eq_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x : M}
  {s : Set M}, x ∈ Submodule.span R s → Submodule.span R (insert x s) = Submodule.span R s
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.isoMk_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (app : (X : Cᵒᵖ) → M₁.obj X ≅ M₂.obj X)
  (naturality :
    autoParam
      (∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (M₁.map f)
            ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y).hom) =
          CategoryTheory.CategoryStruct.comp (app X).hom (M₂.map f))
      PresheafOfModules.isoMk._auto_1)
  (X : Cᵒᵖ), (PresheafOfModules.isoMk app naturality).hom.app X = (app X).hom
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_cofinite_iff : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {f'' : α → E''} {g'' : α → F''},
  (∀ (x : α), g'' x = 0 → f'' x = 0) → (f'' =O[Filter.cofinite] g'' ↔ ∃ C, ∀ (x : α), ‖f'' x‖ ≤ C * ‖g'' x‖)
-- Mathlib.Tactic.CrossRefAttribute
/-- The formatter for Wikidata identifier syntax.  -/
Lean.PrettyPrinter.Formatter.wikidataIdNoAntiquot.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.dotProduct_vecMul_hadamard : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B : Matrix m n α) [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NonUnitalSemiring α] [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] (v : m → α) (w : n → α),
  Matrix.vecMul v (A.hadamard B) ⬝ᵥ w = (Matrix.diagonal v * A * (B * Matrix.diagonal w).transpose).trace
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Fill the premise in with fresh universe and expression metavariables.  -/
Mathlib.Tactic.ClickSuggestions.Premise.forallMetaTelescopeReducing : Mathlib.Tactic.ClickSuggestions.Premise → Lean.MetaM (Lean.Expr × Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- If words `w₁ w₂` are such that `w₁` reduces to `w₂`, then `w₂` reduces to the maximal reduction
of `w₁`.  -/
FreeGroup.reduce.rev : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeGroup.Red L₁ L₂ → FreeGroup.Red L₂ (FreeGroup.reduce L₁)
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite.eq_1 : ∀ {α : Type u_1} (t s s' : Set α), t.ite s s' = s ∩ t ∪ s' \ t
-- Mathlib.Data.Set.Function
/-- **Alias** of `Set.InjOn.image_sdiff_subset`. -/
Set.image_sdiff_of_injOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {t : Set α},
  Set.InjOn f s → t ⊆ s → f '' (s \ t) = f '' s \ f '' t
-- Mathlib.Data.Set.Function
Set.EqOn.injOn_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β}, Set.EqOn f₁ f₂ s → (Set.InjOn f₁ s ↔ Set.InjOn f₂ s)
-- Mathlib.Order.Defs.Unbundled
/-- `IsStrictWeakOrder X lt` means that the binary relation `lt` on `X` is a strict weak order,
that is, `IsStrictOrder X lt` and `¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a`.  -/
IsStrictWeakOrder : (α : Sort u_1) → (α → α → Prop) → Prop
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.mk : {α : Type u} →
  {cmp : autoParam (α → α → Ordering) Std.ExtTreeSet._auto_1} → Std.ExtTreeMap α Unit cmp → Std.ExtTreeSet α cmp
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- An injective continuous function on a Polish space is a measurable embedding.  -/
Continuous.measurableEmbedding : ∀ {γ : Type u_3} {β : Type u_5} [inst : MeasurableSpace β] [tβ : TopologicalSpace β] [T2Space β] {f : γ → β}
  [BorelSpace β] [inst_3 : TopologicalSpace γ] [PolishSpace γ] [inst_5 : MeasurableSpace γ] [BorelSpace γ],
  Continuous f → Function.Injective f → MeasurableEmbedding f
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_C : ∀ {R : Type u} {a : R} [inst : Semiring R] {x : R}, Polynomial.eval x (Polynomial.C a) = a
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.toContextExpr : Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.instSmallDiscrete : ∀ (C : Type u) [Small.{w, u} C], Small.{w, u} (CategoryTheory.Discrete C)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_eq_getD_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, t.getD a fallback = (t.get? a).getD fallback
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
PowerSeries.coeff_pentagonalSeries_eq_zero : ∀ (R : Type u_1) [inst : CommRing R] {n : ℕ},
  n ∉ Set.range pentagonal → (PowerSeries.coeff n) (PowerSeries.pentagonalSeries R) = 0
-- Mathlib.Data.Fintype.Vector
List.Vector.instFinite : ∀ {α : Type u_1} [Finite α] {n : ℕ}, Finite (List.Vector α n)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_eq_isSome_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.contains a = (t.get? a).isSome
-- Init.Data.List.Nat.InsertIdx
List.insertIdx_comm : ∀ {α : Type u} (a b : α) {i j : ℕ} {l : List α},
  i ≤ j → j ≤ l.length → (l.insertIdx i a).insertIdx (j + 1) b = (l.insertIdx j b).insertIdx i a
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- **Alias** of `ZetaAsymptotics.termSum`.

---

Sum of finitely many `term`s.  -/
ZetaAsymptotics.term_sum : ℝ → ℕ → ℝ
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.cyclesOpIso_hom_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology]
  {Z : Cᵒᵖ} (h : Opposite.op S₁.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap (CategoryTheory.ShortComplex.opMap φ))
      (CategoryTheory.CategoryStruct.comp S₁.cyclesOpIso.hom h) =
    CategoryTheory.CategoryStruct.comp S₂.cyclesOpIso.hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ).op h)
-- Mathlib.Data.Nat.Factorial.Basic
_private.Mathlib.Data.Nat.Factorial.Basic.0.Nat.ascFactorialBinary.match_1.eq_3 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1)
  (h_3 : (k n : ℕ) → k = n + 2 → motive n.succ.succ),
  (match n.succ.succ with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | k@h:n.succ.succ => h_3 k n h) =
    h_3 (n + 2) n ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.map_id_equiv : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp},
  (Std.DTreeMap.map (fun x v => v) t).Equiv t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.comp_fin3 : ∀ {R : Type r} {S : Type s} (f : R → S) (a b c : R), f ∘ ![a, b, c] = ![f a, f b, f c]
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.length_rightInvSeq : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B),
  (cs.rightInvSeq ω).length = ω.length
-- Mathlib.Algebra.Field.Subfield.Defs
SubfieldClass.coe_qsmul : ∀ {K : Type u} [inst : DivisionRing K] {S : Type u_1} [inst_1 : SetLike S K] [h : SubfieldClass S K] (s : S) (q : ℚ)
  (x : ↥s), ↑(q • x) = q • ↑x
-- Init.Grind.Ring.Field
Lean.Grind.Field.inv_inv : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a : α), a⁻¹⁻¹ = a
-- Mathlib.Algebra.MvPolynomial.Basic
/-- `X n` is the degree `1` monomial $X_n$.  -/
MvPolynomial.X : {R : Type u} → {σ : Type u_1} → [inst : CommSemiring R] → σ → MvPolynomial σ R
-- Mathlib.Algebra.Group.Action.TransferInstance
/-- Transfer `MulAction` across an `Equiv`  -/
Equiv.mulAction : (M : Type u_1) → {α : Type u_4} → {β : Type u_5} → [inst : Monoid M] → α ≃ β → [MulAction M β] → MulAction M α
-- Init.Data.SInt.Lemmas
Int8.toInt_ofNat_of_lt : ∀ {n : ℕ}, n < 2 ^ 7 → (Int8.ofNat n).toInt = ↑n
-- Mathlib.Data.Finsupp.Fintype
Finsupp.infinite_of_right : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] [Infinite α] [Nonempty ι], Infinite (ι →₀ α)
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
CategoryTheory.IndParallelPairPresentation.hI : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {f g : A ⟶ B}
  (self : CategoryTheory.IndParallelPairPresentation f g), CategoryTheory.IsFiltered self.I
-- Lean.Elab.Binders
Lean.Elab.Term.BinderView.mk : Lean.Syntax → Lean.Syntax → Lean.Syntax → Lean.BinderInfo → Lean.Elab.Term.BinderView
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.TransvectionStruct.toSpecialLinearGroup_coe : ∀ {ι : Type u_1} {F : Type u_2} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommRing F]
  (t : Matrix.TransvectionStruct ι F), ↑t.toSpecialLinearGroup = t.toMatrix
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- **Alias** of `contMDiffOn_finsetProd`. -/
contMDiffOn_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} {t : Finset ι}
  {f : ι → M → G}, (∀ i ∈ t, ContMDiffOn I' I n (f i) s) → ContMDiffOn I' I n (fun x => ∏ i ∈ t, f i x) s
-- Mathlib.Data.Finsupp.Weight
/-- The `weight` of the finitely supported function `f : σ →₀ R`
with respect to `w : σ → M` is the sum `∑ i, f i • w i`.  -/
Finsupp.weight : {σ : Type u_1} →
  {M : Type u_2} →
    {R : Type u_3} → [inst : Semiring R] → (σ → M) → [inst_1 : AddCommMonoid M] → [Module R M] → (σ →₀ R) →+ M
-- Mathlib.Topology.Compactness.Lindelof
instNeBotCoLindelofOfNonLindelofSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [NonLindelofSpace X], (Filter.coLindelof X).NeBot
-- Mathlib.Data.Set.Lattice
forall_sUnion : ∀ {α : Type u_1} {S : Set (Set α)} {p : α → Prop}, (∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instAddCommMonoid : {α : Type u_1} → [inst : AddCommGroup α] → [inst_1 : Preorder α] → [IsOrderedAddMonoid α] → AddCommMonoid (UpperSet α)
-- Mathlib.Control.ULift
/-- Monadic bind.  -/
PLift.bind : {α : Sort u} → {β : Sort v} → PLift α → (α → PLift β) → PLift β
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.Embedding.toPartialEquiv_toEmbedding : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f : L.PartialEquiv M N} (h : f.dom = ⊤), (FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop h).toPartialEquiv = f
-- Mathlib.Combinatorics.Additive.FreimanHom
AddEquivClass.isAddFreimanIso : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α}
  {B : Set β} {n : ℕ} [inst_2 : EquivLike F α β] [AddEquivClass F α β] (f : F),
  Set.BijOn (⇑f) A B → IsAddFreimanIso n A B ⇑f
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalCategoryStruct : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [(i : I) → CategoryTheory.MonoidalCategory (C i)] → CategoryTheory.MonoidalCategoryStruct ((i : I) → C i)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α} {k : α}
  {h : k ∈ Std.ExtDTreeMap.Const.unitOfList l cmp},
  Std.ExtDTreeMap.Const.get (Std.ExtDTreeMap.Const.unitOfList l cmp) k h = ()
-- Init.Grind.Ring.Field
Lean.Grind.Field.toDiv : {α : Type u} → [self : Lean.Grind.Field α] → Div α
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftEq_inv_app_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (l l' : L₁ ⟶ L₂) (h : l = l') (X : CategoryTheory.Comma L₂ R),
  ((CategoryTheory.Comma.mapLeftEq R l l' h).inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.closure_eq_of_subset_coloops : ∀ {α : Type u_1} {M : Matroid α} {K : Set α}, K ⊆ M.coloops → M.closure K = K ∪ M.loops
-- Mathlib.Logic.Equiv.List
Encodable.encodeList.eq_2 : ∀ {α : Type u_1} [inst : Encodable α] (a : α) (l : List α),
  Encodable.encodeList (a :: l) = (Nat.pair (Encodable.encode a) (Encodable.encodeList l)).succ
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_C : ∀ {R : Type u} [inst : Semiring R] (a : R), (Polynomial.C a).toFinsupp = AddMonoidAlgebra.single 0 a
-- Mathlib.Data.Finsupp.ToDFinsupp
sigmaFinsuppEquivDFinsupp_support : ∀ {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [inst : DecidableEq ι] [inst_1 : Zero N]
  [inst_2 : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)] (f : (i : ι) × η i →₀ N),
  (sigmaFinsuppEquivDFinsupp f).support = f.splitSupport
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.coe_subtype : ∀ {α : Sort u_1} (p : α → Prop), ⇑(Function.Embedding.subtype p) = Subtype.val
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLE.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (size : ℕ) (ky : α) (y : β ky)
  (l r : Std.DTreeMap.Internal.Impl α β) (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isLE = true),
  Std.DTreeMap.Internal.Impl.getEntryLE k (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he =
    match hkky : compare k ky with
    | Ordering.gt => Std.DTreeMap.Internal.Impl.getEntryLED k r ⟨ky, y⟩
    | Ordering.eq => ⟨ky, y⟩
    | Ordering.lt => Std.DTreeMap.Internal.Impl.getEntryLE k l ⋯ ⋯
-- Mathlib.Data.Finsupp.Single
Finsupp.zero_update : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a : α) (b : M), Finsupp.update 0 a b = fun₀ | a => b
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.ext : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering} {c c' : Std.DTreeMap.Internal.Cell α β k},
  c.inner = c'.inner → c = c'
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqParam : {pu : Lean.Compiler.LCNF.Purity} → BEq (Lean.Compiler.LCNF.Param pu)
-- Mathlib.Algebra.Group.WithOne.Map
WithOne.map₂.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3}, WithOne.map₂ = Option.map₂
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- The name length of the used lemma.  -/
Mathlib.Tactic.ClickSuggestions.GrwKey.nameLength : Mathlib.Tactic.ClickSuggestions.GrwKey → ℕ
-- Lean.Parser.Syntax
Lean.Parser.Command.postfix.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.measurable_update_cylinderEvents_left : ∀ {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] {Δ : Set ι} {a : ι} [inst : DecidableEq ι]
  {x : X a}, Measurable fun x_1 => Function.update x_1 a x
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- The trivial zeroes of the even Hurwitz zeta function.  -/
HurwitzZeta.hurwitzZetaEven_neg_two_mul_nat_add_one : ∀ (a : UnitAddCircle) (n : ℕ), HurwitzZeta.hurwitzZetaEven a (-2 * (↑n + 1)) = 0
-- Mathlib.Data.Ordmap.Ordnode
/-- O(1). Get the size of the set.

```
size {2, 1, 1, 4} = 3
```  -/
Ordnode.size : {α : Type u_1} → Ordnode α → ℕ
-- Std.Time.Zoned.Database.TZdb
/-- Builds the effective zoneinfo search path by prepending the current `TZDIR` (if set and
exists on disk) to `db.zonesPaths`. Called on every lookup so that runtime changes to
`TZDIR` are reflected immediately.
 -/
Std.Time.Database.TZdb.resolveZonesPaths : Std.Time.Database.TZdb → IO (Array System.FilePath)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.pOpcycles_π_isoOpcyclesOfIsColimit_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] {cc : CategoryTheory.Limits.CokernelCofork S.f}
  (hcc : CategoryTheory.Limits.IsColimit cc),
  CategoryTheory.CategoryStruct.comp S.pOpcycles (S.isoOpcyclesOfIsColimit hcc).inv = CategoryTheory.Limits.Cofork.π cc
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'_eq_zero : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  {P : Ideal S}, (∀ (n : ℕ), ∃ k, Ideal.map (algebraMap R S) p ≤ P ^ k ∧ n < k) → p.ramificationIdx' P = 0
-- Init.Core
/-- `Symm r` means that the binary relation `r` is symmetric, that is, `r a b → r b a`.   -/
Std.Symm : {α : Sort u} → (α → α → Prop) → Prop
-- Mathlib.Algebra.Order.Group.End
RelHom.instMonoid : {α : Type u_1} → {r : α → α → Prop} → Monoid (r →r r)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
zmodCyclicMulEquiv.congr_simp : ∀ {G : Type u_2} [inst : Group G] (h : IsCyclic G), zmodCyclicMulEquiv h = zmodCyclicMulEquiv h
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.enorm_measure_le_variation : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] (μ : MeasureTheory.VectorMeasure X V) (E : Set X), ‖μ E‖ₑ ≤ μ.variation E
-- Mathlib.CategoryTheory.Grothendieck
/-- The morphism between base objects.  -/
CategoryTheory.Grothendieck.Hom.base : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {X Y : CategoryTheory.Grothendieck F} → X.Hom Y → (X.base ⟶ Y.base)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.isWeierstrassDivisionAt_zero : ∀ {A : Type u_1} [inst : CommRing A] (g : PowerSeries A) (I : Ideal A), PowerSeries.IsWeierstrassDivisionAt 0 g 0 0 I
-- Mathlib.Analysis.Calculus.Deriv.Pow
HasDerivAt.pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  {f : 𝕜 → 𝔸} {f' : 𝔸} {x : 𝕜},
  HasDerivAt f f' x → ∀ (n : ℕ), HasDerivAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- The quotient `G ⧸ N` of a complete first countable uniform additive group
`G` by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by
subspaces are complete. In contrast to `QuotientAddGroup.completeSpace_right'`, in this version
`G` is already equipped with a uniform structure.
[N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b]

Even though `G` is equipped with a uniform structure, the quotient `G ⧸ N` does not inherit a
uniform structure, so it is still provided manually via `IsTopologicalAddGroup.rightUniformSpace`.
 -/
QuotientAddGroup.completeSpace_right : ∀ (G : Type u_1) [inst : AddGroup G] [us : UniformSpace G] [inst_1 : IsRightUniformAddGroup G]
  [FirstCountableTopology G] (N : AddSubgroup G) [inst_3 : N.Normal] [hG : CompleteSpace G], CompleteSpace (G ⧸ N)
-- Std.Do.WP.Monad
/-- `WP.wp` preserves `bind`.  -/
Std.Do.WPMonad.wp_bind : ∀ {m : Type u → Type v} {ps : outParam Std.Do.PostShape} {inst : Monad m} [self : Std.Do.WPMonad m ps] {α β : Type u}
  (x : m α) (f : α → m β),
  (Std.Do.wp do
      let a ← x
      f a) =
    do
    let a ← Std.Do.wp x
    Std.Do.wp (f a)
-- Mathlib.Order.BoundedOrder.Monotone
monotone_le : ∀ {α : Type u} [inst : Preorder α] {x : α}, Monotone fun x_1 => x ≤ x_1