mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_eq_iff_eq' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {x₁ x₂ : R} {y₁ y₂ : ↥M},
  IsLocalization.mk' S x₁ y₁ = IsLocalization.mk' S x₂ y₂ ↔ (algebraMap R S) (x₁ * ↑y₂) = (algebraMap R S) (x₂ * ↑y₁)
-- Mathlib.CategoryTheory.Filtered.Final
CategoryTheory.Functor.Initial.exists_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C] [F.Initial] {d : D} {c : C}
  (s s' : F.obj c ⟶ d),
  ∃ c' t, CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s'
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- The operation `(op (.cons hd ·)).tail` is friendly if `op` is friendly.  -/
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.cons_tail : ∀ {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α} {hd : α},
  Tactic.ComputeAsymptotics.Seq.FriendlyOperation op →
    Tactic.ComputeAsymptotics.Seq.FriendlyOperation fun s => (op (Stream'.Seq.cons hd s)).tail
-- Mathlib.Data.Sym.Sym2
Sym2.add_mk : ∀ {M : Type u_4} [inst : AddCommMagma M] (a b : M), s(a, b).add = a + b
-- Std.Time.Zoned.Database.TzIf
/-- The array indicating whether each transition time uses wall clock time or standard time.
 -/
Std.Time.TimeZone.TZif.TZifV1.stdWallIndicators : Std.Time.TimeZone.TZif.TZifV1 → Array Bool
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.insertListIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)), Std.Internal.List.insertListIfNew l [] = l
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_alter_of_compare_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)},
  compare k k' = Ordering.eq → (k' ∈ (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl ↔ (f (t.get? k)).isSome = true)
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_whiskerRight_fst : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b c : B × C} {f g : a ⟶ b} (θ : f ⟶ g) (g_1 : b ⟶ c),
  (CategoryTheory.Bicategory.whiskerRight θ g_1).1 = CategoryTheory.Bicategory.whiskerRight θ.1 g_1.1
-- Init.System.IOError
IO.Error.unsupportedOperation.inj : ∀ {osCode : UInt32} {details : String} {osCode_1 : UInt32} {details_1 : String},
  IO.Error.unsupportedOperation osCode details = IO.Error.unsupportedOperation osCode_1 details_1 →
    osCode = osCode_1 ∧ details = details_1
-- Mathlib.CategoryTheory.GradedObject
/-- Given `X : GradedObject I C` and `p : I → J`, `X.HasMap p` is the condition that
for all `j : J`, the coproduct of all `X i` such `p i = j` exists.  -/
CategoryTheory.GradedObject.HasMap : {I : Type u_1} →
  {J : Type u_2} →
    {C : Type u_4} → [CategoryTheory.Category.{v_1, u_4} C] → CategoryTheory.GradedObject I C → (I → J) → Prop
-- Init.Control.Lawful.Basic
bind_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [LawfulMonad m] (x : m α), x >>= pure = x
-- Std.Internal.Do.Order.Basic
Lean.Order.CompleteLattice.ofProp.eq_1 : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l] (p : Prop),
  Lean.Order.CompleteLattice.ofProp p = if p then Lean.Order.top else Lean.Order.bot
