mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.stmts₁.match_1.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5) (k : K)
  (a : σ → Γ k) (q : Turing.TM2.Stmt Γ Λ σ)
  (h_1 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Γ k) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.push k a q → motive (Turing.TM2.Stmt.push k a q))
  (h_2 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Option (Γ k) → σ) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.peek k a q → motive (Turing.TM2.Stmt.peek k a q))
  (h_3 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Option (Γ k) → σ) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.pop k a q → motive (Turing.TM2.Stmt.pop k a q))
  (h_4 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.load a q → motive (Turing.TM2.Stmt.load a q))
  (h_5 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (a : σ → Bool) →
        (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.branch a q₁ q₂ → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (Q : Turing.TM2.Stmt Γ Λ σ) → (a : σ → Λ) → Q = Turing.TM2.Stmt.goto a → motive (Turing.TM2.Stmt.goto a))
  (h_7 : (Q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.halt → motive Turing.TM2.Stmt.halt),
  (match Turing.TM2.Stmt.push k a q with
    | Q@h:(Turing.TM2.Stmt.push k a q) => h_1 Q k a q h
    | Q@h:(Turing.TM2.Stmt.peek k a q) => h_2 Q k a q h
    | Q@h:(Turing.TM2.Stmt.pop k a q) => h_3 Q k a q h
    | Q@h:(Turing.TM2.Stmt.load a q) => h_4 Q a q h
    | Q@h:(Turing.TM2.Stmt.branch a q₁ q₂) => h_5 Q a q₁ q₂ h
    | Q@h:(Turing.TM2.Stmt.goto a) => h_6 Q a h
    | Q@h:Turing.TM2.Stmt.halt => h_7 Q h) =
    h_1 (Turing.TM2.Stmt.push k a q) k a q ⋯
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepFun_iff : ∀ {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ)
  {β : Type u_3} {γ : Type u_4} [mβ : MeasurableSpace β] [mγ : MeasurableSpace γ] (f : Ω → β) (g : Ω → γ),
  Measurable f →
    Measurable g →
      ∀ (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
        ProbabilityTheory.CondIndepFun m' hm' f g μ ↔
          ∀ (t1 t2 : Set Ω),
            MeasurableSet t1 →
              MeasurableSet t2 →
                μ[(t1 ∩ t2).indicator fun ω => 1 | m'] =ᵐ[μ]
                  μ[t1.indicator fun ω => 1 | m'] * μ[t2.indicator fun ω => 1 | m']
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
NNReal.continuous_nnrpow_const : ∀ (y : NNReal), Continuous fun x => x.nnrpow y
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- To apply Arzela-Ascoli, we need to check that the set of candidates is closed and
equicontinuous. Equicontinuity follows from the Lipschitz control, we check closedness.  -/
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.closed_candidatesB : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y], IsClosed (GromovHausdorff.candidatesB✝ X Y)
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.trans : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x y z : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.Relation F x y → CommRingCat.Colimits.Relation F y z → CommRingCat.Colimits.Relation F x z
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- If `x` is a point of `Spec R`, this is the morphism of `R`-modules from `M` to the stalk of
`M^~` at `x`.
 -/
AlgebraicGeometry.tilde.toStalk : {R : CommRingCat} →
  (M : ModuleCat ↑R) →
    (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top ↑R)) →
      ModuleCat.of ↑R ↑M ⟶ ModuleCat.of ↑R ↑((AlgebraicGeometry.tilde M).presheaf.stalk x)
-- Mathlib.Logic.Equiv.Set
Equiv.Set.image_symm_apply : ∀ {α : Type u_3} {β : Type u_4} (f : α → β) (s : Set α) (H : Function.Injective f) (x : α) (h : f x ∈ f '' s),
  (Equiv.Set.image f s H).symm ⟨f x, h⟩ = ⟨x, ⋯⟩
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- If `A ≃g H` and `B ≃g G` then `A` is contained in `B` if and only if `H` is contained
in `G`.  -/
SimpleGraph.isContained_congr : ∀ {V : Type u_1} {W : Type u_2} {α : Type u_4} {β : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W}
  {A : SimpleGraph α} {B : SimpleGraph β} (e₁ : A ≃g H) (e₂ : B ≃g G), A.IsContained B ↔ H.IsContained G
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_insert_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, (m.insert k v).getKey? k = some k
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.lift_of : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [inst : Monoid K] [inst_1 : (i : ι) → Monoid (G i)]
  [inst_2 : Monoid H] {φ : (i : ι) → H →* G i} (f : (i : ι) → G i →* K) (k : H →* K)
  (hf : ∀ (i : ι), (f i).comp (φ i) = k) {i : ι} (g : G i),
  (Monoid.PushoutI.lift f k hf) ((Monoid.PushoutI.of i) g) = (f i) g
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_sum_measure_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  [Countable ι] {μ : ι → MeasureTheory.Measure α},
  AEMeasurable f (MeasureTheory.Measure.sum μ) ↔ ∀ (i : ι), AEMeasurable f (μ i)
-- Mathlib.Order.Directed
Antitone.directed_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [IsCodirectedOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Directed (fun x1 x2 => x1 ≤ x2) f
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
AddMonoidAlgebra.instFree : ∀ {M : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  [Module.Free R S], Module.Free R (AddMonoidAlgebra S M)
-- Mathlib.CategoryTheory.Action.Concrete
/-- Bundles a type `H` with a multiplicative action of `G` as an `Action`.  -/
Action.ofMulAction : (G : Type u_1) → (H : Type u) → [inst : Monoid G] → [MulAction G H] → Action (Type u) G
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.equivalenceOfEquiv_inverse : ∀ {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (e : J ≃ I),
  (CategoryTheory.Pi.equivalenceOfEquiv C e).inverse =
    CategoryTheory.Functor.pi' fun i' => CategoryTheory.Pi.eval C (e i')
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.ematch.inj : ∀ {origin origin_1 : Lean.Meta.Grind.Origin},
  Lean.Meta.Grind.SplitSource.ematch origin = Lean.Meta.Grind.SplitSource.ematch origin_1 → origin = origin_1
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
/-- **Alias** of the forward direction of `contMDiffOn_iff_contDiffOn`. -/
ContMDiffOn.contDiffOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  {n : WithTop ℕ∞} {f : E → E'} {s : Set E},
  ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f s → ContDiffOn 𝕜 n f s
-- Mathlib.MeasureTheory.Measure.ResolventTransform
MeasureTheory.integrable_resolvent : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : MeasurableSpace 𝕜] [CompleteSpace 𝕜]
  [inst_3 : NormedDivisionRing A] [inst_4 : NormedAlgebra 𝕜 A] [HereditarilyLindelofSpace 𝕜] [OpensMeasurableSpace 𝕜]
  [CompleteSpace A] [SecondCountableTopology A] [inst_9 : MeasurableSpace A] [BorelSpace A]
  {μ : MeasureTheory.Measure 𝕜} [MeasureTheory.IsFiniteMeasure μ] {a : A},
  a ∉ ⇑(algebraMap 𝕜 A) '' μ.support → MeasureTheory.Integrable (resolvent a) μ
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.SizedBalancedTree.mk.congr_simp : ∀ {α : Type u} {β : α → Type v} {lb ub : ℕ} (impl impl_1 : Std.DTreeMap.Internal.Impl α β) (e_impl : impl = impl_1)
  (balanced_impl : impl.Balanced) (lb_le_size_impl : lb ≤ impl.size) (size_impl_le_ub : impl.size ≤ ub),
  { impl := impl, balanced_impl := balanced_impl, lb_le_size_impl := lb_le_size_impl,
      size_impl_le_ub := size_impl_le_ub } =
    { impl := impl_1, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.coe_le_zero : ∀ {α : Type u} [inst : Zero α] [inst_1 : LE α] {a : α}, ↑a ≤ 0 ↔ a ≤ 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_modify : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} {f : β k → β k},
  m.WF → (m.modify k f).getKey? k' = if (k == k') = true then if k ∈ m then some k else none else m.getKey? k'
-- Mathlib.Algebra.BigOperators.Ring.Finset
Fintype.sum_pow : ∀ {ι : Type u_5} {R : Type u_7} [inst : Fintype ι] [inst_1 : CommSemiring R] (f : ι → R) (n : ℕ),
  (∑ a, f a) ^ n = ∑ p, ∏ i, f (p i)
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.inv.eq_1 : ∀ (G : Type u_4) [inst : MeasurableSpace G] [inst_1 : InvolutiveInv G] [inst_2 : MeasurableInv G],
  MeasurableEquiv.inv G = { toEquiv := Equiv.inv G, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Init.Data.String.Lemmas.FindPos
String.Pos.posLT_offset : ∀ {s : String} {p : s.Pos} {h : 0 < p.offset}, s.posLT p.offset h = p.prev ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.equation_some : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (a b : R),
  W'.Equation ![a, b, 1] ↔ W'.toAffine.Equation a b
-- Init.Data.Vector.Lemmas
Vector.map_id : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n), Vector.map id xs = xs
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.contains t.max! = true
-- Mathlib.Data.NNReal.Defs
NNReal.instDistribLattice : DistribLattice NNReal
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.factors_one : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α],
  UniqueFactorizationMonoid.factors 1 = 0
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.lift₂_mk : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {α : Sort u_2}
  (f : R → ↥(ValuativeRel.posSubmonoid R) → R → ↥(ValuativeRel.posSubmonoid R) → α)
  (hf :
    ∀ (x y z w : R) (t s u v : ↥(ValuativeRel.posSubmonoid R)),
      x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → z * ↑u ≤ᵥ w * ↑v → w * ↑v ≤ᵥ z * ↑u → f x s z v = f y t w u)
  (x y : R) (z w : ↥(ValuativeRel.posSubmonoid R)),
  ValuativeRel.ValueGroupWithZero.lift₂ f hf (ValuativeRel.ValueGroupWithZero.mk x z)
      (ValuativeRel.ValueGroupWithZero.mk y w) =
    f x z y w
-- Mathlib.AlgebraicTopology.Reedy.Basic
/-- The opposite of a Reedy structure.  -/
HomotopicalAlgebra.ReedyStructure.op : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      [inst_1 : W₁.IsMultiplicative] →
        [inst_2 : W₂.IsMultiplicative] →
          {α : Type u_2} →
            [inst_3 : LinearOrder α] →
              [inst_4 : OrderBot α] →
                [inst_5 : SuccOrder α] →
                  [inst_6 : WellFoundedLT α] →
                    HomotopicalAlgebra.ReedyStructure W₁ W₂ α → HomotopicalAlgebra.ReedyStructure W₂.op W₁.op α
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec.0.BitVec.reduceBoolPred : Lean.Name → ℕ → ({n : ℕ} → BitVec n → BitVec n → Bool) → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Mathlib.Algebra.Polynomial.Degree.Support
/-- We can reexpress a sum over `p.support` as a sum over `range (p.natDegree + 1)`.
 -/
Polynomial.sum_over_range : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid S] (p : Polynomial R) {f : ℕ → R → S},
  (∀ (n : ℕ), f n 0 = 0) → p.sum f = ∑ a ∈ Finset.range (p.natDegree + 1), f a (p.coeff a)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.minD_eq_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t.WF → t.isEmpty = false → ∀ {km fallback : α}, t.minD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.ext_iff : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} {M N : CStarMatrix m n A}, (∀ (i : m) (j : n), M i j = N i j) ↔ M = N
-- Std.Data.DTreeMap.Internal.Model
/-- Data structure used by the general tree-traversal function `explore`.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.ExplorationStep : (α : Type u) → (α → Type v) → [Ord α] → (α → Ordering) → Type (max u v)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.of_map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v},
  (SimpleGraph.Walk.map f p).IsTrail → p.IsTrail
-- Lean.Structure
Lean.StructureParentInfo.mk : Lean.Name → Bool → Lean.Name → Lean.StructureParentInfo
-- Init.Grind.Interactive
/-- The `!` modifier instructs `grind` to consider only minimal indexable subexpressions
when selecting patterns.
 -/
Lean.Parser.Tactic.grindParam : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.prodZeroIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  (CategoryTheory.Limits.prodZeroIso X).hom = CategoryTheory.Limits.prod.fst
-- Mathlib.Analysis.Convex.Deriv
ConcaveOn.slope_le_of_hasDerivAt : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ}, ConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivAt f f' x → slope f x y ≤ f'
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- The Ore condition of a fraction, expressed in terms of `oreNum` and `oreDenom`.  -/
OreLocalization.OreSet.ore_eq : ∀ {R : Type u_1} {inst : Monoid R} {S : Submonoid R} [self : OreLocalization.OreSet S] (r : R) (s : ↥S),
  ↑(OreLocalization.OreSet.oreDenom r s) * r = OreLocalization.OreSet.oreNum r s * ↑s
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instAddAction'.eq_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α],
  Lex.instAddAction' = { toVAdd := Lex.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }
-- Lean.Environment
/-- Name of the module being compiled.
 -/
Lean.EnvironmentHeader.mainModule : Lean.EnvironmentHeader → Lean.Name
-- Mathlib.CategoryTheory.Discrete.Basic
/-- Promote an equation between the wrapped terms in `X Y : Discrete α` to an isomorphism `X ≅ Y`
in the discrete category.  -/
CategoryTheory.Discrete.eqToIso : {α : Type u₁} → {X Y : CategoryTheory.Discrete α} → X.as = Y.as → (X ≅ Y)
-- Mathlib.Order.PFilter
Order.PFilter.mem_principal : ∀ {P : Type u_1} [inst : Preorder P] {x y : P}, x ∈ Order.PFilter.principal y ↔ y ≤ x
-- Mathlib.Tactic.NormNum.BigOperators
/-- If `s = t` and we can get the result for `t`, then we can get the result for `s`.
 -/
Mathlib.Meta.Multiset.ProveZeroOrConsResult.eq_trans : {u : Lean.Level} →
  {α : Q(Type u)} →
    {s t : Q(Multiset «$α»)} →
      Q(«$s» = «$t») → Mathlib.Meta.Multiset.ProveZeroOrConsResult t → Mathlib.Meta.Multiset.ProveZeroOrConsResult s
