mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.HomClass.toHom_toFun : ∀ {L : FirstOrder.Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : FunLike F M N] [inst_3 : L.HomClass F M N] (a : F) (a_1 : M),
  (FirstOrder.Language.HomClass.toHom a) a_1 = a a_1
-- Mathlib.Topology.Order.NhdsSet
Iic_mem_nhdsSet_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c : α},
  b < c → Set.Iic c ∈ nhdsSet (Set.Ioc a b)
-- Init.Data.Vector.Lemmas
Vector.contains_append : ∀ {α : Type u_1} {n m : ℕ} [inst : BEq α] {xs : Vector α n} {ys : Vector α m} {x : α},
  (xs ++ ys).contains x = (xs.contains x || ys.contains x)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_filter_iff : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Bool},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filter f m)).isEmpty = true ↔
      ∀ (k : α) (h : m.contains k = true), f k (m.get k h) = false)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_add_pi : ∀ (θ : Real.Angle), (θ + ↑Real.pi).cos = -θ.cos
-- Mathlib.ModelTheory.Algebra.Field.Basic
_private.Mathlib.ModelTheory.Algebra.Field.Basic.0.FirstOrder.Field.FieldAxiom.toSentence.match_1.eq_2 : ∀ (motive : FirstOrder.Field.FieldAxiom → Sort u_1) (h_1 : Unit → motive FirstOrder.Field.FieldAxiom.addAssoc)
  (h_2 : Unit → motive FirstOrder.Field.FieldAxiom.zeroAdd)
  (h_3 : Unit → motive FirstOrder.Field.FieldAxiom.negAddCancel)
  (h_4 : Unit → motive FirstOrder.Field.FieldAxiom.mulAssoc) (h_5 : Unit → motive FirstOrder.Field.FieldAxiom.mulComm)
  (h_6 : Unit → motive FirstOrder.Field.FieldAxiom.oneMul) (h_7 : Unit → motive FirstOrder.Field.FieldAxiom.existsInv)
  (h_8 : Unit → motive FirstOrder.Field.FieldAxiom.leftDistrib)
  (h_9 : Unit → motive FirstOrder.Field.FieldAxiom.existsPairNE),
  (match FirstOrder.Field.FieldAxiom.zeroAdd with
    | FirstOrder.Field.FieldAxiom.addAssoc => h_1 ()
    | FirstOrder.Field.FieldAxiom.zeroAdd => h_2 ()
    | FirstOrder.Field.FieldAxiom.negAddCancel => h_3 ()
    | FirstOrder.Field.FieldAxiom.mulAssoc => h_4 ()
    | FirstOrder.Field.FieldAxiom.mulComm => h_5 ()
    | FirstOrder.Field.FieldAxiom.oneMul => h_6 ()
    | FirstOrder.Field.FieldAxiom.existsInv => h_7 ()
    | FirstOrder.Field.FieldAxiom.leftDistrib => h_8 ()
    | FirstOrder.Field.FieldAxiom.existsPairNE => h_9 ()) =
    h_2 ()
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- The domain of an isomorphism.  -/
Mathlib.Tactic.Monoidal.srcExprOfIso : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.Congruence.Hom
/-- The diagram described by the universal property for quotients of rings, when
the ring congruence relation is the kernel of the homomorphism, commutes.  -/
RingCon.kerLiftₐ_mk : ∀ {M : Type u_1} {P : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring P] [inst_4 : Algebra R P] {f : M →ₐ[R] P} (x : M), (RingCon.kerLiftₐ f) ↑x = f x
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Measurable.clog : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ}, Measurable f → Measurable fun x => Complex.log (f x)
-- Std.Http.Data.Headers
/-- Like `get?`, but returns a default value if absent.
 -/
Std.Http.Headers.getD : Std.Http.Headers → Std.Http.Header.Name → Std.Http.Header.Value → Std.Http.Header.Value
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.snd_apply : ∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (self : A × B),
  (StarAlgHom.snd R A B) self = self.2
