mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- This is [grinberg_clifford_2016] Theorem 8  -/
CliffordAlgebra.contractLeft_comm : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (d d' : Module.Dual R M) (x : CliffordAlgebra Q),
  (CliffordAlgebra.contractLeft d) ((CliffordAlgebra.contractLeft d') x) =
    -(CliffordAlgebra.contractLeft d') ((CliffordAlgebra.contractLeft d) x)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_map_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  (U : CategoryTheory.Functor X Y) {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y} (φ : S ⟶ S')
  (X_1 : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).map φ).fst.app X_1 =
    φ.fst.app (U.obj X_1)
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.funext : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : Add α], Function.Periodic f c → (fun x => f (x + c)) = f
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_inter_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  (t₁ ∩ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∉ t₂
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.unitOfList_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k : α},
  Std.ExtHashMap.unitOfList [k] = ∅.insertIfNew k ()
-- Mathlib.CategoryTheory.GuitartExact.Opposite
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence_functor : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  {X₃ : C₃ᵒᵖ} {X₂ : C₂ᵒᵖ} (g : B.op.obj X₃ ⟶ R.op.obj X₂),
  (w.structuredArrowRightwardsOpEquivalence g).functor =
    CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor w g
-- Mathlib.Algebra.Group.Action.Prod
AddAction.prodEquiv.eq_1 : ∀ (M : Type u_1) (N : Type u_2) (α : Type u_5) [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddAction.prodEquiv M N α =
    { toFun := fun x => ⟨AddAction.compHom α (AddMonoidHom.inl M N), ⟨AddAction.compHom α (AddMonoidHom.inr M N), ⋯⟩⟩,
      invFun := fun _insts =>
        have this := ⋯;
        AddAction.prodOfVAddCommClass M N α,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence
/-- Pull back a rigid structure along an equivalence.  -/
CategoryTheory.rigidCategoryOfEquivalence : {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] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              [F.Monoidal] →
                {G : CategoryTheory.Functor D C} →
                  (F ⊣ G) → [F.IsEquivalence] → [CategoryTheory.RigidCategory D] → CategoryTheory.RigidCategory C
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Box.splitLower_eq_bot : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ}, I.splitLower i x = ⊥ ↔ x ≤ I.lower i
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a fallback : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKeyD a (Std.Internal.List.eraseKey k l) fallback =
      if (k == a) = true then fallback else Std.Internal.List.getKeyD a l fallback
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Poly.cancelAux.match_3.eq_2 : ∀ (motive : ℕ → Sort u_1) (fuel : ℕ) (h_1 : Unit → motive 0) (h_2 : (fuel : ℕ) → motive fuel.succ),
  (match fuel.succ with
    | 0 => h_1 ()
    | fuel.succ => h_2 fuel) =
    h_2 fuel
-- Mathlib.InformationTheory.KullbackLeibler.DataProcessing
/-- **Data processing inequality** for the Kullback-Leibler divergence and measurable functions.  -/
InformationTheory.klDiv_map_le : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} (μ ν : MeasureTheory.Measure 𝓧)
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {g : 𝓧 → 𝓨},
  Measurable g →
    InformationTheory.klDiv (MeasureTheory.Measure.map g μ) (MeasureTheory.Measure.map g ν) ≤
      InformationTheory.klDiv μ ν
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.mk : (ℕ → Type u) → (ℕ → Type v) → FirstOrder.Language
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedDecl.default : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu
-- Std.Time.DateTime.Timestamp
/-- Adds a `Minute.Offset` to the given `Timestamp`.
 -/
Std.Time.Timestamp.addMinutes : Std.Time.Timestamp → Std.Time.Minute.Offset → Std.Time.Timestamp
-- Mathlib.Order.Sublattice
Sublattice.mk.injEq : ∀ {α : Type u_2} [inst : Lattice α] (carrier : Set α) (supClosed' : SupClosed carrier) (infClosed' : InfClosed carrier)
  (carrier_1 : Set α) (supClosed'_1 : SupClosed carrier_1) (infClosed'_1 : InfClosed carrier_1),
  ({ carrier := carrier, supClosed' := supClosed', infClosed' := infClosed' } =
      { carrier := carrier_1, supClosed' := supClosed'_1, infClosed' := infClosed'_1 }) =
    (carrier = carrier_1)
-- Mathlib.CategoryTheory.GradedObject
/-- Given a map `p : I → J`, this is the functor `GradedObject I C ⥤ GradedObject J C` which
sends an `I`-object `X` to the graded object `X.mapObj p` which in degree `j : J` is given
by the coproduct of those `X i` such that `p i = j`.  -/
CategoryTheory.GradedObject.map : {I : Type u_1} →
  {J : Type u_2} →
    (C : Type u_4) →
      [inst : CategoryTheory.Category.{v_1, u_4} C] →
        (p : I → J) →
          [∀ (j : J), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ↑(p ⁻¹' {j})) C] →
            CategoryTheory.Functor (CategoryTheory.GradedObject I C) (CategoryTheory.GradedObject J C)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited α] {k : α} {f : β → β} {h : k ∈ Std.ExtDHashMap.Const.modify m k f},
  (Std.ExtDHashMap.Const.modify m k f).getKey k h = k
-- Init.Data.Nat.Bitwise.Lemmas
_private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.two_pow_succ_sub_succ_div_two : ∀ {n x : ℕ}, (2 ^ (n + 1) - (x + 1)) / 2 = 2 ^ n - (x / 2 + 1)
-- Mathlib.Order.Circular
sbtw_trans_right : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c d : α}, sbtw a b c → sbtw a c d → sbtw a b d
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getEntryGT : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      [Std.TransOrd α] →
        (k : α) →
          (t : Std.DTreeMap.Internal.Impl α fun x => β) → t.Ordered → (∃ a ∈ t, compare a k = Ordering.gt) → α × β
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.le_zeroLocus_iff_le_vanishingIdeal : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3}
  {V : Set (σ → K)} {I : Ideal (MvPolynomial σ k)}, V ⊆ MvPolynomial.zeroLocus K I ↔ I ≤ MvPolynomial.vanishingIdeal k V
