mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Instances.Real
range_modelWithCornersEuclideanHalfSpace : ∀ (n : ℕ) [inst : NeZero n], Set.range ↑(modelWithCornersEuclideanHalfSpace n) = {y | 0 ≤ y.ofLp 0}
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.eraseList.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)), Std.Internal.List.eraseList l [] = l
-- Mathlib.Algebra.Quandle
Rack.toEnvelGroup.mapAux.eq_def : ∀ {R : Type u_1} [inst : Rack R] {G : Type u_2} [inst_1 : Group G] (f : ShelfHom R (Quandle.Conj G))
  (x : Rack.PreEnvelGroup R),
  Rack.toEnvelGroup.mapAux f x =
    match x with
    | Rack.PreEnvelGroup.unit => 1
    | Rack.PreEnvelGroup.incl x => f x
    | a.mul b => Rack.toEnvelGroup.mapAux f a * Rack.toEnvelGroup.mapAux f b
    | a.inv => (Rack.toEnvelGroup.mapAux f a)⁻¹
-- Mathlib.RingTheory.RingHom.PurelyInseparable
/-- The identity of a ring is purely inseparable.  -/
RingHom.IsPurelyInseparable.id : ∀ (F : Type u_1) [inst : CommRing F], (RingHom.id F).IsPurelyInseparable
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∪ t₂).get? k = t₁.get? k
-- Mathlib.Algebra.Azumaya.Defs
IsAzumaya.mk : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [toProjective : Module.Projective R A] [toFaithfulSMul : FaithfulSMul R A] [toFinite : Module.Finite R A],
  Function.Bijective ⇑(AlgHom.mulLeftRight R A) → IsAzumaya R A
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_le_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t → ∀ {fallback : α}, (cmp (t.minKeyD fallback) k).isLE = true
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toOuterMeasure_apply : ∀ {α : Type u_1} (p : PMF α) (s : Set α), p.toOuterMeasure s = ∑' (x : α), s.indicator (⇑p) x
-- Mathlib.Order.Max
OrderDual.noTopOrder : ∀ {α : Type u_1} [inst : LE α] [NoBotOrder α], NoTopOrder αᵒᵈ
-- Mathlib.RingTheory.Coalgebra.GroupLike
/-- Identity equivalence between `GroupLike R A` and `{a : A // IsGroupLikeElem R a}`.  -/
GroupLike.valEquiv : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : Module R A] → [inst_3 : Coalgebra R A] → GroupLike R A ≃ Subtype (IsGroupLikeElem R)
-- Mathlib.RingTheory.Kaehler.Basic
/-- The kernel of the multiplication map `S ⊗[R] S →ₐ[R] S`.  -/
KaehlerDifferential.ideal : (R : Type u) →
  (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Ideal (TensorProduct R S S)
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.mem_nhds_top_iff : ∀ {s : Set EReal}, s ∈ nhds ⊤ ↔ ∃ y, Set.Ioi ↑y ⊆ s
-- Mathlib.GroupTheory.Congruence.Opposite
/-- If `c` is an additive congruence on `Mᵃᵒᵖ`, then `(a, b) ↦ c bᵒᵖ aᵒᵖ` is an
additive congruence on `M`.  -/
AddCon.unop : {M : Type u_1} → [inst : Add M] → AddCon Mᵃᵒᵖ → AddCon M
-- Lean.Elab.PreDefinition.Basic
/-- Applies `Lean.instantiateMVars` to the types of values of each predefinition.
 -/
Lean.Elab.instantiateMVarsAtPreDecls : Array Lean.Elab.PreDefinition → Lean.Elab.TermElabM (Array Lean.Elab.PreDefinition)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min!_eq_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → ∀ {km : α}, t.min! = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.mkUnits_eq : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {u : ℚ_[p]} (h : ‖u‖ = 1), ↑↑(PadicInt.mkUnits h) = u
-- Mathlib.Algebra.LinearRecurrence
/-- The space of solutions of `E`, as a `Submodule` over `R` of the module `ℕ → R`.  -/
LinearRecurrence.solSpace : {R : Type u_1} → [inst : CommSemiring R] → LinearRecurrence R → Submodule R (ℕ → R)
-- Init.Core
DoResultSBC.break.inj : ∀ {α σ : Type u} {a a_1 : σ}, DoResultSBC.break a = DoResultSBC.break a_1 → a = a_1
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.zero_ne_mem_conductorSet : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) [NeZero n], 0 ∉ χ.conductorSet
-- Mathlib.Algebra.Group.Pi.Basic
Pi.cancelCommMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → CancelCommMonoid (f i)],
  Pi.cancelCommMonoid = { toMonoid := Pi.leftCancelMonoid.toMonoid, mul_comm := ⋯, toIsLeftCancelMul := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
/-- An orthogonal family of subspaces of `E` satisfies `DirectSum.IsInternal` (that is,
they provide an internal direct sum decomposition of `E`) if and only if their span has trivial
orthogonal complement.  -/
OrthogonalFamily.isInternal_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : DecidableEq ι] [FiniteDimensional 𝕜 E] {V : ι → Submodule 𝕜 E},
  (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → (DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥)
-- Lean.Message
Lean.MessageData.instCoeName : Coe Lean.Name Lean.MessageData
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The fifth cosimplicial identity  -/
CategoryTheory.CosimplicialObject.σ_comp_σ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i j : Fin (n + 1)},
  i ≤ j →
    ∀ {Z : C} (h : X.obj { len := n } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.σ i.castSucc) (CategoryTheory.CategoryStruct.comp (X.σ j) h) =
        CategoryTheory.CategoryStruct.comp (X.σ j.succ) (CategoryTheory.CategoryStruct.comp (X.σ i) h)
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extendMap_id_f : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' : ι'),
  (HomologicalComplex.extendMap (CategoryTheory.CategoryStruct.id K) e).f i' =
    CategoryTheory.CategoryStruct.id ((K.extend e).X i')
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.neg.sizeOf_spec : ∀ (a : Lean.Grind.Linarith.Expr), sizeOf a.neg = 1 + sizeOf a
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.imp_keq_certC.eq_1 : ∀ (lhs rhs : Lean.Grind.CommRing.Expr) (k : ℤ) (p₁ p₂ : Lean.Grind.CommRing.Poly) (c : ℕ),
  Lean.Grind.CommRing.Stepwise.imp_keq_certC lhs rhs k p₁ p₂ c =
    (!k.beq' 0).and' ((((lhs.sub rhs).toPolyC c).beq' p₁).and' (p₂.beq' (Lean.Grind.CommRing.Poly.num 0)))
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SSameSide.trans_wSameSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, s.SSameSide x y → s.WSameSide y z → s.WSameSide x z
-- Mathlib.Analysis.Convex.Function
concaveOn_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : Module 𝕜 β] {s : Set E} (c : β),
  Convex 𝕜 s → ConcaveOn 𝕜 s fun x => c
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.instIsStableUnderBaseChangeScheme : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsPreimmersion
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.ext : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {e e' : SSet.Edge x₀ x₁}, e.edge = e'.edge → e = e'
-- Mathlib.RingTheory.Extension.Basic
/-- The trivial extension of `S`.  -/
Algebra.Extension.self : (R : Type u) →
  (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Extension R S
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.instOrderClosedTopology : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A], OrderClosedTopology A
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] [Inhabited γ] {f : α → β → γ} {k k' : α} {fallback : γ},
  m.getKey? k = some k' → (Std.HashMap.map f m).getD k fallback = (Option.map (f k') m[k]?).getD fallback
-- Aesop.Util.UnionFind
Aesop.UnionFind.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α] (parents sizes : Array USize)
  (toRep : Std.HashMap α USize),
  sizeOf { parents := parents, sizes := sizes, toRep := toRep } = 1 + sizeOf parents + sizeOf sizes + sizeOf toRep
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] (ι : Type w)
  [inst_2 : CategoryTheory.Limits.HasFiniteProducts C] [inst_3 : Finite ι] (X : C) (j : ι) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun x => X) j) h