-- Mathlib.GroupTheory.Torsion
/-- The `p`-primary component is the submonoid of elements `g` such that `g ^ p ^ k = 1`
for some `k`. For prime `p`, these are exactly the elements of `p`-power order.  -/
CommMonoid.primaryComponent : (G : Type u_1) → [inst : CommMonoid G] → ℕ → Submonoid G
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexivePair_hasColimit_of_hasCoequalizer : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C)
  [h :
    CategoryTheory.Limits.HasCoequalizer (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
      (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)],
  CategoryTheory.Limits.HasColimit F
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.rightInvSeq.eq_def : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B),
  cs.rightInvSeq ω =
    match ω with
    | [] => []
    | i :: ω => (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω
-- Mathlib.CategoryTheory.Abelian.LeftDerived
/-- The higher derived functors vanish on projective objects.  -/
CategoryTheory.Functor.isZero_leftDerived_obj_projective_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ) (X : C)
  [CategoryTheory.Projective X], CategoryTheory.Limits.IsZero ((F.leftDerived (n + 1)).obj X)
-- Mathlib.RingTheory.Polynomial.GaussLemma
/-- Integrally closed domains are precisely the domains for in which Gauss's lemma holds
for monic polynomials  -/
Polynomial.isIntegrallyClosed_iff' : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [IsDomain R],
  IsIntegrallyClosed R ↔
    ∀ (p : Polynomial R), p.Monic → (Irreducible p ↔ Irreducible (Polynomial.map (algebraMap R K) p))
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.isSubgraph_eq_le : ∀ {V : Type u_2}, Digraph.IsSubgraph = fun x1 x2 => x1 ≤ x2
-- Mathlib.Algebra.Group.Basic
inv_div_inv : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α), a⁻¹ / b⁻¹ = b / a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_apply_zero : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {f : R → R}, cfcₙ f 0 = 0
-- Mathlib.GroupTheory.Congruence.Basic
/-- The first isomorphism theorem for monoids in the case of a homomorphism with right inverse.  -/
Con.quotientKerEquivOfRightInverse : {M : Type u_1} →
  {P : Type u_3} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass P] → (f : M →* P) → (g : P → M) → Function.RightInverse g ⇑f → (Con.ker f).Quotient ≃* P
-- Mathlib.Order.Partition.Finpartition
/-- Cuts `s` along the finsets in `F`: Two elements of `s` will be in the same part if they are
in the same finsets of `F`.  -/
Finpartition.atomise : {α : Type u_1} → [inst : DecidableEq α] → (s : Finset α) → Finset (Finset α) → Finpartition s
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.mem_ker : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : MulOneClass M] {f : G →* M} {x : G}, x ∈ f.ker ↔ f x = 1
-- Mathlib.Topology.Algebra.SeparationQuotient.Section
SeparationQuotient.outCLM_injective : ∀ (K : Type u_1) (E : Type u_2) [inst : DivisionRing K] [inst_1 : AddCommGroup E] [inst_2 : Module K E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : ContinuousConstSMul K E],
  Function.Injective ⇑(SeparationQuotient.outCLM K E)
-- Std.Data.ExtTreeSet.Basic
/-- Folds the given function over the elements of the tree set in descending order.  -/
Std.ExtTreeSet.foldr : {α : Type u} → {cmp : α → α → Ordering} → {δ : Type w} → [Std.TransCmp cmp] → (α → δ → δ) → δ → Std.ExtTreeSet α cmp → δ
-- Mathlib.RepresentationTheory.FDRep
FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ : ∀ {R : Type u} {G : Type v} [inst : CommRing R] [inst_1 : Monoid G],
  CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.forget₂ (FDRep R G) (Rep.{u, u, v} R G))
