mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.comp_apply : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : AddZero M] [inst_1 : AddZero N] [inst_2 : AddZero P] (g : N →+ P)
  (f : M →+ N) (x : M), (g.comp f) x = g (f x)
-- Mathlib.RingTheory.Coprime.Lemmas
IsCoprime.eq_1 : ∀ {R : Type u} [inst : CommSemiring R] (x y : R), IsCoprime x y = ∃ a b, a * x + b * y = 1
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.fst_comp_inl : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  (AddMonoidHom.fst M N).comp (AddMonoidHom.inl M N) = AddMonoidHom.id M
-- Mathlib.Data.EReal.Operations
EReal.sub_nonneg : ∀ {x y : EReal}, x ≠ ⊤ ∨ y ≠ ⊤ → x ≠ ⊥ ∨ y ≠ ⊥ → (0 ≤ x - y ↔ y ≤ x)
-- Mathlib.LinearAlgebra.Finsupp.Pi
/-- A linear map from a product module `P × M` to `M` induces a linear map from `P^(ℕ)` to `M`,
where the `n`th component is given by `P —ι₁→ P × M` composed with `P × M —f→ M —ι₂→ P × M`
`n` times.  -/
LinearMap.prodOfFinsuppNat : {R : Type u_1} →
  {M : Type u_2} →
    {P : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid P] → [inst_4 : Module R P] → (P × M →ₗ[R] M) → (ℕ →₀ P) →ₗ[R] P × M
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The TM2 emulator machine states written as a TM1 program.
This handles the `go` and `ret` states, which shuttle to and from a stack top.  -/
Turing.TM2to1.tr : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} →
        [DecidableEq K] →
          (Λ → Turing.TM2.Stmt Γ Λ σ) →
            Turing.TM2to1.Λ' K Γ Λ σ → Turing.TM1.Stmt (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ
-- Mathlib.Order.Monotone.Basic
StrictAnti.cmp_map_eq : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  StrictAnti f → ∀ (x y : α), cmp (f x) (f y) = cmp y x
-- Init.Data.List.Count
List.countP_cons : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α},
  List.countP p (a :: l) = List.countP p l + if p a = true then 1 else 0
-- Mathlib.RingTheory.Flat.EquationalCriterion
/-- [Stacks Tag 00NX](https://stacks.math.columbia.edu/tag/00NX) ((1) → (2)) -/
Module.Flat.projective_of_finitePresentation : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  [Module.FinitePresentation R M], Module.Projective R M
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_iff_lt_one_left' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LT α] [MulLeftStrictMono α] [MulLeftReflectLT α] {a b : α},
  a * b < a ↔ b < 1
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.match_1.congr_eq_2 : ∀ (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1) (x : ByteArray.utf8DecodeChar?.FirstByte)
  (h_1 : x = ByteArray.utf8DecodeChar?.FirstByte.invalid → motive ByteArray.utf8DecodeChar?.FirstByte.invalid)
  (h_2 : x = ByteArray.utf8DecodeChar?.FirstByte.done → motive ByteArray.utf8DecodeChar?.FirstByte.done)
  (h_3 : x = ByteArray.utf8DecodeChar?.FirstByte.oneMore → motive ByteArray.utf8DecodeChar?.FirstByte.oneMore)
  (h_4 : x = ByteArray.utf8DecodeChar?.FirstByte.twoMore → motive ByteArray.utf8DecodeChar?.FirstByte.twoMore)
  (h_5 : x = ByteArray.utf8DecodeChar?.FirstByte.threeMore → motive ByteArray.utf8DecodeChar?.FirstByte.threeMore)
  (heq_1 : x = ByteArray.utf8DecodeChar?.FirstByte.done),
  (match h : x with
    | ByteArray.utf8DecodeChar?.FirstByte.invalid => h_1 h
    | ByteArray.utf8DecodeChar?.FirstByte.done => h_2 h
    | ByteArray.utf8DecodeChar?.FirstByte.oneMore => h_3 h
    | ByteArray.utf8DecodeChar?.FirstByte.twoMore => h_4 h
    | ByteArray.utf8DecodeChar?.FirstByte.threeMore => h_5 h) ≍
    h_2 heq_1
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.monotone_eapprox : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f : α → ENNReal), Monotone (MeasureTheory.SimpleFunc.eapprox f)
-- Init.Data.Nat.Basic
Nat.le_lt_asymm : ∀ {a b : ℕ}, a ≤ b → ¬b < a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_insert_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {a : α} {fallback b : β a},
  (Std.DTreeMap.Internal.Impl.insert a b t ⋯).impl.getD a fallback = b
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.IsCyclicallyReduced.flatten_replicate : ∀ {α : Type u} {L : List (α × Bool)},
  FreeAddGroup.IsCyclicallyReduced L → ∀ (n : ℕ), FreeAddGroup.IsCyclicallyReduced (List.replicate n L).flatten
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- The split mono which appears in the factorisation `decompId P`.  -/
CategoryTheory.Idempotents.Karoubi.decompId_i : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.Idempotents.Karoubi C) → P ⟶ { X := P.X, p := CategoryTheory.CategoryStruct.id P.X, idem := ⋯ }
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.foldr_eq_foldr_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {f : α → δ → δ} {init : δ},
  Std.TreeMap.foldr (fun a x d => f a d) init t = List.foldr f init t.keys
