mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a colimit for `F.rightOp : J ⥤ Cᵒᵖ` into a limit for `F : Jᵒᵖ ⥤ C`.  -/
CategoryTheory.Limits.isLimitConeOfCoconeRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ C) →
          {c : CategoryTheory.Limits.Cocone F.rightOp} →
            CategoryTheory.Limits.IsColimit c →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeRightOp c)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.exists_pow_eq : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} [Finite α], f.IsCycle → f x ≠ x → f y ≠ y → ∃ i, (f ^ i) x = y
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKeyD_erase_le_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α},
      (t.erase k).isEmpty = false →
        ∀ {fallback : α}, (cmp ((t.erase k).maxKeyD fallback) (t.maxKeyD fallback)).isLE = true
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.arrowCongr_comp : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} {A₁' : Type uA₁'} {A₂' : Type uA₂'} {A₃' : Type uA₃'}
  [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂] [inst_3 : Semiring A₃] [inst_4 : Semiring A₁']
  [inst_5 : Semiring A₂'] [inst_6 : Semiring A₃'] [inst_7 : Algebra R A₁] [inst_8 : Algebra R A₂]
  [inst_9 : Algebra R A₃] [inst_10 : Algebra R A₁'] [inst_11 : Algebra R A₂'] [inst_12 : Algebra R A₃']
  (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') (e₃ : A₃ ≃ₐ[R] A₃') (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₃),
  (e₁.arrowCongr e₃) (g.comp f) = ((e₂.arrowCongr e₃) g).comp ((e₁.arrowCongr e₂) f)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_3.eq_1 : ∀ {n : ℕ} (motive : Option (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) → Sort u_1)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (h_1 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some (some c)))
  (h_2 : Unit → motive (some none)) (h_3 : Unit → motive none),
  (match some (some c) with
    | some (some c) => h_1 c
    | some none => h_2 ()
    | none => h_3 ()) =
    h_1 c
-- Mathlib.GroupTheory.Congruence.Hom
/-- The homomorphism induced on the quotient of a monoid by the kernel of a monoid homomorphism.  -/
Con.kerLift : {M : Type u_1} →
  {P : Type u_3} → [inst : MulOneClass M] → [inst_1 : MulOneClass P] → (f : M →* P) → (Con.ker f).Quotient →* P
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.inverse_eq : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {f : M →L[R] M₂} {g : M₂ →L[R] M},
  f ∘SL g = ContinuousLinearMap.id R M₂ → g ∘SL f = ContinuousLinearMap.id R M → f.inverse = g
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.Intersecting.eq_1 : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] (s : Set α),
  s.Intersecting = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → ¬Disjoint a b
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Sum of elements in a `Subsemiring` of a `NonAssocSemiring` indexed by a `Finset`
is in the `Subsemiring`.  -/
Subsemiring.sum_mem : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) {ι : Type u_1} {t : Finset ι} {f : ι → R},
  (∀ c ∈ t, f c ∈ s) → ∑ i ∈ t, f i ∈ s
-- Mathlib.Algebra.Star.MonoidHom
/-- The identity map as a star monoid isomorphism.  -/
StarMulEquiv.refl : (A : Type u_2) → [inst : Mul A] → [inst_1 : Star A] → A ≃⋆* A
-- Lean.Meta.Basic
/-- Projections `s.i` are reduced at `whnfCore`, and `whnfCore` is used at `s` during the process.
Recall that `whnfCore` does not perform `delta` reduction (i.e., it will not unfold constant declarations).
 -/
Lean.Meta.ProjReductionKind.yes : Lean.Meta.ProjReductionKind
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The identity as a continuous linear map on the type synonym equipped with the weak operator
topology  -/
ContinuousLinearMapWOT.id : (𝕜₂ : Type u_6) →
  (F : Type u_10) →
    [inst : NormedField 𝕜₂] →
      [inst_1 : AddCommGroup F] → [inst_2 : TopologicalSpace F] → [inst_3 : Module 𝕜₂ F] → F →WOT[𝕜₂] F
