mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instIsLeftCancelMul : ∀ {α : Type u_1} [inst : Mul α] [IsRightCancelMul α], IsLeftCancelMul αᵐᵒᵖ
-- Mathlib.Analysis.Complex.Trigonometric
/-- The complex sine function, defined via `exp`  -/
Complex.sin : ℂ → ℂ
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.piLE.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {X : ι → Type u_4} [inst_1 : (i : ι) → MeasurableSpace (X i)],
  MeasureTheory.Filtration.piLE =
    { seq := fun i => MeasurableSpace.comap (Preorder.restrictLe i) MeasurableSpace.pi, mono' := ⋯, le' := ⋯ }
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.limitConeIsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrpCat)).sections],
  AddCommGrpCat.limitConeIsLimit F =
    CategoryTheory.liftedLimitIsLimit
      (CategoryTheory.Limits.limit.isLimit (F.comp (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)))
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.symm_i₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A),
  P.symm.i₁ = P.i₀
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_toENat_le : ∀ (a : Cardinal.{u_1}), ↑(Cardinal.toENat a) ≤ a
-- Std.Internal.UV.System
/-- Gets the hostname of the machine.
 -/
Std.Internal.UV.System.osGetHostname : IO String
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.sigmaToPi_mk_basicOpen : ∀ {ι : Type u_1} {R : ι → Type u_2} [inst : (i : ι) → CommRing (R i)] [inst_1 : DecidableEq ι] (i : ι) (f : R i),
  PrimeSpectrum.sigmaToPi R '' Sigma.mk i '' ↑(PrimeSpectrum.basicOpen f) = ↑(PrimeSpectrum.basicOpen (Pi.single i f))
-- Mathlib.SetTheory.Ordinal.Enum
_private.Mathlib.SetTheory.Ordinal.Enum.0.Ordinal.enumOrd.eq_def : ∀ (s : Set Ordinal.{u}) (o : Ordinal.{u}), Ordinal.enumOrd s o = sInf (s ∩ {b | ∀ c < o, Ordinal.enumOrd s c < b})
-- Mathlib.Topology.UniformSpace.Cauchy
Cauchy.ultrafilter_of : ∀ {α : Type u} [uniformSpace : UniformSpace α] {l : Filter α} (h : Cauchy l), Cauchy ↑(Ultrafilter.of l)
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafAdjunction_homEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : CategoryTheory.Functor Cᵒᵖ A} {M : A}
  (f : Φ.presheafFiber.obj P ⟶ M), (Φ.skyscraperPresheafAdjunction.homEquiv P M) f = Φ.skyscraperPresheafHomEquiv f
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Harmonicity is an open property.
 -/
InnerProductSpace.isOpen_setOfPred_harmonicAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] (f : E → F),
  IsOpen {x | InnerProductSpace.HarmonicAt f x}