-- Mathlib.MeasureTheory.Measure.FiniteMeasureProd
MeasureTheory.FiniteMeasure.prod_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_2} [inst_1 : MeasurableSpace β]
  (μ : MeasureTheory.FiniteMeasure α) (ν : MeasureTheory.FiniteMeasure β) (s : Set (α × β)),
  MeasurableSet s → (μ.prod ν) s = (∫⁻ (x : α), ↑ν (Prod.mk x ⁻¹' s) ∂↑μ).toNNReal
-- Mathlib.GroupTheory.SchurZassenhaus
Subgroup.instMulActionQuotientDiff : {G : Type u_1} →
  [inst : Group G] →
    {H : Subgroup G} →
      [inst_1 : IsMulCommutative ↥H] → [inst_2 : H.FiniteIndex] → [H.Normal] → MulAction G H.QuotientDiff
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.instCoeFunForall.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N], MulEquiv.instCoeFunForall = { coe := fun f => ⇑f }
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.measure_eq_zero_iff_ae_notMem : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s : Set α}, μ s = 0 ↔ ∀ᵐ (a : α) ∂μ, a ∉ s
-- Mathlib.RepresentationTheory.Induced
Representation.IndV.hom_ext_iff : ∀ {k : Type u_1} {G : Type u_2} {H : Type u_3} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {φ : G →* H}
  {A : Type u_4} {B : Type u_5} [inst_3 : AddCommGroup A] [inst_4 : Module k A] {ρ : Representation k G A}
  [inst_5 : AddCommGroup B] [inst_6 : Module k B] {f g : Representation.IndV φ ρ →ₗ[k] B},
  f = g ↔ ∀ (h : H), f ∘ₗ Representation.IndV.mk φ ρ h = g ∘ₗ Representation.IndV.mk φ ρ h
-- Mathlib.Data.DFinsupp.Interval
Finset.card_dfinsupp : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (α i)] (s : Finset ι)
  (t : (i : ι) → Finset (α i)), (s.dfinsupp t).card = ∏ i ∈ s, (t i).card
-- Mathlib.Topology.Instances.CantorSet
cantorStep_mem_cantorSet : ∀ {x : ℝ}, x ∈ cantorSet → cantorStep x ∈ cantorSet
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
LinearIsometry.norm_compContinuousAlternatingMap : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  (g : F →ₗᵢ[𝕜] G) (f : E [⋀^ι]→L[𝕜] F), ‖g.toContinuousLinearMap.compContinuousAlternatingMap f‖ = ‖f‖
-- Mathlib.Analysis.Distribution.TemperateGrowth
Function.HasTemperateGrowth.id' : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E], Function.HasTemperateGrowth fun x => x
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- A morphism is called a face if it is a `δ i` for some `i : Fin (n + 2)`.  -/
SimplexCategoryGenRel.faces : CategoryTheory.MorphismProperty SimplexCategoryGenRel
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The inner product of a nonzero vector with a negative multiple of
itself, divided by the product of their norms, has value -1.  -/
real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x : F} {r : ℝ},
  x ≠ 0 → r < 0 → inner ℝ x (r • x) / (‖x‖ * ‖r • x‖) = -1
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {a : α} {b : β},
  t.WF → (t.insert a b).WF