-- Aesop.Frontend.Attribute
Aesop.Frontend.Parser.attr_rules_ : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.notMem_bot : ∀ {M : Type u_1} [inst : Add M] {x : M}, x ∉ ⊥
-- Mathlib.CategoryTheory.Action.Basic
Action.mkIso.congr_simp : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (f f_1 : M.V ≅ N.V) (e_f : f = f_1)
  (comm :
    ∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) f.hom = CategoryTheory.CategoryStruct.comp f.hom (N.ρ g)),
  Action.mkIso f comm = Action.mkIso f_1 ⋯
-- Mathlib.RingTheory.AlgebraTower
Module.Basis.smulTower'.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [inst_6 : IsScalarTower R S A] {ι : Type u_5}
  {ι' : Type u_6} (b : Module.Basis ι R S) (c : Module.Basis ι' S A),
  b.smulTower' c = (b.smulTower c).reindex (Equiv.prodComm ι ι')
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero : ∀ {M : Type u_1} [inst : CommGroupWithZero M] {e : M} {L l l' l₀ : Mathlib.Tactic.FieldSimp.NF M},
  L.eval * l.eval = l'.eval → ((0, e) ::ᵣ l).eval = l₀.eval → L.eval * l₀.eval = ((0, e) ::ᵣ l').eval
-- Lean.LocalContext
Lean.LocalContext.getAt? : Lean.LocalContext → ℕ → Option Lean.LocalDecl
-- Mathlib.Logic.IsEmpty.Defs
IsEmpty.instSubsingleton : ∀ {α : Sort u} [IsEmpty α], Subsingleton α
-- Init.Tactics
/-- Applies `subst` to all hypotheses of the form `h : x = t` or `h : t = x`.
 -/
Lean.Parser.Tactic.substVars : Lean.ParserDescr
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_bind_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.minKey?.bind t.getKey? = t.minKey?
-- Mathlib.Tactic.NormNum.DivMod
/-- The `norm_num` extension which identifies expressions of the form `(a : ℤ) ∣ b`,
such that `norm_num` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.NormNum.evalIntDvd : Mathlib.Meta.NormNum.NormNumExt
-- Init.Data.String.TakeDrop
String.trim : String → String
-- Std.Time.Duration
Std.Time.Duration.compare_def : compare = compareLex (compareOn fun x => x.second) (compareOn fun x => x.nano)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable.0.cond.match_1.splitter : (motive : Bool → Sort u_1) → (c : Bool) → (Unit → motive true) → (Unit → motive false) → motive c
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.add_one_ne_zero : ∀ (o : Ordinal.{u_1}), o + 1 ≠ 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_insertMany_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α},
  k ∈ ↑(t.insertMany l ⋯) ↔ k ∈ t ∨ (List.map Sigma.fst l).contains k = true
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_I₀ : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z),
  (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight 𝒰X 𝒰Y f g).I₀ = (𝒰X.I₀ × 𝒰Y.I₀)
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.instHasZeroObjectOppositeShift : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (A : Type u_2) [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] [CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.Limits.HasZeroObject (CategoryTheory.OppositeShift C A)
-- Mathlib.CategoryTheory.Action.Limits
Action.instHasLimits : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [CategoryTheory.Limits.HasLimits V], CategoryTheory.Limits.HasLimits (Action V G)
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.support_bind : ∀ {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → PMF β), (p.bind f).support = ⋃ a ∈ p.support, (f a).support
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.memLp_of_isFiniteMeasure : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  (f : MeasureTheory.SimpleFunc α E) (p : ENNReal) (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp (⇑f) p μ
-- Mathlib.CategoryTheory.Action.Basic
Action.hom_ext_iff : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  {φ₁ φ₂ : M ⟶ N}, φ₁ = φ₂ ↔ φ₁.hom = φ₂.hom
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instSubtractionCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α],
  AddOpposite.instSubtractionCommMonoid = { toSubtractionMonoid := AddOpposite.instSubtractionMonoid, add_comm := ⋯ }
-- Mathlib.Order.KrullDimension
/-- Variant of `height_le_iff` ranging only over those series that end exactly on `a`.
 -/
Order.height_le_iff' : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ∞},
  Order.height a ≤ n ↔ ∀ ⦃p : LTSeries α⦄, RelSeries.last p = a → ↑p.length ≤ n
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.constMergeWith! : ∀ {α : Type u} {β : Type v} {x : Ord α} {mergeFn : α → β → β → β} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β},
  t₁.WF → (Std.DTreeMap.Internal.Impl.Const.mergeWith! mergeFn t₁ t₂).WF
