mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_le_iff : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α},
  BddBelow s → s.Nonempty → (sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a)
-- Aesop.Search.SearchM
Aesop.SearchM.run' : {Q : Type} →
  [inst : Aesop.Queue Q] →
    {α : Type} →
      Aesop.SearchM.Context →
        Aesop.SearchM.State Q → Aesop.Tree → Aesop.SearchM Q α → Aesop.BaseM (α × Aesop.SearchM.State Q × Aesop.Tree)
-- Std.Http.Protocol.H1.Parser
/-- Lifts an `Option` into the parser monad, failing with a generic message if the value is `none`.
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.liftOption : {α : Type} → Option α → Std.Internal.Parsec.ByteArray.Parser α
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.map_add : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (a b : M),
  e (a + b) = e a + e b
-- Mathlib.RingTheory.Congruence.Defs
/-- A function used to define scalar actions on `RingCon.Quotient`. To make sure such actions coming
from different sources are reducibly defeq, they should all go through this function.  -/
RingCon.smulAux : {R : Type u_1} →
  [inst : Add R] →
    [inst_1 : Mul R] →
      {α : Type u_2} →
        [inst_2 : SMul α R] →
          (c : RingCon R) → (∀ (a : α) (x y : R), c x y → c (a • x) (a • y)) → α → c.Quotient → c.Quotient
-- Mathlib.Data.Set.Countable
Set.countable_singleton : ∀ {α : Type u} (a : α), {a}.Countable
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.mk_ball : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {r : ℝ},
  DifferentiableOn 𝕜 f (Metric.ball x r) → ContinuousOn f (Metric.closedBall x r) → DiffContOnCl 𝕜 f (Metric.ball x r)
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_iSup_of_directed : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Sort u_2} [hι : Nonempty ι] {K : ι → AddSubgroup G},
  Directed (fun x1 x2 => x1 ≤ x2) K → ∀ {x : G}, x ∈ iSup K ↔ ∃ i, x ∈ K i
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.comp.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  (f f_1 : MeasureTheory.SimpleFunc β γ),
  f = f_1 → ∀ (g g_1 : α → β) (e_g : g = g_1) (hgm : Measurable g), f.comp g hgm = f_1.comp g_1 ⋯
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_comm : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c : ℝ} {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'},
  Asymptotics.IsBigOWith c l (fun x => f₁ x - f₂ x) g ↔ Asymptotics.IsBigOWith c l (fun x => f₂ x - f₁ x) g
-- Init.Grind.Ordered.Module
Lean.Grind.ExistsAddOfLT.exists_add_of_le : ∀ {α : Type u} {inst : LT α} {inst_1 : Zero α} {inst_2 : Add α} [self : Lean.Grind.ExistsAddOfLT α] {a b : α},
  a < b → ∃ c, 0 < c ∧ b = a + c
-- Mathlib.Analysis.Normed.Group.Basic
NormedAddGroup.nhds_basis_norm_lt : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (x : E), (nhds x).HasBasis (fun ε => 0 < ε) fun ε => {y | ‖-y + x‖ < ε}
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.instIsProbabilityMeasure_stieltjesFunction : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : ProbabilityTheory.IsMeasurableRatCDF f) (a : α),
  MeasureTheory.IsProbabilityMeasure (hf.stieltjesFunction a).measure
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
SemiSimplexCategory.toSimplexCategory_map_homOfMono : ∀ {n m : SemiSimplexCategory}
  (f : SemiSimplexCategory.toSimplexCategory.obj n ⟶ SemiSimplexCategory.toSimplexCategory.obj m)
  [inst : CategoryTheory.Mono f], SemiSimplexCategory.toSimplexCategory.map (SemiSimplexCategory.homOfMono f) = f
-- Mathlib.Data.Finmap
AList.toFinmap.eq_1 : ∀ {α : Type u} {β : α → Type v} (s : AList β), s.toFinmap = { entries := ↑s.entries, nodupKeys := ⋯ }
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.instCoeHomHomObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) →
        {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} → Coe (A.Hom B) (A.obj ⟶ B.obj)
