mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
/-- Glue morphisms along a `0`-hypercover.  -/
CategoryTheory.Precoverage.ZeroHypercover.glueMorphisms : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      [J.toGrothendieck.Subcanonical] →
        {S T : C} →
          (𝒰 : J.ZeroHypercover S) →
            [inst_2 : 𝒰.HasPullbacks] →
              (f : (i : 𝒰.I₀) → 𝒰.X i ⟶ T) →
                (∀ (i j : 𝒰.I₀),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f i) (𝒰.f j)) (f i) =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f i) (𝒰.f j)) (f j)) →
                  (S ⟶ T)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_inverse_obj_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).inverse.obj X).left = X.left
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- The canonical presentation of `S` as the localization of `T` away from `g`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.presRight : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) →
                    Algebra.Presentation (Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D) S Unit Unit
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_C : ∀ {R : Type u} {S : Type v} {a : R} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S),
  Polynomial.eval₂ f x (Polynomial.C a) = f a
-- Init.Data.String.Lemmas.Length
String.length_join : ∀ {l : List String}, (String.join l).length = (List.map String.length l).sum
-- Mathlib.Analysis.Analytic.WithLp
WithLp.analyticOn_ofLp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] (p : ENNReal)
  [inst_5 : Fact (1 ≤ p)] (s : Set (WithLp p (E × F))), AnalyticOn 𝕜 WithLp.ofLp s
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.forIn'_eq_forIn'_toArray : ∀ {α : Type u} {r : Std.Rci α} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_3 : Std.Rxi.IsAlwaysFinite α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_5 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toArray init fun a ha acc => f a ⋯ acc
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.monic_esymm : ∀ {R : Type u_3} {m : ℕ} [inst : CommSemiring R] {i : ℕ},
  i ≤ m → AddMonoidAlgebra.Monic (⇑toLex) (MvPolynomial.esymm (Fin m) R i)
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.eq_of_eqOnSource_univ : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e e' : OpenPartialHomeomorph X Y}, e ≈ e' → e.source = Set.univ → e.target = Set.univ → e = e'
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom.mk : {m : Type → Type} →
  (Mathlib.Tactic.BicategoryLike.CoherenceHom → m Mathlib.Tactic.BicategoryLike.Mor₂Iso) →
    Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom m
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
ContinuousLinearMap.restrictScalars_sub : ∀ {A : Type u_1} {R : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [inst : Ring A] [inst_1 : Ring R]
  [inst_2 : AddCommGroup M₁] [inst_3 : Module A M₁] [inst_4 : Module R M₁] [inst_5 : TopologicalSpace M₁]
  [inst_6 : AddCommGroup M₂] [inst_7 : Module A M₂] [inst_8 : Module R M₂] [inst_9 : TopologicalSpace M₂]
  [inst_10 : LinearMap.CompatibleSMul M₁ M₂ R A] [inst_11 : IsTopologicalAddGroup M₂] (f g : M₁ →L[A] M₂),
  ContinuousLinearMap.restrictScalars R (f - g) =
    ContinuousLinearMap.restrictScalars R f - ContinuousLinearMap.restrictScalars R g
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_mod : ∀ (a b : BitVec 8), { toBitVec := a % b } = { toBitVec := a } % { toBitVec := b }
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toContinuousLinearEquiv_trans : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R}
  {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_5 : RingHomInvPair σ₁₃ σ₃₁] [inst_6 : RingHomInvPair σ₃₁ σ₁₃] [inst_7 : RingHomInvPair σ₂₃ σ₃₂]
  [inst_8 : RingHomInvPair σ₃₂ σ₂₃] [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
  [inst_11 : SeminormedAddCommGroup E] [inst_12 : SeminormedAddCommGroup E₂] [inst_13 : SeminormedAddCommGroup E₃]
  [inst_14 : Module R E] [inst_15 : Module R₂ E₂] [inst_16 : Module R₃ E₃] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃),
  ↑(e.trans e') = (↑e).trans ↑e'
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.Pivot.listTransvecCol.eq_1 : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
  Matrix.Pivot.listTransvecCol M =
    List.ofFn fun i =>
      Matrix.transvection (Sum.inl i) (Sum.inr ()) (-M (Sum.inl i) (Sum.inr ()) / M (Sum.inr ()) (Sum.inr ()))
-- Mathlib.NumberTheory.BernoulliPolynomials
/-- The theorem that $(e^X - 1) * ∑ Bₙ(t)* X^n/n! = Xe^{tX}$  -/
Polynomial.bernoulli_generating_function : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Algebra ℚ A] (t : A),
  (PowerSeries.mk fun n => (Polynomial.aeval t) ((1 / ↑n.factorial) • Polynomial.bernoulli n)) *
      (PowerSeries.exp A - 1) =
    PowerSeries.X * (PowerSeries.rescale t) (PowerSeries.exp A)