-- Std.Data.Internal.List.Associative
Std.Internal.List.alterKey_cons_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} {k' : α}
  {v' : β k'} {l : List ((a : α) × β a)},
  (Std.Internal.List.alterKey k f (⟨k', v'⟩ :: l)).Perm
    (if hk : (k' == k) = true then
      match f (some (cast ⋯ v')) with
      | none => l
      | some v => ⟨k, v⟩ :: l
    else ⟨k', v'⟩ :: Std.Internal.List.alterKey k f l)
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.Rels.smul.sizeOf_spec : ∀ {R : Type u} {ι : Type u_4} {M : Type u_5} [inst : SizeOf R] [inst_1 : SizeOf ι] [inst_2 : SizeOf M] (m : ι → M)
  (i : ι) (r : R) (x : M), sizeOf (exteriorPower.presentation.Rels.smul m i r x) = 1 + sizeOf i + sizeOf r + sizeOf x
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.pred_add_one : ∀ (o : Ordinal.{u_4}), (o + 1).pred = o
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.isoImage_inv_homOfLE_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U V : X.Opens) (e : U ≤ V)
  {Z : AlgebraicGeometry.Scheme} (h : ↑V ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoImage f U).inv
      (CategoryTheory.CategoryStruct.comp (X.homOfLE e) h) =
    CategoryTheory.CategoryStruct.comp (Y.homOfLE ⋯)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoImage f V).inv h)
-- Mathlib.Data.SetLike.Basic
/-- membership is inherited from `S`  -/
SetLike.instSubtype : {X : Type u_3} → {S : Type u_4} → [SetLike S X] → {p : S → Prop} → SetLike { s // p s } X
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflectionPerm_coroot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (self : RootPairing ι R M N) (i j : ι),
  self.coroot j - (self.toLinearMap (self.root i)) (self.coroot j) • self.coroot i =
    self.coroot ((self.reflectionPerm i) j)
-- Mathlib.FieldTheory.LinearDisjoint
/-- Linear disjointness is symmetric.  -/
IntermediateField.LinearDisjoint.symm' : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type w} [inst_3 : Field L]
  [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E] {L' : Type u_1} [inst_7 : Field L']
  [inst_8 : Algebra F L'] [inst_9 : Algebra L' E] [inst_10 : IsScalarTower F L' E],
  (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint L' →
    (IsScalarTower.toAlgHom F L' E).fieldRange.LinearDisjoint L
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.mk : {R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          {L : Type u_3} →
            [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → {x : L →ₗ⁅R⁆ LieDerivation R K K} → K → L → K ⋊⁅x⁆ L
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.coe_addMonoidHom_comp_coe_addMonoidHom_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (e : M ≃+ N),
  (↑e).comp ↑e.symm = AddMonoidHom.id N
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
MeasureTheory.projectiveFamilyFun.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)}
  (P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)) (s : Set ((i : ι) → α i)),
  MeasureTheory.projectiveFamilyFun P s =
    if hs : s ∈ MeasureTheory.measurableCylinders α then
      (P (MeasureTheory.measurableCylinders.finset hs)) (MeasureTheory.measurableCylinders.set hs)
    else 0
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.instPreservesMonomorphismsKaroubiToKaroubi : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C],
  (CategoryTheory.Idempotents.toKaroubi C).PreservesMonomorphisms
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.exists_desc_πQ : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : CategoryTheory.Category.{v_2, u_2} A]
  {ι : CategoryTheory.Functor A C},
  (∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (CategoryTheory.shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0) →
    ∀ {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃}
      {f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)},
      CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈
          CategoryTheory.Pretriangulated.distinguishedTriangles →
        ∀ {K Q : A} {α : (CategoryTheory.shiftFunctor C 1).obj (ι.obj K) ⟶ X₃} {β : X₃ ⟶ ι.obj Q}
          {γ : ι.obj Q ⟶ (CategoryTheory.shiftFunctor C 1).obj ((CategoryTheory.shiftFunctor C 1).obj (ι.obj K))},
          CategoryTheory.Pretriangulated.Triangle.mk α β γ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
            ∀ [inst_7 : ι.Full] [inst_8 : CategoryTheory.Preadditive A] [ι.Faithful] {B : A} (x₂ : X₂ ⟶ B),
              CategoryTheory.CategoryStruct.comp f₁ x₂ = 0 →
                ∃ k, CategoryTheory.CategoryStruct.comp (CategoryTheory.Triangulated.AbelianSubcategory.πQ f₂ β) k = x₂
-- Init.Data.List.Basic
/-- Erases duplicated elements in the list, keeping the first occurrence of duplicated elements.

`O(|l|^2)`.

Examples:
* `[1, 3, 2, 2, 3, 5].eraseDups = [1, 3, 2, 5]`
* `["red", "green", "green", "blue"].eraseDups = ["red", "green", "blue"]`
 -/
List.eraseDups : {α : Type u_1} → [BEq α] → List α → List α
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.ranCompIsoOfPreserves_hom_app : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (L : CategoryTheory.Functor A C)
  [inst_4 : G.PreservesRightKanExtensions L] [inst_5 : ∀ (F : CategoryTheory.Functor A B), L.HasRightKanExtension F]
  [inst_6 : ∀ (F : CategoryTheory.Functor A D), L.HasRightKanExtension F] (X : CategoryTheory.Functor A B),
  (G.ranCompIsoOfPreserves L).hom.app X = (G.rightKanExtensionCompIsoOfPreserves X L).hom
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.addMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : Zero M₁] [inst_2 : SMul ℕ M₁] [inst_3 : AddMonoid M₂]
  (f : M₁ → M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y)
  (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x),
  Function.Injective.addMonoid f hf one mul npow =
    { toAddSemigroup := Function.Injective.addSemigroup f hf mul,
      toZero := (Function.Injective.addZeroClass f hf one mul).toZero, zero_add := ⋯, add_zero := ⋯,
      nsmul := fun n x => n • x, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_smul_nnreal_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (f : X → E) (c : NNReal),
  ∫ᵛ (x : X), f x ∂[B; c • μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- A family of maps from `left a` to `right (J.snd a)`  -/
CategoryTheory.Limits.MultispanIndex.snd : {J : CategoryTheory.Limits.MultispanShape} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (self : CategoryTheory.Limits.MultispanIndex J C) → (a : J.L) → self.left a ⟶ self.right (J.snd a)
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
Rep.d_comp_tateNorm : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G] (M : Rep.{u, u, u} R G),
  CategoryTheory.CategoryStruct.comp ((groupHomology.inhomogeneousChains M).d 1 0) M.tateNorm = 0
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.r.eq_1 : ∀ (α : Type u) [inst : Lean.Grind.Semiring α] (a b c d : α),
  Lean.Grind.Ring.OfSemiring.r α (a, b) (c, d) = ∃ k, a + d + k = b + c + k
-- Mathlib.RingTheory.Ideal.Nonunits
one_notMem_nonunits : ∀ {α : Type u_2} [inst : Monoid α], 1 ∉ nonunits α
-- Mathlib.ModelTheory.Syntax
/-- Casts `L.BoundedFormula α m` as `L.BoundedFormula α n`, where `m ≤ n`.  -/
FirstOrder.Language.BoundedFormula.castLE : {L : FirstOrder.Language} → {α : Type u'} → {m n : ℕ} → m ≤ n → L.BoundedFormula α m → L.BoundedFormula α n
-- Mathlib.Order.Irreducible
InfIrred.finset_inf_eq : ∀ {ι : Type u_1} {α : Type u_2} [inst : SemilatticeInf α] {a : α} [inst_1 : OrderTop α] {s : Finset ι} {f : ι → α},
  InfIrred a → s.inf f = a → ∃ i ∈ s, f i = a
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_pow : ∀ (a : UInt64) (n : ℕ), (a ^ n).toBitVec = a.toBitVec ^ n
-- Init.SimpLemmas
have_unused' : ∀ {α : Sort u} {β : Sort v} (a : α) {b b' : β}, b = b' → (fun x => b) a = b'
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- The *cusps* of a subgroup of `GL(2, ℝ)` are the fixed points of parabolic elements of `g`.  -/
IsCusp : OnePoint ℝ → Subgroup (GL (Fin 2) ℝ) → Prop
-- Mathlib.CategoryTheory.Preadditive.EilenbergMoore
CategoryTheory.Monad.algebraPreadditive_homGroup_neg_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (T : CategoryTheory.Monad C) [inst_2 : T.Additive] (F G : T.Algebra) (α : F ⟶ G), (-α).f = -α.f
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instLeast? : Std.PRange.Least? Int64
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.coindResAdjunction_unit_app : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex] (A : Rep.{max w u v, u, v} k ↥S),
  (Rep.coindResAdjunction k S).unit.app A =
    CategoryTheory.CategoryStruct.comp ((Rep.indResAdjunction k S.subtype).unit.app A)
      ((Rep.resFunctor S.subtype).map A.indCoindIso.hom)
-- Mathlib.Algebra.GroupWithZero.Basic
zero_eq_inv : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a : G₀}, 0 = a⁻¹ ↔ 0 = a
-- Mathlib.Data.Rel.Cover
SetRel.IsCover.nonempty : ∀ {X : Type u_1} {U : SetRel X X} {s N : Set X}, U.IsCover s N → s.Nonempty → N.Nonempty
-- Mathlib.CategoryTheory.Presentable.Adjunction
CategoryTheory.Adjunction.isCardinalPresentable_leftAdjoint_obj : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (κ : Cardinal.{w})
  [inst_2 : Fact κ.IsRegular] (X : C) [CategoryTheory.IsCardinalPresentable X κ] [G.IsCardinalAccessible κ],
  CategoryTheory.IsCardinalPresentable (F.obj X) κ
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
totallyBounded_neg : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {s : Set α},
  TotallyBounded (-s) ↔ TotallyBounded s