-- Mathlib.NumberTheory.ModularForms.NormTrace
SlashInvariantForm.coe_norm : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f : F) [inst : FunLike F UpperHalfPlane ℂ]
  {k : ℤ} [inst_1 : SlashInvariantFormClass F 𝒢 k] [inst_2 : 𝒢.IsFiniteRelIndex ℋ] [inst_3 : ℋ.HasDetPlusMinusOne],
  ⇑(SlashInvariantForm.norm ℋ f) = ∏ q, SlashInvariantForm.quotientFunc f q
-- Batteries.Control.Nondet.Basic
/-- Bind a nondeterministic function over a nondeterministic value,
ensuring the function is run with the relevant backtrackable state at each value.
 -/
Nondet.bind : {σ : Type} →
  {m : Type → Type} →
    [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α β : Type} → Nondet m α → (α → Nondet m β) → Nondet m β
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.IsPushout.of_hasBinaryBiproduct : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.IsPushout CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0 0
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.instIsStableUnderRetractsIsoModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass], P.isoModSerre.IsStableUnderRetracts
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_I₀ : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P]
  {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  (f : W ⟶ X) [inst_2 : W.Over S] [inst_3 : X.Over S] [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰]
  [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S],
  (AlgebraicGeometry.Scheme.Cover.pullbackCoverOver' S 𝒰 f).I₀ = 𝒰.I₀
-- Mathlib.Algebra.DirectSum.Internal
DirectSum.coe_mul_of_apply_aux : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddMonoid ι] [inst_5 : SetLike.GradedMonoid A]
  (r : DirectSum ι fun i => ↥(A i)) {i : ι} (r' : ↥(A i)) {j n : ι},
  (∀ (x : ι), x + i = n ↔ x = j) → ↑((r * (DirectSum.of (fun i => ↥(A i)) i) r') n) = ↑(r j) * ↑r'
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.of_forall_getKey_eq_of_forall_constGet?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.WF →
    t₂.WF →
      (∀ (k : α) (hk : k ∈ t₁) (hk' : k ∈ t₂), t₁.getKey k hk = t₂.getKey k hk') →
        (∀ (k : α), Std.DTreeMap.Raw.Const.get? t₁ k = Std.DTreeMap.Raw.Const.get? t₂ k) → t₁.Equiv t₂
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.mk : {R : Type u_1} →
  [inst : PartialOrder R] →
    [inst_1 : Semiring R] →
      [inst_2 : IsStrictOrderedRing R] →
        {X : Type u_2} →
          {Y : Type u_3} →
            [inst_3 : Convexity.ConvexSpace R X] →
              [inst_4 : Convexity.ConvexSpace R Y] →
                (toFun : X → Y) →
                  autoParam (Convexity.IsAffineMap R toFun)
                      Convexity.ConvexSpace.AffineMap.isAffineMap_toFun._autoParam →
                    Convexity.ConvexSpace.AffineMap R X Y
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.map_zero : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [Nonempty ι], f 0 = 0
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom : ∀ {R : Type u} [inst : CommRing R] {S : Type u} [inst_1 : CommRing S] (f : R →+* S)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S))
  (hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier)
  (s : ↑((AlgebraicGeometry.Spec.structureSheaf R).obj.obj (Opposite.op U))) (p : ↥V),
  ↑((AlgebraicGeometry.StructureSheaf.comapₗ f.toSemilinearMap U V hUV) s) p =
    (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) (↑s ⟨PrimeSpectrum.comap f ↑p, ⋯⟩)
-- Mathlib.Analysis.InnerProductSpace.PiL2
stdOrthonormalBasis.congr_simp : ∀ (𝕜 : Type u_7) [inst : RCLike 𝕜] (E : Type u_8) [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E], stdOrthonormalBasis 𝕜 E = stdOrthonormalBasis 𝕜 E
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly_k.eq_1 : ∀ (e : Lean.Grind.CommRing.Expr),
  e.toPoly_k =
    Lean.Grind.CommRing.Expr.rec (fun k => Lean.Grind.CommRing.Poly.num k) (fun k => Lean.Grind.CommRing.Poly.num ↑k)
      (fun k => Lean.Grind.CommRing.Poly.num k) (fun x => Lean.Grind.CommRing.Poly.ofVar x)
      (fun x ih => Lean.Grind.CommRing.Poly.mulConst_k (-1) ih) (fun x x_1 ih₁ ih₂ => ih₁.combine_k ih₂)
      (fun x x_1 ih₁ ih₂ => ih₁.combine_k (Lean.Grind.CommRing.Poly.mulConst_k (-1) ih₂))
      (fun x x_1 ih₁ ih₂ => ih₁.mul ih₂)
      (fun a k ih =>
        Bool.rec
          (Lean.Grind.CommRing.Expr.rec (fun n => Lean.Grind.CommRing.Poly.num (n ^ k))
            (fun n => Lean.Grind.CommRing.Poly.num (↑n ^ k)) (fun n => Lean.Grind.CommRing.Poly.num (n ^ k))
            (fun x =>
              Lean.Grind.CommRing.Poly.ofMon
                (Lean.Grind.CommRing.Mon.mult { x := x, k := k } Lean.Grind.CommRing.Mon.unit))
            (fun x x_1 => ih.pow k) (fun x x_1 x_2 x_3 => ih.pow k) (fun x x_1 x_2 x_3 => ih.pow k)
            (fun x x_1 x_2 x_3 => ih.pow k) (fun x x_1 x_2 => ih.pow k) a)
          (Lean.Grind.CommRing.Poly.num 1) (k.beq 0))
      e
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteSpanningSetsIn.set_mem : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)}
  (self : μ.FiniteSpanningSetsIn C) (i : ℕ), self.set i ∈ C
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- Over a characteristic-zero division ring, the centroids given by
two subsets of the points of a simplex are equal if and only if those
faces are given by the same subset of points.  -/
Affine.Simplex.centroid_eq_iff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [CharZero k] {n : ℕ} (s : Affine.Simplex k P n) {fs₁ fs₂ : Finset (Fin (n + 1))} {m₁ m₂ : ℕ},
  fs₁.card = m₁ + 1 → fs₂.card = m₂ + 1 → (Finset.centroid k fs₁ s.points = Finset.centroid k fs₂ s.points ↔ fs₁ = fs₂)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.ISize.minValueSealed_def : ISize.minValueSealed✝ = ISize.minValue
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.equiv_of_beq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : BEq β] [LawfulBEq β],
  m₁.WF → m₂.WF → Std.DTreeMap.Raw.Const.beq m₁ m₂ = true → m₁.Equiv m₂