-- Init.Data.Fin.Lemmas
Fin.pred_lt_pred_iff : ∀ {n : ℕ} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0}, a.pred ha < b.pred hb ↔ a < b
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsAEKolmogorovProcess.aemeasurable_edist : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E},
  ProbabilityTheory.IsAEKolmogorovProcess X P p q M → ∀ {s t : T}, AEMeasurable (fun ω => edist (X s ω) (X t ω)) P
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.coe_mul_star_self : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : ↥(spinGroup Q)), ↑x * ↑(star x) = 1
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.binomial_one_eq_bernoulliMeasure : ∀ (p : ↑unitInterval), ProbabilityTheory.binomial 1 p = ProbabilityTheory.bernoulliMeasure 1 0 p
-- Mathlib.Analysis.Seminorm
Seminorm.sub_mem_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) (x₁ x₂ y : E) (r : ℝ), x₁ - x₂ ∈ p.ball y r ↔ x₁ ∈ p.ball (x₂ + y) r
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.variableChange_c₄ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R),
  (C • W).c₄ = ↑C.u⁻¹ ^ 4 * W.c₄
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
ContDiffWithinAt.derivWithin : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m n : WithTop ℕ∞} {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜},
  ContDiffWithinAt 𝕜 n f s x → UniqueDiffOn 𝕜 s → m + 1 ≤ n → x ∈ s → ContDiffWithinAt 𝕜 m (derivWithin f s) s x
-- Mathlib.CategoryTheory.Category.Quiv
/-- Naturality of `pathComposition`.  -/
CategoryTheory.Quiv.pathCompositionNaturality : {C : Type u} →
  {D : Type u₁} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} D] →
        (F : CategoryTheory.Functor C D) →
          (CategoryTheory.Cat.freeMap F.toPrefunctor).comp (CategoryTheory.pathComposition D) ≅
            (CategoryTheory.pathComposition C).comp F
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- Auxiliary definition for `associativityIso`.  -/
SSet.Truncated.HomotopyCategory.BinaryProduct.associativity'Iso : (X Y Z : SSet.Truncated 2) →
  (CategoryTheory.prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse.comp
      (((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).prod
            (CategoryTheory.Functor.id Z.HomotopyCategory)).comp
        ((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
              Z).comp
          (SSet.Truncated.mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom))) ≅
    ((CategoryTheory.Functor.id X.HomotopyCategory).prod
          (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse Y Z)).comp
      (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasSum.add : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f g : β → α} {a b : α}
  {L : SummationFilter β} [ContinuousAdd α], HasSum f a L → HasSum g b L → HasSum (fun b => f b + g b) (a + b) L
-- Mathlib.Order.Interval.Finset.Defs
WithTop.Ioo_coe_top : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : LocallyFiniteOrder α] (a : α),
  Finset.Ioo ↑a ⊤ = Finset.map Function.Embedding.some (Finset.Ioi a)
-- Lean.Environment
_private.Lean.Environment.0.Lean.ImportedModule.mk.sizeOf_spec : ∀ (toEffectiveImport : Lean.EffectiveImport) (parts irParts : Array (Lean.ModuleData × Lean.CompactedRegion))
  (needsIRTrans : Bool),
  sizeOf { toEffectiveImport := toEffectiveImport, parts := parts, irParts := irParts, needsIRTrans := needsIRTrans } =
    1 + sizeOf toEffectiveImport + sizeOf parts + sizeOf irParts + sizeOf needsIRTrans
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_ne_zero_iff : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : CommMonoidWithZero γ] [Nontrivial γ] [NoZeroDivisors γ] [inst_5 : (i : ι) → DecidableEq (β i)]
  {f : Π₀ (i : ι), β i} {g : (i : ι) → β i → γ}, f.prod g ≠ 0 ↔ ∀ i ∈ f.support, g i (f i) ≠ 0
-- Mathlib.Data.Matrix.Mul
dotProduct_one : ∀ {n : Type u_3} {α : Type v} [inst : Fintype n] [inst_1 : MulOneClass α] [inst_2 : AddCommMonoid α] (v : n → α),
  v ⬝ᵥ 1 = ∑ i, v i
