mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.pre_post : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_3 : CategoryTheory.Category.{v', u'} D]
  (E : CategoryTheory.Functor K J) (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D)
  [inst_4 : CategoryTheory.Limits.HasLimit F] [inst_5 : CategoryTheory.Limits.HasLimit (E.comp F)]
  [inst_6 : CategoryTheory.Limits.HasLimit (F.comp G)] [h : CategoryTheory.Limits.HasLimit ((E.comp F).comp G)],
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.limit.pre F E))
      (CategoryTheory.Limits.limit.post (E.comp F) G) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.post F G)
      (CategoryTheory.Limits.limit.pre (F.comp G) E)
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.brecOn.eq : ∀ {α : Type u} {motive_1 : Lean.Widget.TaggedText α → Sort u_1} {motive_2 : Array (Lean.Widget.TaggedText α) → Sort u_1}
  {motive_3 : List (Lean.Widget.TaggedText α) → Sort u_1} (t : Lean.Widget.TaggedText α)
  (F_1 : (t : Lean.Widget.TaggedText α) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Widget.TaggedText α)) → Lean.Widget.TaggedText.below_1 t → motive_2 t)
  (F_3 : (t : List (Lean.Widget.TaggedText α)) → Lean.Widget.TaggedText.below_2 t → motive_3 t),
  t.brecOn F_1 F_2 F_3 = F_1 t (Lean.Widget.TaggedText.brecOn.go t F_1 F_2 F_3).2
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsAddFoelner.eventually_meas_ne_top : ∀ {G : Type u_4} {X : Type u_5} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_6} {l : Filter ι} {F : ι → Set X},
  IsAddFoelner G μ l F → ∀ᶠ (i : ι) in l, μ (F i) ≠ ⊤
-- Mathlib.Computability.EpsilonNFA
/-- `M.IsPath` represents a traversal in `M` from a start state to an end state by following a list
of transitions in order.  -/
εNFA.IsPath : {α : Type u} → {σ : Type v} → εNFA α σ → σ → σ → List (Option α) → Prop
-- Mathlib.RingTheory.Ideal.Maps
/-- A ring isomorphism sends a maximal ideal to a maximal ideal.  -/
Ideal.map_isMaximal_of_equiv : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {E : Type u_4} [inst_2 : EquivLike E R S]
  [RingEquivClass E R S] (e : E) {p : Ideal R} [hp : p.IsMaximal], (Ideal.map e p).IsMaximal
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.insertEntryIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k : α) (v : β k) (l : List ((a : α) × β a)),
  Std.Internal.List.insertEntryIfNew k v l = bif Std.Internal.List.containsKey k l then l else ⟨k, v⟩ :: l
-- Lean.DocString.Parser
/-- Parses mathematics.
 -/
Lean.Doc.Parser.math : Lean.Parser.ParserFn
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.congr_norm : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : α → E} {g : α → F},
  MeasureTheory.MemLp f p μ →
    MeasureTheory.AEStronglyMeasurable g μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖) → MeasureTheory.MemLp g p μ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {fallback : α},
  (t.insert k v).minKeyD fallback = t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k'
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.mem_adjoin_pair_left : ∀ (K : Type u_1) {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (x y : L), x ∈ K⟮x, y⟯
-- Mathlib.Algebra.Group.Shrink
equivShrink_sub : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Sub α] (x y : α),
  (equivShrink α) (x - y) = (equivShrink α) x - (equivShrink α) y