-- Lean.Parser.Term
Lean.Parser.Term.matchExpr.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_union : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, (m₁.union m₂).getKey! k = m₂.getKeyD k (m₁.getKey! k)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- Promote an isomorphism in `SemiNormedGrp` to an isomorphism in `SemiNormedGrp₁`.  -/
SemiNormedGrp₁.mkIso : {M N : SemiNormedGrp} →
  (f : M ≅ N) →
    (SemiNormedGrp.Hom.hom f.hom).NormNoninc →
      (SemiNormedGrp.Hom.hom f.inv).NormNoninc →
        ({ carrier := M.carrier, str := M.str } ≅ { carrier := N.carrier, str := N.str })
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.changeDiag_diag : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P : CategoryTheory.Limits.LimitPresentation J X) {F : CategoryTheory.Functor J C} (e : F ≅ P.diag),
  (P.changeDiag e).diag = F
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_ne_top : ∀ {c : Cardinal.{u}}, Cardinal.toENat c ≠ ⊤ ↔ c < Cardinal.aleph0
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_add : ∀ {p q : ℝ}, 0 ≤ p → 0 ≤ q → ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.addRecAux_eq_cpopTree : ∀ {len w : ℕ} {x : BitVec (len * w)}, BitVec.addRecAux✝ x len 0#w = BitVec.cast ⋯ x.cpopTree
-- Mathlib.Combinatorics.Enumerative.Schroder
Nat.largeSchroder_succ : ∀ (n : ℕ), (n + 1).largeSchroder = n.largeSchroder + ∑ i ≤ n, i.largeSchroder * (n - i).largeSchroder
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_zero : ∀ {F : Type u} [inst : Field F], Polynomial.natSepDegree 0 = 0
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.instInhabitedState : Inhabited Lean.Compiler.CSimp.State
-- Mathlib.RingTheory.Coprime.Lemmas
Int.isCoprime_iff_gcd_eq_one : ∀ {m n : ℤ}, IsCoprime m n ↔ m.gcd n = 1
-- Batteries.Control.LawfulMonadState
/-- `StateT` has lawful state operations if the underlying monad is lawful.
This is applied for `StateM` as well due to the reducibility of that definition.  -/
LawfulMonadStateOf.instStateTOfLawfulMonad : ∀ {m : Type u_1 → Type u_2} {σ : Type u_1} [inst : Monad m] [LawfulMonad m], LawfulMonadStateOf σ (StateT σ m)
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.mk : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)},
  (∀ t₁ ∈ s, ∀ t₂ ∈ s, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ s, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂) →
    ⋃₀ s = Set.univ → t = TopologicalSpace.generateFrom s → TopologicalSpace.IsTopologicalBasis s
-- Lean.Meta.Tactic.Split
_private.Lean.Meta.Tactic.Split.0.Lean.Meta.Split.simpMatchCore.pre : Lean.Name → Lean.Name → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Lean.Exception
/-- Macro for throwing error exceptions. The argument can be an interpolated string.
It is a convenient way of building `MessageData` objects.
The first argument must be a `Syntax` that provides position information for
the error message.
`throwErrorAt ref msg` is equivalent to `withRef ref <| throwError msg`
 -/
Lean.termThrowErrorAt____ : Lean.ParserDescr
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sum_inv_height_sq_smul_vsub_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n),
  ∑ i, (s.height i)⁻¹ ^ 2 • (s.points i -ᵥ s.altitudeFoot i) = 0
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
/-- A first quadrant `E₂`-cohomological spectral sequence has differentials
given by the vector `(r, 1 - r)` on the `r`th page for `2 ≤ r`.  -/
CategoryTheory.E₂CohomologicalSpectralSequenceNat : (C : Type u_1) → [inst : CategoryTheory.Category.{u_3, u_1} C] → [CategoryTheory.Abelian C] → Type (max u_1 u_3)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.zeroLocus_inf : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (I J : Ideal ↑(X.presheaf.obj (Opposite.op U))),
  X.zeroLocus ↑(I ⊓ J) = X.zeroLocus ↑I ∪ X.zeroLocus ↑J
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
/-- Every self-adjoint `LinearPMap` is closed.  -/
IsSelfAdjoint.isClosed : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {A : E →ₗ.[𝕜] E}, IsSelfAdjoint A → A.IsClosed
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue_alterKey_self : ∀ {α : Type u} [inst : BEq α] {β : Type v} [inst_1 : EquivBEq α] (k : α) (f : Option β → Option β)
  (l : List ((_ : α) × β)) (hl : Std.Internal.List.DistinctKeys l)
  (hc : Std.Internal.List.containsKey k (Std.Internal.List.Const.alterKey k f l) = true),
  Std.Internal.List.getValue k (Std.Internal.List.Const.alterKey k f l) hc = (f (Std.Internal.List.getValue? k l)).get ⋯
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (hab : b ≤ a)
  (X : C),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLTLTIsoLT a b hab).inv.app X)
      ((t.eTruncLT.obj b).map ((t.eTruncLTι a).app X)) =
    CategoryTheory.CategoryStruct.id ((t.eTruncLT.obj b).obj X)
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.single_inf : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → SemilatticeInf (f i)]
  [inst_2 : (i : I) → Zero (f i)] (i : I) (x y : f i), Pi.single i (x ⊓ y) = Pi.single i x ⊓ Pi.single i y
