mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Jacobson.Ring
/-- Used to bootstrap the more general `quotient_mk_comp_C_isIntegral_of_jacobson`  -/
_private.Mathlib.RingTheory.Jacobson.Ring.0.Polynomial.quotient_mk_comp_C_isIntegral_of_jacobson' : ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal (Polynomial R)) [hP : P.IsMaximal] [Nontrivial R],
  IsJacobsonRing R → (∀ (x : R), Polynomial.C x ∈ P → x = 0) → ((Ideal.Quotient.mk P).comp Polynomial.C).IsIntegral
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- Topology whose open sets are upper sets.

Note: In general the upper set topology does not coincide with the upper topology.  -/
Topology.upperSet : (α : Type u_4) → [Preorder α] → TopologicalSpace α
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- For any valuation `v` compatible with the valuative relation on `R`, the closed unit ball
around zero `{x | v x ≤ 1}` is clopen in the valuative topology.  -/
Valuation.isClopen_integer : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible], IsClopen ↑v.integer
-- Lean.Elab.App
/-- Information about an eliminator used by the elab-as-elim elaborator.
This is not to be confused with `Lean.Meta.ElimInfo`, which is for `induction` and `cases`.
The elab-as-elim routine is less restrictive in what counts as an eliminator, and it doesn't need
to have a strict notion of what is a "target" — all it cares about are
1. that the return type of a function is of the form `m ...` where `m` is a parameter
   (unlike `induction` and `cases` eliminators, the arguments to `m`, known as "discriminants",
   can be any expressions, not just parameters), and
2. which arguments should be eagerly elaborated, to make discriminants be as elaborated as
   possible for the expected type generalization procedure,
   and which should be postponed (since they are the "minor premises").

Note that the routine isn't doing induction/cases *on* particular expressions.
The purpose of elab-as-elim is to successfully solve the higher-order unification problem
between the return type of the function and the expected type.
 -/
Lean.Elab.Term.ElabElimInfo : Type
-- Init.Data.SInt.Basic
/-- Converts 32-bit signed integers to 64-bit signed integers that denote the same number.

This function is overridden at runtime with an efficient implementation.
 -/
Int32.toInt64 : Int32 → Int64
-- Init.Data.Nat.Fold
/-- Checks whether `f` returns `true` for every number strictly less than a bound.

Examples:
* `Nat.all 4 (fun i _ => i < 5) = true`
* `Nat.all 7 (fun i _ => i < 5) = false`
* `Nat.all 7 (fun i _ => i % 2 = 0) = false`
* `Nat.all 1 (fun i _ => i % 2 = 0) = true`
 -/
Nat.all : (n : ℕ) → ((i : ℕ) → i < n → Bool) → Bool
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.instCoeFunForallSetPresieve : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      CoeFun (CategoryTheory.Pretopology C) fun x => (X : C) → Set (CategoryTheory.Presieve X)
-- Mathlib.Analysis.Convex.Between
wbtw_vadd_const_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : V} (p : P), Wbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Wbtw R x y z
-- Mathlib.NumberTheory.Padics.RingHoms
/-- One part of the universal property of `ℤ_[p]` as a projective limit.
See also `PadicInt.lift_unique`.
 -/
PadicInt.lift_spec : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)]
  (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (n : ℕ),
  (PadicInt.toZModPow n).comp (PadicInt.lift f_compat) = f n
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
CategoryTheory.instWellFoundedLTSubobjectOfIsArtinianObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.IsArtinianObject X],
  WellFoundedLT (CategoryTheory.Subobject X)
-- Lean.Server.Completion.EligibleHeaderDecls
Lean.Server.Completion.EligibleDecl : Type
-- Mathlib.Order.Hom.Basic
/-- The bijection `ULift.{v} α ≃ α` as an isomorphism of orders.  -/
ULift.orderIso : {α : Type u} → [inst : Preorder α] → ULift.{v, u} α ≃o α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.mapArrowLeft_id : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {f₁ : CategoryTheory.Arrow C₁}
  {f₂ : CategoryTheory.Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom),
  sq₁₂.mapArrowLeft sq₁₂ (CategoryTheory.CategoryStruct.id f₁) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk sq₁₂.ι)