-- Mathlib.Topology.DiscreteSubset
codiscreteWithin_eq_bot_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set X}, Filter.codiscreteWithin S = ⊥ ↔ IsDiscrete S
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.TreeMap.ofList l cmp).getKeyD k' fallback = k
-- Init.Data.UInt.Lemmas
UInt64.ofNatLT_uInt16ToNat : ∀ (n : UInt16), UInt64.ofNatLT n.toNat ⋯ = n.toUInt64
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.instHasSheafifyBotGrothendieckTopology : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} A],
  CategoryTheory.HasSheafify ⊥ A
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.mapArrowRight_comp_assoc : ∀ {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₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {f₁ : CategoryTheory.Arrow C₁}
  {f₃ f₃' : CategoryTheory.Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom)
  {f₃'' : CategoryTheory.Arrow C₃} (sq₁₃'' : G.PullbackObjObj f₁.hom f₃''.hom) (sq : f₃ ⟶ f₃') (sq' : f₃' ⟶ f₃'')
  {Z : CategoryTheory.Arrow C₂} (h : CategoryTheory.Arrow.mk sq₁₃''.π ⟶ Z),
  CategoryTheory.CategoryStruct.comp (sq₁₃.mapArrowRight sq₁₃' sq)
      (CategoryTheory.CategoryStruct.comp (sq₁₃'.mapArrowRight sq₁₃'' sq') h) =
    CategoryTheory.CategoryStruct.comp (sq₁₃.mapArrowRight sq₁₃'' (CategoryTheory.CategoryStruct.comp sq sq')) h
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearMap.baseChange_neg : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : Ring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  (f : M →ₗ[R] N), LinearMap.baseChange A (-f) = -LinearMap.baseChange A f
-- Std.Async.IO
Std.Async.IO.AsyncRead.mk : {α β : Type} → (α → Std.Async.Async β) → Std.Async.IO.AsyncRead α β
-- Mathlib.Order.Interval.Set.SurjOn
surjOn_Ico_of_monotone_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β},
  Monotone f → Function.Surjective f → ∀ (a b : α), Set.SurjOn f (Set.Ico a b) (Set.Ico (f a) (f b))
-- Mathlib.Analysis.Convex.Exposed
/-- A useful way to build exposed sets from intersecting `A` with half-spaces (modelled by an
inequality with a functional).  -/
ContinuousLinearMap.toExposed : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : TopologicalSpace 𝕜] →
      [inst_1 : Ring 𝕜] →
        [PartialOrder 𝕜] →
          [inst_3 : AddCommMonoid E] →
            [inst_4 : TopologicalSpace E] → [inst_5 : Module 𝕜 E] → StrongDual 𝕜 E → Set E → Set E
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_inf : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] (s t : Submodule R M),
  Submodule.restrictScalars S (s ⊓ t) = Submodule.restrictScalars S s ⊓ Submodule.restrictScalars S t
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.inj : Lean.Meta.Grind.AttrKind
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.R1Space : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω],
  R1Space (MeasureTheory.ProbabilityMeasure Ω)
-- Mathlib.Data.List.Rotate
List.nodup_rotate : ∀ {α : Type u} {l : List α} {n : ℕ}, (l.rotate n).Nodup ↔ l.Nodup
-- Mathlib.Geometry.Euclidean.Triangle
/-- A variant of the law of sines, (two given sides are nonzero), vector angle form.  -/
InnerProductGeometry.sin_angle_div_norm_eq_sin_angle_div_norm : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  x ≠ 0 →
    x - y ≠ 0 →
      Real.sin (InnerProductGeometry.angle x y) / ‖x - y‖ = Real.sin (InnerProductGeometry.angle y (x - y)) / ‖x‖
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.comp_unify : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [DirectedSystem G fun i j h => ⇑(f i j h)] {α : Type u_1}
  {x : α → FirstOrder.Language.Structure.Sigma f} {i j : ι} (ij : i ≤ j)
  (h : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))),
  ⇑(f i j ij) ∘ FirstOrder.Language.DirectLimit.unify f x i h = FirstOrder.Language.DirectLimit.unify f x j ⋯
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.coe_sSup : ∀ {R : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : TopologicalSpace N]
  [inst_3 : Module R N] [inst_4 : ContinuousAdd N] [inst_5 : ContinuousConstSMul R N] (S : Set (ClosedSubmodule R N)),
  ↑(sSup S) = closure (⨆ s ∈ S, ↑s).carrier