-- Mathlib.GroupTheory.Nilpotent
AddGroup.IsNilpotent.nilpotent : ∀ (G : Type u_2) [inst : AddGroup G] [AddGroup.IsNilpotent G], ∃ n, AddSubgroup.upperCentralSeries G n = ⊤
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.ofClass_mk : ∀ {α : Type u_2} {β : Type u_3} {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β}
  (f : α →*₀ β) (hf : Monotone ⇑f), MonoidWithZeroHom.ofClass { toMonoidWithZeroHom := f, monotone' := hf } = f
-- Init.Data.UInt.Lemmas
instLawfulIdentityUInt8HAddOfNat : Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Option.isSome.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((val : α) → motive (some val)) → (Unit → motive none) → motive x
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- **Alias** of the reverse direction of `hasFDerivWithinAt_insert_self`. -/
HasFDerivWithinAt.insert : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x → HasFDerivWithinAt f f' (insert x s) x
-- Mathlib.Topology.Semicontinuity.Basic
IsOpen.upperSemicontinuousAt_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s : Set α} {x : α} {y : β} [inst_1 : Zero β]
  [inst_2 : Preorder β], IsOpen s → y ≤ 0 → UpperSemicontinuousAt (s.indicator fun _x => y) x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaGrpObj.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (G : C)
  [inst_2 : CategoryTheory.GrpObj G],
  CategoryTheory.yonedaGrpObj G =
    { obj := fun X => GrpCat.of (Opposite.unop X ⟶ G),
      map := fun {X Y} φ => GrpCat.ofHom (MonCat.Hom.hom ((CategoryTheory.yonedaMonObj G).map φ)), map_id := ⋯,
      map_comp := ⋯ }
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddCommGroupOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup Mᵃᵒᵖ], DomAddAct.instAddCommGroupOfAddOpposite = inst
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- The image of the normalizer is equal to the normalizer of the image of an isomorphism.  -/
Subgroup.map_equiv_normalizer_eq : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup G) (f : G ≃* N),
  Subgroup.map f.toMonoidHom (Subgroup.normalizer ↑H) = Subgroup.normalizer ↑(Subgroup.map f.toMonoidHom H)