-- Mathlib.Order.RelSeries
RelSeries.last_reverse : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r), p.reverse.last = p.head
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X Y : C} (φ : X ⟶ Y),
  ((t.triangleLTGE n).map φ).hom₁ = (t.truncLT n).map φ
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedFunctor.instIsHomLiftObjPIdObj : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴) (a : 𝒳.obj),
  𝒴.p.IsHomLift (CategoryTheory.CategoryStruct.id (𝒳.p.obj a)) (CategoryTheory.CategoryStruct.id (F.obj a))
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.truncTotal_coe_eq_self_iff : ∀ {σ : Type u_1} {R : Type u_2} {n : ℕ} [inst : Finite σ] [inst_1 : CommSemiring R] (p : MvPolynomial σ R),
  n ≠ 0 → ((MvPowerSeries.truncTotal n) ↑p = p ↔ p.totalDegree < n)
-- Mathlib.Data.NNReal.Defs
NNReal.coe_zero : ↑0 = 0
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableSMul.measurable_smul_const : ∀ {M : Type u_2} {α : Type u_3} {inst : SMul M α} {inst_1 : MeasurableSpace M} {inst_2 : MeasurableSpace α}
  [self : MeasurableSMul M α] (x : α), Measurable fun x_1 => x_1 • x
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The functor `Sheaf J A ⥤ Cᵒᵖ ⥤ A` is fully faithful.  -/
CategoryTheory.fullyFaithfulSheafToPresheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} A] → (CategoryTheory.sheafToPresheaf J A).FullyFaithful
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Result.step.inj : ∀ {e' : Lean.Expr} {done : Bool} {e'_1 : Lean.Expr} {done_1 : Bool},
  Lean.Meta.Sym.DSimp.Result.step e' done = Lean.Meta.Sym.DSimp.Result.step e'_1 done_1 → e' = e'_1 ∧ done = done_1
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.mul_inverse_cancel : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (x : M₀), IsUnit x → x * Ring.inverse x = 1
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The submodule of `G`-invariant elements of a continuous representation.  -/
ContRepresentation.invariants : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : Monoid G] →
        [inst_1 : Ring R] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : TopologicalSpace V] →
              [inst_4 : IsTopologicalAddGroup V] → [inst_5 : Module R V] → ContRepresentation R G V → Submodule R V
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.single_mul_single : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {a b : Γ} {r s : R},
  (HahnSeries.single a) r * (HahnSeries.single b) s = (HahnSeries.single (a + b)) (r * s)
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_right_Q : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ)
  (hpq : (c r).prev pq' = pq) (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData._auto_3),
  (X.spectralSequenceHomologyData data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃'
          n₀ n₁ n₂ hn₁' hn₁ hn₂).right.Q =
    X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯
-- Lean.Environment
/-- Diagnostic information collected during kernel execution.

Remark: We store kernel diagnostic information in an environment field to simplify the interface
with the kernel implemented in C/C++. Thus, we can only track declarations in methods, such as
`addDecl`, which return a new environment. `Kernel.isDefEq` and `Kernel.whnf` do not update the
statistics. We claim this is ok since these methods are mainly used for debugging.
 -/
Lean.Kernel.Environment.diagnostics : Lean.Kernel.Environment → Lean.Kernel.Diagnostics
-- Mathlib.Topology.Order.Category.AlexDisc
/-- The category of Alexandrov-discrete spaces.  -/
AlexDisc : Type (u_1 + 1)
-- Mathlib.MeasureTheory.Measure.Haar.DistribChar
MeasureTheory.distribHaarChar_apply : ∀ {G : Type u_1} (A : Type u_2) [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  [inst_3 : TopologicalSpace A] [inst_4 : IsTopologicalAddGroup A] [inst_5 : LocallyCompactSpace A]
  [inst_6 : ContinuousConstSMul G A] (g : G),
  (MeasureTheory.distribHaarChar A) g =
    (DomMulAct.mk g • MeasureTheory.Measure.addHaar).addHaarScalarFactor MeasureTheory.Measure.addHaar
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.apply_eq_true_of_revSkipWhile_le_bool : ∀ {p : Char → Bool} {s : String} {pos pos' : s.Pos} (h₁ : pos' < pos), pos.revSkipWhile p ≤ pos' → p (pos'.get ⋯) = true
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_add : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {f g : α → E} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ →
      MeasureTheory.setToFun μ T hT (f + g) = MeasureTheory.setToFun μ T hT f + MeasureTheory.setToFun μ T hT g
-- Init.Data.Vector.Range
Vector.getElem_range' : ∀ {start size step i : ℕ} (h : i < size), (Vector.range' start size step)[i] = start + step * i
-- Mathlib.Order.DirSupClosed
DirSupClosed.mem_iff_of_antisymmRel : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α],
  DirSupClosed s → ∀ {a b : α}, AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → (a ∈ s ↔ b ∈ s)
-- Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
/-- Shows that `Aₙ = bₙ * Aₙ₋₁ + aₙ * Aₙ₋₂` and `Bₙ = bₙ * Bₙ₋₁ + aₙ * Bₙ₋₂`.  -/
GenContFract.conts_recurrence : ∀ {K : Type u_1} {g : GenContFract K} {n : ℕ} [inst : DivisionRing K] {gp ppred pred : GenContFract.Pair K},
  g.s.get? (n + 1) = some gp →
    g.conts n = ppred →
      g.conts (n + 1) = pred →
        g.conts (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
-- Mathlib.SetTheory.Ordinal.Veblen
/-- `veblenWith f o₁ a ≤ veblenWith f o₂ b` iff one of the following holds:
* `o₁ = o₂` and `a ≤ b`
* `o₁ < o₂` and `a ≤ veblenWith f o₂ b`
* `o₁ > o₂` and `veblenWith f o₁ a ≤ b`  -/
Ordinal.veblenWith_le_veblenWith_iff : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a b : Ordinal.{u}},
  Order.IsNormal f →
    (Ordinal.veblenWith f o₁ a ≤ Ordinal.veblenWith f o₂ b ↔
      o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ Ordinal.veblenWith f o₂ b ∨ o₂ < o₁ ∧ Ordinal.veblenWith f o₁ a ≤ b)
-- Lean.Meta.SynthInstance
Lean.Meta.synthInstance.maxHeartbeats : Lean.Option ℕ
-- Std.Do.SPred.Notation
/-- Unexpander that reconstructs `spred(... ∧ ...)⌝` syntax from applications of `SPred.and`, lifting
nested applications of `spred(...)` from the arguments.
 -/
