mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Matrix.Basis
/-- See also `single_eq_updateRow_zero` and `single_eq_updateCol_zero`.  -/
Matrix.single_eq_of_single_single : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α] (i : m)
  (j : n) (a : α), Matrix.single i j a = Matrix.of (Pi.single i (Pi.single j a))
-- Mathlib.Data.Complex.BigOperators
Complex.re_balance : ∀ {α : Type u_1} [inst : Fintype α] (f : α → ℂ) (a : α), (Fintype.balance f a).re = Fintype.balance (Complex.re ∘ f) a
-- Mathlib.Algebra.Module.Basic
Set.indicator_smul_left : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] (s : Set α)
  (r : α → R) (f : α → M), (s.indicator fun a => r a • f a) = fun a => s.indicator r a • f a
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CtorInfo.isScalar : Lean.Compiler.LCNF.CtorInfo → Bool
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.isFiniteIndex' : ∀ {G : Type u_1} [inst : AddGroup G] (self : FiniteIndexNormalAddSubgroup G), self.FiniteIndex
-- Mathlib.Algebra.Group.Submonoid.Basic
IsUnit.submonoid.eq_1 : ∀ (M : Type u_4) [inst : Monoid M], IsUnit.submonoid M = { carrier := Set.ofPred IsUnit, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Algebra.Group.Submonoid.Membership
ofAdd_image_multiples_eq_powers_ofAdd : ∀ {A : Type u_2} [inst : AddMonoid A] {x : A},
  ⇑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x) = ↑(Submonoid.powers (Multiplicative.ofAdd x))
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_ext : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l l' : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys l' →
      (∀ (a : α), Std.Internal.List.getValueCast? a l = Std.Internal.List.getValueCast? a l') → l.Perm l'
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.transfer.congr_simp : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p p_1 : G.Walk u v) (e_p : p = p_1) (H : SimpleGraph V)
  (h : ∀ e ∈ p.edges, e ∈ H.edgeSet), p.transfer H h = p_1.transfer H ⋯
-- Mathlib.CategoryTheory.NatTrans
/-- The naturality square for a given morphism.  -/
CategoryTheory.NatTrans.naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (self : CategoryTheory.NatTrans F G) ⦃X Y : C⦄ (f : X ⟶ Y) {Z : D}
  (h : G.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (self.app Y) h) =
    CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp (G.map f) h)
-- Lean.Meta.Tactic.Assert
Lean.Meta.AssertAfterResult.mk.sizeOf_spec : ∀ (fvarId : Lean.FVarId) (mvarId : Lean.MVarId) (subst : Lean.Meta.FVarSubst),
  sizeOf { fvarId := fvarId, mvarId := mvarId, subst := subst } = 1 + sizeOf fvarId + sizeOf mvarId + sizeOf subst
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.toReal.eq_1 : ∀ (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion []), ms.toReal = ms
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.smul_of_tower_def : ∀ {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [inst : SetLike S α] [inst_1 : SMul M N] [inst_2 : SMul M α]
  [inst_3 : Monoid N] [inst_4 : MulAction N α] [inst_5 : SMulMemClass S N α] [inst_6 : IsScalarTower M N α] (s : S)
  (r : M) (x : ↥s), r • x = ⟨r • ↑x, ⋯⟩
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.aestronglyMeasurable : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b → MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc a b))
-- Lean.AddDecl
_private.Lean.AddDecl.0.Lean.isNamespaceName : Lean.Name → Bool
-- Init.System.IO
/-- Starts a child process with the provided configuration. The child process is spawned using operating
system primitives, and it can be written in any language.

The child process runs in parallel with the parent.

If the child process's standard input is a pipe, use `IO.Process.Child.takeStdin` to make it
possible to close the child's standard input before the process terminates, which provides the child with an end-of-file marker.
 -/