-- Mathlib.Combinatorics.Enumerative.Partition.GenFun
/-- Alternative form of `summable_genFun_term` that unshifts the first index.  -/
Nat.Partition.summable_genFun_term' : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] (f : ℕ → ℕ → R) {i : ℕ},
  i ≠ 0 → Summable fun j => f i (j + 1) • PowerSeries.X ^ (i * (j + 1))
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.id_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F),
  (CategoryTheory.CategoryStruct.id A).val = CategoryTheory.CategoryStruct.id A.obj
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_eq_last_iff : ∀ {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)},
  a ≠ Fin.last (n + 1) → (a.succAbove b = Fin.last (n + 1) ↔ b = Fin.last n)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.inv_uIcc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] (a b : α),
  (Set.uIcc a b)⁻¹ = Set.uIcc a⁻¹ b⁻¹
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.ε_tensorHom_comp_μ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] {X : C} {Y : D} (f : Y ⟶ F.obj X) {Z : D}
  (h :
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Functor.LaxMonoidal.ε F) f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv) h))
-- Mathlib.Algebra.Notation.Prod
Prod.add_def : ∀ {M : Type u_8} {N : Type u_9} [inst : Add M] [inst_1 : Add N] (p q : M × N), p + q = (p.1 + q.1, p.2 + q.2)
-- Aesop.RuleTac.RuleTerm
Aesop.ElabRuleTerm : Type
-- Lean.DocString.Types
Lean.Doc.Block.brecOn.go : {i : Type u} →
  {b : Type v} →
    {motive_1 : Lean.Doc.Block i b → Sort u_1} →
      {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
        {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
          {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1} →
            {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
              {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
                {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} →
                  {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1} →
                    {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1} →
                      (t : Lean.Doc.Block i b) →
                        ((t : Lean.Doc.Block i b) → t.below → motive_1 t) →
                          ((t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                              Lean.Doc.Block.below_1 t → motive_2 t) →
                            ((t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                Lean.Doc.Block.below_2 t → motive_3 t) →
                              ((t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t) →
                                ((t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                                    Lean.Doc.Block.below_4 t → motive_5 t) →
                                  ((t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                      Lean.Doc.Block.below_5 t → motive_6 t) →
                                    ((t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t) →
                                      ((t : Lean.Doc.ListItem (Lean.Doc.Block i b)) →
                                          Lean.Doc.Block.below_7 t → motive_8 t) →
                                        ((t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) →
                                            Lean.Doc.Block.below_8 t → motive_9 t) →
                                          motive_1 t ×' t.below
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.range_toLinearMap : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂),
  Set.range ⇑↑f = Set.range ⇑f
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
/-- `extremalNumber (card V) H` is greater than `x` if and only if there exists a `H`-free simple
graph `G` with more than `x` edges.  -/
SimpleGraph.lt_extremalNumber_iff : ∀ {V : Type u_1} {W : Type u_2} [inst : Fintype V] (H : SimpleGraph W) (m : ℕ),
  m < SimpleGraph.extremalNumber (Fintype.card V) H ↔ ∃ G x, H.Free G ∧ m < G.edgeFinset.card
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.Functor.toCostructuredArrow_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C)
  (F : CategoryTheory.Functor C D) (X : D) (f : (Y : E) → F.obj (G.obj Y) ⟶ X)
  (h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (F.map (G.map g)) (f Z) = f Y) (Y : E),
  (G.toCostructuredArrow F X f h).obj Y = CategoryTheory.CostructuredArrow.mk (f Y)
-- Init.Data.String.Basic
ByteArray.validateUTF8.go : (b : ByteArray) → (i : ℕ) → i ≤ b.size → Bool
-- Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Complex.measurableEquivRealProd_symm_apply : ∀ (p : ℝ × ℝ), Complex.measurableEquivRealProd.symm p = { re := p.1, im := p.2 }
-- Mathlib.Order.UpperLower.Relative
IsRelLowerSet.union : ∀ {α : Type u_1} {s t : Set α} {P : α → Prop} [inst : LE α],
  IsRelLowerSet s P → IsRelLowerSet t P → IsRelLowerSet (s ∪ t) P
-- Mathlib.Logic.Equiv.Prod
/-- `PUnit` is a right identity for type product up to an equivalence.  -/
Equiv.prodPUnit : (α : Type u_9) → α × PUnit.{u_10 + 1} ≃ α
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- A fraction `r /ₒ s` is equal to its expansion by an arbitrary factor `t` if `t * s ∈ S`.  -/
OreLocalization.expand : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] (r : X) (s : ↥S) (t : R) (hst : t * ↑s ∈ S), r /ₒ s = t • r /ₒ ⟨t * ↑s, hst⟩
-- Batteries.Data.List.Lemmas
List.countPBefore.go.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (s : ℕ) (head : α) (tail : List α), List.countPBefore.go p (head :: tail) 0 s = s
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- Closed intervals `Set.Icc (x - ε) (x + ε)`, `ε ≠ 0`, form a basis of neighborhoods of an
extended nonnegative real number `x ≠ ∞`. We use `Set.Icc` instead of `Set.Ioo` because this way the
statement works for `x = 0`.
 -/
ENNReal.hasBasis_nhds_of_ne_top' : ∀ {x : ENNReal}, x ≠ ⊤ → (nhds x).HasBasis (fun x => x ≠ 0) fun ε => Set.Icc (x - ε) (x + ε)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegralClosure.mk'_zero : ∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] (h : optParam (IsIntegral R 0) ⋯),
  IsIntegralClosure.mk' A 0 h = 0
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- The right homology data on a short complex equipped with a splitting.  -/
CategoryTheory.ShortComplex.Splitting.rightHomologyData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} → [CategoryTheory.Limits.HasZeroObject C] → S.Splitting → S.RightHomologyData
-- Mathlib.Topology.Spectral.Hom
IsSpectralMap.toContinuous : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  IsSpectralMap f → Continuous f
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.splitMonoBiproductComparison'_retraction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁}
  (F : CategoryTheory.Functor C D) (f : J → C) [inst_4 : CategoryTheory.Limits.HasBiproduct f]
  [inst_5 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] [inst_6 : F.PreservesZeroMorphisms],
  (F.splitMonoBiproductComparison' f).retraction = F.biproductComparison f
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.cancel_left : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : MulOne P] {g : N →* P}
  {f₁ f₂ : M →* N}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Order.Filter.Map
Filter.disjoint_map : ∀ {α : Type u_1} {β : Type u_2} {m : α → β},
  Function.Injective m → ∀ {f₁ f₂ : Filter α}, Disjoint (Filter.map m f₁) (Filter.map m f₂) ↔ Disjoint f₁ f₂
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.Hom.id_toFun : ∀ (X : Pointed) (a : X.X), (Pointed.Hom.id X).toFun a = id a
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.transfer_transfer : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet)
  {K : SimpleGraph V} (hp' : ∀ e ∈ (p.transfer H hp).edges, e ∈ K.edgeSet),
  (p.transfer H hp).transfer K hp' = p.transfer K ⋯
-- Mathlib.Order.SupClosed
IsSublattice.infClosed : ∀ {α : Type u_3} [inst : Lattice α] {s : Set α}, IsSublattice s → InfClosed s
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.subst.sizeOf_spec : ∀ (x : Lean.Grind.Linarith.Var) (c₁ c₂ : Lean.Meta.Grind.Arith.Linear.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.EqCnstrProof.subst x c₁ c₂) = 1 + sizeOf x + sizeOf c₁ + sizeOf c₂
-- Mathlib.Order.Sublattice
Sublattice.gc_map_comap : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β),
  GaloisConnection (Sublattice.map f) (Sublattice.comap f)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The norm of `x` is `∏ w, (normAtPlace x) ^ mult w`. It is defined such that the norm of
`mixedEmbedding K a` for `a : K` is equal to the absolute value of the norm of `a` over `ℚ`,
see `norm_eq_norm`.  -/
NumberField.mixedEmbedding.norm : {K : Type u_1} → [inst : Field K] → [NumberField K] → NumberField.mixedEmbedding.mixedSpace K →*₀ ℝ
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapIso_functor_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (i : S ≅ S')
  {X Y : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T} (f : X ⟶ Y),
  ((CategoryTheory.StructuredArrow.mapIso i).functor.map f).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.comp_app : ∀ {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Init.Data.Int.DivMod.Lemmas
Int.mul_fdiv_assoc : ∀ (a : ℤ) {b c : ℤ}, c ∣ b → (a * b).fdiv c = a * b.fdiv c
-- Mathlib.Topology.ContinuousOn
ContinuousOn.image_comp_continuous : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set α},
  ContinuousOn g (f '' s) → Continuous f → ContinuousOn (g ∘ f) s
-- Mathlib.RepresentationTheory.Basic
Representation.asGroupHom.eq_1 : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Group G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V), ρ.asGroupHom = MonoidHom.toHomUnits ρ
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop_bot : ∀ {M : Type u_2} [inst : AddZeroClass M], ⊥.unop = ⊥
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.State.exprToNCRingId : Lean.Meta.Grind.Arith.CommRing.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ
-- Mathlib.Algebra.GCDMonoid.Basic
/-- `0` is right-absorbing.  -/
GCDMonoid.lcm_zero_right : ∀ {α : Type u_2} {inst : CommMonoidWithZero α} [self : GCDMonoid α] (a : α), lcm a 0 = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ZeroExtend
Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go_denote_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (w : ℕ) (input : aig.RefVec w)
  (newWidth curr : ℕ) (hcurr : curr ≤ newWidth) (s : aig.RefVec curr) (assign : α → Bool) (idx : ℕ)
  (hidx1 : idx < newWidth),
  curr ≤ idx →
    ⟦assign,
        { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go aig w input newWidth curr hcurr s).aig,
          ref :=
            (Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend.go aig w input newWidth curr hcurr s).vec.get idx
              hidx1 }⟧ =
      if hidx : idx < w then ⟦assign, { aig := aig, ref := input.get idx hidx }⟧ else false
-- Mathlib.Algebra.Regular.Basic
IsLeftRegular.right_of_commute : ∀ {R : Type u_1} [inst : Mul R] {a : R}, (∀ (b : R), Commute a b) → IsLeftRegular a → IsRightRegular a
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.toSubmodule_iInf : ∀ {ι : Sort u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] (f : ι → ClosedSubmodule R M), ↑(⨅ i, f i) = ⨅ i, ↑(f i)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- If `α` is a 2-morphism between right adjoints whose conjugate 2-morphism is
an isomorphism, then `α` is an isomorphism. The converse is given in `conjugateEquiv_symm_iso`.
 -/
CategoryTheory.Bicategory.conjugateEquiv_symm_of_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ : c ⟶ d} {r₁ r₂ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (α : r₁ ⟶ r₂)
  [CategoryTheory.IsIso ((CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂).symm α)], CategoryTheory.IsIso α
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.limitIsoOfIsRightKanExtension_inv_π_assoc : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] [inst_4 : CategoryTheory.Limits.HasLimit F]
  [inst_5 : CategoryTheory.Limits.HasLimit F'] (i : C) {Z : H} (h : F.obj i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F'.limitIsoOfIsRightKanExtension α).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F' (L.obj i))
        (CategoryTheory.CategoryStruct.comp (α.app i) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F i) h
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.map_map : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β]
  [inst_2 : BooleanAlgebra γ] {L : BooleanSubalgebra α} (g : BoundedLatticeHom β γ) (f : BoundedLatticeHom α β),
  BooleanSubalgebra.map g (BooleanSubalgebra.map f L) = BooleanSubalgebra.map (g.comp f) L
-- Mathlib.Data.Num.ZNum
ZNum.succ.eq_3 : ∀ (a : PosNum), (ZNum.neg a).succ = a.pred'.toZNumNeg
-- Init.Omega.IntList
_private.Init.Omega.IntList.0.List.getElem?_zipWithAll.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Option α → Option β → Sort u_3) →
      (x : Option α) →
        (x_1 : Option β) →
          (Unit → motive none none) →
            ((a? : Option α) → (b? : Option β) → (a? = none → b? = none → False) → motive a? b?) → motive x x_1