-- Mathlib.GroupTheory.Congruence.Basic
/-- The **third isomorphism theorem for monoids**.  -/
Con.quotientQuotientEquivQuotient : {M : Type u_1} → [inst : MulOneClass M] → (c d : Con M) → (h : c ≤ d) → (Con.ker (c.map d h)).Quotient ≃* d.Quotient
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.instDivInvMonoid : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommGroup Γ] →
      [inst_1 : LinearOrder Γ] → [IsOrderedAddMonoid Γ] → [inst : Field R] → DivInvMonoid (HahnSeries Γ R)
-- Mathlib.Algebra.Group.Defs
/-- An abbreviation for `npowRec` with an additional typeclass assumption on associativity
so that we can use `@[csimp]` to replace it with an implementation by repeated squaring
in compiled code.
 -/
npowRecAuto : {M : Type u_2} → [Semigroup M] → [One M] → ℕ → M → M
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Product of seminormed groups, using the sup norm.  -/
Prod.seminormedGroup : {E : Type u_2} → {F : Type u_3} → [SeminormedGroup E] → [SeminormedGroup F] → SeminormedGroup (E × F)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infiniteNeg_add_infiniteNeg : ∀ {x y : ℝ*}, x.InfiniteNeg → y.InfiniteNeg → (x + y).InfiniteNeg
-- Aesop.Tree.Data
Aesop.RappRef : Type
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → γ a} {k : α} [inst_1 : Inhabited (γ k)],
  t.WF → (Std.DTreeMap.Raw.map f t).get! k = (Option.map (f k) (t.get? k)).get!
-- Mathlib.RingTheory.WittVector.Complete
WittVector.frobeniusEquiv.congr_simp : ∀ (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [inst : CommRing R] [inst_1 : CharP R p] [inst_2 : PerfectRing R p],
  WittVector.frobeniusEquiv p R = WittVector.frobeniusEquiv p R
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.functor_map_hom_app : ∀ (P : TopCat → Prop) [inst : CompHausLike.HasExplicitFiniteCoproducts P] [inst_1 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  {X Y : Type (max u w)} (f : X ⟶ Y) (x : (CompHausLike P)ᵒᵖ),
  ((CompHausLike.LocallyConstant.functor P hs).map f).hom.app x =
    TypeCat.ofHom fun t => LocallyConstant.map (⇑(CategoryTheory.ConcreteCategory.hom f)) t
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.add_sub_add_right : ∀ {α : Type u} [inst : SubtractionMonoid α] {c : α}, IsAddUnit c → ∀ (a b : α), a + c - (b + c) = a - b
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.comp_nsmul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C} (f : P ⟶ Q)
  (g : Q ⟶ R) (n : ℕ), CategoryTheory.CategoryStruct.comp f (n • g) = n • CategoryTheory.CategoryStruct.comp f g
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
CategoryTheory.EnrichedCat.instCoeSortType : (V : Type v) →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] → CoeSort (CategoryTheory.EnrichedCat V) (Type u)
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- A cocone `c` on `F : J ⥤ C` lifts to a cocone in `Over c.pt` with cone point `𝟙 c.pt`.  -/
CategoryTheory.Limits.Cocone.toOver : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cocone F) →
            CategoryTheory.Limits.Cocone (c.toCostructuredArrow.comp (CategoryTheory.CostructuredArrow.toOver F c.pt))