IO.Process.spawn : (args : IO.Process.SpawnArgs) → IO (IO.Process.Child args.toStdioConfig)
-- Mathlib.Data.Finset.Sups
Finset.exists_compls_iff : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Finset α} {p : α → Prop}, (∃ a ∈ s.compls, p a) ↔ ∃ a ∈ s, p aᶜ
-- Mathlib.Data.Vector.Basic
/-- Cast a vector to an array.  -/
List.Vector.toArray : {α : Type u_1} → {n : ℕ} → List.Vector α n → Array α
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- One can reformulate smoothness within a set at a point as continuity within this set at this
point, and smoothness in the corresponding extended chart in the target.  -/
mdifferentiableWithinAt_iff_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M},
  MDiffAt[s] f x ↔ ContinuousWithinAt f s x ∧ MDiffAt[s] (↑(extChartAt I' (f x)) ∘ f) x
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infiniteNeg_mul_infiniteNeg : ∀ {x y : ℝ*}, x.InfiniteNeg → y.InfiniteNeg → (x * y).InfinitePos
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl)
A cocone for the diagram `(D ⋙ forget T) ⋙ T` found by composing the natural transformation `γ`
with the colimiting cocone for `D ⋙ forget T`.
 -/
CategoryTheory.Monad.ForgetCreatesColimits.newCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      {J : Type u} →
        [inst_1 : CategoryTheory.Category.{v, u} J] →
          {D : CategoryTheory.Functor J T.Algebra} →
            CategoryTheory.Limits.Cocone (D.comp T.forget) →
              CategoryTheory.Limits.Cocone ((D.comp T.forget).comp T.toFunctor)
-- Lean.SubExpr
/-- A subexpression of some root expression. Both its value and its position
within the root are stored.  -/
Lean.SubExpr : Type
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.instInhabitedState : Inhabited Lean.Meta.Sym.Arith.State
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.restrict_dirac : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} {a : α} [MeasurableSingletonClass α]
  [inst_2 : Decidable (a ∈ s)],
  (MeasureTheory.Measure.dirac a).restrict s = if a ∈ s then MeasureTheory.Measure.dirac a else 0
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.extensionValuation_apply_coe : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀]
  (x : K), Valued.extensionValuation ↑x = Valued.v x
-- Mathlib.Data.PNat.Basic
PNat.instOrderBot : OrderBot ℕ+
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.map_vanishingIdeal : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (Z : TopologicalSpace.Closeds ↥X),
  (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal Z).map f =
    AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure (⇑f '' ↑Z))
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.lift_mk : ∀ {R : Type u} [inst : Ring R] (I : Ideal R) {a : R} {S : Type v} [inst_1 : I.IsTwoSided] [inst_2 : Semiring S]
  (f : R →+* S) (H : ∀ a ∈ I, f a = 0), (Ideal.Quotient.lift I f H) ((Ideal.Quotient.mk I) a) = f a
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.nontrivial_iff : ∀ (R : Type u_1) {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Nontrivial (Submodule R M) ↔ Nontrivial M
-- Init.Data.Array.Lemmas
Array.getElem?_eq_none : ∀ {α : Type u_1} {i : ℕ} {xs : Array α}, xs.size ≤ i → xs[i]? = none
-- Mathlib.Topology.Algebra.IsUniformGroup.Constructions
/-- The discrete uniformity makes a group a `IsUniformGroup`.  -/
instIsUniformGroupOfDiscreteUniformity : ∀ {G : Type u_1} [inst : Group G] [inst_1 : UniformSpace G] [DiscreteUniformity G], IsUniformGroup G
-- Mathlib.Topology.Category.Compactum
/-- The functor `compactumToCompHaus` is faithful.  -/
compactumToCompHaus.faithful : compactumToCompHaus.Faithful
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
span_range_eq_top_iff_surjective_finsuppLinearCombination : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : α → M}, Submodule.span R (Set.range v) = ⊤ ↔ Function.Surjective ⇑(Finsupp.linearCombination R v)
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
/-- This instance is used to see through the synonym `a ⟶ b = Discrete (a.as ⟶ b.as)`.  -/
CategoryTheory.LocallyDiscrete.subsingleton2Hom : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {a b : CategoryTheory.LocallyDiscrete C} (f g : a ⟶ b),
  Subsingleton (f ⟶ g)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelCompIsIso_inv : ∀ {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) [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.IsIso g],
  (CategoryTheory.Limits.cokernelCompIsIso f g).inv =
    CategoryTheory.Limits.cokernel.desc f
      (CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp f g)))
      ⋯
