mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.le_unzeroD_iff : ∀ {α : Type u_1} [inst : LE α] {x : WithZero α} {a b : α}, x ≠ 0 → (b ≤ WithZero.unzeroD a x ↔ ↑b ≤ x)
-- Mathlib.Computability.RegularExpressions
RegularExpression.zero : {α : Type u} → RegularExpression α
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.sizeUpTo_length : ∀ {n : ℕ} (c : Composition n), c.sizeUpTo c.length = n
-- Mathlib.Algebra.Category.ModuleCat.Ulift
ModuleCat.instPreservesFiniteColimitsUliftFunctor : ∀ (R : Type u) [inst : Ring R], CategoryTheory.Limits.PreservesFiniteColimits (ModuleCat.uliftFunctor.{v', v, u} R)
-- Init.Data.Sum.Basic
Sum.lex_inr_inr : ∀ {α : Type u_1} {r : α → α → Prop} {β : Type u_2} {s : β → β → Prop} {b₁ b₂ : β},
  Sum.Lex r s (Sum.inr b₁) (Sum.inr b₂) ↔ s b₁ b₂
-- Std.Data.HashMap.Raw
/-- Support for the `for` loop construct in `do` blocks.  -/
Std.HashMap.Raw.forIn : {α : Type u} →
  {β : Type v} →
    {m : Type w → Type w'} → [Monad m] → {γ : Type w} → (α → β → γ → m (ForInStep γ)) → γ → Std.HashMap.Raw α β → m γ
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.case.sizeOf_spec : ∀ (a a_1 : Turing.ToPartrec.Code), sizeOf (a.case a_1) = 1 + sizeOf a + sizeOf a_1
-- Batteries.Tactic.Congr
/-- Function elaborating `Congr.Config`  -/
Batteries.Tactic.Congr.elabConfig : Lean.Syntax →
  optParam Batteries.Tactic.Congr.Config { } →
    optParam Bool true → Lean.Elab.Tactic.TacticM Batteries.Tactic.Congr.Config
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Oplax associativity.  -/
CategoryTheory.OplaxFunctor.map₂_associator : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.OplaxFunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom)
      (CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.comp g h))
        (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h))) =
    CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g) (self.map h))
        (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.trivial_V : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {V : Type w} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V], ↑(Rep.trivial k G V) = V
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Coproduct of two continuous homomorphisms to the same space.  -/
ContinuousMonoidHom.coprod : {A : Type u_2} →
  {B : Type u_3} →
    {E : Type u_6} →
      [inst : Monoid A] →
        [inst_1 : Monoid B] →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : TopologicalSpace B] →
              [inst_4 : CommMonoid E] →
                [inst_5 : TopologicalSpace E] → [ContinuousMul E] → (A →ₜ* E) → (B →ₜ* E) → A × B →ₜ* E
-- Std.Sat.AIG.RelabelNat
_private.Std.Sat.AIG.RelabelNat.0.Std.Sat.AIG.RelabelNat.State.ofAIGAux.go.match_1.eq_3 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (lhs rhs : Std.Sat.AIG.Fanin)
  (h_1 : (a : α) → Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.atom a → motive (Std.Sat.AIG.Decl.atom a))
  (h_2 : Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_3 :
    (lhs_1 rhs_1 : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.gate lhs_1 rhs_1 → motive (Std.Sat.AIG.Decl.gate lhs_1 rhs_1)),
  (match hdecl : Std.Sat.AIG.Decl.gate lhs rhs with
    | Std.Sat.AIG.Decl.atom a => h_1 a hdecl
    | Std.Sat.AIG.Decl.false => h_2 hdecl
    | Std.Sat.AIG.Decl.gate lhs_1 rhs_1 => h_3 lhs_1 rhs_1 hdecl) =
    h_3 lhs rhs ⋯
-- Mathlib.CategoryTheory.Presentable.Adjunction
CategoryTheory.Equivalence.isCardinalLocallyPresentable : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  (e : C ≌ D) (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular] [CategoryTheory.IsCardinalLocallyPresentable C κ],
  CategoryTheory.IsCardinalLocallyPresentable D κ
-- Mathlib.Algebra.DirectSum.Module
DirectSum.IsInternal.addSubmonoid_iSupIndep : ∀ {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_2} [inst : AddCommMonoid M] {A : ι → AddSubmonoid M},
  DirectSum.IsInternal A → iSupIndep A
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.forM_eq_forM_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → m PUnit.{w + 1}}, (forM t fun a => f a.fst) = Array.forM f t.keysArray
-- Mathlib.Data.Finset.Powerset
Finset.powerset_mono : ∀ {α : Type u_1} {s t : Finset α}, s.powerset ⊆ t.powerset ↔ s ⊆ t
-- Mathlib.Topology.EMetricSpace.Basic
EMetric.totallyBounded_iff' : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α},
  TotallyBounded s ↔ ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, Metric.eball y ε
