mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.addVal_def : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (r : R) (u : Rˣ)
  {ϖ : R}, Irreducible ϖ → ∀ (n : ℕ), r = ↑u * ϖ ^ n → (IsDiscreteValuationRing.addVal R) r = ↑n
-- Mathlib.Topology.Separation.Hausdorff
T2Quotient.lift.congr_simp : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : T2Space Y]
  {f f_1 : X → Y} (e_f : f = f_1) (hf : Continuous f) (a a_1 : T2Quotient X),
  a = a_1 → T2Quotient.lift hf a = T2Quotient.lift ⋯ a_1
-- Mathlib.Order.Hom.Basic
map_inv_lt_iff : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : EquivLike F α β]
  [OrderIsoClass F α β] (f : F) {a : α} {b : β}, EquivLike.inv f b < a ↔ b < f a
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffAt.div₀ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : GroupWithZero G] [ContMDiffInv₀ I n G]
  [ContMDiffMul I n G] {E' : Type u_5} [inst_9 : NormedAddCommGroup E'] [inst_10 : NormedSpace 𝕜 E'] {H' : Type u_6}
  [inst_11 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] {f g : M → G} {a : M},
  ContMDiffAt I' I n f a → ContMDiffAt I' I n g a → g a ≠ 0 → ContMDiffAt I' I n (f / g) a
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.List.head?_dropWhile_not.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match none with
    | some x => h_1 x
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- Taking the sum under `h` is an additive homomorphism of finsupps,if `h` is an additive
homomorphism. This is a more specific version of `Finsupp.sum_add_index` with simpler
hypotheses.  -/
Finsupp.sum_add_index' : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] {f g : α →₀ M}
  {h : α → M → N},
  (∀ (a : α), h a 0 = 0) → (∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) → (f + g).sum h = f.sum h + g.sum h
-- Init.Data.Int.DivMod.Lemmas
Int.one_bmod_two : Int.bmod 1 2 = -1
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.mk_coe : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (f : L →ₗ[R] M) (h₁ : ∀ (a b : L), f ⁅a, b⁆ = ⁅a, f b⁆ - ⁅b, f a⁆), ⇑{ toLinearMap := f, leibniz' := h₁ } = ⇑f
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.mul_subset_iff_left : ∀ {α : Type u_2} [inst : Mul α] [inst_1 : DecidableEq α] {s t u : Finset α}, s * t ⊆ u ↔ ∀ a ∈ s, a • t ⊆ u
-- Mathlib.Algebra.Lie.TensorProduct
TensorProduct.LieModule.mapIncl_def : ∀ {R : Type u} [inst : CommRing R] {L : Type v} {M : Type w} {N : Type w₁} [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N] (M' : LieSubmodule R L M) (N' : LieSubmodule R L N),
  TensorProduct.LieModule.mapIncl M' N' = TensorProduct.LieModule.map M'.incl N'.incl
-- Mathlib.Analysis.Convex.Basic
Convex.add_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E},
  Convex 𝕜 s → ∀ {p q : 𝕜}, 0 ≤ p → 0 ≤ q → (p + q) • s = p • s + q • s
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.fst_inv_eq_snd_inv : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [Quiver.IsThin J] {i j : J}
  (k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)) {U : (F.obj i).Opens}
  (h₁ : AlgebraicGeometry.Scheme.Hom.opensRange (F.map k₁.snd.1) ≤ U)
  (h₂ : AlgebraicGeometry.Scheme.Hom.opensRange (F.map k₂.snd.1) ≤ U),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoOpensRange (F.map k₁.snd.1)).inv
        (F.map k₁.snd.2)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoOpensRange (F.map k₂.snd.1)).inv
        (F.map k₂.snd.2))
-- Aesop.Stats.File
Aesop.StatsFileRecord.mk.injEq : ∀ (toStats : Aesop.Stats) («syntax» file : String) (position : Option Lean.Position) (declaration : Option Lean.Name)
  (goalSolved : Bool) (toStats_1 : Aesop.Stats) (syntax_1 file_1 : String) (position_1 : Option Lean.Position)
  (declaration_1 : Option Lean.Name) (goalSolved_1 : Bool),
  ({ toStats := toStats, «syntax» := «syntax», file := file, position := position, declaration := declaration,
        goalSolved := goalSolved } =
      { toStats := toStats_1, «syntax» := syntax_1, file := file_1, position := position_1,
        declaration := declaration_1, goalSolved := goalSolved_1 }) =
    (toStats = toStats_1 ∧
      «syntax» = syntax_1 ∧
        file = file_1 ∧ position = position_1 ∧ declaration = declaration_1 ∧ goalSolved = goalSolved_1)