-- Mathlib.Order.BooleanSubalgebra
/-- The image of a Boolean subalgebra along a monoid homomorphism is a Boolean subalgebra.  -/
BooleanSubalgebra.map : {α : Type u_2} →
  {β : Type u_3} →
    [inst : BooleanAlgebra α] →
      [inst_1 : BooleanAlgebra β] → BoundedLatticeHom α β → BooleanSubalgebra α → BooleanSubalgebra β
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.hasDerivAt_sinh : ∀ (x : ℝ), HasDerivAt Real.sinh (Real.cosh x) x
-- Mathlib.Order.Hom.Basic
OrderIso.instOrderIsoClass : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β], OrderIsoClass (α ≃o β) α β
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R),
  { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm ((algebraMap R K) r)) } ∈
    IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Polynomial.Chebyshev.sumZeroes_T_zero : ∀ {n : ℕ}, n ≠ 0 → Polynomial.Chebyshev.sumZeroes n (Polynomial.Chebyshev.T ℝ 0) = Real.pi
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
sInf_ne_of_notMem : ∀ {α : Type u_5} [inst : CompleteLinearOrder α] {s : Set α}, s.Finite → ∀ {a : α}, a ≠ ⊤ → a ∉ s → sInf s ≠ a
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.isIso_leftHomologyMap'_of_isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [CategoryTheory.IsIso φ] (h₁ : S₁.LeftHomologyData)
  (h₂ : S₂.LeftHomologyData), CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂)
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.shiftFunctor₁XXIso_refl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (a b x : ℤ),
  K.shiftFunctor₁XXIso a x (a + x) ⋯ b =
    CategoryTheory.Iso.refl ((((HomologicalComplex₂.shiftFunctor₁ C x).obj K).X a).X b)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_inter_eq_size_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∈ t₂) → (t₁ ∩ t₂).size = t₁.size
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.instCoeSortMatType : (R : Type u) → CoeSort (CategoryTheory.Mat R) (Type u)
-- Mathlib.Algebra.Ring.Commute
Commute.neg_right : ∀ {R : Type u} [inst : Mul R] [inst_1 : HasDistribNeg R] {a b : R}, Commute a b → Commute a (-b)
-- Mathlib.Algebra.Ring.NegOnePow
Int.negOnePow_even : ∀ (n : ℤ), Even n → n.negOnePow = 1
-- Mathlib.Order.Hom.Lattice
/-- `Subtype.val` as an `InfHom`.  -/
InfHom.subtypeVal : {β : Type u_3} →
  [inst : SemilatticeInf β] → {P : β → Prop} → (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)) → InfHom { x // P x } β
-- Lean.Elab.Tactic.Simp
/-- Configuration for `dsimp`, for supporting tactic configuration option syntax.
 -/
Lean.Meta.DSimp.ConfigWithOptions : Type
-- Mathlib.Order.Hom.Basic
/-- A strictly monotone map from a linear order is an order embedding.  -/
OrderEmbedding.ofStrictMono : {α : Type u_6} → {β : Type u_7} → [inst : LinearOrder α] → [inst_1 : Preorder β] → (f : α → β) → StrictMono f → α ↪o β
-- Mathlib.Order.RelSeries
SetRel.FiniteDimensional.mk : ∀ {α : Type u_1} {r : SetRel α α}, (∃ x, ∀ (y : RelSeries r), y.length ≤ x.length) → r.FiniteDimensional
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The span of a set of points in a projective space is defined inductively to be the set of points
which contains the original set, and contains all points determined by the (nonzero) sum of two
nonzero vectors, each of which determine points in the span.  -/
Projectivization.Subspace.spanCarrier : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → Set (Projectivization K V) → Set (Projectivization K V)
-- Mathlib.Combinatorics.Enumerative.Composition
/-- **Alias** of the reverse direction of `Composition.length_pos_iff`. -/
Composition.length_pos_of_pos : ∀ {n : ℕ} (c : Composition n), 0 < n → 0 < c.length
-- Mathlib.Logic.Nonempty
nonempty_sum : ∀ {α : Type u_1} {β : Type u_2}, Nonempty (α ⊕ β) ↔ Nonempty α ∨ Nonempty β
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- The categorical binary product of type-valued functors is `prod F G`.  -/
CategoryTheory.FunctorToTypes.binaryProductIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F G : CategoryTheory.Functor C (Type w)) → F ⨯ G ≅ CategoryTheory.FunctorToTypes.prod F G
-- Mathlib.CategoryTheory.Galois.Decomposition
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.has_decomp_connected_components_aux : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (n : ℕ) (X : C),
  n = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), CategoryTheory.PreGaloisCategory.IsConnected (f i)) ∧ Finite ι
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- **Alias** of `Left.mul_lt_mul_of_nonneg`.