-- Mathlib.Combinatorics.Matroid.Map
Matroid.restrictSubtype_isBasis_iff : ∀ {α : Type u_1} {M : Matroid α} {Y : Set α} {I X : Set ↑Y},
  (M.restrictSubtype Y).IsBasis I X ↔ M.IsBasis' (Subtype.val '' I) (Subtype.val '' X)
-- Mathlib.Logic.Equiv.Option
Equiv.optionCongr_injective : ∀ {α : Type u_1} {β : Type u_2}, Function.Injective Equiv.optionCongr
-- Mathlib.RingTheory.DedekindDomain.Basic
Ring.DimensionLEOne.eq_bot_of_lt : ∀ {R : Type u_1} [inst : CommRing R] [Ring.DimensionLEOne R] (p P : Ideal R) [p.IsPrime] [P.IsPrime], p < P → p = ⊥
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- Replacing an empty cone in `IsLimit` by another with the same cone point
is an equivalence.  -/
CategoryTheory.Limits.isLimitEmptyConeEquiv : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F₁ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C} →
      {F₂ : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w' + 1}) C} →
        (c₁ : CategoryTheory.Limits.Cone F₁) →
          (c₂ : CategoryTheory.Limits.Cone F₂) →
            (c₁.pt ≅ c₂.pt) → CategoryTheory.Limits.IsLimit c₁ ≃ CategoryTheory.Limits.IsLimit c₂
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_sq_add_S_sq : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.S R n ^ 2 + Polynomial.Chebyshev.S R (n + 1) ^ 2 -
      Polynomial.X * Polynomial.Chebyshev.S R n * Polynomial.Chebyshev.S R (n + 1) =
    1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.inter_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₂.Equiv m₃ → (m₁ ∩ m₂).Equiv (m₁ ∩ m₃)
-- Mathlib.Computability.Reduce
Equiv.Computable.trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {e₁ : α ≃ β} {e₂ : β ≃ γ}, e₁.Computable → e₂.Computable → (e₁.trans e₂).Computable
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.cosimplicialSimplicialEquiv_counitIso_hom_app_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor SimplexCategoryᵒᵖ Cᵒᵖ)
  (X_1 : SimplexCategoryᵒᵖ),
  ((CategoryTheory.cosimplicialSimplicialEquiv C).counitIso.hom.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Mathlib.MeasureTheory.Measure.Map
/-- If we map a measure along a measurable equivalence, we can compute the measure on all sets
(not just the measurable ones).  -/
MeasurableEquiv.map_apply : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  (f : α ≃ᵐ β) (s : Set β), (MeasureTheory.Measure.map (⇑f) μ) s = μ (⇑f ⁻¹' s)
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Φ_coeff_φ_natDegree_ne_zero : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ → (RatFunc.Luroth.Φ✝ E).coeff (RatFunc.Luroth.φ✝ E).natDegree ≠ 0
-- Mathlib.Data.Semiquot
Semiquot.pure_isPure : ∀ {α : Type u_1} (a : α), (pure a).IsPure
-- Mathlib.LinearAlgebra.Matrix.BaseChange
Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_left : ∀ {m : Type u_1} {n : Type u_2} {L : Type u_3} [Finite m] [inst : Fintype n] [inst_1 : DecidableEq m] [inst_2 : Field L]
  (e : m ≃ n) (K : Subfield L) {A : Matrix m n L} {B : Matrix n m L},
  A * B = 1 → (∀ (i : n) (j : m), B i j ∈ K) → ∀ (i : m) (j : n), A i j ∈ K
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.Subcanonical.le_canonical : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C}
  [self : J.Subcanonical], J ≤ CategoryTheory.Sheaf.canonicalTopology C
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.isOrtho_top_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {V : Submodule 𝕜 E}, ⊤ ⟂ V ↔ V = ⊥
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- Equivalent additive monoids have additively isomorphic additive monoid algebras.

`AddMonoidAlgebra.mapDomain` as an `AddEquiv`.  -/
AddMonoidAlgebra.mapDomainAddEquiv : (R : Type u_3) →
  {M : Type u_6} →
    {N : Type u_7} →
      [inst : Semiring R] → [inst_1 : Add M] → [inst_2 : Add N] → M ≃ N → AddMonoidAlgebra R M ≃+ AddMonoidAlgebra R N
-- Mathlib.Probability.Independence.CharacteristicFunction
/-- A finite number of random variables are independent if and only if their joint characteristic
function is equal to the product of the characteristic functions. This is the version for Hilbert
spaces, see `iIndepFun_iff_charFunDual_pi` for the Banach space version.  -/
ProbabilityTheory.iIndepFun_iff_charFun_pi : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} [inst : Fintype ι]
  [MeasureTheory.IsProbabilityMeasure P] {E : ι → Type u_3} {mE : (i : ι) → MeasurableSpace (E i)}
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [∀ (i : ι), CompleteSpace (E i)] [∀ (i : ι), BorelSpace (E i)]
  [∀ (i : ι), SecondCountableTopology (E i)] {X : (i : ι) → Ω → E i} [inst_6 : (i : ι) → InnerProductSpace ℝ (E i)],
  (∀ (i : ι), AEMeasurable (X i) P) →
    (ProbabilityTheory.iIndepFun X P ↔
      ∀ (t : WithLp 2 ((x : ι) → E x)),
        MeasureTheory.charFun (MeasureTheory.Measure.map (fun ω => WithLp.toLp 2 fun x => X x ω) P) t =
          ∏ i, MeasureTheory.charFun (MeasureTheory.Measure.map (X i) P) (t.ofLp i))
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDF.isRatStieltjesPoint_ae : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ℚ → ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsRatCondKernelCDF f κ ν →
    ∀ (a : α), ∀ᵐ (b : β) ∂ν a, ProbabilityTheory.IsRatStieltjesPoint f (a, b)