-- Lean.Elab.BuiltinNotation
_private.Lean.Elab.BuiltinNotation.0.Lean.Elab.Term.mkMPairs.loop : Array Lean.Term → ℕ → Lean.Term → Lean.MacroM Lean.Term
-- Mathlib.Tactic.Abel
/-- Configuration for `abel_nf`.  -/
Mathlib.Tactic.Abel.AbelNF.Config : Type
-- Mathlib.Data.Fintype.Sort
finSumEquivOfFinset_inl : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] [inst_2 : LinearOrder α] {m n : ℕ} {s : Finset α}
  (hm : s.card = m) (hn : sᶜ.card = n) (i : Fin m), (finSumEquivOfFinset hm hn) (Sum.inl i) = (s.orderEmbOfFin hm) i
-- Mathlib.Data.Vector3
Vector3.cons_head_tail : ∀ {α : Type u_1} {n : ℕ} (v : Vector3 α (n + 1)), Vector3.cons v.head v.tail = v
-- Mathlib.Data.Complex.Basic
Complex.addCommGroup : AddCommGroup ℂ
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.IntegrableOn.comp_neg : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : AddGroup G] [MeasurableNeg G] [μ.IsNegInvariant] {f : G → F} {s : Set G},
  MeasureTheory.IntegrableOn f s μ → MeasureTheory.IntegrableOn (fun x => f (-x)) (-s) μ
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonian.supportGetEquiv_symm_apply_val : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b} (hp : p.IsHamiltonian) (a_1 : α),
  ↑(hp.supportGetEquiv.symm a_1) = List.idxOf a_1 p.support
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_hom_inv_id : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantFrom i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (i₀ ⟶ i)),
  CategoryTheory.CategoryStruct.comp (F.map φ) (h.isoMap φ hφ).inv = CategoryTheory.CategoryStruct.id (F.obj i)
-- Mathlib.Algebra.Algebra.Unitization
NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom.congr_simp : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B]
  [inst_9 : StarHomClass F A B] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Std.Internal.Do.WP.Basic
/-- Soundness for `Option`: if `wp prog P` holds, then `P` holds of the result.  -/
Std.Internal.Do.Option.of_wp_eq : ∀ {α : Type u} {x prog : Option α},
  prog = x → ∀ (P : Option α → Prop), Std.Internal.Do.wp prog (fun a => P (some a)) (P none) → P x
-- Mathlib.Algebra.Field.TransferInstance
/-- Transfer `NNRatCast` across an `Equiv`  -/
Equiv.nnratCast : {α : Type u_1} → {β : Type u_2} → α ≃ β → [NNRatCast β] → NNRatCast α
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.copy_comp_apply_prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  (a : α) {s t : Set β},
  MeasurableSet s → MeasurableSet t → (((ProbabilityTheory.Kernel.copy β).comp κ) a) (s ×ˢ t) = (κ a) (s ∩ t)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- The data of local generators of a sheaf of modules is finite type if
each family of generators is finite type.  -/
SheafOfModules.LocalGeneratorsData.IsFiniteType : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        {M : SheafOfModules R} →
          [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
            [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] → M.LocalGeneratorsData → Prop
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.Hom.ext_iff : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} {a b : F.Grothendieck}
  (f g : a ⟶ b),
  f = g ↔ ∃ (hfg : f.base = g.base), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f.fiber = g.fiber