-- Lean.LocalContext
_private.Lean.LocalContext.0.Lean.LocalContext.mkLocalDeclExported : Lean.LocalContext → Lean.FVarId → Lean.Name → Lean.Expr → Lean.BinderInfo → Lean.LocalContext
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_union_of_not_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (∀ a ∈ m₁, a ∉ m₂) → (m₁ ∪ m₂).size = m₁.size + m₂.size
-- Std.Time.Date.PlainDate
Std.Time.PlainDate.instHAddOffset : HAdd Std.Time.PlainDate Std.Time.Day.Offset Std.Time.PlainDate
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- A product monoid algebra is a nested monoid algebra.  -/
MonoidAlgebra.curryRingEquiv : {R : Type u_1} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : Monoid M] → [inst_2 : Monoid N] → MonoidAlgebra R (M × N) ≃+* MonoidAlgebra (MonoidAlgebra R N) M
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.instIsIntegralHomNormalizationPullback : ∀ {X S Y : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f],
  AlgebraicGeometry.IsIntegralHom (AlgebraicGeometry.Scheme.Hom.normalizationPullback f g)
-- Mathlib.SetTheory.Cardinal.Aleph
/-- For the theorem `0 < ω`, see `omega0_pos`.  -/
Ordinal.omega_pos : ∀ (o : Ordinal.{u_1}), 0 < Ordinal.omega o
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtDHashMap α β) (e_m : m = m_1) (a a_1 : α) (e_a : a = a_1) (h : a ∈ m), m.getKey a h = m_1.getKey a_1 ⋯
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarCoord_target : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  (NumberField.mixedEmbedding.polarCoord K).target = Set.univ ×ˢ Set.univ.pi fun i => Complex.polarCoord.target
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.AddMonoidHom.coe_toIntLinearMap_comap : ∀ {A : Type u_9} {A₂ : Type u_10} [inst : AddCommGroup A] [inst_1 : AddCommGroup A₂] (f : A →+ A₂) (s : AddSubgroup A₂),
  Submodule.comap f.toIntLinearMap (AddSubgroup.toIntSubmodule s) = AddSubgroup.toIntSubmodule (AddSubgroup.comap f s)
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_intCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (z : ℤ),
  Int.fract ↑z = 0
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.nilpotent_iff_finite_ascending_central_series`.

---

A group `G` is nilpotent iff there exists an ascending central series which reaches `G` in
finitely many steps.  -/
nilpotent_iff_finite_ascending_central_series : ∀ (G : Type u_1) [inst : Group G], Group.IsNilpotent G ↔ ∃ n H, Subgroup.IsAscendingCentralSeries H ∧ H n = ⊤
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasProd_extend_one : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
  {g : β → γ}, Function.Injective g → (HasProd (Function.extend g f 1) a ↔ HasProd f a)
-- Mathlib.Analysis.Convex.Side
AffineSubspace.not_sOppSide_self : ∀ {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 : P), ¬s.SOppSide x x
-- Mathlib.LinearAlgebra.Finsupp.Pi
Finsupp.comap_lsingle_submodule : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_5}
  (p : α → Submodule R M) (i : α), Submodule.comap (Finsupp.lsingle i) (Finsupp.submodule p) = p i
-- Mathlib.RingTheory.Coalgebra.Convolution
LinearMap.convMul_def : ∀ {R : Type u_1} {A : Type u_3} {C : Type u_5} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] [inst_5 : AddCommMonoid C]
  [inst_6 : Module R C] [inst_7 : CoalgebraStruct R C] (f g : WithConv (C →ₗ[R] A)),
  f * g = WithConv.toConv (LinearMap.mul' R A ∘ₗ TensorProduct.map f.ofConv g.ofConv ∘ₗ CoalgebraStruct.comul)
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
/-- A typeclass which expresses that the order type of a well-order equals (the initial ordinal of)
its cofinality.

If `α` is infinite, this implies that `α` is order isomorphic to `Iio c.ord` for some regular
cardinal `c`. In the informal literature, one often says that `α` is a regular cardinal, by abuse
of notation.  -/
IsRegularCardinalOrder : (α : Type u_2) → [inst : LinearOrder α] → [WellFoundedLT α] → Prop
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiffAt.cle_arrowCongr : ∀ {𝕜 : 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] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {F₄ : Type u_11}
  [inst_12 : NormedAddCommGroup F₄] [inst_13 : NormedSpace 𝕜 F₄] {n : WithTop ℕ∞} {f : M → F₁ ≃L[𝕜] F₂}
  {g : M → F₃ ≃L[𝕜] F₄} {x : M},
  ContMDiffAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₁)) n (fun x => ↑(f x).symm) x →
    ContMDiffAt I (modelWithCornersSelf 𝕜 (F₃ →L[𝕜] F₄)) n (fun x => ↑(g x)) x →
      ContMDiffAt I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄)) n (fun y => ↑((f y).arrowCongr (g y))) x
-- Mathlib.GroupTheory.GroupAction.Basic
_private.Mathlib.GroupTheory.GroupAction.Basic.0.MulAction.termΩ : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Finsupp.Pi
/-- Given a family `Sᵢ` of `R`-submodules of `M` indexed by a type `α`, this is the `R`-submodule
of `α →₀ M` of functions `f` such that `f i ∈ Sᵢ` for all `i : α`.  -/
Finsupp.submodule : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → {α : Type u_5} → (α → Submodule R M) → Submodule R (α →₀ M)
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- Copy of a `FractionalIdeal` with a new underlying set equal to the old one.
Useful to fix definitional equalities.  -/
FractionalIdeal.copy : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} →
        [inst_1 : CommRing P] →
          [inst_2 : Algebra R P] → (p : FractionalIdeal S P) → (s : Set P) → s = ↑p → FractionalIdeal S P
-- Std.Data.DHashMap.Raw
_private.Std.Data.DHashMap.Raw.0.Std.DHashMap.Raw.filter.eq_1 : ∀ {α : Type u} {β : α → Type v} (f : (a : α) → β a → Bool) (m : Std.DHashMap.Raw α β),
  Std.DHashMap.Raw.filter f m = if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.filter f ⟨m, h⟩) else ∅
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (F : CategoryTheory.Functor (↑(Set.Iic j)) C) (X : C) (i : ↑(Set.Iic j)),
  CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj F X ⟨↑i, ⋯⟩ = F.obj i
-- Mathlib.Algebra.Module.GradedModule
DirectSum.Gmodule.instSMulOfDecidableEq : {ιA : Type u_1} →
  {ιB : Type u_2} →
    (A : ιA → Type u_3) →
      (M : ιB → Type u_4) →
        [inst : AddMonoid ιA] →
          [inst_1 : VAdd ιA ιB] →
            [inst_2 : (i : ιA) → AddCommMonoid (A i)] →
              [inst_3 : (i : ιB) → AddCommMonoid (M i)] →
                [DecidableEq ιA] →
                  [DecidableEq ιB] →
                    [inst_6 : GradedMonoid.GMonoid A] →
                      [DirectSum.Gmodule A M] → SMul (DirectSum ιA fun i => A i) (DirectSum ιB fun i => M i)