-- Init.Data.Option.Lemmas
Option.guard.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (a : α), Option.guard p a = if p a = true then some a else none
-- Mathlib.Order.Filter.Pointwise
/-- The filter `f +ᵥ g` is generated by `{s +ᵥ t | s ∈ f, t ∈ g}` in locale
`Pointwise`.  -/
Filter.instVAdd : {α : Type u_2} → {β : Type u_3} → [VAdd α β] → VAdd (Filter α) (Filter β)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.lintegral_mono_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f : MeasureTheory.SimpleFunc α ENNReal},
  μ ≤ ν → f.lintegral μ ≤ f.lintegral ν
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mul_nonempty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α}, (s * t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- The `Set` of edges of a walk.  -/
SimpleGraph.Walk.edgeSet : {V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → Set (Sym2 V)
-- Lean.Elab.Import
_private.Lean.Elab.Import.0.Lean.Elab.osForbiddenChars : Array Char
-- Lean.Data.DeclarationRange
Lean.DeclarationLocation.mk.inj : ∀ {module : Lean.Name} {range : Lean.DeclarationRange} {module_1 : Lean.Name} {range_1 : Lean.DeclarationRange},
  { module := module, range := range } = { module := module_1, range := range_1 } → module = module_1 ∧ range = range_1
-- Mathlib.Order.GaloisConnection.Defs
/-- Main property of a Galois insertion.  -/
GaloisInsertion.le_l_u : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
  (self : GaloisInsertion l u) (x : β), x ≤ l (u x)
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y Z T : C} {a₁ a₂ a₃ a₁₂ a₂₃ a : M} (α : CategoryTheory.ShiftedHom X Y a₁)
  (β : CategoryTheory.ShiftedHom Y Z a₂) (γ : CategoryTheory.ShiftedHom Z T a₃) (h₁₂ : a₂ + a₁ = a₁₂)
  (h₂₃ : a₃ + a₂ = a₂₃) (h : a₃ + a₂ + a₁ = a), (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, panicking if no such key exists.
 -/
Std.DTreeMap.Raw.getKeyLE! : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.DTreeMap.Raw α β cmp → α → α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k a : α}
  {v : β} {h₁ : a ∈ t.insertIfNew k v},
  (t.insertIfNew k v).getKey a h₁ = if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKey a ⋯
-- Mathlib.Algebra.Module.SpanRank
Submodule.lift_spanRank_le_iff_exists_span_set_card_le : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M)
  {a : Cardinal.{max u v}},
  Cardinal.lift.{v, u} p.spanRank ≤ a ↔ ∃ s, Cardinal.lift.{v, u} (Cardinal.mk ↑s) ≤ a ∧ Submodule.span R s = p
-- Init.Data.Array.QSort.Basic
_private.Init.Data.Array.QSort.Basic.0.Array.qsort.sort : {α : Type u_1} →
  (α → α → Bool) →
    {n : ℕ} →
      Vector α n →
        (lo hi : ℕ) →
          autoParam (lo ≤ hi) Array.qsort._auto_2✝ →
            autoParam (lo < n) Array.qsort._auto_4✝ → autoParam (hi < n) Array.qsort._auto_6✝ → Vector α n
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_zero : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : Zero R], HahnSeries.cardSupp 0 = 0
-- Init.Data.String.Lemmas.FindPos
String.Slice.posLT_eq_iff : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : 0 < p} {q : s.Pos},
  s.posLT p h = q ↔ q.offset < p ∧ ∀ (q' : s.Pos), q'.offset < p → q' ≤ q
-- Mathlib.RingTheory.Coalgebra.TensorProduct
Coalgebra.TensorProduct.assoc_toLinearEquiv : ∀ {R : Type u_5} {S : Type u_6} {M : Type u_7} {N : Type u_8} {P : Type u_9} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R P] [inst_9 : Module S M]
  [inst_10 : IsScalarTower R S M] [inst_11 : Coalgebra S M] [inst_12 : Module S N] [inst_13 : IsScalarTower R S N]
  [inst_14 : Coalgebra S N] [inst_15 : Coalgebra R P],
  (Coalgebra.TensorProduct.assoc R S M N P).toLinearEquiv = TensorProduct.AlgebraTensorModule.assoc R S S M N P
-- Init.Data.Range.Polymorphic.UInt
UInt16.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? UInt16
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableAt.inverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_5} [inst_3 : NormedRing R] [HasSummableGeomSeries R]
  [inst_5 : NormedAlgebra 𝕜 R] {h : E → R} {z : E},
  DifferentiableAt 𝕜 h z → IsUnit (h z) → DifferentiableAt 𝕜 (fun x => Ring.inverse (h x)) z
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.commute_of_mem_adjoin_singleton_of_commute : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {a b c : A},
  c ∈ R[b] → Commute a b → Commute a c
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.lanAdjunction_unit : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) (H : Type u_3)
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F], (L.lanAdjunction H).unit = L.lanUnit
-- Mathlib.MeasureTheory.Function.LpOrder
MeasureTheory.MemLp.abs : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  [inst : NormedAddCommGroup E] [inst_1 : Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] {f : α → E},
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp |f| p μ
-- Mathlib.SetTheory.ZFC.PSet
PSet.empty.eq_1 : PSet.empty = PSet.mk PEmpty.{u_1 + 1} PEmpty.elim
-- Init.Data.Vector.Range
Vector.toArray_range' : ∀ {start size step : ℕ}, (Vector.range' start size step).toArray = Array.range' start size step
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.Groupoid.isoEquivHom_symm_apply_hom : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (X Y : C) (f : X ⟶ Y),
  ((CategoryTheory.Groupoid.isoEquivHom X Y).symm f).hom = f