-- Aesop.Rule
Aesop.LocalNormSimpRule.mk.injEq : ∀ (id : Lean.Name) (simpTheorem : Lean.Term) (id_1 : Lean.Name) (simpTheorem_1 : Lean.Term),
  ({ id := id, simpTheorem := simpTheorem } = { id := id_1, simpTheorem := simpTheorem_1 }) =
    (id = id_1 ∧ simpTheorem = simpTheorem_1)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- Stitching together colimiting cocones gives a colimiting cocone.  -/
CategoryTheory.Limits.combinedIsColimit : {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] →
            (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
              (c : (k : K) → CategoryTheory.Limits.ColimitCocone (F.flip.obj k)) →
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.combineCocones F c)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_mul_natCast : ∀ (x : NNReal) (y : ℝ) (n : ℕ), x ^ (y * ↑n) = (x ^ y) ^ n
-- Mathlib.NumberTheory.LSeries.Convergence
/-- If `‖f n‖` is `O(n^x)`, then the abscissa of absolute convergence
of `f` is bounded by `x + 1`.  -/
LSeries.abscissaOfAbsConv_le_of_isBigO_rpow : ∀ {f : ℕ → ℂ} {x : ℝ}, (f =O[Filter.atTop] fun n => ↑n ^ x) → LSeries.abscissaOfAbsConv f ≤ ↑x + 1
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvection.baseChange : ∀ {R : Type u_3} {V : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : CommRing A] [inst_4 : Algebra R A] {f : Module.Dual R V} {v : V} (h : f v = 0)
  (hA : autoParam (((Module.Dual.baseChange A) f) (1 ⊗ₜ[R] v) = 0) LinearEquiv.transvection.baseChange._auto_1),
  LinearEquiv.baseChange R A V V (LinearEquiv.transvection h) = LinearEquiv.transvection hA
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.continuous_eval₂ : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {φ : R →+* S} {a : S}
  [inst_2 : UniformSpace R] [inst_3 : UniformSpace S] [IsUniformAddGroup R] [IsTopologicalSemiring R]
  [IsUniformAddGroup S] [T2Space S] [CompleteSpace S] [IsTopologicalRing S] [IsLinearTopology S S],
  Continuous ⇑φ → PowerSeries.HasEval a → Continuous (PowerSeries.eval₂ φ a)