-- Init.Data.Rat.Lemmas
Rat.zpow_add : ∀ {q : ℚ}, q ≠ 0 → ∀ (m n : ℤ), q ^ (m + n) = q ^ m * q ^ n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Complex.tendsto_norm_tan_atTop : ∀ (k : ℤ),
  Filter.Tendsto (fun x => ‖Complex.tan x‖) (nhdsWithin ((2 * ↑k + 1) * ↑Real.pi / 2) {(2 * ↑k + 1) * ↑Real.pi / 2}ᶜ)
    Filter.atTop
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.sign_of_pow_two_eq_one : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α},
  σ ^ 2 = 1 → Equiv.Perm.sign σ = (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / 2)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.precomp_surjective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C (n + 1)),
  ∃ F₀ X₀ f₀, F = F₀.precomp f₀
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.monoidalCategoryStruct_tensorObj : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] (X Y : (i : I) → C i) (i : I),
  CategoryTheory.MonoidalCategoryStruct.tensorObj X Y i = CategoryTheory.MonoidalCategoryStruct.tensorObj (X i) (Y i)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.lt_lt_combine_cert.eq_1 : ∀ (p₁ p₂ p₃ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.lt_lt_combine_cert p₁ p₂ p₃ =
    (decide (↑p₂.leadCoeff.natAbs > 0) && decide (↑p₁.leadCoeff.natAbs > 0) &&
      p₃ == (p₁.mul ↑p₂.leadCoeff.natAbs).combine (p₂.mul ↑p₁.leadCoeff.natAbs))
-- Mathlib.Util.AtomM.Recurse
Mathlib.Tactic.AtomM.Recurse.instReprConfig.repr : Mathlib.Tactic.AtomM.Recurse.Config → ℕ → Std.Format
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.toList_keysIter : ∀ {α : Type u} {β : α → Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m.keysIter.toList = m.keys
-- Mathlib.RingTheory.Bezout
IsBezout.iff_span_pair_isPrincipal : ∀ {R : Type u} [inst : CommRing R], IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
-- Mathlib.RingTheory.ReesAlgebra
reesAlgebra.monomial_mem : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {i : ℕ} {r : R}, (Polynomial.monomial i) r ∈ reesAlgebra I ↔ r ∈ I ^ i
-- Mathlib.Logic.Equiv.Defs
Equiv.forall₂_congr' : ∀ {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} {p : α₁ → β₁ → Prop} {q : α₂ → β₂ → Prop}
  (eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂),
  (∀ {x : α₂} {y : β₂}, p (eα.symm x) (eβ.symm y) ↔ q x y) → ((∀ (x : α₁) (y : β₁), p x y) ↔ ∀ (x : α₂) (y : β₂), q x y)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.forIn_eq_forIn_toArray : ∀ {α : Type u} {δ : Type w} {m' : Type w → Type w'} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst : Monad m'] [LawfulMonad m'] {f : α → β → δ → m' (ForInStep δ)} {init : δ},
  Std.DHashMap.Raw.forIn f init ↑m = forIn (Std.DHashMap.Raw.Const.toArray ↑m) init fun a b => f a.1 a.2 b
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instNorm : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] → [inst_1 : SeminormedAddCommGroup β] → Norm (BoundedContinuousFunction α β)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.mul_k : Int.Internal.Linear.Poly → ℤ → Int.Internal.Linear.Poly
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instArg : List Lean.Name →
  List Lean.Level →
    Lean.Compiler.LCNF.Arg Lean.Compiler.LCNF.Purity.pure → Lean.Compiler.LCNF.Arg Lean.Compiler.LCNF.Purity.pure
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isNone_getElem?_toList_rco_eq : ∀ {m n i : ℕ}, ((m...n).toList[i]?.isNone = true) = (n ≤ i + m)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.instCategorySplit : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.Category.{v_1, max u_1 v_1} (CategoryTheory.SimplicialObject.Split C)
-- Mathlib.Data.Finsupp.SMulWithZero
Finsupp.distribSMul : (α : Type u_1) → (M : Type u_5) → {R : Type u_11} → [inst : AddZeroClass M] → [DistribSMul R M] → DistribSMul R (α →₀ M)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imI_natCast : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (n : ℕ), (↑n).imI = 0
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.comp_liftCycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0)
  [inst_2 : S.HasLeftHomology] {A' : C} (α : A' ⟶ A),
  CategoryTheory.CategoryStruct.comp α (S.liftCycles k hk) = S.liftCycles (CategoryTheory.CategoryStruct.comp α k) ⋯