-- Mathlib.CategoryTheory.Yoneda
/-- the natural bijection `(X ⟶ Y) ≃ F.obj Y`.  -/
CategoryTheory.Functor.CorepresentableBy.homEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C (Type v)} → {X : C} → F.CorepresentableBy X → {Y : C} → (X ⟶ Y) ≃ F.obj Y
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_le_indicator_nonneg : ∀ {α : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : LinearOrder M] (s : Set α) (f : α → M),
  s.indicator f ≤ {a | 0 ≤ f a}.indicator f
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- Together `TrivSqZeroExt.detInvertibleOfInvertible` and `TrivSqZeroExt.invertibleOfDetInvertible`
form an equivalence, although both sides of the equiv are subsingleton anyway.  -/
TrivSqZeroExt.invertibleEquivInvertibleFst : {R : Type u} →
  {M : Type v} →
    [inst : AddCommGroup M] →
      [inst_1 : Semiring R] →
        [inst_2 : Module Rᵐᵒᵖ M] →
          [inst_3 : Module R M] → [SMulCommClass R Rᵐᵒᵖ M] → (x : TrivSqZeroExt R M) → Invertible x ≃ Invertible x.fst
-- Init.Data.List.Find
List.idxOf?_nil : ∀ {α : Type u_1} {a : α} [inst : BEq α], List.idxOf? a [] = none
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.prodMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {δ : Type u_3} [inst_3 : PseudoEMetricSpace δ] {f : α → β} {g : γ → δ},
  Isometry f → Isometry g → Isometry (Prod.map f g)
-- Mathlib.Order.Hom.Basic
OrderHomClass.toOrderHom.congr_simp : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : FunLike F α β]
  [inst_3 : OrderHomClass F α β] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Mathlib.CategoryTheory.Action.Monoidal
/-- When `V` is braided the forgetful functor `Action V G` to `V` is braided.  -/
Action.instBraidedForget : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) →
      [inst_1 : Monoid G] →
        [inst_2 : CategoryTheory.MonoidalCategory V] →
          [inst_3 : CategoryTheory.BraidedCategory V] → (Action.forget V G).Braided
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pos_of_mul_pos_left : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : Preorder α] [MulPosReflectLT α], 0 < a * b → 0 ≤ b → 0 < a
-- Mathlib.Topology.PartialHomeomorph.Basic
Topology.IsEmbedding.toPartialHomeomorph_left_inv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
  (h : Topology.IsEmbedding f) [inst_2 : Nonempty X] {x : X},
  ↑(Topology.IsEmbedding.toPartialHomeomorph f h).symm (f x) = x
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso_inv_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ : CategoryTheory.Arrow C) {W : C}
  [inst_3 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorRight W)],
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso X₁ X₂).inv.left =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.HasColimit.isoOfNatIso
          (CategoryTheory.Limits.spanExt (CategoryTheory.MonoidalCategoryStruct.associator X₁.left X₂.left W)
            (CategoryTheory.MonoidalCategoryStruct.associator X₁.right X₂.left W)
            (CategoryTheory.MonoidalCategoryStruct.associator X₁.left X₂.right W) ⋯ ⋯)).inv
      ⋯.isoPushout.inv
-- Init.Data.Repr
ReprTuple.reprTuple : {α : Type u} → [self : ReprTuple α] → α → List Std.Format → List Std.Format
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.limitsClosure_eq_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] [P.IsClosedUnderIsomorphisms]
  [∀ (a : α), P.IsClosedUnderLimitsOfShape (J a)], P.limitsClosure J = P
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafifyMap_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  (P : CategoryTheory.Functor Cᵒᵖ D),
  CategoryTheory.sheafifyMap J (CategoryTheory.CategoryStruct.id P) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.sheafify J P)