-- Mathlib.LinearAlgebra.Multilinear.Curry
multilinearCurryLeftEquiv_apply : ∀ (R : Type uR) {n : ℕ} (M : Fin n.succ → Type v) (M₂ : Type v₂) [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (f : MultilinearMap R M M₂),
  (multilinearCurryLeftEquiv R M M₂) f = f.curryLeft
-- Init.Data.Option.Basic
/-- Lifts an ordering relation to `Option` such that `none` is the *greatest* element.

It can be understood as adding a distinguished greatest element, represented by `none`, to both `α`
and `β`.

Caution: Given `LT α`, `Option.SomeLtNone.lt LT.lt` differs from the `LT (Option α)` instance,
which is implemented by `Option.lt Lt.lt`.

Examples:
 * `Option.lt (fun n k : Nat => n < k) none none = False`
 * `Option.lt (fun n k : Nat => n < k) none (some 3) = False`
 * `Option.lt (fun n k : Nat => n < k) (some 3) none = True`
 * `Option.lt (fun n k : Nat => n < k) (some 4) (some 5) = True`
 * `Option.le (fun n k : Nat => n < k) (some 5) (some 4) = False`
 * `Option.lt (fun n k : Nat => n < k) (some 4) (some 4) = False`
 -/
Option.SomeLtNone.lt : {β : Type u_1} → {α : Type u_2} → (α → β → Prop) → Option α → Option β → Prop
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α}, (t₁ \ t₂).get? k = if k ∈ t₂ then none else t₁.get? k
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyMapIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
  (CategoryTheory.ShortComplex.leftHomologyMapIso e).inv = CategoryTheory.ShortComplex.leftHomologyMap e.inv
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- A version of `NormedSpace.exp_sum_of_commute` for a commutative Banach-algebra.  -/
NormedSpace.exp_sum : ∀ {𝔸 : Type u_2} [inst : NormedCommRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] {ι : Type u_3} (s : Finset ι)
  (f : ι → 𝔸), NormedSpace.exp (∑ i ∈ s, f i) = ∏ i ∈ s, NormedSpace.exp (f i)
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
/-- Key lemma for Sylvester's law of inertia: compute the signature of a weighted sum of squares.  -/
QuadraticForm.sigPos_weightedSumSquares : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] {ι : Type u_5} [inst_2 : Fintype ι] {w : ι → 𝕜}
  [IsStrictOrderedRing 𝕜], sigPos (QuadraticMap.weightedSumSquares 𝕜 w) = {i | 0 < w i}.ncard
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.addCayley_erase_zero : ∀ {M : Type u_1} (s : Set M) [inst : AddZeroClass M], SimpleGraph.addCayley (s \ {0}) = SimpleGraph.addCayley s
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.inducedFunctor_map : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] (F : C → D)
  {X Y : CategoryTheory.InducedCategory D F} (f : X ⟶ Y), (CategoryTheory.inducedFunctor F).map f = f.hom
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- `G.PreservesLeftKanExtensions L` means that `G : B ⥤ D` preserves all left Kan extensions along
`L : A ⥤ C` of every functor `A ⥤ B`.  -/
CategoryTheory.Functor.PreservesLeftKanExtensions : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                CategoryTheory.Functor B D → CategoryTheory.Functor A C → Prop
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_self_le_mul_self_iff : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [PosMulStrictMono R] [MulPosMono R] {a b : R},
  0 ≤ a → 0 ≤ b → (a ≤ b ↔ a * a ≤ b * b)
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.fold.eq_1 : ∀ {α : Type u} (x : α) (f : (i : ℕ) → i < 0 → α → α), Nat.fold 0 f x = x
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.hasForgetToCommMonCat.eq_1 : CommGrpCat.hasForgetToCommMonCat =
  {
    forget₂ :=
      { obj := fun X => CommMonCat.of ↑X, map := fun {X Y} f => CommMonCat.ofHom (CommGrpCat.Hom.hom f),
        map_id := CommGrpCat.hasForgetToCommMonCat._proof_1, map_comp := @CommGrpCat.hasForgetToCommMonCat._proof_2 },
    forget_comp := CommGrpCat.hasForgetToCommMonCat._proof_4 }
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
Filter.EventuallyEq.extDeriv : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {x : E}, ω₁ =ᶠ[nhds x] ω₂ → extDeriv ω₁ =ᶠ[nhds x] extDeriv ω₂
-- Init.Try
/-- If `merge` is `true`, it tries to compress suggestions such as
```
induction a
· grind only [= f]
· grind only [→ g]
```
as
```
induction a <;> grind only [= f, → g]
```
 -/