-- Batteries.Data.UInt
UInt16.toUInt8_toNat : ∀ (x : UInt16), x.toUInt8.toNat = x.toNat % 2 ^ 8
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.CC_comp_zero : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2)
  (y : LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ℤ),
  (Profinite.NobelingProof.Linear_CC' C hsC ho) ((Profinite.NobelingProof.πs C o) y) = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` reflects limits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F.rightOp : C ⥤ Dᵒᵖ` reflects
colimits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.reflectsColimit_rightOp : ∀ {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.ReflectsLimit K.op F],
  CategoryTheory.Limits.ReflectsColimit K F.rightOp
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_inter!_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₁ = false →
          Std.DTreeMap.Internal.Impl.Const.get! (m₁.inter! m₂) k = default
-- Mathlib.Data.Multiset.ZeroCons
Multiset.rel_flip_eq : ∀ {α : Type u_1} {s t : Multiset α}, Multiset.Rel (fun a b => b = a) s t ↔ s = t
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndep.meas_biInter : ∀ {Ω : Type u_1} {ι : Type u_2} {m : ι → MeasurableSpace Ω} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {S : Finset ι} {s : ι → Set Ω},
  ProbabilityTheory.iIndep m μ → (∀ i ∈ S, MeasurableSet (s i)) → μ (⋂ i ∈ S, s i) = ∏ i ∈ S, μ (s i)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.edgeSet.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.edgeSet = {e | e ∈ p.edges}
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.mk_map_le : ∀ {X : SSet} {n m : ℕ} (x : X.obj (Opposite.op { len := n })) (f : { len := m } ⟶ { len := n }),
  { dim := m, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) x } ≤ { dim := n, simplex := x }
-- Init.Data.Nat.Gcd
Nat.gcd_dvd_left : ∀ (m n : ℕ), m.gcd n ∣ m
-- Mathlib.Analysis.Normed.Module.Bases
/-- The basis constant for unconditional bases (supremum over all finite sets) as `nnnorm`.
It requires completeness to guarantee that the supremum is finite,
see lemma `bddAbove_range_nnnorm_proj` below.  -/
UnconditionalSchauderBasis.nnnormProjBound : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {X : Type u_2} →
      [inst_1 : NormedAddCommGroup X] →
        [inst_2 : NormedSpace 𝕜 X] → {β : Type u_3} → UnconditionalSchauderBasis β 𝕜 X → NNReal
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.exists_of_le_one : ∀ {R : Type u} {Γ₀ : Type v} [inst : CommRing R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O R],
  v.Integers O → ∀ ⦃r : R⦄, v r ≤ 1 → ∃ x, (algebraMap O R) x = r
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  (S : J.MayerVietorisSquare),
  S.shortComplex.g =
    CategoryTheory.Limits.biprod.desc
      ((CategoryTheory.presheafToSheaf J AddCommGrpCat).map
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.yoneda.map S.f₂₄) AddCommGrpCat.free))
      ((CategoryTheory.presheafToSheaf J AddCommGrpCat).map
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.yoneda.map S.f₃₄) AddCommGrpCat.free))
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev?_eq_some_prev : ∀ {s : String} {p : s.Pos} (h : p ≠ s.startPos), p.prev? = some (p.prev h)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.stdPart_omega : ArchimedeanClass.stdPart Hyperreal.omega = 0
-- Std.Data.String.ToNat
String.Slice.toNat?_eq_none : ∀ {s : String.Slice}, s.isNat = false → s.toNat? = none
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_eq_zero : ∀ {p : ℝ}, ENNReal.ofReal p = 0 ↔ p ≤ 0
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- This mathematically trivial result is complementary to `norm_eq_one` below.  -/
IsPrimitiveRoot.norm_eq_neg_one_pow : ∀ {K : Type u} {L : Type v} [inst : CommRing L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L],
  IsPrimitiveRoot ζ 2 → ∀ [IsDomain L], (Algebra.norm K) ζ = (-1) ^ Module.finrank K L
-- Mathlib.Topology.Order.LawsonTopology
Topology.WithLawson.ofLawson_inj : ∀ {α : Type u_1} {a b : Topology.WithLawson α}, Topology.WithLawson.ofLawson a = Topology.WithLawson.ofLawson b ↔ a = b
-- Lean.Elab.Tactic.Basic
/-- Runs `x` with only the first unsolved goal as the goal.
Fails if there are no goal to be solved.
 -/