-- Mathlib.Data.EReal.Operations
EReal.mul_bot_of_neg : ∀ {x : EReal}, x < 0 → x * ⊥ = ⊤
-- Init.Data.String.Lemmas.Pattern.Basic
_private.Init.Data.String.Lemmas.Pattern.Basic.0.String.Slice.Pattern.Model.matchAt?.eq_def : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} (startPos : s.Pos),
  String.Slice.Pattern.Model.matchAt? pat startPos =
    if h : ∃ endPos, String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos then some h.choose else none
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.image_eq_inter_preimage_of_subset_support : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E] {s : Set M},
  s ⊆ Function.support ↑f →
    ↑(extChartAt I c) '' s =
      Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I ∩ ↑(extChartAt I c).symm ⁻¹' s
-- Init.Data.Ord.SInt
Int8.instLawfulEqOrd : Std.LawfulEqOrd Int8
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.add_right_cancel : ∀ {a b : Ordinal.{u_4}} (n : ℕ), a + ↑n = b + ↑n ↔ a = b
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.brecOn_1.go : {pu : Lean.Compiler.LCNF.Purity} →
  {motive_1 : Lean.Compiler.LCNF.Alt pu → Sort u} →
    {motive_2 : Lean.Compiler.LCNF.FunDecl pu → Sort u} →
      {motive_3 : Lean.Compiler.LCNF.Cases pu → Sort u} →
        {motive_4 : Lean.Compiler.LCNF.Code pu → Sort u} →
          {motive_5 : Array (Lean.Compiler.LCNF.Alt pu) → Sort u} →
            {motive_6 : List (Lean.Compiler.LCNF.Alt pu) → Sort u} →
              (t : Array (Lean.Compiler.LCNF.Alt pu)) →
                ((t : Lean.Compiler.LCNF.Alt pu) → t.below → motive_1 t) →
                  ((t : Lean.Compiler.LCNF.FunDecl pu) → t.below → motive_2 t) →
                    ((t : Lean.Compiler.LCNF.Cases pu) → t.below → motive_3 t) →
                      ((t : Lean.Compiler.LCNF.Code pu) → t.below → motive_4 t) →
                        ((t : Array (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_1 t → motive_5 t) →
                          ((t : List (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_2 t → motive_6 t) →
                            motive_5 t ×' Lean.Compiler.LCNF.Alt.below_1 t
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddModObj.add_vadd_self_flip_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M] (X : C) [inst_3 : CategoryTheory.AddModObj M X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.AddModObj.vadd)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add X)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd h))