Lean.Try.Config.merge : Lean.Try.Config → Bool
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X),
  (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv F U).unitIso =
    TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso F U
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns an array of all keys present in the tree map in ascending  order.  -/
Std.DTreeMap.Raw.keysArray : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → Array α
-- Mathlib.LinearAlgebra.Ray
/-- Negating a nonzero vector twice produces the original vector.  -/
RayVector.instInvolutiveNeg : {M : Type u_2} → [inst : AddCommGroup M] → {R : Type u_4} → InvolutiveNeg (RayVector R M)
-- Mathlib.MeasureTheory.Measure.OpenPos
IsClosed.measure_eq_one_iff_eq_univ : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure]
  {F : Set X} [OpensMeasurableSpace X] [MeasureTheory.IsProbabilityMeasure μ], IsClosed F → (μ F = 1 ↔ F = Set.univ)
-- Mathlib.RingTheory.Etale.Locus
Algebra.isOpen_etaleLocus : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FinitePresentation R A], IsOpen (Algebra.etaleLocus R A)
-- Mathlib.Topology.MetricSpace.Bounded
Metric.hasBasis_cobounded_compl_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] (c : α),
  (Bornology.cobounded α).HasBasis (fun x => True) fun r => (Metric.closedBall c r)ᶜ
-- Init.Data.ToString.Basic
/-- Types that can be converted into a string for display.

There is no expectation that the resulting string can be parsed back to the original data (see
`Repr` for a similar class with this expectation).
 -/