-- Mathlib.LinearAlgebra.Basis.Exact
Submodule.top_le_span_of_exact_of_retraction : ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K] [inst_6 : Module R P]
  {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K},
  s ∘ₗ f = LinearMap.id →
    Function.Exact ⇑f ⇑g →
      ∀ {ι : Type u_5} {κ : Type u_6} {σ : Type u_7} {v : ι → M} {a : κ → ι} {b : σ → ι},
        Function.Surjective ⇑g →
          (∀ (i : κ), s (v (a i)) = 0) →
            LinearIndependent R (⇑s ∘ v ∘ b) →
              Codisjoint (Set.range a) (Set.range b) →
                ⊤ ≤ Submodule.span R (Set.range v) → ⊤ ≤ Submodule.span R (Set.range (⇑g ∘ v ∘ a))
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.exp_zero : ∀ {M : Type u_4} [inst : AddMonoid M], WithZero.exp 0 = 1
-- Mathlib.Algebra.Group.Action.Basic
/-- If `G` acts on `A`, then it acts also on `A → B`, by `(g +ᵥ F) a = F (g⁻¹ +ᵥ a)`  -/
arrowAddAction : {G : Type u_7} → {A : Type u_8} → {B : Type u_9} → [inst : SubtractionMonoid G] → [AddAction G A] → AddAction G (A → B)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_filter_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getKey? k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) =
      if Std.Internal.List.containsKey k l₂ = true then Std.Internal.List.getKey? k l₁ else none
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.sZMod_eq_sMod : ∀ (p i : ℕ), LucasLehmer.sZMod p i = ↑(LucasLehmer.sMod p i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.containsThenInsertIfNew_fst : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k},
  (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew k v t ⋯).1 = Std.DTreeMap.Internal.Impl.contains k t
-- Mathlib.CategoryTheory.Preadditive.EndoFunctor
CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_add_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (F : CategoryTheory.Functor C C) [inst_2 : F.Additive] (A₁ A₂ : CategoryTheory.Endofunctor.Coalgebra F)
  (α β : A₁ ⟶ A₂), (α + β).f = α.f + β.f
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instCartesianMonoidalCategory.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.AddGrp.instCartesianMonoidalCategory =
    { toMonoidalCategory := CategoryTheory.AddGrp.instMonoidalCategory,
      isTerminalTensorUnit :=
        CategoryTheory.Limits.IsTerminal.ofUniqueHom
          (fun G => CategoryTheory.AddGrp.homMk' (CategoryTheory.SemiCartesianMonoidalCategory.toUnit G.toAddMon)) ⋯,
      fst := fun G H =>
        CategoryTheory.AddGrp.homMk' (CategoryTheory.SemiCartesianMonoidalCategory.fst G.toAddMon H.toAddMon),
      snd := fun G H =>
        CategoryTheory.AddGrp.homMk' (CategoryTheory.SemiCartesianMonoidalCategory.snd G.toAddMon H.toAddMon),
      fst_def := ⋯, snd_def := ⋯,
      tensorProductIsBinaryProduct := fun G H =>
        CategoryTheory.Limits.BinaryFan.IsLimit.mk
          (CategoryTheory.Limits.BinaryFan.mk
            (CategoryTheory.AddGrp.homMk' (CategoryTheory.SemiCartesianMonoidalCategory.fst G.toAddMon H.toAddMon))
            (CategoryTheory.AddGrp.homMk' (CategoryTheory.SemiCartesianMonoidalCategory.snd G.toAddMon H.toAddMon)))
          (fun {T} f g => { hom := CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom }) ⋯ ⋯ ⋯ }
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded_left : ∀ {ι : Type u_1} {E : Type u_2} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated] [inst : NormedAddCommGroup E]
  {a : ι → ℝ} {f : ℝ → E} {I a₀ b : ℝ},
  (∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) b) MeasureTheory.volume) →
    Filter.Tendsto a l (nhds a₀) →
      (∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Set.Ioc (a i) b, ‖f x‖ ≤ I) →
        MeasureTheory.IntegrableOn f (Set.Ioc a₀ b) MeasureTheory.volume
-- Mathlib.Order.Minimal
Maximal.not_gt : ∀ {α : Type u_2} {P : α → Prop} {x y : α} [inst : Preorder α], Maximal P x → P y → ¬x < y
-- Mathlib.Order.Filter.Pointwise
Filter.pureZeroHom_apply : ∀ {α : Type u_2} [inst : Zero α] (a : α), Filter.pureZeroHom a = pure a
-- Mathlib.Analysis.Convex.Function
ConvexOn.sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  {s : Set E} {f g : E → β}, ConvexOn 𝕜 s f → ConcaveOn 𝕜 s g → ConvexOn 𝕜 s (f - g)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastMul : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.BinaryRefVec fun {len} => Std.Tactic.BVDecide.BVExpr.bitblast.blastMul
-- Mathlib.Order.BoundedOrder.Basic
OrderTop.mk : {α : Type u} → [inst : LE α] → [toTop : Top α] → (∀ (a : α), a ≤ ⊤) → OrderTop α
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingField.instIsScalarTower : ∀ {K : Type u_2} [inst : Field K] (f : Polynomial K) {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R K],
  IsScalarTower R K f.SplittingField
-- Std.Internal.Parsec.String
/-- `Parser α` is a parser that consumes a `String` input using a `Sigma String.Pos` and returns a result of type `α`.
 -/
Std.Internal.Parsec.String.Parser : Type → Type
-- Mathlib.Algebra.BigOperators.ModEq
Int.ModEq.listSum_zero : ∀ {n : ℤ} {l : List ℤ}, (∀ x ∈ l, x ≡ 0 [ZMOD n]) → l.sum ≡ 0 [ZMOD n]
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.add_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a b c : X ⟶ Y), a + b + c = a + (b + c)
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncateFun_nsmul : ∀ {p : ℕ} (n : ℕ) {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (m : ℕ) (x : WittVector p R),
  WittVector.truncateFun n (m • x) = m • WittVector.truncateFun n x
-- Init.Data.Nat.Coprime
Nat.Coprime.gcd_left : ∀ {m n : ℕ} (k : ℕ), m.Coprime n → (k.gcd m).Coprime n
-- Aesop.Util.Basic
Aesop.runTacticCapturingPostState : Lean.Syntax.Tactic → Lean.Meta.SavedState → List Lean.MVarId → Lean.MetaM (Lean.Meta.SavedState × List Lean.MVarId)
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.hermite.eq_def : ∀ (x : ℕ),
  Polynomial.hermite x =
    match x with
    | 0 => 1
    | n.succ => Polynomial.X * Polynomial.hermite n - Polynomial.derivative (Polynomial.hermite n)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSemanticTokens : Lean.FromJson Lean.Lsp.SemanticTokens
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.pow_zero_eq_zeta : ArithmeticFunction.pow 0 = ArithmeticFunction.zeta
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.coinduced.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] [inst : AddGroup β] (f : α → β),
  AddGroupTopology.coinduced f = sInf {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.instHasHomologyObjSingle : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C) (i : ι), ((HomologicalComplex.single C c j).obj A).HasHomology i
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.normal_addSubgroupOf_centralizer_normalizer : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G),
  ((AddSubgroup.centralizer s).addSubgroupOf (AddSubgroup.normalizer s)).Normal