-- Mathlib.Algebra.Ring.Ext
AddCommMonoidWithOne.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : AddCommMonoidWithOne R⦄, HAdd.hAdd = HAdd.hAdd → One.one = One.one → inst₁ = inst₂
-- Lean.Meta.DecLevel
/-- This method is useful for inferring universe level parameters for function that take arguments such as `{α : Type u}`.
Recall that `Type u` is `Sort (u+1)` in Lean. Thus, given `α`, we must infer its universe level,
instantiate and normalize it, and then decrement 1 to obtain `u`.  -/
Lean.Meta.getDecLevel : Lean.Expr → Lean.MetaM Lean.Level
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.LocalGeneratorsData.coversTop : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R}
  [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (self : M.LocalGeneratorsData),
  J.CoversTop self.X
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- To give an image map for a commutative square with `f` at the top and `g` at the bottom, it
suffices to give a map between any mono factorisation of `f` and any image factorisation of `g`.  -/
CategoryTheory.Limits.ImageMap.transport : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      [inst_1 : CategoryTheory.Limits.HasImage f.hom] →
        [inst_2 : CategoryTheory.Limits.HasImage g.hom] →
          (sq : f ⟶ g) →
            (F : CategoryTheory.Limits.MonoFactorisation f.hom) →
              {F' : CategoryTheory.Limits.MonoFactorisation g.hom} →
                CategoryTheory.Limits.IsImage F' →
                  {map : F.I ⟶ F'.I} →
                    CategoryTheory.CategoryStruct.comp map F'.m =
                        CategoryTheory.CategoryStruct.comp F.m (CategoryTheory.Arrow.Hom.right sq) →
                      CategoryTheory.Limits.ImageMap sq
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Int.trailingZeros_aux_irrel : ∀ {i : ℤ} {k k' acc : ℕ} (hi : i ≠ 0) (hk : i.natAbs ≤ k) (hk' : i.natAbs ≤ k'),
  Int.trailingZeros.aux k i hi hk acc = Int.trailingZeros.aux k' i hi hk' acc
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.tr.match_1.eq_8 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (fs : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (f : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k f q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 :
    (fs : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k)))
  (h_9 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k.cons₂))
  (h_10 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k)))
  (h_11 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k)))
  (h_12 : Unit → motive (Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt)),
  (match Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k) with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k f q => h_2 k f q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k) => h_8 fs k
    | Turing.PartrecToTM2.Λ'.ret k.cons₂ => h_9 k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k) => h_10 f k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k) => h_11 f k
    | Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt => h_12 ()) =
    h_8 fs k