-- Mathlib.Order.Bounds.Basic
isLeast_univ_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsLeast Set.univ a ↔ IsBot a
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2to1.trStmts₁.match_1.splitter : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} →
      {σ : Type u_4} →
        (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5) →
          (x : Turing.TM2.Stmt Γ Λ σ) →
            ((k : K) → (f : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k f q)) →
              ((k : K) →
                  (f : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k f q)) →
                ((k : K) →
                    (f : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k f q)) →
                  ((a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q)) →
                    ((a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂)) →
                      ((x : Turing.TM2.Stmt Γ Λ σ) →
                          (∀ (k : K) (f : σ → Γ k) (q : Turing.TM2.Stmt Γ Λ σ),
                              x = Turing.TM2.Stmt.push k f q → False) →
                            (∀ (k : K) (f : σ → Option (Γ k) → σ) (q : Turing.TM2.Stmt Γ Λ σ),
                                x = Turing.TM2.Stmt.peek k f q → False) →
                              (∀ (k : K) (f : σ → Option (Γ k) → σ) (q : Turing.TM2.Stmt Γ Λ σ),
                                  x = Turing.TM2.Stmt.pop k f q → False) →
                                (∀ (a : σ → σ) (q : Turing.TM2.Stmt Γ Λ σ), x = Turing.TM2.Stmt.load a q → False) →
                                  (∀ (a : σ → Bool) (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ),
                                      x = Turing.TM2.Stmt.branch a q₁ q₂ → False) →
                                    motive x) →
                        motive x
-- Mathlib.Algebra.NoZeroSMulDivisors.Defs
IsAddTorsionFree.to_noZeroSMulDivisors_int : ∀ {G : Type u_3} [inst : AddGroup G] [IsAddTorsionFree G], NoZeroSMulDivisors ℤ G
-- Mathlib.Topology.UniformSpace.UniformEmbedding
/-- The lift of a complete space to another universe is still complete.  -/
ULift.instCompleteSpace : ∀ {α : Type u} [inst : UniformSpace α] [CompleteSpace α], CompleteSpace (ULift.{u_1, u} α)
-- Mathlib.Data.PNat.Factors
PrimeMultiset.coe_coeNatMonoidHom : ⇑PrimeMultiset.coeNatMonoidHom = PrimeMultiset.toNatMultiset
-- Mathlib.Algebra.Category.Ring.Limits
RingCat.limitRing : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J RingCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] →
        Ring (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget RingCat))).pt
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
WeakDual.gelfandTransform.congr_simp : ∀ (𝕜 : Type u_1) (A : Type u_2) [inst : CommRing 𝕜] [inst_1 : NoZeroDivisors 𝕜] [inst_2 : TopologicalSpace 𝕜]
  [inst_3 : IsTopologicalRing 𝕜] [inst_4 : TopologicalSpace A] [inst_5 : Semiring A] [inst_6 : Algebra 𝕜 A],
  WeakDual.gelfandTransform 𝕜 A = WeakDual.gelfandTransform 𝕜 A
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.instEssSurjAlgebraToMonadAdjComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C),
  (CategoryTheory.Monad.comparison T.adj).EssSurj
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.Hom.comp_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁.Hom S₂) (φ₂₃ : S₂.Hom S₃),
  (φ₁₂.comp φ₂₃).τ₂ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₂ φ₂₃.τ₂
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Construct a `NormalizedHom.cons` term in `m`.  -/
Mathlib.Tactic.BicategoryLike.NormalizedHom.consM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
      Mathlib.Tactic.BicategoryLike.NormalizedHom →
        Mathlib.Tactic.BicategoryLike.Atom₁ → m Mathlib.Tactic.BicategoryLike.NormalizedHom
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : Inhabited α] [inst_1 : EquivBEq α]
  [inst_2 : LawfulHashable α] {a : α}, m.contains a = false → m.get! a = default
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_sSup : ∀ (s : Set ENNReal), (sSup s)⁻¹ = ⨅ a ∈ s, a⁻¹
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.pow_inj_mod : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, IsOfFinOrder x → ∀ {n m : ℕ}, x ^ n = x ^ m ↔ n % orderOf x = m % orderOf x
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {t : Finset β}
  [inst : (a : α) → (b : β) → Decidable (r a b)],
  ∑ a ∈ s, (Finset.bipartiteAbove r t a).card = ∑ b ∈ t, (Finset.bipartiteBelow r s b).card