ToString : Type u → Type u
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.flip_X_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (i : I₂) (j : I₁), (K.flip.X i).X j = (K.X j).X i
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whisker_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Y' : C}
  (f : Y ⟶ Y') (Z : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) Z =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z))
        (CategoryTheory.MonoidalCategoryStruct.associator X Y' Z).inv)
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
_private.Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet.0.Associates.FactorSet.prod.match_1.eq_1 : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] (motive : Associates.FactorSet α → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (s : Multiset { a // Irreducible a }) → motive (some s)),
  (match none with
    | none => h_1 ()
    | some s => h_2 s) =
    h_1 ()
-- Init.Data.Format.Basic
/-- Insert a newline and then `f`, all nested by the default indent amount.  -/
Std.Format.indentD : Std.Format → Std.Format
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.Option.elim.match_1.splitter : {α : Type u_1} →
  {β : Sort u_3} →
    (motive : Option α → β → (α → β) → Sort u_2) →
      (x : Option α) →
        (x_1 : β) →
          (x_2 : α → β) →
            ((x : α) → (x_3 : β) → (f : α → β) → motive (some x) x_3 f) →
              ((y : β) → (x : α → β) → motive none y x) → motive x x_1 x_2
-- Mathlib.Algebra.GroupWithZero.Divisibility
/-- Given two elements `b`, `c` of a cancellative `MonoidWithZero` and a nonzero element `a`,
`a*b` divides `a*c` iff `b` divides `c`.  -/
mul_dvd_mul_iff_left : ∀ {α : Type u_1} [inst : MonoidWithZero α] [IsLeftCancelMulZero α] {a b c : α}, a ≠ 0 → (a * b ∣ a * c ↔ b ∣ c)
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.map_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {K K' : ChainComplex C ℕ} (f : K ⟶ K') (Δ : SimplexCategoryᵒᵖ),
  (AlgebraicTopology.DoldKan.Γ₀.map f).app Δ =
    (AlgebraicTopology.DoldKan.Γ₀.splitting K).desc Δ fun A =>
      CategoryTheory.CategoryStruct.comp (f.f (Opposite.unop A.fst).len)
        (((AlgebraicTopology.DoldKan.Γ₀.splitting K').cofan Δ).inj A)
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_pow_atTop_nhdsWithin_zero_of_lt_one : ∀ {𝕜 : Type u_4} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [ExistsAddOfLE 𝕜] [Archimedean 𝕜]
  [inst_5 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜},
  0 < r → r < 1 → Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))
-- Batteries.Data.List.Interleave
List.interleave_perm_append : ∀ {α : Type u_1} {l₁ l₂ : List α}, (l₁.interleave l₂).Perm (l₁ ++ l₂)
-- Mathlib.Data.Stream.Init
Stream'.mem_interleave_right : ∀ {α : Type u} {a : α} {s₁ : Stream' α} (s₂ : Stream' α), a ∈ s₂ → a ∈ s₁ ⋈ s₂
-- Mathlib.Combinatorics.Hindman
/-- Additive semigroup structure on `Ultrafilter M` induced by an additive semigroup
structure on `M`.  -/
Ultrafilter.addSemigroup : {M : Type u_1} → [AddSemigroup M] → AddSemigroup (Ultrafilter M)
-- Mathlib.Data.Set.Basic
Set.inter_comm : ∀ {α : Type u} (a b : Set α), a ∩ b = b ∩ a
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_apply_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Zero M] {s : Set α} {a : α} (f : α → β → M) (b : β),
  s.indicator f a b = s.indicator (fun i => f i b) a
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_inv : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Inv F] [inst_2 : Inv β]
  [IsInvApply F α β] (f : F), ⇑f⁻¹ = (⇑f)⁻¹
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The natural group isomorphism between fixing subgroups.  -/
SubMulAction.fixingSubgroupInsertEquiv : {M : Type u_1} →
  {α : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M α] →
        (a : α) →
          (s : Set ↥(SubMulAction.ofStabilizer M a)) →
            ↥(fixingSubgroup M (insert a (Subtype.val '' s))) ≃* ↥(fixingSubgroup (↥(MulAction.stabilizer M a)) s)
-- Mathlib.Control.Random
/-- Sample a bounded element of this type from the provided generator.  -/
BoundedRandom.randomR : {m : Type u → Type u_1} →
  {α : Type u} →
    {inst : Preorder α} →
      [self : BoundedRandom m α] →
        {g : Type} → (lo hi : α) → lo ≤ hi → [RandomGen g] → RandGT g m { a // lo ≤ a ∧ a ≤ hi }
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.sup_le : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup β] {l : Filter α} {f g h : α → β},
  f ≤ᶠ[l] h → g ≤ᶠ[l] h → f ⊔ g ≤ᶠ[l] h
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.sset : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    ℕ →
      ℕ →
        Lean.FVarId →
          Lean.Expr →
            Lean.Compiler.LCNF.Code pu →
              autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_11 →
                Lean.Compiler.LCNF.Code pu
-- Mathlib.Analysis.Convex.Body
ConvexBody.coe_mk : ∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V] (s : Set V)
  (h₁ : Convex ℝ s) (h₂ : IsCompact s) (h₃ : s.Nonempty),
  ↑{ carrier := s, convex' := h₁, isCompact' := h₂, nonempty' := h₃ } = s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.keyAtIdx!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {i : ℕ}, t₁.Equiv t₂ → t₁.keyAtIdx! i = t₂.keyAtIdx! i
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.congr_fun : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] {f g : M ≃* N}, f = g → ∀ (x : M), f x = g x
-- Mathlib.Data.Rat.Cast.Defs
/-- If monoid with zero homs `f` and `g` from `ℚ≥0` agree on the naturals then they are equal.

See note [partially-applied ext lemmas] for why `comp` is used here.  -/
MonoidWithZeroHomClass.ext_nnrat : ∀ {M₀ : Type u_5} [inst : MonoidWithZero M₀] {f g : ℚ≥0 →*₀ M₀},
  f.comp (MonoidWithZeroHom.ofClass (Nat.castRingHom ℚ≥0)) = g.comp (MonoidWithZeroHom.ofClass (Nat.castRingHom ℚ≥0)) →
    f = g
-- Lean.Meta.Tactic.Simp.Main
/-- Routine for simplifying `let` expressions.

If it is a `have`, we use `simpHaveTelescope` to simplify entire telescopes at once, to avoid quadratic behavior
arising from locally nameless expression representations.

We assume that dependent `let`s are dependent,
but if `Config.letToHave` is enabled then we attempt to transform it into a `have`.
If that does not change it, then it is only `dsimp`ed.
 -/
Lean.Meta.Simp.simpLet : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Mathlib.RingTheory.Noetherian.Defs
isNoetherian_submodule_right : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M}, IsNoetherian R ↥N ↔ ∀ (s : Submodule R M), (s ⊓ N).FG
-- Lean.Meta.Basic
Lean.Meta.Cache.defEqPerm : Lean.Meta.Cache → Lean.Meta.DefEqCache
-- Mathlib.Order.Minimal
minimal_eq_iff : ∀ {α : Type u_2} {x y : α} [inst : LE α], Minimal (fun x => x = y) x ↔ x = y
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_homOfLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U V : Y.Opens) (e : U ≤ V),
  CategoryTheory.CategoryStruct.comp (f ∣_ U) (Y.homOfLE e) = CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯) (f ∣_ V)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.mapNatTrans_τ₃ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  {F G : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms]
  (τ : F ⟶ G), (S.mapNatTrans τ).τ₃ = τ.app S.X₃
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
RootPairing.GeckConstruction.isNilpotent_f : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : CharZero R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {P : RootPairing ι R M N} [inst_7 : P.IsCrystallographic] [P.IsReduced] {b : P.Base} [inst_9 : Fintype ι]
  [inst_10 : DecidableEq ι] (i : ↥b.support), IsNilpotent (RootPairing.GeckConstruction.f i)
