mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Basic
ite_mul_one : ∀ {M : Type u_4} [inst : MulOneClass M] {P : Prop} [inst_1 : Decidable P] {a b : M},
  (if P then a * b else 1) = (if P then a else 1) * if P then b else 1
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_lt_rpow_of_neg : ∀ {x : NNReal} {z : ℝ} {y : NNReal}, 0 < x → x < y → z < 0 → y ^ z < x ^ z
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.le_inf_add : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {β : Type u_5} [inst_2 : SemilatticeInf β]
  [inst_3 : OrderTop β] {s t : Finset α} {f : α → β} {a : β}, a ≤ (s + t).inf f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x + y)
-- Mathlib.Data.Setoid.Partition
/-- This lemma is analogous to `Quotient.out_eq'`.  -/
IndexedPartition.proj_out : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : hs.Quotient), hs.proj (hs.out x) = x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_add_eq_add_pi : ∀ {x y : ℝ}, 1 < x * y → 0 < x → Real.arctan x + Real.arctan y = Real.arctan ((x + y) / (1 - x * y)) + Real.pi
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_natCast_mul : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {a k : ℕ}, (↑a * p).coeff k = ↑a * p.coeff k
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
/-- Given a root pairing, this is an invariant symmetric bilinear form.  -/
RootPairing.InvariantForm : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → Type (max u_2 u_4)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁.Hom S₂) (g : S₂.Hom S₃),
  (f.comp g).f₁ = CategoryTheory.CategoryStruct.comp f.f₁ g.f₁
-- Mathlib.CategoryTheory.Triangulated.Adjunction
/-- The identity equivalence is triangulated.
 -/
CategoryTheory.Equivalence.IsTriangulated.refl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C],
  CategoryTheory.Equivalence.refl.IsTriangulated
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueAdd.iff_existsUnique : ∀ {G : Type u_1} [inst : Add G] {A B : Finset G} {a0 b0 : G},
  a0 ∈ A → b0 ∈ B → (UniqueAdd A B a0 b0 ↔ ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 + ab.2 = a0 + b0)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.pruneLT.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (lowerBound : α) (sz : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.pruneLT✝ (Std.DTreeMap.Internal.Impl.inner sz k v l r) lowerBound =
    match compare lowerBound k with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.inner sz k v (Std.DTreeMap.Internal.Impl.pruneLT✝ l lowerBound) r
    | Ordering.eq => r
    | Ordering.gt => Std.DTreeMap.Internal.Impl.pruneLT✝ r lowerBound
-- Mathlib.Algebra.Quaternion
Quaternion.eq_re_of_eq_coe : ∀ {R : Type u_3} [inst : CommRing R] {a : Quaternion R} {x : R}, a = ↑x → a = ↑a.re
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.of_le : ∀ {α : 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 g p μ →
    MeasureTheory.AEStronglyMeasurable f μ → (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖) → MeasureTheory.MemLp f p μ
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
/-- If the `eLpNorm` of a collection of `AEStronglyMeasurable` functions that converges almost
everywhere is bounded by some constant `C`, then the `eLpNorm` of its limit is also bounded by
`C`.  -/
MeasureTheory.Lp.eLpNorm_le_of_ae_tendsto : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : SeminormedAddGroup E] {ι : Type u_3} {u : Filter ι} [u.NeBot] [u.IsCountablyGenerated] {f : ι → α → E}
  {g : α → E} {C : ENNReal},
  (∀ᶠ (n : ι) in u, MeasureTheory.eLpNorm (f n) p μ ≤ C) →
    (∀ (n : ι), MeasureTheory.AEStronglyMeasurable (f n) μ) →
      (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun x_1 => f x_1 x) u (nhds (g x))) → MeasureTheory.eLpNorm g p μ ≤ C
