mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
ergodic_add_left_of_denseRange_zsmul : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [SecondCountableTopology G] [BorelSpace G] {g : G},
  (DenseRange fun x => x • g) →
    ∀ (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [μ.IsAddLeftInvariant],
      Ergodic (fun x => g + x) μ
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
/-- If `P` is a submersive presentation, `H¹` of the associated cotangent complex vanishes.  -/
Algebra.SubmersivePresentation.subsingleton_h1Cotangent : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ),
  Subsingleton P.toExtension.H1Cotangent
-- Mathlib.Algebra.Category.Ring.Constructions
CategoryTheory.Iso.commRingCatIsoToRingEquiv.eq_1 : ∀ {R S : CommRingCat} (e : R ≅ S),
  e.commRingCatIsoToRingEquiv = RingEquiv.ofRingHom (CommRingCat.Hom.hom e.hom) (CommRingCat.Hom.hom e.inv) ⋯ ⋯
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanRank_span_of_linearIndepOn : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [RankCondition R]
  (s : Set M), LinearIndepOn R id s → (Submodule.span R s).spanRank = Cardinal.mk ↑s
-- Mathlib.Order.Category.HeytAlg
HeytAlg.ofHom_comp : ∀ {X Y Z : Type u} [inst : HeytingAlgebra X] [inst_1 : HeytingAlgebra Y] [inst_2 : HeytingAlgebra Z]
  (f : HeytingHom X Y) (g : HeytingHom Y Z),
  HeytAlg.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (HeytAlg.ofHom f) (HeytAlg.ofHom g)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- One can prove `AddQuotientMeasureEqMeasurePreimage` by checking behavior with
respect to a single additive fundamental domain.  -/
MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α ν] [Countable G] [MeasurableConstVAdd G α]
  {μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))} {s : Set α},
  MeasureTheory.IsAddFundamentalDomain G s ν →
    μ = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict s) →
      MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ
-- Mathlib.Data.Nat.Nth
Nat.gc_count_nth : ∀ {p : ℕ → Prop} [inst : DecidablePred p], (Set.ofPred p).Infinite → GaloisConnection (Nat.count p) (Nat.nth p)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply : ∀ {n : ℕ} {K : Type u} [inst : Field K] {ζ : K} [inst_1 : NeZero n] [inst_2 : CharZero K]
  [inst_3 : IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n) (a : NumberField.RingOfIntegers K),
  hζ.adjoinEquivRingOfIntegers.symm a = (IsIntegralClosure.lift ℤ (↥ℤ[ζ]) K) a
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapM.match_1.eq_2 : ∀ {β β' : Type u_1} {n : Type u_1 → Type u_2} {f : β → n (Option β')} [inst : MonadAttach n] (out : β)
  (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) (out' : β')
  (hf : MonadAttach.CanReturn (f out) (some out')) (h_1 : (hf : MonadAttach.CanReturn (f out) none) → motive ⟨none, hf⟩)
  (h_2 : (out' : β') → (hf : MonadAttach.CanReturn (f out) (some out')) → motive ⟨some out', hf⟩),
  (match ⟨some out', hf⟩ with
    | ⟨none, hf⟩ => h_1 hf
    | ⟨some out', hf⟩ => h_2 out' hf) =
    h_2 out' hf
-- Init.Data.BitVec.Bitblast
BitVec.ushiftRightRec_zero : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂), x.ushiftRightRec y 0 = x >>> (y &&& BitVec.twoPow w₂ 0)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_erase_eq_of_not_compare_eq_maxKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α},
  (∀ {km : α}, t.maxKey? = some km → ¬compare k km = Ordering.eq) →
    (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.maxKey? = t.maxKey?
-- Mathlib.Data.Set.Basic
/-- Given a predicate `p : α → Prop`, produces an equivalence between
`Set {a : α // p a}` and `{s : Set α // ∀ a ∈ s, p a}`.  -/
Equiv.setSubtypeComm : {α : Type u_1} → (p : α → Prop) → Set { a // p a } ≃ { s // ∀ a ∈ s, p a }
-- Init.Sym.DSimp.DSimprocDSL
Lean.Parser.Category.sym_dsimproc : Lean.Parser.Category
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of `ValuativeRel.mul_vlt_mul_left`.

---

**Alias** of the reverse direction of `ValuativeRel.mul_vlt_mul_iff_left`. -/
ValuativeRel.vlt_mul_right : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, 0 <ᵥ z → x <ᵥ y → x * z <ᵥ y * z
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.mem_span_singleton_self : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M), x ∈ R ∙ x
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'_eq_find : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  [inst_3 : DecidablePred fun n => ∀ (k : ℕ), Ideal.map (algebraMap R S) p ≤ P ^ k → k ≤ n]
  (h : ∃ n, ∀ (k : ℕ), Ideal.map (algebraMap R S) p ≤ P ^ k → k ≤ n), p.ramificationIdx' P = Nat.find h
-- Mathlib.Data.Bool.Basic
Bool.not_ne_id : not ≠ id
-- Lean.Parser.Extra
Lean.Parser.optional.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.ker_toSpecΓ : ∀ (X : AlgebraicGeometry.Scheme) [CompactSpace ↥X], AlgebraicGeometry.Scheme.Hom.ker X.toSpecΓ = ⊥
-- Mathlib.RingTheory.Congruence.Defs
RingConGen.Rel.below.symm : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop}
  {motive : (a a_1 : R) → RingConGen.Rel r a a_1 → Prop} {x y : R} (a : RingConGen.Rel r x y),
  RingConGen.Rel.below a → motive x y a → RingConGen.Rel.below ⋯
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- This is [grinberg_clifford_2016] Theorem 13  -/
CliffordAlgebra.contractRight_contractRight : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (d : Module.Dual R M) (x : CliffordAlgebra Q),
  (CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d)) d = 0
-- Mathlib.Algebra.Homology.ModelCategory.Injective
/-- The Quillen model category structure on the category `CochainComplex.Plus C`
of bounded below cochain complexes in an abelian category `C` with enough injectives.  -/
CochainComplex.Plus.modelCategoryQuillen.instModelCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [CategoryTheory.EnoughInjectives C] → HomotopicalAlgebra.ModelCategory (CochainComplex.Plus C)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.forget₂AddMon_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.AddGrp C} (f : A ⟶ B), ((CategoryTheory.AddGrp.forget₂Mon C).map f).hom = f.hom.hom
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- An algebraically closed field is one where every polynomial splits. Equivalently, all
non-constant polynomials have a root. See `IsAlgClosed.exists_root` and
`IsAlgClosed.of_exists_root`.  -/
IsAlgClosed : (k : Type u) → [Field k] → Prop
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.adjp_none_none : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ)
  (A : Matrix (Option n) (Option n) R), Matrix.adjp s A none none = Matrix.detp s (A.submatrix some some)
-- Mathlib.Algebra.Group.ULift
ULift.neg_down : ∀ {α : Type u} {x : ULift.{w, u} α} [inst : Neg α], (-x).down = -x.down
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- This lemma is superseded by `MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm` where we
allow `p = ∞`.  -/
MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  {f : ι → α → E} {g : α → E} [inst : SeminormedAddCommGroup E],
  p ≠ 0 →
    p ≠ ⊤ →
      (∀ (n : ι), MeasureTheory.AEStronglyMeasurable (f n) μ) →
        MeasureTheory.AEStronglyMeasurable g μ →
          ∀ {l : Filter ι},
            Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) l (nhds 0) →
              MeasureTheory.TendstoInMeasure μ f l g
-- Mathlib.Algebra.Module.Submodule.Range
/-- If `N ⊆ M` then submodules of `N` are the same as submodules of `M` contained in `N`.  -/
Submodule.mapIic : {R : Type u_1} →
  {M : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (p : Submodule R M) → Submodule R ↥p ≃o ↑(Set.Iic p)
-- Mathlib.Order.Antisymmetrization
/-- **Alias** of `not_lt_of_antisymmRel`. -/
AntisymmRel.not_lt : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → ¬a < b
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.trans_refl : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
  e.trans (LinearEquiv.refl S M₂) = e
-- Mathlib.Algebra.Ring.Opposite
RingHom.unop.eq_1 : ∀ {R : Type u_2} {S : Type u_3} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S],
  RingHom.unop = RingHom.op.symm