-- Mathlib.SetTheory.ZFC.PSet
PSet.Mem.congr_right : ∀ {x y : PSet.{u}}, x.Equiv y → ∀ {w : PSet.{u}}, w ∈ x ↔ w ∈ y
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.associator.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F G : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  (H : CategoryTheory.Functor C V) [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution G H]
  [inst_6 :
    CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)]
  [inst_7 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H]
  [inst_8 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_9 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)],
  CategoryTheory.MonoidalCategory.DayConvolution.associator F G H =
    CategoryTheory.MonoidalCategory.DayConvolution.associator F G H
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- The chosen wedge for each functor `Jᵒᵖ ⥤ J ⥤ C`.  -/
CategoryTheory.Limits.ChosenEndsOfShape.wedge : {J : Type u_3} →
  {inst : CategoryTheory.Category.{v_3, u_3} J} →
    {C : Type u_4} →
      {inst_1 : CategoryTheory.Category.{v_4, u_4} C} →
        [self : CategoryTheory.Limits.ChosenEndsOfShape J C] →
          (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) → CategoryTheory.Limits.Wedge F
-- Plausible.Random
Plausible.instMonadLiftTRandGTOfMonadLift : {m : Type u_1 → Type u_2} →
  {n : Type u_1 → Type u_3} → {g : Type} → [MonadLift m n] → MonadLiftT (Plausible.RandGT g m) (Plausible.RandGT g n)
-- Mathlib.Algebra.Group.Basic
neg_one_zsmul_add : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a b : α), -1 • (a + b) = -1 • b + -1 • a
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.sub_add_right : ∀ {α : Type u} [inst : SubtractionCommMonoid α] {a : α}, IsAddUnit a → ∀ (b : α), a - (a + b) = 0 - b
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.opowAux2.match_3.eq_2 : ∀ (motive : ONote × ℕ → Sort u_1) (h_1 : Unit → motive (ONote.zero, 0)) (h_2 : Unit → motive (ONote.zero, 1))
  (h_3 : (m : ℕ) → motive (ONote.zero, m.succ))
  (h_4 : (a a0 : ONote) → (a_1 : ℕ+) → (a_2 : ONote) → a = a0.oadd a_1 a_2 → (m : ℕ) → motive (a0.oadd a_1 a_2, m)),
  (match (ONote.zero, 1) with
    | (ONote.zero, 0) => h_1 ()
    | (ONote.zero, 1) => h_2 ()
    | (ONote.zero, m.succ) => h_3 m
    | (a@h:(a0.oadd a_1 a_2), m) => h_4 a a0 a_1 a_2 h m) =
    h_2 ()
-- Mathlib.CategoryTheory.Limits.Yoneda
/-- The coyoneda embeddings jointly reflect limits.  -/
CategoryTheory.coyonedaJointlyReflectsLimits : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        (F : CategoryTheory.Functor J C) →
          (c : CategoryTheory.Limits.Cone F) →
            ((X : Cᵒᵖ) → CategoryTheory.Limits.IsLimit ((CategoryTheory.coyoneda.obj X).mapCone c)) →
              CategoryTheory.Limits.IsLimit c
-- Mathlib.Algebra.Module.Presentation.Free
Module.presentationFinsupp_var : ∀ (A : Type u) [inst : Ring A] (G : Type w₀)
  (g : { G := G, R := PEmpty.{w₁ + 1}, relation := fun r => PEmpty.casesOn (fun x => G →₀ A) r }.G),
  (Module.presentationFinsupp A G).var g = fun₀ | g => 1
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G} [S.FiniteIndex],
  (Rep.coindFunctor k S.subtype).IsLeftAdjoint
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_at_apply : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {S : Type u_1} [inst_1 : Semiring S] (f : R →+* S) (r : R),
  Polynomial.eval₂ f (f r) p = f (Polynomial.eval r p)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.inverse_rpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] (a : A) (x : ℝ),
  x ≠ 0 → autoParam (IsStrictlyPositive a) CFC.inverse_rpow._auto_1 → Ring.inverse (a ^ x) = a ^ (-x)
-- Mathlib.Data.Fin.SuccPred
/-- The `Fin.succ_one_eq_two` in `Lean` only applies in `Fin (n+2)`.
This one instead uses a `NeZero n` typeclass hypothesis.
 -/
Fin.succ_one_eq_two' : ∀ {n : ℕ} [NeZero n], Fin.succ 1 = 2
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.smul_mem_rootSet_iff_of_isUnit : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CommRing S] [inst_3 : Algebra S R]
  {G : Type u_1} [inst_4 : Monoid G] [inst_5 : MulSemiringAction G R] [SMulCommClass G S R] {f : Polynomial S} {g : G},
  IsUnit g → ∀ {x : R}, g • x ∈ f.rootSet R ↔ x ∈ f.rootSet R
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (kind : Lean.Elab.DefKind) (levelParams : List Lean.Name) (modifiers : Lean.Elab.Modifiers)
  (declName : Lean.Name) (binders : Lean.Syntax) (numSectionVars : ℕ) (type value : Lean.Expr)
  (termination : Lean.Elab.TerminationHints),
  sizeOf
      { ref := ref, kind := kind, levelParams := levelParams, modifiers := modifiers, declName := declName,
        binders := binders, numSectionVars := numSectionVars, type := type, value := value,
        termination := termination } =
    1 + sizeOf ref + sizeOf kind + sizeOf levelParams + sizeOf modifiers + sizeOf declName + sizeOf binders +
            sizeOf numSectionVars +
          sizeOf type +
        sizeOf value +
      sizeOf termination