-- Mathlib.GroupTheory.Congruence.Defs
Con.instPowQuotientNat.eq_1 : ∀ {M : Type u_4} [inst : Monoid M] (c : Con M),
  c.instPowQuotientNat = { pow := fun x n => Quotient.map' (fun x => x ^ n) ⋯ x }
-- Batteries.Data.AssocList
/-- An empty list  -/
Batteries.AssocList.nil : {α : Type u} → {β : Type v} → Batteries.AssocList α β
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.map_id : ∀ {α : Type u_1}, FreeMonoid.map id = MonoidHom.id (FreeMonoid α)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.interSnd_s₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  (F : CategoryTheory.PreOneHypercover S)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)]
  [inst_2 :
    ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
      CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
        (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))]
  {i j : (E.inter F).I₀} (k : (E.inter F).I₁ i j), (E.interSnd F).s₁ k = k.2
-- Mathlib.Analysis.Normed.Group.AddTorsor
nndist_vadd_left : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (v : V) (x : P), nndist (v +ᵥ x) x = ‖v‖₊
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- Archimedean class of the input is transferred to `HahnSeries.orderTop`.  -/
HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [IsOrderedAddMonoid R] [Archimedean R] (x : ↥(↑f).domain),
  (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (↑↑f x)).orderTop = ArchimedeanClass.mk ↑x
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.SubseqResult.suffix.sizeOf_spec : ∀ (s : Lean.Grind.AC.Seq), sizeOf (Lean.Grind.AC.SubseqResult.suffix s) = 1 + sizeOf s
-- Mathlib.Data.Num.Prime
/-- Primality predicate for a `PosNum`.  -/
PosNum.Prime : PosNum → Prop
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassPExcept_def : ∀ (L : PeriodPair) (l₀ : ↥L.lattice) (z : ℂ),
  L.weierstrassPExcept (↑l₀) z = L.weierstrassP z + (1 / ↑l₀ ^ 2 - 1 / (z - ↑l₀) ^ 2)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_finsetProd_of_notMem : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : CommMonoid β] [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) → ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.IndepFun (∏ j ∈ s, f j) (f i) μ
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` preserves limits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F : C ⥤ Dᵒᵖ` preserves
colimits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.preservesColimit_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesLimit K.op F.leftOp],
  CategoryTheory.Limits.PreservesColimit K F
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.ofClass.eq_1 : ∀ {S : Type u_3} {M : Type u_4} [inst : Monoid M] [inst_1 : SetLike S M] [inst_2 : SubmonoidClass S M] (s : S),
  Submonoid.ofClass s = { carrier := ↑s, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
/-- Make an `IntFractPair` printable.  -/
GenContFract.IntFractPair.instRepr : {K : Type u_1} → [Repr K] → Repr (GenContFract.IntFractPair K)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.chainBotCoeff_eq_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {b : P.Base}
  [inst_5 : CharZero R] [inst_6 : IsDomain R] [inst_7 : P.IsCrystallographic] [inst_8 : Finite ι] {i j : ↥b.support},
  RootPairing.chainBotCoeff ↑i ↑j = 0