-- Init.Data.String.Basic
String.Slice.Pos.get.eq_1 : ∀ {s : String.Slice} (pos : s.Pos) (h : pos ≠ s.endPos),
  pos.get h = s.str.decodeChar (s.startInclusive.offset.byteIdx + pos.offset.byteIdx) ⋯
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.isFiniteMeasure_withDensity_ofReal : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.HasFiniteIntegral f μ → MeasureTheory.IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))
-- Init.Core
PNonScalar.mk.sizeOf_spec : ∀ (v : ℕ), sizeOf (PNonScalar.mk v) = 1 + sizeOf v
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.inv_map_inv_app : ∀ {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]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X Y : C} (e : X ≅ Y) (Z : D),
  CategoryTheory.inv ((F.map e.inv).app Z) = (F.map e.hom).app Z
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
TopologicalSpace.Opens.sheafRestrict_map_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} (U : TopologicalSpace.Opens ↑X)
  {X_1 Y : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) C} (f : X_1 ⟶ Y)
  (X_2 : (TopologicalSpace.Opens ↑(TopCat.of ↥U))ᵒᵖ),
  (U.sheafRestrict.map f).hom.app X_2 = f.hom.app (Opposite.op (⋯.functor.obj (Opposite.unop X_2)))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instMonoidalMonMapMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : CategoryTheory.BraidedCategory C] →
                [inst_5 : CategoryTheory.BraidedCategory D] → [inst_6 : F.Braided] → F.mapMon.Monoidal
-- Mathlib.GroupTheory.SemidirectProduct
/-- The element of G  -/
SemidirectProduct.right : {N : Type u_1} → {G : Type u_2} → [inst : Group N] → [inst_1 : Group G] → {φ : G →* MulAut N} → N ⋊[φ] G → G
-- Mathlib.RingTheory.Noetherian.Basic
fg_of_injective : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module S P] [IsNoetherian S P]
  {N : Submodule R M} {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (f : M →ₛₗ[σ] P),
  Function.Injective ⇑f → N.FG
-- Lean.Meta.ACLt
Lean.Meta.ACLt.ReduceMode.none.sizeOf_spec : sizeOf Lean.Meta.ACLt.ReduceMode.none = 1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.minD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {fallback : α},
  t₁.Equiv t₂ → t₁.minD fallback = t₂.minD fallback
-- Mathlib.Data.Sign.Defs
/-- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
so we only define the `CommGroupWithZero`.  -/
SignType.instCommGroupWithZero : CommGroupWithZero SignType
-- Lean.Meta.Tactic.Constructor
/-- When the goal `mvarId` type is an inductive datatype,
`constructor` calls `apply` with the first matching constructor.
 -/
Lean.MVarId.constructor : Lean.MVarId → optParam Lean.Meta.ApplyConfig { } → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_infty_iff_fderivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F},
  UniqueDiffOn 𝕜 s → (ContDiffOn 𝕜 (↑⊤) f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑⊤) (fderivWithin 𝕜 f s) s)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.indexing_modeUnindexed : Lean.ParserDescr
-- Init.Data.Int.Linear
Int.Internal.Linear.instBEqPoly.beq.eq_1 : ∀ (a b : ℤ),
  Int.Internal.Linear.instBEqPoly.beq (Int.Internal.Linear.Poly.num a) (Int.Internal.Linear.Poly.num b) = (a == b)