---

Assumes left strict covariance.  -/
mul_lt_mul_of_nonneg : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b c d : α} [inst_1 : Preorder α] [PosMulStrictMono α] [MulPosMono α],
  a < b → c < d → 0 ≤ a → 0 ≤ c → a * c < b * d
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.IsCyclicallyReduced.flatten_replicate : ∀ {α : Type u} {L : List (α × Bool)},
  FreeGroup.IsCyclicallyReduced L → ∀ (n : ℕ), FreeGroup.IsCyclicallyReduced (List.replicate n L).flatten
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.weakLimit.w : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasWeakLimit F] {j j' : J} (f : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakLimit.π F j) (F.map f) =
    CategoryTheory.Limits.weakLimit.π F j'
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.toList.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Batteries.AssocList α β → Sort u_3)
  (h_1 : Unit → motive Batteries.AssocList.nil)
  (h_2 : (a : α) → (b : β) → (es : Batteries.AssocList α β) → motive (Batteries.AssocList.cons a b es)),
  (match Batteries.AssocList.nil with
    | Batteries.AssocList.nil => h_1 ()
    | Batteries.AssocList.cons a b es => h_2 a b es) =
    h_1 ()
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edge_other_ne : ∀ {V : Type u} (G : SimpleGraph V) {e : Sym2 V}, e ∈ G.edgeSet → ∀ {v : V} (h : v ∈ e), Sym2.Mem.other h ≠ v
-- Aesop.RuleSet.Member
Aesop.LocalRuleSetMember.global.injEq : ∀ (m m_1 : Aesop.GlobalRuleSetMember),
  (Aesop.LocalRuleSetMember.global m = Aesop.LocalRuleSetMember.global m_1) = (m = m_1)
-- Mathlib.Order.Disjoint
Disjoint.of_disjoint_inf_of_le : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b c : α}, Disjoint (a ⊓ b) c → a ≤ c → Disjoint a b
-- Mathlib.Data.Matrix.Mul
Matrix.mul_smul : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : AddCommMonoid α] [inst_1 : Mul α]
  [inst_2 : Fintype n] [inst_3 : Monoid R] [inst_4 : DistribMulAction R α] [SMulCommClass R α α] (M : Matrix m n α)
  (a : R) (N : Matrix n l α), M * a • N = a • (M * N)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.tail_nil : ∀ {α : Type u}, Stream'.WSeq.nil.tail = Stream'.WSeq.nil
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
IicProdIoc_preimage : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : DecidableLE ι] {X : ι → Type u_2}
  [inst_3 : LocallyFiniteOrderBot ι] {a b : ι} (hab : a ≤ b) (s : (i : ↥(Finset.Iic b)) → Set (X ↑i)),
  IicProdIoc a b ⁻¹' Set.univ.pi s = Set.univ.pi (Preorder.frestrictLe₂ hab s) ×ˢ Set.univ.pi (Finset.restrict₂ ⋯ s)
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.x_mul_y_mul_z_eq_u_mul_w_cube : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  FermatLastTheoremForThreeGen.Solution.x✝ S * FermatLastTheoremForThreeGen.Solution.y✝ S *
      FermatLastTheoremForThreeGen.Solution.z✝ S =
    ↑(FermatLastTheoremForThreeGen.Solution'.u✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S)) *
      FermatLastTheoremForThreeGen.Solution.w✝ S ^ 3
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.QuotientMeasureEqMeasurePreimage.projection_respects_measure' : ∀ {G : Type u_1} {α : Type u_3} {inst : Group G} {inst_1 : MulAction G α} {inst_2 : MeasurableSpace α}
  {ν : autoParam (MeasureTheory.Measure α) MeasureTheory.QuotientMeasureEqMeasurePreimage._auto_1}
  {μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))}
  [self : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ] (t : Set α),
  MeasureTheory.IsFundamentalDomain G t ν →
    μ = MeasureTheory.Measure.map (Quotient.mk (MulAction.orbitRel G α)) (ν.restrict t)
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.SimpCongrTheorem.hypothesesPos : Lean.Meta.SimpCongrTheorem → Array ℕ
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.fundamentalSequence.match_1.eq_1 : ∀ (motive : Option ONote ⊕ (ℕ → ONote) → ℕ → Sort u_1) (h_1 : Unit → motive (Sum.inl none) 0)
  (h_2 : (m : ℕ) → motive (Sum.inl none) m.succ) (h_3 : (a' : ONote) → motive (Sum.inl (some a')) 0)
  (h_4 : (a' : ONote) → (m : ℕ) → motive (Sum.inl (some a')) m.succ) (h_5 : (f : ℕ → ONote) → motive (Sum.inr f) 0)
  (h_6 : (f : ℕ → ONote) → (m : ℕ) → motive (Sum.inr f) m.succ),
  (match Sum.inl none, 0 with
    | Sum.inl none, 0 => h_1 ()
    | Sum.inl none, m.succ => h_2 m
    | Sum.inl (some a'), 0 => h_3 a'
    | Sum.inl (some a'), m.succ => h_4 a' m
    | Sum.inr f, 0 => h_5 f
    | Sum.inr f, m.succ => h_6 f m) =
    h_1 ()
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.leftInvOn : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), Set.LeftInvOn (↑e.symm) (↑e) e.source
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.archimedeanClassOrderIso_apply : ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  (a : ArchimedeanClass M),
  (DivisibleHull.archimedeanClassOrderIso M) a = (ArchimedeanClass.orderHom (DivisibleHull.coeOrderAddMonoidHom M)) a
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.fromNormalizedChainComplex_toNormalizedChainComplex_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) {Z : ChainComplex C ℕ}
  (h : X.normalizedChainComplex R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.fromNormalizedChainComplex R)
      (CategoryTheory.CategoryStruct.comp (X.toNormalizedChainComplex R) h) =
    h
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateAddSubgroup.nsmul_inter_nsmul : ∀ {G : Type u_1} [inst : AddGroup G] {A B : Set G} {K L : ℝ} {m n : ℕ},
  IsApproximateAddSubgroup K A →
    IsApproximateAddSubgroup L B →
      2 ≤ m → 2 ≤ n → IsApproximateAddSubgroup (K ^ (2 * m - 1) * L ^ (2 * n - 1)) (m • A ∩ n • B)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The cokernel of `biproduct.ι f i` is `⨁ Subtype.restrict {i}ᶜ f`.  -/