Std.Do.SPred.Notation.unexpandAnd : Lean.PrettyPrinter.Unexpander
-- Lean.Meta.MethodSpecs
/-- Whether the specs should be public or private  -/
_private.Lean.Meta.MethodSpecs.0.Lean.MethodSpecsInfo.privateSpecs : Lean.MethodSpecsInfo✝ → Bool
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.ExtendScalars.hom_ext_iff : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S} {M : ModuleCat R}
  {N : ModuleCat S} {α β : (ModuleCat.extendScalars f).obj M ⟶ N},
  α = β ↔
    ∀ (m : ↑M),
      (CategoryTheory.ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (CategoryTheory.ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach.0.Std.IterM.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The inner product of a nonzero vector with a nonzero multiple of
itself, divided by the product of their norms, has absolute value 1.  -/
norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x : E} {r : 𝕜}, x ≠ 0 → r ≠ 0 → ‖inner 𝕜 x (r • x)‖ / (‖x‖ * ‖r • x‖) = 1
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
CategoryTheory.Sheaf.H.addEquiv₀_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] {F G : CategoryTheory.Sheaf J AddCommGrpCat}
  (f : F ⟶ G) (x : F.H 0),
  CategoryTheory.Abelian.Ext.addEquiv₀ ((CategoryTheory.Sheaf.H.map f 0) x) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.Ext.addEquiv₀ x) f
-- Mathlib.Logic.Small.Defs
small_lift : ∀ (α : Type u) [hα : Small.{v, u} α], Small.{max v w, u} α
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The tangent of an angle in a right-angled triangle as a ratio of sides, version subtracting
vectors.  -/
Orientation.tan_oangle_sub_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle y (y - x)).tan = ‖x‖ / ‖y‖
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.IsStandardSmooth.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  f.IsStandardSmooth = Algebra.IsStandardSmooth R S
-- ProofWidgets.Component.RefreshComponent
/-- Create a `RefreshComponent` together with a dedicated thread that drives it by running `k`.

The typeclass assumptions essentially require `m` to extend `CoreM`.
For early cooperative cancellation of `CoreM` computations,
we automatically pass `RefreshToken.cancelTk` to `Core.Context`.  -/
ProofWidgets.mkRefreshComponentM : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT BaseIO m] →
      [MonadSaveCtx m (EIO Lean.Exception)] →
        [MonadWithReaderOf Lean.Core.Context m] →
          ProofWidgets.Html → (ProofWidgets.RefreshToken → m Unit) → m ProofWidgets.Html
-- Mathlib.Order.Interval.Set.Pi
/-- If `x`, `y`, `x'`, and `y'` are functions `Π i : ι, α i`, then
the set difference between the box `[x, y]` and the product of the open intervals `(x' i, y' i)`
is covered by the union of the following boxes: for each `i : ι`, we take
`[x, update y i (x' i)]` and `[update x i (y' i), y]`.