-- Mathlib.CategoryTheory.Sites.LocallyInjective
/-- If `φ : F₁ ⟶ F₂` is a morphism of sheaves, this is an abbreviation for
`Presheaf.IsLocallyInjective J φ.val`. Under suitable assumptions, it
is equivalent to the injectivity of all maps `φ.val.app X`,
see `isLocallyInjective_iff_injective`.  -/
CategoryTheory.Sheaf.IsLocallyInjective : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {FD : D → D → Type u_1} →
          {CD : D → Type w} →
            [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
              [CategoryTheory.ConcreteCategory D FD] →
                {J : CategoryTheory.GrothendieckTopology C} → {F₁ F₂ : CategoryTheory.Sheaf J D} → (F₁ ⟶ F₂) → Prop
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
AlgebraNorm.toSeminorm : {R : Type u_1} →
  [inst : SeminormedCommRing R] →
    {S : Type u_2} → [inst_1 : Ring S] → [inst_2 : Algebra R S] → AlgebraNorm R S → Seminorm R S
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- Composing with an isomorphism on the codomain does not change the kernel.  -/
MonoidHom.ker_mulEquiv_comp : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {P : Type u_8} [inst_2 : MulOneClass P] (f : G →* N)
  (iso : N ≃* P), ((↑iso).comp f).ker = f.ker
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.inl_opProdIsoCoprod_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.opProdIsoCoprod A B).inv =
    CategoryTheory.Limits.prod.fst.op