-- Mathlib.Algebra.Group.Pi.Lemmas
AddMonoidHom.pi.eq_1 : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → AddZeroClass (f i)] {γ : Type w} [inst_1 : AddZeroClass γ]
  (g : (i : I) → γ →+ f i), AddMonoidHom.pi g = { toFun := fun x i => (g i) x, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.instConcreteCategoryMonoidHomCarrierToGrp.eq_1 : FiniteGrp.instConcreteCategoryMonoidHomCarrierToGrp =
  { hom := @FiniteGrp.instConcreteCategoryMonoidHomCarrierToGrp._aux_1,
    ofHom := @FiniteGrp.instConcreteCategoryMonoidHomCarrierToGrp._aux_3,
    hom_ofHom := @FiniteGrp.instConcreteCategoryMonoidHomCarrierToGrp._proof_5,
    ofHom_hom := @FiniteGrp.instConcreteCategoryMonoidHomCarrierToGrp._proof_6,
    id_apply := @FiniteGrp.instConcreteCategoryMonoidHomCarrierToGrp._proof_7,
    comp_apply := @FiniteGrp.instConcreteCategoryMonoidHomCarrierToGrp._proof_8 }
-- Mathlib.Analysis.SpecialFunctions.Arcosh
/-- The function `Real.arcosh` is real analytic.  -/
Real.analyticOnNhd_arcosh : ∀ {s : Set ℝ}, s ⊆ Set.Ioi 1 → AnalyticOnNhd ℝ Real.arcosh s
-- Mathlib.Data.List.InsertIdx
List.getElem_insertIdx_add_succ : ∀ {α : Type u} (l : List α) (x : α) (n k : ℕ) (hk' : n + k < l.length)
  (hk : optParam (n + k + 1 < (l.insertIdx n x).length) ⋯), (l.insertIdx n x)[n + k + 1] = l[n + k]
-- Mathlib.Tactic.DepRewrite
_private.Mathlib.Tactic.DepRewrite.0.Mathlib.Tactic.DepRewrite.traceClsVisit : Lean.Name
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coe_inclusion : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N N' : LieSubmodule R L M} (h : N ≤ N') (m : ↥N),
  ↑((LieSubmodule.inclusion h) m) = ↑m
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.dvd_of_mod_eq_zero : ∀ {a b : Ordinal.{u_4}}, a % b = 0 → b ∣ a