Lean.Elab.Tactic.focus : {α : Type} → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.TacticM α
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.biUnionIndex_le : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) (J : BoxIntegral.Box ι), π.biUnionIndex πi J ≤ I
-- Mathlib.Computability.AkraBazzi.AkraBazzi
AkraBazziRecurrence.mk.congr_simp : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
  (n₀ n₀_1 : ℕ) (e_n₀ : n₀ = n₀_1) (n₀_gt_zero : 0 < n₀) (a_pos : ∀ (i : α), 0 < a i) (b_pos : ∀ (i : α), 0 < b i)
  (b_lt_one : ∀ (i : α), b i < 1) (g_nonneg : ∀ x ≥ 0, 0 ≤ g x) (g_grows_poly : AkraBazziRecurrence.GrowsPolynomially g)
  (h_rec : ∀ (n : ℕ), n₀ ≤ n → T n = ∑ i, a i * T (r i n) + g ↑n) (T_gt_zero' : ∀ n < n₀, 0 < T n)
  (r_lt_n : ∀ (i : α) (n : ℕ), n₀ ≤ n → r i n < n)
  (dist_r_b : ∀ (i : α), (fun n => ↑(r i n) - b i * ↑n) =o[Filter.atTop] fun n => ↑n / Real.log ↑n ^ 2),
  { n₀ := n₀, n₀_gt_zero := n₀_gt_zero, a_pos := a_pos, b_pos := b_pos, b_lt_one := b_lt_one, g_nonneg := g_nonneg,
      g_grows_poly := g_grows_poly, h_rec := h_rec, T_gt_zero' := T_gt_zero', r_lt_n := r_lt_n, dist_r_b := dist_r_b } =
    { n₀ := n₀_1, n₀_gt_zero := ⋯, a_pos := a_pos, b_pos := b_pos, b_lt_one := b_lt_one, g_nonneg := g_nonneg,
      g_grows_poly := g_grows_poly, h_rec := ⋯, T_gt_zero' := ⋯, r_lt_n := ⋯, dist_r_b := dist_r_b }
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalSubalgebra.starClosure_le : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : IsScalarTower R A A]
  [inst_7 : SMulCommClass R A A] {S₁ : NonUnitalSubalgebra R A} {S₂ : NonUnitalStarSubalgebra R A},
  S₁ ≤ S₂.toNonUnitalSubalgebra → S₁.starClosure ≤ S₂
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapFst.eq_1 : ∀ {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] {A' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'}
  {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'}
  (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R'),
  CategoryTheory.Comma.mapFst α β =
    CategoryTheory.NatIso.ofComponents
      (fun x => CategoryTheory.Iso.refl (((CategoryTheory.Comma.map α β).comp (CategoryTheory.Comma.fst L' R')).obj x))
      ⋯
-- Mathlib.Computability.Partrec
Partrec.bind_decode₂_iff : ∀ {α : Type u_1} {σ : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α →. σ},
  Partrec f ↔ Nat.Partrec fun n => (↑(Encodable.decode₂ α n)).bind fun a => Part.map Encodable.encode (f a)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.nodup_toList : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxo.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] {a b : α}, (a<...b).toList.Nodup
-- Lean.Parser.Extra
Lean.Parser.identWithPartialTrailingDot.formatter : Lean.PrettyPrinter.Formatter
-- Init.Control.Lawful.Instances
EStateM.instLawfulMonad : ∀ {ε σ : Type u_1}, LawfulMonad (EStateM ε σ)
-- Aesop.Tree.Data
Aesop.GoalState.isUnprovable : Aesop.GoalState → Bool
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `One` across an `Equiv`  -/
Equiv.one : {α : Type u_2} → {β : Type u_3} → α ≃ β → [One β] → One α
-- Aesop.Main
_private.Aesop.Main.0.Aesop.evalAesop.go : Lean.Syntax → Lean.MVarId → StateRefT' IO.RealWorld Aesop.Stats Lean.Elab.Tactic.TacticM Bool
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.categoryParser.parenthesizer : Lean.Name → ℕ → Lean.PrettyPrinter.Parenthesizer
-- Init.Data.List.Pairwise
List.Pairwise.rel_of_mem_append : ∀ {α : Type u_1} {R : α → α → Prop} {x y : α} {l₁ l₂ : List α}, List.Pairwise R (l₁ ++ l₂) → x ∈ l₁ → y ∈ l₂ → R x y
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.filter_key_equiv_self_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {f : α → Bool},
  (Std.DTreeMap.filter (fun k x => f k) t).Equiv t ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) = true
-- Mathlib.Algebra.Exact.Basic
/-- Given an exact sequence `0 → M → N → P`, giving a section `P → N` is equivalent to giving a
splitting `N ≃ M × P`.  -/
Function.Exact.splitSurjectiveEquiv : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      {P : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : AddCommGroup P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      {f : M →ₗ[R] N} →
                        {g : N →ₗ[R] P} →
                          Function.Exact ⇑f ⇑g →
                            Function.Injective ⇑f →
                              { l // g ∘ₗ l = LinearMap.id } ≃
                                { e // f = ↑e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ ↑e }
-- Batteries.Recycling.RBTree.Basic
RBTree.RBMap.instCoeHeadKeysList : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → CoeHead (RBTree.RBMap.Keys α β cmp) (List α)
-- Mathlib.Data.Finsupp.Basic
Finsupp.split.eq_1 : ∀ {ι : Type u_4} {M : Type u_5} {αs : ι → Type u_12} [inst : Zero M] (l : (i : ι) × αs i →₀ M) (i : ι),
  l.split i = Finsupp.comapDomain (Sigma.mk i) l ⋯
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftEquiv'_counitIso : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] (i j : A) (h : i + j = 0),
  (CategoryTheory.shiftEquiv' C i j h).counitIso = CategoryTheory.shiftFunctorCompIsoId C j i ⋯
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.Candidate.appStx : Lean.Server.FileWorker.SignatureHelp.Candidate → Lean.Syntax
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumInl_injective : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language}, FirstOrder.Language.LHom.sumInl.Injective
-- Init.Data.Slice.List.Lemmas
ListSlice.toList_mkSlice_rio : ∀ {α : Type u_1} {xs : ListSlice α} {hi : ℕ},
  Std.Slice.toList (Std.Rio.Sliceable.mkSlice xs *...hi) = List.take hi (Std.Slice.toList xs)
-- Init.Data.String.Decode
UInt8.utf8ByteSize.fun_cases_unfolding : ∀ (c : UInt8) (_h : c.IsUTF8FirstByte) (motive : ℕ → Prop),
  (c &&& 128 = 0 → motive 1) →
    (¬c &&& 128 = 0 → c &&& 224 = 192 → motive 2) →
      (¬c &&& 128 = 0 → ¬c &&& 224 = 192 → c &&& 240 = 224 → motive 3) →
        (¬c &&& 128 = 0 → ¬c &&& 224 = 192 → ¬c &&& 240 = 224 → motive 4) → motive (c.utf8ByteSize _h)
-- Init.Data.UInt.Lemmas
UInt16.neg_inj : ∀ {a b : UInt16}, -a = -b ↔ a = b
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (i : D.J),
  CategoryTheory.CategoryStruct.comp
      (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)
      D.isoCarrier.inv =
    (D.ι i).base
-- Mathlib.Computability.Language
/-- Terminal symbols (of the same type as the language)  -/
Symbol.terminal : {T : Type u_4} → {N : Type u_5} → T → Symbol T N
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.brecOn.eq : ∀ {motive : Turing.ToPartrec.Cont → Sort u} (t : Turing.ToPartrec.Cont)
  (F_1 : (t : Turing.ToPartrec.Cont) → Turing.ToPartrec.Cont.below t → motive t),
  Turing.ToPartrec.Cont.brecOn t F_1 = F_1 t (Turing.ToPartrec.Cont.brecOn.go t F_1).2
-- Mathlib.RingTheory.Polynomial.Basic
/-- If `I` is an ideal, and `pᵢ` is a finite family of polynomials each satisfying
`∀ k, (pᵢ)ₖ ∈ Iⁿⁱ⁻ᵏ` for some `nᵢ`, then `p = ∏ pᵢ` also satisfies `∀ k, pₖ ∈ Iⁿ⁻ᵏ` with `n = ∑ nᵢ`.
 -/
Polynomial.coeff_prod_mem_ideal_pow_tsub : ∀ {R : Type u} [inst : CommSemiring R] {ι : Type u_2} (s : Finset ι) (f : ι → Polynomial R) (I : Ideal R) (n : ι → ℕ),
  (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.functor_obj : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) (i : I),
  (CategoryTheory.Discrete.functor F).obj { as := i } = F i
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imI_one : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Zero R] [inst_1 : One R], QuaternionAlgebra.imI 1 = 0