-- Std.Do.SPred.SPred
Std.Do.SPred.imp_nil : ∀ {P Q : Std.Do.SPred []}, spred(P → Q) = { down := P.down → Q.down }
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.coprodAssoc_apply_inl_inl : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : AddMonoid P]
  (x : M), (AddEquiv.coprodAssoc M N P) (AddMonoid.Coprod.inl (AddMonoid.Coprod.inl x)) = AddMonoid.Coprod.inl x
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Mathlib.Tactic.Bicategory.naturality_whiskerRight : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {p : a ⟶ b} {f g : b ⟶ c} {h : c ⟶ d} {pf : a ⟶ c}
  {pfh : a ⟶ d} {η : f ≅ g} (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf)
  (η_g : CategoryTheory.CategoryStruct.comp p g ≅ pf) (η_fh : CategoryTheory.CategoryStruct.comp pf h ≅ pfh),
  CategoryTheory.Bicategory.whiskerLeftIso p η ≪≫ η_g = η_f →
    CategoryTheory.Bicategory.whiskerLeftIso p (CategoryTheory.Bicategory.whiskerRightIso η h) ≪≫
        Mathlib.Tactic.Bicategory.normalizeIsoComp η_g η_fh =
      Mathlib.Tactic.Bicategory.normalizeIsoComp η_f η_fh
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Hom.ext : ∀ {X Y : PartOrdEmb} {x y : X.Hom Y}, x.hom' = y.hom' → x = y
-- Mathlib.RingTheory.Adjoin.FG
Subalgebra.FG.sup : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {S S' : Subalgebra R A}, S.FG → S'.FG → (S ⊔ S').FG