-- Init.Data.SInt.Lemmas
Int64.toInt8_neg : ∀ (x : Int64), (-x).toInt8 = -x.toInt8
-- Mathlib.Analysis.Calculus.TangentCone.Pi
UniqueDiffWithinAt.pi : ∀ {𝕜 : Type u_1} [inst : DivisionSemiring 𝕜] {ι : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (E i)]
  [inst_2 : (i : ι) → Module 𝕜 (E i)] [inst_3 : TopologicalSpace 𝕜] [(nhdsWithin 0 {0}ᶜ).NeBot]
  [inst_5 : (i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousAdd (E i)] [∀ (i : ι), ContinuousSMul 𝕜 (E i)]
  {s : (i : ι) → Set (E i)} {x : (i : ι) → E i} {I : Set ι},
  (∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)) → UniqueDiffWithinAt 𝕜 (I.pi s) x
-- Mathlib.RingTheory.Smooth.Locus
Algebra.smoothLocus_eq_univ_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FinitePresentation R A], Algebra.smoothLocus R A = Set.univ ↔ Algebra.FormallySmooth R A
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkInjectiveTheoremTypeCore?.mkArgs2.match_1.eq_2 : ∀ (motive : Lean.Expr → Sort u_1) (x : Lean.Expr)
  (h_1 :
    (n : Lean.Name) → (d b : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE n d b binderInfo))
  (h_2 : (x : Lean.Expr) → motive x),
  (∀ (n : Lean.Name) (d b : Lean.Expr) (binderInfo : Lean.BinderInfo), x = Lean.Expr.forallE n d b binderInfo → False) →
    (match x with
      | Lean.Expr.forallE n d b binderInfo => h_1 n d b binderInfo
      | x => h_2 x) =
      h_2 x
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.extendHom`.

---

There is a morphism from a cocone to its extension.  -/
CategoryTheory.Limits.Cocones.extend : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (s : CategoryTheory.Limits.Cocone F) → {X : C} → (f : s.pt ⟶ X) → s ⟶ s.extend f
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.eq_6 : ∀ (a b : Lean.Grind.CommRing.Expr), (a.mul b).toPoly = a.toPoly.mul b.toPoly
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.instBEqOfLawfulEqCmp : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.LawfulEqCmp cmp] → [(k : α) → BEq (β k)] → BEq (Std.DTreeMap.Raw α β cmp)
-- Mathlib.GroupTheory.NoncommPiCoprod
AddSubgroup.noncommPiCoprod.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} [inst_1 : Fintype ι]
  (hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y),
  AddSubgroup.noncommPiCoprod hcomm = AddMonoidHom.noncommPiCoprod (fun i => (H i).subtype) ⋯
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertMax.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (t : Std.DTreeMap.Internal.Impl α β) (hl : t.Balanced),
  Std.DTreeMap.Internal.Impl.insertMax k v t hl =
    match t, hl with
    | Std.DTreeMap.Internal.Impl.leaf, hl =>
      { impl := Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf,
        balanced_impl := ⋯, size_impl := ⋯ }
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hl =>
      match Std.DTreeMap.Internal.Impl.insertMax k v r' ⋯ with
      | { impl := r'', balanced_impl := hr''₁, size_impl := hr''₂ } =>
        { impl := Std.DTreeMap.Internal.Impl.balanceR k' v' l' r'' ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ }
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_natCast_mul : ∀ {x : ℝ} (m : ℕ), Irrational (↑m * x) → Irrational x
-- Lean.IdentifierSuggestion
_private.Lean.IdentifierSuggestion.0.Lean.identifierSuggestionsImpl : Lean.PersistentEnvExtension (Lean.Name × Array Lean.Name) (Lean.Name × Array Lean.Name) (Lean.NameMap Lean.NameSet) ×
  Lean.PersistentEnvExtension (Lean.Name × Array Lean.Name) (Lean.Name × Array Lean.Name) (Lean.NameMap Lean.NameSet)
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.zsmul_natCast_eq_nsmul : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] (n : ℕ) (a : Lean.Grind.IntModule.OfNatModule.Q α),
  Lean.Grind.IntModule.OfNatModule.zsmul (↑n) a = Lean.Grind.IntModule.OfNatModule.nsmul n a
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w))
  (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)),
  ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.obj X).fst = X.base
-- Mathlib.Algebra.Order.GroupWithZero.Submonoid
Submonoid.mem_pos : ∀ {α : Type u_1} [inst : MulZeroOneClass α] [inst_1 : PartialOrder α] [inst_2 : PosMulStrictMono α]
  [inst_3 : ZeroLEOneClass α] [inst_4 : NeZero 1] {a : α}, a ∈ Submonoid.pos α ↔ 0 < a
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.ιTotal.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), K.ιTotal c₁₂ i₁ i₂ i₁₂ h = K.ιTotal c₁₂ i₁ i₂ i₁₂ h
-- Mathlib.Data.Finset.Dedup
/-- `toFinset l` removes duplicates from the list `l` to produce a finset.  -/
List.toFinset : {α : Type u_1} → [DecidableEq α] → List α → Finset α
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsInaccessible.preOmega_ord : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible → Ordinal.preOmega c.ord = c.ord
-- Mathlib.Dynamics.TopologicalEntropy.Subset
/-- Topological entropy `CoverEntropy T` as a `SupBotHom` function of the subset.  -/
Dynamics.coverEntropySupBotHom : {X : Type u_1} → [UniformSpace X] → (X → X) → SupBotHom (Set X) EReal
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_le_iff_inv_le : ∀ {a b : ENNReal}, a⁻¹ ≤ b ↔ b⁻¹ ≤ a
-- Mathlib.CategoryTheory.Limits.Cones
/-- The isomorphism between a cocone on `F` and an element of the functor `F.cocones`.  -/
CategoryTheory.Limits.Cocone.equiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) → CategoryTheory.Limits.Cocone F ≅ (X : C) × F.cocones.obj X
-- Mathlib.Analysis.Normed.Group.Hom
exists_pos_bound_of_bound : ∀ {V : Type u_1} {W : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W] {f : V → W}
  (M : ℝ), (∀ (x : V), ‖f x‖ ≤ M * ‖x‖) → ∃ N, 0 < N ∧ ∀ (x : V), ‖f x‖ ≤ N * ‖x‖
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.ExactPairing.evaluation_coevaluation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  [inst_2 : CategoryTheory.ExactPairing X Y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (η_ X Y) X)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y X).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (ε_ X Y))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v).getKey k ⋯ = k
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.instCreatesColimitsPresheafedSpaceForgetToPresheafedSpaceOfHasLimits : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasLimits C] →
      CategoryTheory.CreatesColimits AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace
-- Mathlib.Algebra.Homology.Embedding.Boundary
/-- The lower boundary of an embedding `e : Embedding c c'`, as a predicate on `ι`.
It is satisfied by `j : ι` when there exists `i' : ι'` not in the image of `e.f`
such that `c'.Rel i' (e.f j)`.  -/
ComplexShape.Embedding.BoundaryGE : {ι : Type u_1} → {ι' : Type u_2} → {c : ComplexShape ι} → {c' : ComplexShape ι'} → c.Embedding c' → ι → Prop
-- Mathlib.Data.List.Sym
List.Sublist.sym2 : ∀ {α : Type u_1} {xs ys : List α}, xs.Sublist ys → xs.sym2.Sublist ys.sym2
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instNontrivialOfNonempty : ∀ {α : Type u_1} [inst : TopologicalSpace α] [Nonempty α], Nontrivial (TopologicalSpace.Compacts α)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.self_trans_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (e : M ≃ₜ+ N), e.trans e.symm = ContinuousAddEquiv.refl M
-- Init.Prelude
Nat.zero_lt_succ : ∀ (n : ℕ), 0 < n.succ
-- Lean.Parser.Term
Lean.Parser.Term.privateDecl.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.List.Lemmas
List.flatten_eq_append_iff : ∀ {α : Type u_1} {xss : List (List α)} {ys zs : List α},
  xss.flatten = ys ++ zs ↔
    (∃ as bs, xss = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
      ∃ as bs c cs ds, xss = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ zs = c :: cs ++ ds.flatten
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.fundamentalSequence.match_1.eq_2 : ∀ (motive : Option ONote ⊕ (ℕ → ONote) → ℕ → Sort u_1) (m : ℕ) (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, m.succ 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_2 m
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.IsStandardSmooth.localization_away : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [IsLocalization.Away r S], Algebra.IsStandardSmooth R S
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
/-- The obvious functor `(J ⥤ ShortComplex C) ⥤ ShortComplex (J ⥤ C)`.  -/
CategoryTheory.ShortComplex.FunctorEquivalence.inverse : (J : Type u_1) →
  (C : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          CategoryTheory.Functor (CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
            (CategoryTheory.ShortComplex (CategoryTheory.Functor J C))
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.IsDescendingCentralSeries.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : ℕ → AddSubgroup G),
  AddSubgroup.IsDescendingCentralSeries H = (H 0 = ⊤ ∧ ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1))
-- Mathlib.Order.Monotone.Defs
Subsingleton.antitone : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] [Subsingleton α] (f : α → β), Antitone f
-- Mathlib.Data.ENat.Basic
/-- **Alias** of the reverse direction of `ENat.natCast_toNat_eq_self`. -/
ENat.natCast_toNat : ∀ {n : ℕ∞}, n ≠ ⊤ → ↑n.toNat = n
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.directive.withFence : ℕ →
  (Lean.SourceInfo → String → Lean.Parser.ParserFn) →
    Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.TriggerCondition.accept.injEq : ∀ {ctx : Type u_1} (context context_1 : ctx),
  (Mathlib.TacticAnalysis.TriggerCondition.accept context = Mathlib.TacticAnalysis.TriggerCondition.accept context_1) =
    (context = context_1)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter_apply_pos : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] {p : ι → Prop} [inst_1 : DecidablePred p]
  (f : Π₀ (i : ι), β i) {i : ι}, p i → (DFinsupp.filter p f) i = f i
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.forget₂_commAlgCat_map : ∀ {R : Type u} [inst : CommRing R] {A B : CommBialgCat R} (f : A ⟶ B),
  (CategoryTheory.forget₂ (CommBialgCat R) (CommAlgCat R)).map f = CommAlgCat.ofHom ↑(CommBialgCat.Hom.hom f)
-- Mathlib.Algebra.Group.TransferInstance
Equiv.smul_def : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : SMul M β] (n : M) (x : α), n • x = e.symm (n • e x)
-- Init.Data.UInt.Basic
UInt8.modn : UInt8 → ℕ → UInt8
-- Mathlib.Algebra.Field.Defs
/-- A `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  -/
Field : Type u → Type u
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
unitInterval.sigmoid_injective : Function.Injective unitInterval.sigmoid
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.CongrCache : Type
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} {c : C} (i : c ⟶ b) (h : c ⟶ a)
  (hi : CategoryTheory.CategoryStruct.comp (F.map i) f' = CategoryTheory.CategoryStruct.comp (F.map h) g)
  [inst_2 : F.Full], hf'.lift' i h hi = hf'.lift (F.map i) h hi
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.coeff_div : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  (f : PowerSeries A) [inst_1 : IsPrecomplete I A] (i : ℕ), (PowerSeries.coeff i) (H.div f) = ↑(H.divCoeff f i)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_sub : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {S : Subalgebra R A}
  (x y : ↥S), ↑(x - y) = ↑x - ↑y