-- Mathlib.Algebra.Algebra.Defs
/-- An auxiliary lemma used to prove theorems of the form
`RingHom.X (algebraMap R S) ↔ Algebra.X R S`.  -/
toAlgebra_algebraMap : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  (algebraMap R S).toAlgebra = inst_2
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
/-- If `a₁ a₂ : A ⟶ Y` is a kernel pair for `g : Y ⟶ Z`, then `a₁ ×[Z] X` and `a₂ ×[Z] X`
(`A ×[Z] X ⟶ Y ×[Z] X`) is a kernel pair for `Y ×[Z] X ⟶ X`.  -/
CategoryTheory.IsKernelPair.pullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z A : C} {g : Y ⟶ Z} {a₁ a₂ : A ⟶ Y}
  (h : CategoryTheory.IsKernelPair g a₁ a₂) (f : X ⟶ Z) [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp a₁ g)],
  CategoryTheory.IsKernelPair (CategoryTheory.Limits.pullback.fst f g)
    (CategoryTheory.Limits.pullback.map f (CategoryTheory.CategoryStruct.comp a₁ g) f g
      (CategoryTheory.CategoryStruct.id X) a₁ (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)
    (CategoryTheory.Limits.pullback.map f (CategoryTheory.CategoryStruct.comp a₁ g) f g
      (CategoryTheory.CategoryStruct.id X) a₂ (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instNeZeroIdealOfIsMaximal : ∀ (K : Type u_1) [inst : Field K] [NumberField K] {I : Ideal (NumberField.RingOfIntegers K)} [hI : I.IsMaximal],
  NeZero I
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.Functor.map_commSq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y}
  {h : X ⟶ Z} {i : Y ⟶ Z}, CategoryTheory.CommSq f g h i → CategoryTheory.CommSq (F.map f) (F.map g) (F.map h) (F.map i)
-- Mathlib.Algebra.DirectSum.Algebra
/-- A direct sum of copies of an `Algebra` inherits the algebra structure.  -/
Algebra.directSumGAlgebra : {ι : Type uι} →
  {R : Type u_1} →
    {A : Type u_2} →
      [inst : AddMonoid ι] →
        [inst_1 : CommSemiring R] → [inst_2 : Semiring A] → [inst_3 : Algebra R A] → DirectSum.GAlgebra R fun x => A
-- Mathlib.NumberTheory.MaricaSchoenheim
/-- Statement of Graham's conjecture (which is now a theorem in the literature).

Graham's conjecture states that if $0 < a_1 < \dots a_n$ are integers, then
$\max_{i, j} \frac{a_i}{\gcd(a_i, a_j)} \ge n$.  -/
Nat.GrahamConjecture : ℕ → (ℕ → ℕ) → Prop
-- Lean.Server.Rpc.Basic
Lean.Lsp.RpcRef.mk : USize → Lean.Lsp.RpcRef
-- Mathlib.Algebra.Ring.Semireal.Defs
/-- A semireal ring is a commutative ring (with unit) in which `-1` is *not* a sum of
squares. We define the predicate `IsSemireal R` for structures `R` equipped with
a multiplication, an addition, a multiplicative unit and an additive unit.
 -/
IsSemireal : (R : Type u_1) → [Add R] → [Mul R] → [One R] → [Zero R] → Prop
-- Mathlib.Testing.Plausible.Functions
Plausible.InjectiveFunction.instRepr : (α : Type u) → [Repr α] → Repr (Plausible.InjectiveFunction α)
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstLVal : Lean.Parser.Parser
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_pos_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α}, 0 < s.addEnergy t ↔ s.Nonempty ∧ t.Nonempty
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.instForMSigmaOfMonad : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → {m : Type w → Type w₂} → [Monad m] → ForM m (Std.DTreeMap α β cmp) ((a : α) × β a)
-- Mathlib.Topology.MetricSpace.Infsep
Set.le_edist_of_le_einfsep : ∀ {α : Type u_1} [inst : EDist α] {s : Set α} {d : ENNReal} {x : α},
  x ∈ s → ∀ {y : α}, y ∈ s → x ≠ y → d ≤ s.einfsep → d ≤ edist x y
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α}, m.WF → (Std.DHashMap.Raw.filter f m).contains k = Option.any (f k) (m.get? k)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.instPreadditive : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (R : CategoryTheory.Sheaf J RingCat) → CategoryTheory.Preadditive (SheafOfModules R)
-- Mathlib.Order.RelClasses
Prod.wellFoundedGT : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [WellFoundedGT α] [inst_2 : Preorder β] [WellFoundedGT β],
  WellFoundedGT (α × β)