-- Mathlib.Algebra.Module.Submodule.LinearMap
/-- A linear map `f : M → M₂` whose values lie in the image of an injective linear map
`p : M₂' → M₂` admits a unique lift to a linear map `M → M₂'`.  -/
LinearMap.codLift : {R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R →+* R₂} →
                      (f : M →ₛₗ[σ₁₂] M₂) →
                        {M₂' : Type u_10} →
                          [inst_6 : AddCommMonoid M₂'] →
                            [inst_7 : Module R₂ M₂'] →
                              (p : M₂' →ₗ[R₂] M₂) →
                                Function.Injective ⇑p → (∀ (c : M), f c ∈ Set.range ⇑p) → M →ₛₗ[σ₁₂] M₂'
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_sup : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → (max a b).toReal = max a.toReal b.toReal
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- Given a cell `c` of rank `j` for a rank function `f` for a proper
pairing of a subcomplex of a simplicial set, this is the inclusion of
`Δ[c.dim + 1]` into `f.sigmaStdSimplex j`.  -/
SSet.Subcomplex.Pairing.RankFunction.Cell.ιSigmaStdSimplex : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} →
        [inst : LinearOrder ι] →
          {f : P.RankFunction ι} →
            {j : ι} → (c : f.Cell j) → SSet.stdSimplex.obj { len := c.dim + 1 } ⟶ f.sigmaStdSimplex j
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of `(· - x) ^ n` at `x` is `n`.  -/
meromorphicOrderAt_pow_id_sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℕ},
  meromorphicOrderAt ((fun x_1 => x_1 - x) ^ n) x = ↑n
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.PartialMatch.mk.injEq : ∀ (todo : Array Lean.Expr) (score : ℕ) (c : Lean.Meta.LazyDiscrTree.TrieIndex) (todo_1 : Array Lean.Expr) (score_1 : ℕ)
  (c_1 : Lean.Meta.LazyDiscrTree.TrieIndex),
  ({ todo := todo, score := score, c := c } = { todo := todo_1, score := score_1, c := c_1 }) =
    (todo = todo_1 ∧ score = score_1 ∧ c = c_1)
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.instIsIdempotentCompleteHomologicalComplex : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  (c : ComplexShape ι) [CategoryTheory.IsIdempotentComplete C],
  CategoryTheory.IsIdempotentComplete (HomologicalComplex C c)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.move.injEq : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (a : Turing.Dir) (a_1 : Turing.TM1.Stmt Γ Λ σ) (a_2 : Turing.Dir)
  (a_3 : Turing.TM1.Stmt Γ Λ σ), (Turing.TM1.Stmt.move a a_1 = Turing.TM1.Stmt.move a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective : ∀ (D : AlgebraicGeometry.Scheme.GlueData) (x : ↥D.glued), ∃ i y, (D.ι i) y = x
-- Mathlib.RingTheory.Kaehler.TensorProduct
/-- (Implementation). `A`-action on `S ⊗[R] Ω[A⁄R]`.  -/
KaehlerDifferential.mulActionBaseChange : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            [inst_3 : CommRing A] → [inst_4 : Algebra R A] → MulAction A (TensorProduct R S Ω[A⁄R])
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {obj : (X : Cᵒᵖ) → ModuleCat ↑(R.obj X)}
  {map : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → obj X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (obj Y)}
  {map_id :
    autoParam
      (∀ (X : Cᵒᵖ),
        map (CategoryTheory.CategoryStruct.id X) =
          (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.id X))) ⋯).inv.app
            (obj X))
      PresheafOfModules.map_id._autoParam}
  {map_comp :
    autoParam
      (∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
        map (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (map f)
            (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (map g))
              ((ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                      (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.comp f g))) ⋯).inv.app
                (obj Z))))
      PresheafOfModules.map_comp._autoParam}
  {obj_1 : (X : Cᵒᵖ) → ModuleCat ↑(R.obj X)}
  {map_1 : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → obj_1 X ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (obj_1 Y)}
  {map_id_1 :
    autoParam
      (∀ (X : Cᵒᵖ),
        map_1 (CategoryTheory.CategoryStruct.id X) =
          (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.id X))) ⋯).inv.app
            (obj_1 X))
      PresheafOfModules.map_id._autoParam}
  {map_comp_1 :
    autoParam
      (∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
        map_1 (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (map_1 f)
            (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (map_1 g))
              ((ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                      (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.comp f g))) ⋯).inv.app
                (obj_1 Z))))
      PresheafOfModules.map_comp._autoParam},
  { obj := obj, map := map, map_id := map_id, map_comp := map_comp } =
      { obj := obj_1, map := map_1, map_id := map_id_1, map_comp := map_comp_1 } →
    obj = obj_1 ∧ map ≍ map_1