-- Mathlib.LinearAlgebra.Span.Defs
/-- An `R`-submodule of `M` is principal if it is generated by one element.  -/
Submodule.IsPrincipal : {R : Type u_1} →
  {M : Type u_4} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → Prop
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
Polynomial.aeval_iterate_derivative_of_lt : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A] (p : Polynomial R)
  (q : ℕ) (r : A) {p' : Polynomial A},
  Polynomial.map (algebraMap R A) p = (Polynomial.X - Polynomial.C r) ^ q * p' →
    ∀ {k : ℕ}, k < q → (Polynomial.aeval r) ((⇑Polynomial.derivative)^[k] p) = 0
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_add_const_Iio : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => x + a) '' Set.Iio b = Set.Iio (b + a)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Algebra.IsPushout.isIntegral : ∀ (R : Type u_1) (A : Type u_2) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing S]
  [inst_3 : Algebra R A] [inst_4 : Algebra R S] [int : Algebra.IsIntegral R S] (SA : Type u_5) [inst_5 : CommRing SA]
  [inst_6 : Algebra R SA] [inst_7 : Algebra S SA] [inst_8 : Algebra A SA] [inst_9 : IsScalarTower R S SA]
  [inst_10 : IsScalarTower R A SA] [h : Algebra.IsPushout R S A SA], Algebra.IsIntegral A SA
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesIsoLeftHomology_inv_hom_id_assoc : ∀ {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.HasLeftHomology] (hf : S.f = 0) {Z : C} (h : S.leftHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.cyclesIsoLeftHomology hf).inv
      (CategoryTheory.CategoryStruct.comp S.leftHomologyπ h) =
    h
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.coe_ofFinEmb : ∀ (n : ℕ) (β : Type u_2) (f : Fin n ↪ β), ↑(Set.powersetCard.ofFinEmb n β f) = Set.range ⇑f
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.zero_of_epi_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  (f : X ⟶ Y) {g : Y ⟶ Z} [CategoryTheory.Epi f], CategoryTheory.CategoryStruct.comp f g = 0 → g = 0
-- Mathlib.Data.List.Basic
_private.Mathlib.Data.List.Basic.0.List.filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Algebra.Group.Int.Units
Int.natAbs_of_isUnit : ∀ {u : ℤ}, IsUnit u → u.natAbs = 1
-- Init.Data.Vector.Basic
/-- Pad a vector on the left with a given element.

Note that we immediately simplify this to an `++` operation,
and do not provide separate verification theorems.
 -/
Vector.leftpad : {α : Type u_1} → {m : ℕ} → (n : ℕ) → α → Vector α m → Vector α (max n m)
-- Mathlib.Geometry.Euclidean.Similarity
/-- If two triangles have proportional adjacent sides and an equal included angle, then the
triangles are similar.  -/
EuclideanGeometry.similar_of_side_angle_side : ∀ {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [inst : NormedAddCommGroup V₁]
  [inst_1 : NormedAddCommGroup V₂] [inst_2 : InnerProductSpace ℝ V₁] [inst_3 : InnerProductSpace ℝ V₂]
  [inst_4 : MetricSpace P₁] [inst_5 : MetricSpace P₂] [inst_6 : NormedAddTorsor V₁ P₁] [inst_7 : NormedAddTorsor V₂ P₂]
  {a b c : P₁} {a' b' c' : P₂},
  ¬Collinear ℝ {a, b, c} →
    ¬Collinear ℝ {a', b', c'} →
      EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c' →
        dist a b * dist b' c' = dist b c * dist a' b' → Similar ![a, b, c] ![a', b', c']
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAtFilter.eq_1 : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousSMul 𝕜 F] (f : 𝕜 → F) (f' : F) (L : Filter (𝕜 × 𝕜)),
  HasDerivAtFilter f f' L = HasFDerivAtFilter f (ContinuousLinearMap.toSpanSingleton 𝕜 f') L
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.functor_obj_map_obj : ∀ {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑Y),
  hf.functor.obj ((TopologicalSpace.Opens.map f).obj U) = hf.functor.obj ⊤ ⊓ U
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.hexnum.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
Ideal.toTwoSided.congr_simp : ∀ {R : Type u_1} [inst : Ring R] (I I_1 : Ideal R) (e_I : I = I_1) [inst_1 : I.IsTwoSided],
  I.toTwoSided = I_1.toTwoSided
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] {ι : Type u_1}
  [Finite ι] {F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsColimit c), CategoryTheory.IsUniversalColimit c
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Unitary.symm_mulLeft : ∀ {R : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : CStarRing A] [inst_3 : Ring R]
  [inst_4 : Module R A] [inst_5 : SMulCommClass R A A] (u : ↥(unitary A)),
  ((Unitary.mulLeft R A) u).symm = (Unitary.mulLeft R A) (star u)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (U : (X ⨿ Y).Opens) {Z : CommRingCat}
  (h : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inl.base).obj U)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.coprodPresheafObjIso U).hom
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app CategoryTheory.Limits.coprod.inl U) h