-- Mathlib.Algebra.Lie.Rank
LieModule.exists_isRegular_of_finrank_le_card : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M] [inst_9 : Module.Finite R M] [inst_10 : Module.Free R M]
  [IsDomain R], ↑(Module.finrank R M) ≤ Cardinal.mk R → ∃ x, LieModule.IsRegular R M x
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.fst.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B],
  ContinuousAddMonoidHom.fst A B = { toAddMonoidHom := AddMonoidHom.fst A B, continuous_toFun := ⋯ }
-- Mathlib.Algebra.Order.Field.Basic
one_lt_div_iff : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
-- Mathlib.LinearAlgebra.AffineSpace.Ceva
/-- A version of **Ceva's theorem** for a finite indexed affinely independent family of points:
consider some lines, each through one of the points and an affine combination of the points, and
suppose they concur at `p'`; then `p'` is an affine combination of the points with weights
proportional to those in the respective affine combinations.  -/
AffineIndependent.exists_affineCombination_eq_smul_eq_of_fintype : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] {p : ι → P},
  AffineIndependent k p →
    ∀ {s : Set ι},
      s.Nonempty →
        ∀ {w : ↑s → ι → k},
          (∀ (i : ↑s), ∑ j, w i j = 1) →
            ∀ {p' : P},
              (∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k Finset.univ p) (w i)]) →
                ∃ w',
                  ∑ j, w' j = 1 ∧
                    (Finset.affineCombination k Finset.univ p) w' = p' ∧
                      ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator w' j
-- Batteries.Data.Nat.Basic
/-- Recursor identical to `Nat.recOn` but uses notations `0` for `Nat.zero` and `·+1` for `Nat.succ`
 -/