-- Batteries.Data.Fin.Lemmas
Fin.findRev?_succ : ∀ {n : ℕ} {p : Fin (n + 1) → Bool},
  Fin.findRev? p =
    if p (Fin.last n) = true then some (Fin.last n) else Option.map Fin.castSucc (Fin.findRev? fun i => p i.castSucc)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.toIsValuedIn : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {P : RootPairing ι R M N} [self : P.EmbeddedG2],
  P.IsValuedIn ℤ
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.add_iff_right : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, f₁ =o[l] g → ((fun x => f₁ x + f₂ x) =o[l] g ↔ f₂ =o[l] g)
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.dim_eq_of_eq : ∀ {X : SSet} {s t : X.S}, s = t → s.dim = t.dim
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.HoCat.resolutionMap_fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj X)
      (HomotopicalAlgebra.FibrantObject.HoCat.resolutionMap f) =
    CategoryTheory.CategoryStruct.comp f (HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj Y)
-- Mathlib.Data.Vector.Basic
List.Vector.pmap.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} (f f_1 : (a : α) → p a → β),
  f = f_1 →
    ∀ (v v_1 : List.Vector α n) (e_v : v = v_1) (a : ∀ x ∈ v.toList, p x),
      List.Vector.pmap f v a = List.Vector.pmap f_1 v_1 ⋯
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_const_smul_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} {𝕜 : Type u_14} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F']
  [inst_2 : NormedField 𝕜] {f : α → E} {g' : α → F'} {l : Filter α} [inst_3 : NormedSpace 𝕜 F'] {c : 𝕜},
  c ≠ 0 → ((f =Θ[l] fun x => c • g' x) ↔ f =Θ[l] g')
-- Mathlib.Order.Bounds.Basic
/-- If `s` is bounded, then so is `s ∩ t`  -/
BddBelow.inter_of_left : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, BddBelow s → BddBelow (s ∩ t)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSpanningSubgraph.anti_right : ∀ {α : Type u_1} {β : Type u_2} {G H K : Graph α β}, H ≤ K → K ≤ G → H ≤s G → H ≤s K
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.zero_cpow_eq_iff : ∀ {x a : ℂ}, 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstr.brecOn.go : {motive_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.Linear.EqCnstrProof → Sort u} →
    {motive_3 : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Sort u} →
      {motive_4 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Sort u} →
        {motive_5 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Sort u} →
          {motive_6 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof → Sort u} →
            {motive_7 : Lean.Meta.Grind.Arith.Linear.UnsatProof → Sort u} →
              (t : Lean.Meta.Grind.Arith.Linear.IneqCnstr) →
                ((t : Lean.Meta.Grind.Arith.Linear.EqCnstr) → t.below → motive_1 t) →
                  ((t : Lean.Meta.Grind.Arith.Linear.EqCnstrProof) → t.below → motive_2 t) →
                    ((t : Lean.Meta.Grind.Arith.Linear.IneqCnstr) → t.below → motive_3 t) →
                      ((t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) → t.below → motive_4 t) →
                        ((t : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) → t.below → motive_5 t) →
                          ((t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) → t.below → motive_6 t) →
                            ((t : Lean.Meta.Grind.Arith.Linear.UnsatProof) → t.below → motive_7 t) →
                              motive_3 t ×' t.below
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.symmetricIcc.eq_1 : ∀ (G : Type u_1) [inst : Neg G] [inst_1 : Preorder G] [inst_2 : LocallyFiniteOrder G],
  SummationFilter.symmetricIcc G = { filter := Filter.map (fun g => Finset.Icc (-g) g) Filter.atTop }
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.postcomposeEquivalence.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G),
  CategoryTheory.Limits.Cone.postcomposeEquivalence α =
    { functor := CategoryTheory.Limits.Cone.postcompose α.hom, inverse := CategoryTheory.Limits.Cone.postcompose α.inv,
      unitIso :=
        CategoryTheory.NatIso.ofComponents
          (fun s =>
            CategoryTheory.Limits.Cone.ext
              (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)).obj s).pt) ⋯)
          ⋯,
      counitIso :=
        CategoryTheory.NatIso.ofComponents
          (fun s =>
            CategoryTheory.Limits.Cone.ext
              (CategoryTheory.Iso.refl
                (((CategoryTheory.Limits.Cone.postcompose α.inv).comp
                        (CategoryTheory.Limits.Cone.postcompose α.hom)).obj
                    s).pt)
              ⋯)
          ⋯,
      functor_unitIso_comp := ⋯ }
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.insert.go.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.eq) → (Unit → motive Ordering.gt) → (Unit → motive Ordering.lt) → motive x
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
evalRingHom_mapMatrix_comp_compRingEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {m : Type u_4}
  [inst_3 : Fintype m] [inst_4 : DecidableEq m],
  (Polynomial.evalRingHom 0).mapMatrix.comp ↑(Matrix.compRingEquiv m n (Polynomial R)) =
    (Matrix.compRingEquiv m n R).toRingHom.comp (Polynomial.evalRingHom 0).mapMatrix.mapMatrix
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.coloops.eq_1 : ∀ {α : Type u_1} (M : Matroid α), M.coloops = M✶.loops
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Ico_right : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b : α}, a₂ < a₁ → Set.Icc b a₂ ⊆ Set.Ico b a₁
-- Batteries.Tactic.Lint.Frontend
Batteries.Tactic.Lint.instInhabitedLintVerbosity.default : Batteries.Tactic.Lint.LintVerbosity
-- Mathlib.Data.Set.Semiring
SetSemiring.instMulOneClass : {α : Type u_1} → [MulOneClass α] → MulOneClass (SetSemiring α)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_eq_iff : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] (a b : A),
  autoParam (0 ≤ a) CFC.sqrt_eq_iff._auto_1 → autoParam (0 ≤ b) CFC.sqrt_eq_iff._auto_3 → (CFC.sqrt a = b ↔ b * b = a)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : β → β}, (Std.DHashMap.Const.modify m k f).size = m.size
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Arrow.homMk_hom : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q W : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : W.IsMultiplicative] {A B : P.Arrow Q W} (f : A.left ⟶ B.left)
  (g : A.right ⟶ B.right)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp f B.hom = CategoryTheory.CategoryStruct.comp A.hom g)
      CategoryTheory.MorphismProperty.Arrow.homMk._auto_1)
  (hf : autoParam (Q f) CategoryTheory.MorphismProperty.Arrow.homMk._auto_3)
  (hg : autoParam (W g) CategoryTheory.MorphismProperty.Arrow.homMk._auto_5),
  CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Arrow.homMk f g w hf hg) =
    CategoryTheory.Arrow.homMk f g w