-- Init.Data.Nat.Coprime
Nat.Coprime.pow : ∀ {k l : ℕ} (m n : ℕ), k.Coprime l → (k ^ m).Coprime (l ^ n)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasStrictFDerivAt_finCons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] (i : Fin n.succ) → F' i},
  HasStrictFDerivAt (fun x => Fin.cons (φ x) (φs x)) φ' x ↔
    HasStrictFDerivAt φ (ContinuousLinearMap.proj 0 ∘SL φ') x ∧
      HasStrictFDerivAt φs (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') x
-- Mathlib.Analysis.Convex.Between
AffineSubspace.right_mem_of_wbtw : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P} {s : AffineSubspace R P},
  Wbtw R x y z → x ∈ s → y ∈ s → x ≠ y → z ∈ s
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.uset.injEq : ∀ (x : Lean.IR.VarId) (i : ℕ) (y : Lean.IR.VarId) (b : Lean.IR.FnBody) (x_1 : Lean.IR.VarId) (i_1 : ℕ)
  (y_1 : Lean.IR.VarId) (b_1 : Lean.IR.FnBody),
  (Lean.IR.FnBody.uset x i y b = Lean.IR.FnBody.uset x_1 i_1 y_1 b_1) = (x = x_1 ∧ i = i_1 ∧ y = y_1 ∧ b = b_1)
-- Mathlib.LinearAlgebra.Projection
LinearMap.ker_linearProjOfIsCompl : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (q : Submodule R E)
  {F : Type u_7} [inst_3 : AddCommGroup F] [inst_4 : Module R F] (i : F →ₗ[R] E) (hi : Function.Injective ⇑i)
  (h : IsCompl i.range q), (LinearMap.linearProjOfIsCompl q i hi h).ker = q
-- Mathlib.Analysis.Analytic.Constructions
/-- `f x / g x` is analytic away from `g x = 0`  -/
AnalyticWithinAt.div : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f g : E → 𝕝}
  {s : Set E} {x : E},
  AnalyticWithinAt 𝕜 f s x → AnalyticWithinAt 𝕜 g s x → g x ≠ 0 → AnalyticWithinAt 𝕜 (fun x => f x / g x) s x