-- Mathlib.Data.Finsupp.SMul
Finsupp.single_smul : ∀ {α : Type u_1} {M : Type u_3} {R : Type u_6} [inst : Zero M] [inst_1 : MonoidWithZero R]
  [inst_2 : MulActionWithZero R M] (a b : α) (f : α → M) (r : R), (fun₀ | a => r) b • f a = (fun₀ | a => r • f b) b
-- Mathlib.Algebra.Category.Ring.Basic
_private.Mathlib.Algebra.Category.Ring.Basic.0.CommSemiRingCat.Hom.mk.inj : ∀ {R S : CommSemiRingCat} {hom' hom'_1 : ↑R →+* ↑S}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Lean.HeadIndex
/-- Slower version of `toHeadIndexQuick?` that "expands" let-declarations to make
sure we never hit a loose bound variable.
The performance of the `letE` alternative can be improved, but this function should not be in the hotpath
since `toHeadIndexQuick?` succeeds most of the time.
 -/
_private.Lean.HeadIndex.0.Lean.Expr.toHeadIndexSlow : Lean.Expr → Lean.HeadIndex
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor_obj_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.toArrowArrowFunctor.obj sq).hom.right = sq.f₃₄
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isGE_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) (n : ℤ), K.IsGE n ↔ ∀ i < n, HomologicalComplex.ExactAt K i
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.reduce_to_affine_nbhd : ∀ (P : (X : AlgebraicGeometry.Scheme) → ↥X → Prop),
  (∀ (R : CommRingCat) (x : ↥(AlgebraicGeometry.Spec R)), P (AlgebraicGeometry.Spec R) x) →
    (∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (x : ↥X), P X x → P Y (f x)) →
      ∀ (X : AlgebraicGeometry.Scheme) (x : ↥X), P X x
-- Mathlib.Analysis.Normed.Group.Indicator
indicator_enorm_le_enorm_self : ∀ {α : Type u_1} {ε : Type u_2} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] {s : Set α} (f : α → ε)
  (a : α), s.indicator (fun a => ‖f a‖ₑ) a ≤ ‖f a‖ₑ
-- Mathlib.Order.Max
OrderDual.noMinOrder : ∀ {α : Type u_1} [inst : LT α] [NoMaxOrder α], NoMinOrder αᵒᵈ
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- A version of `StructuredArrow.ofDiagEquivalence` with the roles of the first and second
projection swapped.  -/
CategoryTheory.StructuredArrow.ofDiagEquivalence' : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    (X : T × T) →
      CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T) ≌
        CategoryTheory.StructuredArrow X.1 (CategoryTheory.Under.forget X.2)