CategoryTheory.Limits.cokernelBiproductιIso : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : J → C) →
          (i : J) →
            [inst_2 : CategoryTheory.Limits.HasBiproduct f] →
              [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun j => j ≠ i) f)] →
                CategoryTheory.Limits.cokernel (CategoryTheory.Limits.biproduct.ι f i) ≅
                  ⨁ Subtype.restrict (fun j => j ≠ i) f
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mulPow.eq_def : ∀ (pw : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.mulPow pw m =
    match m with
    | Lean.Grind.CommRing.Mon.unit => Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit
    | Lean.Grind.CommRing.Mon.mult pw' m =>
      bif pw.varLt pw' then Lean.Grind.CommRing.Mon.mult pw (Lean.Grind.CommRing.Mon.mult pw' m)
      else
        bif pw'.varLt pw then Lean.Grind.CommRing.Mon.mult pw' (Lean.Grind.CommRing.Mon.mulPow pw m)
        else Lean.Grind.CommRing.Mon.mult { x := pw.x, k := pw.k + pw'.k } m
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
/-- Given a pair of morphisms `p`, `q` to `X` which factor through `f`, they factor through any kernel
pair of `f`.
 -/
CategoryTheory.IsKernelPair.lift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R X Y : C} →
      {f : X ⟶ Y} →
        {a b : R ⟶ X} →
          {S : C} →
            CategoryTheory.IsKernelPair f a b →
              (p q : S ⟶ X) → CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp q f → (S ⟶ R)
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.inf_assoc : ∀ {α : Type u_1} [inst : BooleanRing α] (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
-- Mathlib.Data.Int.Cast.Prod
Prod.instAddGroupWithOne : {α : Type u_1} → {β : Type u_2} → [AddGroupWithOne α] → [AddGroupWithOne β] → AddGroupWithOne (α × β)
-- Mathlib.Algebra.Group.ULift
AddEquiv.ulift.eq_1 : ∀ {α : Type u} [inst : Add α], AddEquiv.ulift = { toEquiv := Equiv.ulift, map_add' := ⋯ }
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.isNum? : Nat.Internal.Linear.Poly → Option ℕ
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.touchpoint_injective : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs → Function.Injective (s.touchpoint signs)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} {inst : CommSemiring R} {inst_1 : StarRing R}
  {inst_2 : MetricSpace R} {inst_3 : IsTopologicalSemiring R} {inst_4 : ContinuousStar R} {inst_5 : Ring A}
  {inst_6 : StarRing A} {inst_7 : MetricSpace A} {inst_8 : Algebra R A}
  [self : IsometricContinuousFunctionalCalculus R A p], ContinuousFunctionalCalculus R A p
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.insertMin.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Sort u_3) →
      (t : Std.DTreeMap.Internal.Impl α β) →
        (hr : t.Balanced) →
          ((hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hr) →
            ((sz : ℕ) →
                (k' : α) →
                  (v' : β k') →
                    (l' r' : Std.DTreeMap.Internal.Impl α β) →
                      (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) →
                        motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr) →
              motive t hr
-- Mathlib.Order.Filter.Tendsto
/-- **Alias** of the reverse direction of `Filter.map_mapsTo_Iic_iff_tendsto`. -/
Filter.Tendsto.map_mapsTo_Iic : ∀ {α : Type u_1} {β : Type u_2} {F : Filter α} {G : Filter β} {m : α → β},
  Filter.Tendsto m F G → Set.MapsTo (Filter.map m) (Set.Iic F) (Set.Iic G)
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel.eq_1 : ∀ (G : Type u_1) (α : Type u_2) [inst : AddGroup G] [inst_1 : AddAction G α],
  AddAction.orbitRel G α = { r := fun a b => a ∈ AddAction.orbit G b, iseqv := ⋯ }
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.isMulRightInvariant_smul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] {μ : MeasureTheory.Measure G} [μ.IsMulRightInvariant]
  (c : ENNReal), (c • μ).IsMulRightInvariant
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
/-- Inverse of the `exp` function. Returns values such that `(log x).im > - π` and `(log x).im ≤ π`.
`log 0 = 0`  -/
Complex.log : ℂ → ℂ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β},
  Std.DHashMap.Const.getD (m₁.union m₂) k fallback =
    Std.DHashMap.Const.getD m₂ k (Std.DHashMap.Const.getD m₁ k fallback)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.fold_filterMap : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {ps : Std.Do.PostShape} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Std.Do.WPMonad m ps]
  [inst_5 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {f : β → Option γ} {g : δ → γ → δ} {init : δ}
  {it : Std.IterM m β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.IterM.fold
        (fun d b =>
          match f b with
          | some c => g d c
          | x => d)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.fold g init (Std.IterM.filterMap f it) ⦃Q⦄
-- Init.Data.String.Iterator
_private.Init.Data.String.Iterator.0.String.Legacy.Iterator.remainingBytes.match_1.eq_1 : ∀ (motive : String.Legacy.Iterator → Sort u_1) (s : String) (i : String.Pos.Raw)
  (h_1 : (s : String) → (i : String.Pos.Raw) → motive { s := s, i := i }),
  (match { s := s, i := i } with
    | { s := s, i := i } => h_1 s i) =
    h_1 s i
-- Mathlib.RingTheory.Ideal.Colon
Submodule.colon_eq_top_iff_subset : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Submodule R M}
  (S : Set M), N.colon S = ⊤ ↔ S ⊆ ↑N
-- Mathlib.Analysis.RCLike.Basic
RCLike.nonpos_iff : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, z ≤ 0 ↔ RCLike.re z ≤ 0 ∧ RCLike.im z = 0
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.degree.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (f : LaurentPolynomial R), f.degree = f.coeff.support.max
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- A hypergraph is trivial if it has at least one vertex but no edges.  -/
Hypergraph.IsTrivial : {α : Type u_1} → Hypergraph α → Prop
-- Mathlib.Topology.UniformSpace.UniformEmbedding
_private.Mathlib.Topology.UniformSpace.UniformEmbedding.0.termψ : Lean.ParserDescr
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addRightCancelSemigroup : {I : Type u} → {f : I → Type v₁} → [(i : I) → AddRightCancelSemigroup (f i)] → AddRightCancelSemigroup ((i : I) → f i)
-- Init.Data.Vector.MapIdx
Vector.getElem?_mapFinIdx : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : (i : ℕ) → α → i < n → β} {i : ℕ},
  (xs.mapFinIdx f)[i]? = xs[i]?.pbind fun b h => some (f i b ⋯)