Nat.recAuxOn : {motive : ℕ → Sort u_1} → (t : ℕ) → motive 0 → ((n : ℕ) → motive n → motive (n + 1)) → motive t
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Composition of non-unital ring homomorphisms is a non-unital ring homomorphism.  -/
NonUnitalRingHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : NonUnitalNonAssocSemiring α] →
        [inst_1 : NonUnitalNonAssocSemiring β] →
          [inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γ
-- Mathlib.RingTheory.DedekindDomain.LinearDisjoint
Module.Basis.ofIsCoprimeDifferentIdeal.congr_simp : ∀ (A : Type u_1) (B : Type u_2) {K : Type u_3} {L : Type u_4} [inst : CommRing A] [inst_1 : Field K]
  [inst_2 : Algebra A K] [inst_3 : IsFractionRing A K] [inst_4 : CommRing B] [inst_5 : Field L] [inst_6 : Algebra B L]
  [inst_7 : Algebra A L] [inst_8 : Algebra K L] [inst_9 : FiniteDimensional K L] [inst_10 : IsScalarTower A K L]
  (R₁ : Type u_5) (R₂ : Type u_6) [inst_11 : CommRing R₁] [inst_12 : CommRing R₂] [inst_13 : IsDomain R₁]
  [inst_14 : Algebra A R₁] [inst_15 : Algebra A R₂] [inst_16 : Algebra R₁ B] [inst_17 : Algebra R₂ B]
  [inst_18 : Algebra R₁ L] [inst_19 : Algebra R₂ L] [inst_20 : IsScalarTower A R₁ L] [inst_21 : IsScalarTower R₁ B L]
  [inst_22 : IsScalarTower R₂ B L] [inst_23 : Module.Finite A R₂] {F₁ F₂ : IntermediateField K L}
  [inst_24 : Algebra R₁ ↥F₁] [inst_25 : Algebra R₂ ↥F₂] [inst_26 : Module.IsTorsionFree R₁ ↥F₁]
  [inst_27 : IsScalarTower A (↥F₂) L] [inst_28 : IsScalarTower A R₂ ↥F₂] [inst_29 : IsScalarTower R₁ (↥F₁) L]
  [inst_30 : IsScalarTower R₂ (↥F₂) L] [inst_31 : Algebra.IsSeparable K ↥F₂] [inst_32 : Algebra.IsSeparable (↥F₁) L]
  [inst_33 : IsDomain A] [inst_34 : IsDedekindDomain B] [inst_35 : IsDedekindDomain R₁] [inst_36 : IsDedekindDomain R₂]
  [inst_37 : IsFractionRing B L] [inst_38 : IsFractionRing R₁ ↥F₁] [inst_39 : IsFractionRing R₂ ↥F₂]
  [inst_40 : IsIntegrallyClosed A] [inst_41 : IsIntegralClosure B R₁ L] [inst_42 : Module.IsTorsionFree R₁ B]
  [inst_43 : Module.IsTorsionFree R₂ B], ⋯
-- Init.Data.Int.DivMod.Lemmas
Int.sub_mul_fdiv_left : ∀ (a : ℤ) {b : ℤ} (c : ℤ), b ≠ 0 → (a - b * c).fdiv b = a.fdiv b - c
-- Mathlib.Combinatorics.Configuration
Configuration.instMembershipDual : (P : Type u_1) → (L : Type u_2) → [Membership P L] → Membership (Configuration.Dual L) (Configuration.Dual P)
-- Init.Data.Option.Lemmas
Option.left_lt_of_merge_lt : ∀ {α : Type u_1} [inst : LT α] {f : α → α → α},
  (∀ (a b c : α), f a b < c → a < c) → ∀ {o₁ o₂ o₃ : Option α}, Option.merge f o₁ o₂ < o₃ → o₁ < o₃
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upcrossings.eq_1 : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] [inst_1 : OrderBot ι] [inst_2 : InfSet ι] (a b : ℝ) (f : ι → Ω → ℝ)
  (ω : Ω), MeasureTheory.upcrossings a b f ω = ⨆ N, ↑(MeasureTheory.upcrossingsBefore a b f N ω)
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- Auxiliary definition for `colimitCoconeIsColimit`.  -/
SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J SemiRingCat} →
      [inst_1 : CategoryTheory.IsFiltered J] →
        (t : CategoryTheory.Limits.Cocone F) → ↑(SemiRingCat.FilteredColimits.R F) →* ↑t.pt
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_pow : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (p : Polynomial (Polynomial R)) (n : ℕ),
  Polynomial.evalEval x y (p ^ n) = Polynomial.evalEval x y p ^ n
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- For a functor `G : J ⥤ K ⥤ C`, its limit `K ⥤ C` is given by `(G' : K ⥤ J ⥤ C) ⋙ lim`.
Note that this does not require `K` to be small.
 -/