-- Mathlib.Topology.NoetherianSpace
/-- [Stacks Tag 0052](https://stacks.math.columbia.edu/tag/0052) ((3)) -/
TopologicalSpace.NoetherianSpace.exists_isOpen_nonempty_subset_irreducibleComponent : ∀ {α : Type u_1} [inst : TopologicalSpace α] [TopologicalSpace.NoetherianSpace α],
  ∀ Z ∈ irreducibleComponents α, ∃ o, IsOpen o ∧ o.Nonempty ∧ o ⊆ Z
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.BalancedAtRoot.erase_left : ∀ {l l' r : ℕ},
  Std.DTreeMap.Internal.Impl.BalancedAtRoot l r →
    l - 1 ≤ l' → l' ≤ l → Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r l'
-- Mathlib.Topology.Order
Subsingleton.uniqueTopologicalSpace : {α : Type u} → [Subsingleton α] → Unique (TopologicalSpace α)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.instOrderBot : OrderBot Ordinal.{u_1}
-- Mathlib.Data.Rat.Defs
Rat.div_def' : ∀ (q r : ℚ), q / r = Rat.divInt (q.num * ↑r.den) (↑q.den * r.num)
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.zpow.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.zpow = { pow := fun a n => ⟨↑a ^ n, ⋯⟩ }
-- Mathlib.ModelTheory.Types
/-- The underlying theory  -/
FirstOrder.Language.Theory.CompleteType.toTheory : {L : FirstOrder.Language} → {T : L.Theory} → {α : Type w} → T.CompleteType α → (L.withConstants α).Theory
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.denoteInt.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (k : ℤ),
  Lean.Grind.CommRing.denoteInt k = Bool.rec (OfNat.ofNat k.natAbs) (-OfNat.ofNat k.natAbs) (k.blt' 0)
-- Lean.Attributes
Lean.AttributeExtensionState.newEntries : Lean.AttributeExtensionState → List Lean.AttributeExtensionOLeanEntry
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.mk : {A : Type u} → [inst : Ring A] → (G : Type w₀) → (R : Type w₁) → (R → G →₀ A) → Module.Relations A
-- Mathlib.NumberTheory.LSeries.SumCoeff
/-- A version of `LSeries_eq_mul_integral` where we use the stronger condition that the partial sums
`∑ k ∈ Icc 1 n, ‖f k‖` are `O(n ^ r)` to deduce the integral representation.  -/
LSeries_eq_mul_integral' : ∀ (f : ℕ → ℂ) {r : ℝ},
  0 ≤ r →
    ∀ {s : ℂ},
      r < s.re →
        ((fun n => ∑ k ∈ Finset.Icc 1 n, ‖f k‖) =O[Filter.atTop] fun n => ↑n ^ r) →
          LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Finset.Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.add.injEq : ∀ (k : ℤ) (v : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly) (k_1 : ℤ) (v_1 : Int.Internal.Linear.Var)
  (p_1 : Int.Internal.Linear.Poly),
  (Int.Internal.Linear.Poly.add k v p = Int.Internal.Linear.Poly.add k_1 v_1 p_1) = (k = k_1 ∧ v = v_1 ∧ p = p_1)
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.vertexCoverNum_ne_top_of_finite_edgeSet : ∀ {V : Type u_1} {G : SimpleGraph V}, G.edgeSet.Finite → G.vertexCoverNum ≠ ⊤
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_atTop_zero : ∀ {β : Type u_2} [Nonempty β] [inst : SemilatticeSup β] {f : β → ENNReal},
  Filter.Tendsto f Filter.atTop (nhds 0) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε
-- Mathlib.CategoryTheory.Enriched.Basic
/-- `X ⟶[V] Y` is the `V` object of morphisms from `X` to `Y`.  -/
CategoryTheory.«term_⟶[_]_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Group.Pi.Basic
/-- If the zero function is surjective, the codomain is trivial.  -/
uniqueOfSurjectiveZero : (α : Type u_4) → {β : Type u_5} → [inst : Zero β] → Function.Surjective 0 → Unique β
-- Init.Data.Array.MapIdx
_private.Init.Data.Array.MapIdx.0.Array.mapFinIdx_induction.go : ∀ {α : Type u_1} {β : Type u_2} (xs : Array α) (f : (i : ℕ) → α → i < xs.size → β) (motive : ℕ → Prop)
  (p : (i : ℕ) → β → i < xs.size → Prop),
  (∀ (i : ℕ) (h : i < xs.size), motive i → p i (f i xs[i] h) h ∧ motive (i + 1)) →
    ∀ {bs : Array β} {i j : ℕ} {h : i + j = xs.size},
      j = bs.size →
        (∀ (i : ℕ) (h : i < xs.size) (h' : i < bs.size), p i bs[i] h) →
          motive j →
            let as := (Array.mapFinIdxM.map xs (fun x1 x2 x3 => pure (f x1 x2 x3)) i j h bs).run;
            motive xs.size ∧ ∃ (eq : as.size = xs.size), ∀ (i_1 : ℕ) (h_1 : i_1 < xs.size), p i_1 as[i_1] h_1
-- Mathlib.Order.RelSeries
/-- A type is infinite dimensional if it has `LTSeries` of at least arbitrary length  -/
InfiniteDimensionalOrder : (γ : Type u_3) → [Preorder γ] → Prop
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.op_smul_set_smul_eq_smul_smul_set : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul αᵐᵒᵖ β] [inst_1 : SMul β γ] [inst_2 : SMul α γ] (a : α)
  (s : Set β) (t : Set γ),
  (∀ (a : α) (b : β) (c : γ), (MulOpposite.op a • b) • c = b • a • c) → (MulOpposite.op a • s) • t = s • a • t
-- Init.Data.Float.Model.Float32
/-- The underlying bit pattern is valid according to the IEEE `binary32` format.  -/
Float32.Model.valid : ∀ (self : Float32.Model), Float.Model.Format.binary32.Valid self.toBits.toBitVec
-- Init.Data.Array.Lemmas
Array.swap_comm : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ} (hi : i < xs.size) (hj : j < xs.size), xs.swap i j hi hj = xs.swap j i hj hi
-- Mathlib.Topology.Separation.Regular
instRegularSpaceForall : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), RegularSpace (X i)],
  RegularSpace ((i : ι) → X i)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ D` creates limits of shape `Jᵒᵖ`, then `F.rightOp : C ⥤ Dᵒᵖ` creates colimits
of shape `J`.  -/
CategoryTheory.Limits.createsColimitsOfShapeRightOp : {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] →
            (F : CategoryTheory.Functor Cᵒᵖ D) →
              [CategoryTheory.CreatesLimitsOfShape Jᵒᵖ F] → CategoryTheory.CreatesColimitsOfShape J F.rightOp
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_alter_of_not_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 ↔ k' ∈ t)
-- Mathlib.RingTheory.RootsOfUnity.Basic
/-- Equivalence between the `k`-th roots of unity in `R` and the `k`-th roots of `1`.

This is implemented as equivalence of subtypes,
because `rootsOfUnity` is a subgroup of the group of units,
whereas `nthRoots` is a multiset.  -/
rootsOfUnityEquivNthRoots : (R : Type u_4) →
  (k : ℕ) →
    [NeZero k] →
      [inst : CommRing R] → [inst_1 : IsDomain R] → ↥(rootsOfUnity k R) ≃ { x // x ∈ Polynomial.nthRoots k 1 }
-- Mathlib.Data.Nat.SuccPred
Fin.covBy_iff : ∀ {n : ℕ} {a b : Fin n}, a ⋖ b ↔ ↑a ⋖ ↑b
-- Lean.Declaration
Lean.instBEqConstantVal.beq : Lean.ConstantVal → Lean.ConstantVal → Bool
-- Mathlib.Analysis.Normed.Group.Pointwise
Bornology.IsBounded.add : ∀ {E : Type u_1} [inst : SeminormedAddGroup E] {s t : Set E},
  Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s + t)
-- Mathlib.LinearAlgebra.TensorProduct.Basic
LinearMap.compr₂.congr_simp : ∀ {A : Type u_1} {R : Type u_2} [inst : Semiring A] [inst_1 : CommSemiring R] {M : Type u_5} {Nₗ : Type u_8}
  {Pₗ : Type u_9} {Qₗ : Type u_10} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid Nₗ] [inst_4 : AddCommMonoid Pₗ]
  [inst_5 : AddCommMonoid Qₗ] [inst_6 : Module R Nₗ] [inst_7 : Module R Pₗ] [inst_8 : Module R Qₗ]
  [inst_9 : Module A Pₗ] [inst_10 : SMulCommClass R A Pₗ] [inst_11 : Module R A] [inst_12 : Module A M]
  [inst_13 : Module A Qₗ] [inst_14 : SMulCommClass R A Qₗ] [inst_15 : IsScalarTower R A Qₗ]
  [inst_16 : IsScalarTower R A Pₗ] (f f_1 : M →ₗ[A] Nₗ →ₗ[R] Pₗ),
  f = f_1 → ∀ (g g_1 : Pₗ →ₗ[A] Qₗ), g = g_1 → f.compr₂ g = f_1.compr₂ g_1
-- Mathlib.RepresentationTheory.FDRep
FDRep.forget₂_ρ : ∀ {R : Type u} {G : Type v} [inst : CommRing R] [inst_1 : Monoid G] (V : FDRep R G),
  ((CategoryTheory.forget₂ (FDRep R G) (Rep.{u, u, v} R G)).obj V).ρ = V.ρ
-- Mathlib.Order.WellFoundedSet
IsAntichain.partiallyWellOrderedOn_iff : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α} [Std.Refl r], IsAntichain r s → (s.PartiallyWellOrderedOn r ↔ s.Finite)