-- Mathlib.Logic.Function.Basic
Function.leftInverse_iff_comp : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α}, Function.LeftInverse f g ↔ f ∘ g = id
-- Aesop.Script.Tactic
Aesop.Script.STactic.mk.inj : ∀ {numSubgoals : ℕ} {run : Array (Array Lean.Syntax.Tactic) → Lean.Syntax.Tactic} {numSubgoals_1 : ℕ}
  {run_1 : Array (Array Lean.Syntax.Tactic) → Lean.Syntax.Tactic},
  { numSubgoals := numSubgoals, run := run } = { numSubgoals := numSubgoals_1, run := run_1 } →
    numSubgoals = numSubgoals_1 ∧ run = run_1
-- Mathlib.Algebra.Group.Prod
Prod.subNegMonoid : {G : Type u_1} → {H : Type u_2} → [SubNegMonoid G] → [SubNegMonoid H] → SubNegMonoid (G × H)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.functorExt.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1}
  {F G : CategoryTheory.Functor (CategoryTheory.Limits.WidePullbackShape ι) C} (base base_1 : F.obj none ≅ G.obj none)
  (e_base : base = base_1) (comp comp_1 : (i : ι) → F.obj (some i) ≅ G.obj (some i)) (e_comp : comp = comp_1)
  (w :
    ∀ (i : ι),
      CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term i)) base.hom =
        CategoryTheory.CategoryStruct.comp (comp i).hom (G.map (CategoryTheory.Limits.WidePullbackShape.Hom.term i))),
  CategoryTheory.Limits.WidePullbackShape.functorExt base comp w =
    CategoryTheory.Limits.WidePullbackShape.functorExt base_1 comp_1 ⋯
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instInvolutiveInv.eq_1 : ∀ {α : Type u_1} [inst : InvolutiveInv α], OrderDual.instInvolutiveInv = { toInv := OrderDual.instInv, inv_inv := ⋯ }
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_mul_apply_right : ∀ {R : Type u_1} {G : Type u_3} [inst : Semiring R] [inst_1 : Group G] (x y : MonoidAlgebra R G) (g : G),
  (x * y).coeff g = y.coeff.sum fun h r => x.coeff (g * h⁻¹) * r
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.mutuallySingular_compProd_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν],
  (μ.compProd κ).MutuallySingular (ν.compProd η) ↔
    ∀ (ξ : MeasureTheory.Measure α),
      MeasureTheory.SFinite ξ →
        ξ.AbsolutelyContinuous μ → ξ.AbsolutelyContinuous ν → (ξ.compProd κ).MutuallySingular (ξ.compProd η)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.coe_pi : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M₁ i)]
  [inst_2 : (i : ι) → Module R (M₁ i)] [inst_3 : (i : ι) → TopologicalSpace (M₁ i)] {ι' : Type u_1} {M' : ι' → Type u_2}
  [inst_4 : (i : ι') → AddCommMonoid (M' i)] [inst_5 : (i : ι') → TopologicalSpace (M' i)]
  [inst_6 : (i : ι') → Module R (M' i)] (f : (i : ι') → ContinuousMultilinearMap R M₁ (M' i)),
  ⇑(ContinuousMultilinearMap.pi f) = fun m j => (f j) m
-- Lean.Meta.RecursorInfo
Lean.Meta.recursorAttribute : Lean.ParametricAttribute ℕ
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.Cauchy.ring : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Ring β] → {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → Ring (CauSeq.Completion.Cauchy abv)
-- Mathlib.Probability.ProductMeasure
/-- This is the key theorem to build the product of an arbitrary family of probability measures:
the `piContent` of a decreasing sequence of cylinders with empty intersection converges to `0`.

This implies the `σ`-additivity of `piContent` (see `addContent_iUnion_eq_sum_of_tendsto_zero`),
which allows to extend it to the `σ`-algebra by Carathéodory's theorem.  -/
MeasureTheory.piContent_tendsto_zero : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {A : ℕ → Set ((i : ι) → X i)},
  (∀ (n : ℕ), A n ∈ MeasureTheory.measurableCylinders X) →
    Antitone A → ⋂ n, A n = ∅ → Filter.Tendsto (fun n => (MeasureTheory.piContent μ) (A n)) Filter.atTop (nhds 0)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
pow_sub_of_lt : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {m n : ℕ} (a : G₀), n < m → a ^ (m - n) = a ^ m * (a ^ n)⁻¹
-- Mathlib.CategoryTheory.Sites.Whiskering
CategoryTheory.instFullSheafSheafComposeOfFaithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C)
  (F : CategoryTheory.Functor A B) [inst_3 : J.HasSheafCompose F] [F.Full] [F.Faithful],
  (CategoryTheory.sheafCompose J F).Full
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
String.Slice.Pattern.Model.ForwardSliceSearcher.toList_emptyAt_eq : ∀ (s : String.Slice) (pos : s.Pos) (h : pos ≠ s.endPos),
  { internalState := String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h }.toList =
    String.Slice.Pattern.SearchStep.rejected pos (pos.next h) ::
      { internalState := String.Slice.Pattern.ForwardSliceSearcher.emptyBefore (pos.next h) }.toList
-- Mathlib.Order.Sublocale
Sublocale.iInf_mem : ∀ {X : Type u_1} [inst : Order.Frame X] {ι : Sort u_2} {S : Sublocale X} {f : ι → X},
  (∀ (i : ι), f i ∈ S) → ⨅ i, f i ∈ S