CategoryTheory.Limits.limitIsoSwapCompLim : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] →
              (G : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
                CategoryTheory.Limits.limit G ≅
                  (CategoryTheory.Functor.curry.obj
                        ((CategoryTheory.Prod.swap K J).comp (CategoryTheory.Functor.uncurry.obj G))).comp
                    CategoryTheory.Limits.lim
-- Init.Data.Slice.List.Iterator
instForInListSliceOfMonad : {α : Type u} → {m : Type v → Type w} → [Monad m] → ForIn m (ListSlice α) α
-- Mathlib.Algebra.Category.ModuleCat.Simple
/-- A simple module is a simple object in the category of modules.  -/
simple_of_isSimpleModule : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSimpleModule R M],
  CategoryTheory.Simple (ModuleCat.of R M)
-- Lean.Compiler.IR.Format
_private.Lean.Compiler.IR.Format.0.Lean.IR.formatArg : Lean.IR.Arg → Std.Format
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, (t₁ ∪ t₂).getKeyD k fallback = t₂.getKeyD k (t₁.getKeyD k fallback)
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.piCongrLeft_toEquiv : ∀ {ι : Type u_4} {ι' : Type u_5} {β : ι' → Type u_6} [inst : (j : ι') → UniformSpace (β j)] (e : ι ≃ ι'),
  (UniformEquiv.piCongrLeft e).toEquiv = Equiv.piCongrLeft β e
-- Mathlib.Analysis.Normed.Affine.AddTorsor
nndist_left_lineMap : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜),
  nndist p₁ ((AffineMap.lineMap p₁ p₂) c) = ‖c‖₊ * nndist p₁ p₂
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.eval₂_eq_sum_range : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] (f : R →+* S) (x : S),
  Polynomial.eval₂ f x p = ∑ i ∈ Finset.range (p.natDegree + 1), f (p.coeff i) * x ^ i
-- Mathlib.Algebra.Group.Submonoid.Membership
/-- An induction principle for elements of `⨆ i, S i`.
If `C` holds for `0` and all elements of `S i` for all `i`, and is preserved under addition,
then it holds for all elements of the supremum of `S`.  -/
AddSubmonoid.iSup_induction : ∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_4} (S : ι → AddSubmonoid M) {motive : M → Prop} {x : M},
  x ∈ ⨆ i, S i →
    (∀ (i : ι), ∀ x ∈ S i, motive x) → motive 0 → (∀ (x y : M), motive x → motive y → motive (x + y)) → motive x
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.inlCLM_apply : ∀ (R : Type u_3) (M : Type u_4) [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [inst_2 : CommSemiring R]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (r : R), (TrivSqZeroExt.inlCLM R M) r = TrivSqZeroExt.inl r
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.length_eq_dist_of_subwalk : ∀ {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'},
  p₁.length = G.dist u v → p₂.IsSubwalk p₁ → p₂.length = G.dist u' v'
-- Mathlib.Order.OmegaCompletePartialOrder
/-- An omega-complete partial order is a partial order with a supremum
operation on increasing sequences indexed by natural numbers (which we
call `ωSup`). In this sense, it is strictly weaker than join complete
semi-lattices as only ω-sized totally ordered sets have a supremum.

See the definition on page 114 of [gunter1992].  -/
OmegaCompletePartialOrder : Type u_6 → Type u_6