-- Lean.Meta.Eqns
Lean.Meta.EqnsExtState.mk.injEq : ∀ (mapInv mapInv_1 : Lean.PHashMap Lean.Name Lean.Name),
  ({ mapInv := mapInv } = { mapInv := mapInv_1 }) = (mapInv = mapInv_1)
-- Mathlib.Order.Filter.TendstoCofinite
Filter.TendstoCofinite.mapDomain.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} (f : α → β) [inst : AddCommMonoid M] [inst_1 : Filter.TendstoCofinite f]
  (v : α → M) (i : β), Filter.TendstoCofinite.mapDomain f v i = ⋯.toFinset.sum v
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.CommaMorphism.w : ∀ {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] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R} (self : CategoryTheory.CommaMorphism X Y),
  CategoryTheory.CategoryStruct.comp (L.map self.left) Y.hom =
    CategoryTheory.CategoryStruct.comp X.hom (R.map self.right)
-- Mathlib.Data.Sym.Basic
Sym.replicate_right_inj : ∀ {α : Type u_1} {a b : α} {n : ℕ}, n ≠ 0 → (Sym.replicate n a = Sym.replicate n b ↔ a = b)
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.of_carrier : ∀ (R : CommSemiRingCat), CommSemiRingCat.of ↑R = R
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
SymmetricPower.module : (R ι : Type u) →
  [inst : CommSemiring R] →
    (M : Type v) → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Module R (SymmetricPower R ι M)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- The presheaf of smooth functions from `M` to `G`, for `G` a Lie group, as a presheaf of groups.
 -/
smoothPresheafGroup : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              ModelWithCorners 𝕜 EM HM →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [ChartedSpace HM M] →
                                  (G : Type u) →
                                    [inst_9 : TopologicalSpace G] →
                                      [inst_10 : ChartedSpace H G] →
                                        [inst_11 : Group G] → [LieGroup I (↑⊤) G] → TopCat.Presheaf GrpCat (TopCat.of M)
-- Std.Data.Internal.List.Associative
Std.Internal.List.le_minKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {k fallback : α},
        (compare k (Std.Internal.List.minKeyD l fallback)).isLE = true ↔
          ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k k').isLE = true
-- Init.Core
instNonemptyProd : ∀ {α : Type u_1} {β : Type u_2} [h1 : Nonempty α] [h2 : Nonempty β], Nonempty (α × β)
-- Mathlib.RingTheory.SimpleModule.Isotypic
IsIsotypic.of_self : ∀ {R : Type u_2} (M : Type u) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleRing R],
  IsIsotypic R R → IsIsotypic R M
-- Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
alternatingGroup.mem_kleinFour_of_order_two_pow : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  Nat.card α = 4 →
    ∀ {g : Equiv.Perm α}, g ∈ alternatingGroup α → ∀ {n : ℕ}, orderOf g ∣ 2 ^ n → g.cycleType = ∅ ∨ g.cycleType = {2, 2}
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- Taking the `sum` under `h` is an additive homomorphism, if `h` is an additive homomorphism.
This is a more specific version of `SkewMonoidAlgebra.sum_add_index` with simpler hypotheses.  -/
SkewMonoidAlgebra.sum_add_index' : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {S : Type u_3} [inst_1 : AddCommMonoid S]
  {f g : SkewMonoidAlgebra k G} {h : G → k → S},
  (∀ (i : G), h i 0 = 0) → (∀ (a : G) (b₁ b₂ : k), h a (b₁ + b₂) = h a b₁ + h a b₂) → (f + g).sum h = f.sum h + g.sum h
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabStep1.mk : Lean.Elab.Command.InductiveView →
  (Array Lean.Elab.Command.ElabHeaderResult →
      Lean.Elab.Command.ElabHeaderResult → Array Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep2) →
    Lean.Elab.Command.InductiveElabStep1
-- Mathlib.Analysis.Calculus.FDeriv.Mul
fderiv_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [inst_8 : IsBoundedSMul 𝕜' F] [inst_9 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'},
  DifferentiableAt 𝕜 c x →
    DifferentiableAt 𝕜 f x → fderiv 𝕜 (c • f) x = c x • fderiv 𝕜 f x + (fderiv 𝕜 c x).smulRight (f x)