-- Mathlib.Order.Hom.WithTopBot
WithTop.subtypeOrderIso_apply_coe : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : DecidablePred fun x => x = ⊤]
  (a : { a // a ≠ ⊤ }), WithTop.subtypeOrderIso ↑a = ↑a
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.nonDegenerate_ext₁ : ∀ {p q n : ℕ}
  {z₁ z₂ :
    ↑((CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
            (SSet.stdSimplex.obj { len := q })).nonDegenerate
        n)},
  (↑z₁).1 = (↑z₂).1 → autoParam (p + q = n) SSet.prodStdSimplex.nonDegenerate_ext₁._auto_1 → z₁ = z₂
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceBackward_forget_forget : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X),
  f.iteratedSliceBackward.comp ((CategoryTheory.Over.forget f).comp (CategoryTheory.Over.forget X)) =
    CategoryTheory.Over.forget f.left
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.of_id : ∀ (R : Type u_1) [inst : CommRing R], Algebra.EssFiniteType R R
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.ordConnectedProj.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Set α) (x : ↑s), s.ordConnectedProj x = ⋯.some
-- Lean.Data.Lsp.Basic
Lean.Lsp.instAppendTextEditBatch : Append Lean.Lsp.TextEditBatch
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.exists_rightDescent_of_ne_one : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W},
  w ≠ 1 → ∃ i, cs.IsRightDescent w i
-- Mathlib.RingTheory.FiniteType
/-- If `R[M]` is of finite type then `M` is finitely generated.  -/
MonoidAlgebra.fg_of_finiteType : ∀ {R : Type u_1} {M : Type u_2} [inst : Monoid M] [inst_1 : CommRing R] [Nontrivial R]
  [h : Algebra.FiniteType R (MonoidAlgebra R M)], Monoid.FG M
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (Std.ExtDTreeMap.ofList l cmp).get? k' = some (cast ⋯ v)
-- Lean.Meta.ACLt
_private.Lean.Meta.ACLt.0.Lean.Meta.ACLt.main.ltApp : Lean.Meta.ACLt.ReduceMode → Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.StructureSheaf.toPushforwardStalk_comp_assoc : ∀ {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum ↑R) {Z : CommRingCat}
  (h :
    ((TopCat.Presheaf.pushforward CommRingCat (AlgebraicGeometry.Spec.topMap f)).obj
            (AlgebraicGeometry.Spec.structureSheaf ↑S).obj).stalk
        p ⟶
      Z),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toPushforwardStalk f p) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk (↑R) p)
      (CategoryTheory.CategoryStruct.comp
        ((TopCat.Presheaf.stalkFunctor CommRingCat p).map (AlgebraicGeometry.Spec.sheafedSpaceMap f).hom.c) h)
-- Mathlib.MeasureTheory.SetSemiring
_private.Mathlib.MeasureTheory.SetSemiring.0.MeasureTheory.IsSetSemiring.disjointOfUnion_coe : ∀ {α : Type u_1} {C : Set (Set α)} {J : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hJ : ↑J ⊆ C) (j : ↥J),
  hC.disjointOfUnion hJ ↑j = ⋯.choose.parts
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the sign of the angle between three points is positive, the first and third points are not
equal.  -/
EuclideanGeometry.left_ne_right_of_oangle_sign_eq_one : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign = 1 → p₁ ≠ p₃
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y}
  [inst_2 : CategoryTheory.IsSplitEpi f] {c : CategoryTheory.Limits.KernelFork f} (i : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel i).inr = CategoryTheory.section_ f
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.toStructuredArrowCompProj_hom_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (X : J),
  c.toStructuredArrowCompProj.hom.app X = CategoryTheory.CategoryStruct.id X
-- Aesop.Rule.Name
Aesop.BuilderName.cases : Aesop.BuilderName
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.comap_prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel β γ)
  [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel β δ) [ProbabilityTheory.IsSFiniteKernel η]
  {f : α → β} (hf : Measurable f), (κ.prod η).comap f hf = (κ.comap f hf).prod (η.comap f hf)