E.g., if `x' = x` and `y' = y`, then this lemma states that the difference between a closed box
`[x, y]` and the corresponding open box `{z | ∀ i, x i < z i < y i}` is covered by the union
of the faces of `[x, y]`.  -/
Set.Icc_sdiff_pi_univ_Ioo_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → LinearOrder (α i)]
  (x y x' y' : (i : ι) → α i),
  (Set.Icc x y \ Set.univ.pi fun i => Set.Ioo (x' i) (y' i)) ⊆
    (⋃ i, Set.Icc x (Function.update y i (x' i))) ∪ ⋃ i, Set.Icc (Function.update x i (y' i)) y
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.IsCardinalFiltered.nonempty_cocone : ∀ {J : Type u} {inst : CategoryTheory.Category.{v, u} J} {κ : Cardinal.{w}} {inst_1 : Fact κ.IsRegular}
  [self : CategoryTheory.IsCardinalFiltered J κ] {A : Type w} [inst_2 : CategoryTheory.SmallCategory A]
  (F : CategoryTheory.Functor A J), HasCardinalLT (CategoryTheory.Arrow A) κ → Nonempty (CategoryTheory.Limits.Cocone F)
-- Mathlib.Order.Lattice
sup_right_comm : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c : α), a ⊔ b ⊔ c = a ⊔ c ⊔ b
-- Mathlib.Util.Superscript
/-- Applies the alignment mapping to a `Syntax`.  -/
_private.Mathlib.Util.Superscript.0.Mathlib.Tactic.Superscript.scriptFnNoAntiquot.alignSyntax : Lean.Parser.ParserContext → Array (String.Pos.Raw × String.Pos.Raw) → Lean.Syntax → Lean.Syntax
-- Init.Data.SInt.Lemmas
Int8.toUInt8_mul : ∀ (a b : Int8), (a * b).toUInt8 = a.toUInt8 * b.toUInt8
-- Mathlib.Algebra.Category.Ring.Basic
/-- Build a `RingEquiv` from an isomorphism in the category `CommRingCat`.  -/
CategoryTheory.Iso.commRingCatIsoToRingEquiv : {R S : CommRingCat} → (R ≅ S) → ↑R ≃+* ↑S
-- Aesop.Rule
Aesop.UnfoldRule.decl : Aesop.UnfoldRule → Lean.Name
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.index_eq_two : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] [Nontrivial α], (alternatingGroup α).index = 2
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Construct an affine map by verifying the relation between the map and its linear part at one
base point. Namely, this function takes a map `f : P₁ → P₂`, a linear map `f' : V₁ →ₗ[k] V₂`, and
a point `p` such that for any other point `p'` we have `f p' = f' (p' -ᵥ p) +ᵥ f p`.  -/
AffineMap.mk' : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        {P2 : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V1] →
              [inst_2 : Module k V1] →
                [inst_3 : AddTorsor V1 P1] →
                  [inst_4 : AddCommGroup V2] →
                    [inst_5 : Module k V2] →
                      [inst_6 : AddTorsor V2 P2] →
                        (f : P1 → P2) →
                          (f' : V1 →ₗ[k] V2) → (p : P1) → (∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p) → P1 →ᵃ[k] P2
-- Lean.ToExpr
Lean.instToExprInt.mkNat : ℕ → Lean.Expr
-- Mathlib.Data.List.Cycle
List.next_cons_cons_eq : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x z : α) (h : x ∈ x :: z :: l), (x :: z :: l).next x h = z
-- Mathlib.Tactic.GRewrite.Core
/-- Unify the given generalized rewrite lemma with the goal, so as to rewrite with it.
If `symm := true`, first use the `symm` tactic to swap the direction of the lemma.
`gcongr_forward` is used to deal with the case where the lemma is `a < b` and the goal is `a ≤ b`.
Returns whether the goal was closed by the lemma.
 -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.GRewriteLemma.apply : Mathlib.Tactic.GRewrite.GRewriteLemma✝ → Lean.MVarId → Bool → Mathlib.Tactic.GRewrite.Config → Lean.MetaM Bool
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFunDual_map : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {mF : MeasurableSpace F} {μ : MeasureTheory.Measure E}
  [OpensMeasurableSpace E] [BorelSpace F] (L : E →L[ℝ] F) (L' : StrongDual ℝ F),
  MeasureTheory.charFunDual (MeasureTheory.Measure.map (⇑L) μ) L' = MeasureTheory.charFunDual μ (L' ∘SL L)
-- Mathlib.Algebra.Group.Nat.Even
Nat.even_add_one : ∀ {n : ℕ}, Even (n + 1) ↔ ¬Even n
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.toLinearEquiv_mk' : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} {e : V ≃ₗ[A] W} (he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e),
  (Representation.Equiv.mk e he).toLinearEquiv = e
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_insertIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m → ∀ {a : α} {b : β a}, Std.DHashMap.Internal.Raw.WFImp ↑(m.insertIfNew a b)
-- Lean.DocString.Markdown
Lean.Doc.MarkdownM.InlineCtx.mk.sizeOf_spec : ∀ (inEmph inBold inLink : Bool),
  sizeOf { inEmph := inEmph, inBold := inBold, inLink := inLink } = 1 + sizeOf inEmph + sizeOf inBold + sizeOf inLink
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.map_X : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] (f : R →+* S),
  (PowerSeries.map f) PowerSeries.X = PowerSeries.X
-- Mathlib.Algebra.CharP.Basic
Prod.charZero_of_right : ∀ (R : Type u_1) (S : Type u_2) [inst : AddMonoidWithOne R] [inst_1 : AddMonoidWithOne S] [CharZero S], CharZero (R × S)