-- Mathlib.Analysis.Convex.Quasiconvex
Antitone.quasiconcaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {f : E → β}, Antitone f → QuasiconcaveOn 𝕜 Set.univ f
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.mulVecBilin.congr_simp : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_4) (S : Type u_5) {A : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : SMulCommClass S R A]
  [inst_6 : SMulCommClass S A A] [inst_7 : IsScalarTower R A A] [inst_8 : Fintype n],
  Matrix.mulVecBilin R S = Matrix.mulVecBilin R S
-- Lean.Structure
Lean.StructureFieldInfo.lt : Lean.StructureFieldInfo → Lean.StructureFieldInfo → Bool
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange.addEquiv_toAddMonoidHom : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (e : M ≃+ N),
  ↑(Finsupp.mapRange.addEquiv e) = Finsupp.mapRange.addMonoidHom e.toAddMonoidHom
-- Mathlib.Data.Seq.Computation
Computation.Equiv.symm : ∀ {α : Type u} {s t : Computation α}, s.Equiv t → t.Equiv s
-- Mathlib.Condensed.Light.TopCatAdjunction
LightCondSet.topCatAdjunctionUnit_hom_app : ∀ (X : LightCondSet) (S : LightProfiniteᵒᵖ),
  X.topCatAdjunctionUnit.hom.app S =
    TypeCat.ofHom fun x =>
      {
        toFun := fun s =>
          (CategoryTheory.ConcreteCategory.hom (X.obj.map (CompHausLike.const (LightProfinite.of PUnit.{u + 1}) s).op))
            x,
        continuous_toFun := ⋯ }
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulReflectLT.to_contravariantClass_pos_mul_lt : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [PosMulReflectLT α],
  ContravariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x1 x2 => x1 < x2
-- Mathlib.Topology.Instances.CantorSet
zero_mem_preCantorSet : ∀ (n : ℕ), 0 ∈ preCantorSet n
-- Mathlib.Data.Nat.PrimeFin
Nat.primeFactors_one : Nat.primeFactors 1 = ∅
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- The variation of the identity on `Icc a b` is `b - a`.  -/
eVariationOn_id_Icc : ∀ (a b : ℝ), eVariationOn id (Set.Icc a b) = ENNReal.ofReal (b - a)
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.norm_le_card_mul_iSup_norm_inner : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E),
  ‖x‖ ≤ √↑(Fintype.card ι) * ⨆ i, ‖inner 𝕜 (b i) x‖
-- Mathlib.Data.Complex.Basic
Complex.normSq_apply : ∀ (z : ℂ), Complex.normSq z = z.re * z.re + z.im * z.im
-- Mathlib.NumberTheory.Harmonic.Int
/-- The n-th harmonic number is not an integer for n ≥ 2.  -/
harmonic_not_int : ∀ {n : ℕ}, 2 ≤ n → ¬(harmonic n).isInt = true
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- If a functor creates coequalizers and coproducts, it creates colimits.

We additionally require the rather strong condition that the functor reflects isomorphisms. It is
unclear whether the statement remains true without this condition. There are various definitions of
"creating colimits" in the literature, and whether or not the condition can be dropped seems to
depend on the specific definition that is used.  -/
CategoryTheory.Limits.createsColimitsOfSizeOfCreatesCoequalizersAndCoproducts : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [CategoryTheory.Limits.HasCoequalizers D] →
          [CategoryTheory.Limits.HasCoproducts D] →
            (G : CategoryTheory.Functor C D) →
              [G.ReflectsIsomorphisms] →
                [CategoryTheory.CreatesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] →
                  [(J : Type w) → CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete J) G] →
                    CategoryTheory.CreatesColimitsOfSize.{w, w, v, v₂, u, u₂} G