-- Mathlib.Algebra.Torsor.Defs
Equiv.constSMul.eq_1 : ∀ {G : Type u_1} (P : Type u_2) [inst : Group G] [inst_1 : Torsor G P] (v : G),
  Equiv.constSMul P v = { toFun := fun x => v • x, invFun := fun x => v⁻¹ • x, left_inv := ⋯, right_inv := ⋯ }
-- Std.Data.Iterators.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Combinators.Monadic.Drop.0.Std.Iterators.Types.Drop.ProductiveRel : {α β : Type w} →
  (m : Type w → Type w') →
    [inst : Std.Iterator α m β] → [Std.Iterators.Productive α m] → Std.IterM m β → Std.IterM m β → Prop
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedTheoremGuard.default : Lean.Meta.Grind.TheoremGuard
-- Mathlib.Data.List.Defs
/-- Auxiliary definition for `mapIdxM'`.  -/
List.mapIdxMAux' : {m : Type v → Type w} → [Monad m] → {α : Type u_7} → (ℕ → α → m PUnit.{v + 1}) → ℕ → List α → m PUnit.{v + 1}
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- `sinh` is injective, `∀ a b, sinh a = sinh b → a = b`.  -/
Real.sinh_injective : Function.Injective Real.sinh
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.Monic.irreducible_of_degree_eq_one : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] {p : Polynomial R}, p.degree = 1 → p.Monic → Irreducible p
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.lift_residue_apply : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : Field S] (f : R →+* S)
  [inst_3 : IsLocalHom f] (x : R), (IsLocalRing.ResidueField.lift f) ((IsLocalRing.residue R) x) = f x
-- Init.Data.List.Monadic
/-- This lemma identifies monadic maps over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
 -/
List.mapM_subtype : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {p : α → Prop}
  {l : List { x // p x }} {f : { x // p x } → m β} {g : α → m β},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → List.mapM f l = List.mapM g l.unattach
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.reverse_surjective : ∀ {n : ℕ}, Function.Surjective Composition.reverse
-- Mathlib.Topology.Instances.NNReal.Lemmas
Real.iSup_pow_of_ne_zero : ∀ {ι : Sort u_1} {n : ℕ} {f : ι → ℝ}, (∀ (i : ι), 0 ≤ f i) → n ≠ 0 → (⨆ i, f i) ^ n = ⨆ i, f i ^ n
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.sphere.instHasDistribNeg : {𝕜 : Type u_1} →
  [inst : SeminormedRing 𝕜] → [inst_1 : NormMulClass 𝕜] → [inst_2 : NormOneClass 𝕜] → HasDistribNeg ↑(Metric.sphere 0 1)
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.symm_iff : ∀ {S : Type u_3} [inst : Add S] {a b : S}, AddCommute a b ↔ AddCommute b a
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.finite : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.EssFiniteType R S], Module.Finite S Ω[S⁄R]
-- Mathlib.Data.Fintype.Card
/-- If two subtypes of a fintype have equal cardinality, so do their complements.  -/
Fintype.card_compl_eq_card_compl : ∀ {α : Type u_1} [Finite α] (p q : α → Prop) [inst : Fintype { x // p x }] [inst_1 : Fintype { x // ¬p x }]
  [inst_2 : Fintype { x // q x }] [inst_3 : Fintype { x // ¬q x }],
  Fintype.card { x // p x } = Fintype.card { x // q x } → Fintype.card { x // ¬p x } = Fintype.card { x // ¬q x }
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
rothNumberNat_def : ∀ (n : ℕ), rothNumberNat n = addRothNumber (Finset.range n)
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsMinor.trans_isStrictMinor : ∀ {α : Type u_1} {M M' N : Matroid α}, N ≤m M → M <m M' → N <m M'