mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.op_X₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C), sq.op.X₃ = Opposite.op sq.X₃
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.tendsto_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α} {t : Set β},
  ContinuousWithinAt f s x → Set.MapsTo f s t → Filter.Tendsto f (nhdsWithin x s) (nhdsWithin (f x) t)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- (Implementation) `t'` in the glue data for `𝒪ₓ/I`.  -/
AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux : {X : AlgebraicGeometry.Scheme} →
  (I : X.IdealSheafData) →
    (U V W U₀ : ↑X.affineOpens) →
      ↑U ⊓ ↑W ≤ ↑U₀ →
        (CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))
            (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ⟶
          I.glueDataObjPullback V U₀)
-- Mathlib.Order.Birkhoff
OrderEmbedding.infIrredUpperSet_apply : ∀ {α : Type u_1} [inst : PartialOrder α] (a : α), OrderEmbedding.infIrredUpperSet a = ⟨UpperSet.Ici a, ⋯⟩
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_conj : ∀ {𝔸 : Type u_1} [inst : NormedDivisionRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (y x : 𝔸),
  y ≠ 0 → NormedSpace.exp (y * x * y⁻¹) = y * NormedSpace.exp x * y⁻¹
-- Init.Data.Vector.Zip
Vector.map_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {δ : Type u_4} {f : α → β} {g : γ → δ → α} {as : Vector γ n}
  {bs : Vector δ n}, Vector.map f (Vector.zipWith g as bs) = Vector.zipWith (fun x y => f (g x y)) as bs
-- Mathlib.Data.Set.Prod
Set.decidableMemProd : {α : Type u_1} →
  {β : Type u_2} →
    {s : Set α} →
      {t : Set β} → [DecidablePred fun x => x ∈ s] → [DecidablePred fun x => x ∈ t] → DecidablePred fun x => x ∈ s ×ˢ t
-- Mathlib.Order.Lattice
Lattice.toSemilatticeSup : {α : Type u} → [self : Lattice α] → SemilatticeSup α
-- Mathlib.Computability.TuringMachine.Tape
_private.Mathlib.Computability.TuringMachine.Tape.0.Turing.ListBlank.modifyNth.match_1.splitter : {Γ : Type u_1} →
  [inst : Inhabited Γ] →
    (motive : ℕ → Turing.ListBlank Γ → Sort u_2) →
      (x : ℕ) →
        (x_1 : Turing.ListBlank Γ) →
          ((L : Turing.ListBlank Γ) → motive 0 L) →
            ((n : ℕ) → (L : Turing.ListBlank Γ) → motive n.succ L) → motive x x_1
-- Mathlib.Topology.UniformSpace.Cauchy
isComplete_univ : ∀ {α : Type u} [inst : UniformSpace α] [CompleteSpace α], IsComplete Set.univ
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.componentwiseDiagram_obj : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) [inst_2 : CategoryTheory.Limits.HasColimit F]
  (U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F)) (j : Jᵒᵖ),
  (AlgebraicGeometry.PresheafedSpace.componentwiseDiagram F U).obj j =
    (F.obj (Opposite.unop j)).presheaf.obj
      (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.Limits.colimit.ι F (Opposite.unop j)).base).obj U))
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.minView!.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k' : α) (v' : β k')
  (l' r' : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r')),
  (match Std.DTreeMap.Internal.Impl.inner size k' v' l' r' with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r' => h_2 size k' v' l' r') =
    h_2 size k' v' l' r'
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.instInhabitedLabel : Inhabited Lean.Meta.NormCast.Label
-- Mathlib.Lean.Expr.Basic
/-- Auxiliary for `Name.fromComponents`  -/
_private.Mathlib.Lean.Expr.Basic.0.Lean.Name.fromComponents.go : Lean.Name → List Lean.Name → Lean.Name
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- Given a morphism property `P` in a category `C`, a functor `F : C ⥤ D` and a morphism
`f : X ⟶ Y` in `D`. Then `f` satisfies the morphism property `P.relative` with respect to `F` iff:
* The morphism is representable with respect to `F`
* For any morphism `g : F.obj a ⟶ Y`, the property `P` holds for any represented pullback of
  `f` by `g`.  -/
CategoryTheory.MorphismProperty.relative : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty D
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.getEntryGE.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] (k : α)
  (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.Ordered → (∃ a ∈ x, (compare a k).isGE = true) → Sort u_3)
  (size : ℕ) (ky : α) (y : β) (l r : Std.DTreeMap.Internal.Impl α fun x => β)
  (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isGE = true)
  (h_1 :
    (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
      (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isGE = true) →
        motive Std.DTreeMap.Internal.Impl.leaf x he)
  (h_2 :
    (size : ℕ) →
      (ky : α) →
        (y : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isGE = true) →
                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he),
  (match Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => h_1 x he
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he => h_2 size ky y l r ho he) =
    h_2 size ky y l r ho he
-- Mathlib.Data.ENat.Basic
ENat.toNat_one : ENat.toNat 1 = 1
-- Mathlib.Topology.Convenient.Category
/-- The unit (isomorphism) of the adjunction `GeneratedByTopCat.adj` between
the categories `GeneratedByTopCat X` and `TopCat`.  -/
GeneratedByTopCat.adjUnitIso : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      CategoryTheory.Functor.id (GeneratedByTopCat X) ≅ GeneratedByTopCat.toTopCat.comp TopCat.toGeneratedByTopCat
-- Mathlib.Logic.Function.Basic
Function.IsPartialInv.comp : ∀ {α : Type u_4} {β : Type u_5} {γ : Sort u_6} {f : α → β} {g : β → Option α} {h : β → γ} {i : γ → Option β},
  Function.IsPartialInv f g → Function.IsPartialInv h i → Function.IsPartialInv (h ∘ f) fun x => (i x).bind g
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- The identity on `R[X₁, ..., Xₙ]` as a map of presentations of `T` to `S`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.fhom : {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.Generators.PresentationOfFreeCotangent.Aux.presLeft✝ D).Hom P
-- Mathlib.Computability.Reduce
toNat.eq_1 : ∀ {α : Type u} [inst : Primcodable α] [inst_1 : Inhabited α] (p : Set α),
  toNat p = {n | p ((Encodable.decode n).getD default)}
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
ProbabilityTheory.BrownianReal.isProjectiveMeasureFamily_projectiveFamily : MeasureTheory.IsProjectiveMeasureFamily ProbabilityTheory.BrownianReal.projectiveFamily
-- Lean.Util.Trace
Lean.TraceElem.ref : Lean.TraceElem → Lean.Syntax
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.grind.param.codeAction : Lean.Option Bool
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- Lift a ring hom to `WithAbs`.  -/
WithAbs.map : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] →
      [inst_1 : PartialOrder S] →
        [inst_2 : Semiring R] →
          (v : AbsoluteValue R S) →
            {T : Type u_3} → [inst_3 : Semiring T] → (w : AbsoluteValue T S) → (R →+* T) → WithAbs v →+* WithAbs w
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.forIn_eq_forIn_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ}, forIn t init f = forIn t.toArray init f
-- Lean.Meta.Tactic.Grind.Split
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.Action.isCompressibleAlts : Array (List (Lean.TSyntax `grind)) → Bool
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousWithinAt.congr_of_eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r r' : α → β → Prop} {s : Set α} {a : α},
  SemicontinuousWithinAt r s a →
    a ∈ s → (∀ᶠ (x : α) in nhdsWithin a s, ∀ (y : β), r x y ↔ r' x y) → SemicontinuousWithinAt r' s a
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.map_rel : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] (φ : L.Hom M N)
  {n : ℕ} (r : L.Relations n) (x : Fin n → M),
  FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.mk_pow : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] (x : Submonoid A) (i : HomogeneousLocalization.NumDenSameDeg 𝒜 x) (n : ℕ),
  HomogeneousLocalization.mk (i ^ n) = HomogeneousLocalization.mk i ^ n
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
HasFDerivAt.clog : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E},
  HasFDerivAt f f' x → f x ∈ Complex.slitPlane → HasFDerivAt (fun t => Complex.log (f t)) ((f x)⁻¹ • f') x
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
/-- **Alias** of the reverse direction of `Multiplicative.toAdd_lt`. -/
Multiplicative.toAdd_strictMono : ∀ {α : Type u_1} [inst : Preorder α] {a b : Multiplicative α}, a < b → Multiplicative.toAdd a < Multiplicative.toAdd b
-- Aesop.EMap
Aesop.EMap.instForMProdExpr : {m : Type → Type u_1} → [Monad m] → {α : Type u_2} → ForM m (Aesop.EMap α) (Lean.Expr × α)
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_nonneg : ∀ {α : Type u_1} {G' : Type u_7} {G'' : Type u_8} [inst : NormedAddCommGroup G''] [inst_1 : PartialOrder G'']
  [IsOrderedAddMonoid G''] [inst_3 : NormedSpace ℝ G''] [inst_4 : NormedAddCommGroup G'] [inst_5 : PartialOrder G']
  [inst_6 : NormedSpace ℝ G'] {m : MeasurableSpace α} (T : Set α → G' →L[ℝ] G''),
  (∀ (s : Set α) (x : G'), 0 ≤ x → 0 ≤ (T s) x) →
    ∀ (f : MeasureTheory.SimpleFunc α G'), 0 ≤ f → 0 ≤ MeasureTheory.SimpleFunc.setToSimpleFunc T f
-- Mathlib.Order.SuccPred.Limit
/-- A predecessor pre-limit is a value that isn't covered by any other.

It's so named because in a predecessor order, a predecessor pre-limit can't be the predecessor of
anything smaller.

Use `IsPredLimit` to exclude the case of a maximal element.  -/
Order.IsPredPrelimit : {α : Type u_1} → [LT α] → α → Prop
-- Mathlib.Order.Fin.Basic
Fin.strictMono_castPred_comp : ∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : α → Fin (n + 1)} (hf : ∀ (a : α), f a ≠ Fin.last n),
  StrictMono f → StrictMono fun a => (f a).castPred ⋯
-- Mathlib.Algebra.Group.Subgroup.Basic
CommGroup.normalizer_eq_top : ∀ {G : Type u_5} [inst : CommGroup G] (s : Set G), Subgroup.normalizer s = ⊤
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Taking sub-families preserves equicontinuity on a subset.  -/
EquicontinuousOn.comp : ∀ {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α]
  {F : ι → X → α} {S : Set X}, EquicontinuousOn F S → ∀ (u : κ → ι), EquicontinuousOn (F ∘ u) S
-- Mathlib.Analysis.Calculus.Deriv.Inv
deriv_const_div_id : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} (c : 𝕜), deriv (fun x => c / x) x = -c / x ^ 2
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.rightUnitor_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom =
    CategoryTheory.SemiCartesianMonoidalCategory.fst X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Init.Data.String.Basic
String.Pos.ofToSlice_lt : ∀ {s : String} {p q : s.toSlice.Pos}, String.Pos.ofToSlice p < String.Pos.ofToSlice q ↔ p < q
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.FindSplitImpl.Context : Type
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ico_subset : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop} (a b : { x // p x }), Subtype.val '' Set.Ico a b ⊆ Set.Ico ↑a ↑b
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.ext_iff : ∀ {x y : ZFSet.{u}}, x = y ↔ ∀ (z : ZFSet.{u}), z ∈ x ↔ z ∈ y
-- Mathlib.Data.ENNReal.Basic
ENNReal.recTopCoe_top : ∀ {C : ENNReal → Sort u_2} (top : C ⊤) (coe : (x : NNReal) → C ↑x), ENNReal.recTopCoe top coe ⊤ = top
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.congr_mul : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] (f₁ f₂ : M ≃ₗ[A] M)
  (g₁ g₂ : N ≃ₗ[R] N),
  TensorProduct.AlgebraTensorModule.congr (f₁ * f₂) (g₁ * g₂) =
    TensorProduct.AlgebraTensorModule.congr f₁ g₁ * TensorProduct.AlgebraTensorModule.congr f₂ g₂
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- Construct a morphism from the coend using its universal property.  -/
CategoryTheory.Limits.Cowedge.IsColimit.desc : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
          {c : CategoryTheory.Limits.Cowedge F} →
            CategoryTheory.Limits.IsColimit c →
              {X : C} →
                (f : (j : J) → (F.obj (Opposite.op j)).obj j ⟶ X) →
                  (∀ ⦃i j : J⦄ (g : i ⟶ j),
                      CategoryTheory.CategoryStruct.comp ((F.map g.op).app i) (f i) =
                        CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j)) →
                    (c.pt ⟶ X)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.associative_ε₂_ε₁ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6}
  (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₃ : ComplexShape I₃) (c₁₂ : ComplexShape I₁₂) (c₂₃ : ComplexShape I₂₃)
  (c : ComplexShape J) [inst : TotalComplexShape c₁ c₂ c₁₂] [inst_1 : TotalComplexShape c₁₂ c₃ c]
  [inst_2 : TotalComplexShape c₂ c₃ c₂₃] [inst_3 : TotalComplexShape c₁ c₂₃ c] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
  c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₁ c₃ c₂₃ (i₂, i₃) =
    c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coe_mul : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : Mul R]
  [inst_3 : BoundedMul R] [inst_4 : ContinuousMul R] (f g : BoundedContinuousFunction α R), ⇑(f * g) = ⇑f * ⇑g
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_insertIfNew : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β k}, a ∈ m.insertIfNew k v ↔ (k == a) = true ∨ a ∈ m
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.monoidal_whiskerLeft_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X x x_1 : CategoryTheory.Comon C) (f : x ⟶ x_1),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X f.hom
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsBlock.disjoint_vadd_right : ∀ {M : Type u_1} {X : Type u_2} [inst : AddMonoid M] [inst_1 : AddAction M X] {B : Set X} {s : Set M},
  AddAction.IsBlock M B → ¬B ⊆ s +ᵥ B → Disjoint B (s +ᵥ B)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
/-- The `n`-th rescaled Chebyshev polynomial of the second kind (Vieta–Fibonacci polynomial)
evaluates on `2 * cosh θ` to the value `sinh ((n + 1) * θ) / sinh θ`.  -/
Polynomial.Chebyshev.S_two_mul_real_cosh : ∀ (θ : ℝ) (n : ℤ),
  Polynomial.eval (2 * Real.cosh θ) (Polynomial.Chebyshev.S ℝ n) * Real.sinh θ = Real.sinh ((↑n + 1) * θ)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- An induction principle for closure membership. If `p` holds for `0`, `1`, and all elements
of `s`, and is preserved under addition, negation, and multiplication, then `p` holds for all
elements of the closure of `s`.  -/
NonUnitalSubring.closure_induction : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R} {p : (x : R) → x ∈ NonUnitalSubring.closure s → Prop},
  (∀ (x : R) (hx : x ∈ s), p x ⋯) →
    p 0 ⋯ →
      (∀ (x y : R) (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s),
          p x hx → p y hy → p (x + y) ⋯) →
        (∀ (x : R) (hx : x ∈ NonUnitalSubring.closure s), p x hx → p (-x) ⋯) →
          (∀ (x y : R) (hx : x ∈ NonUnitalSubring.closure s) (hy : y ∈ NonUnitalSubring.closure s),
              p x hx → p y hy → p (x * y) ⋯) →
            ∀ {x : R} (hx : x ∈ NonUnitalSubring.closure s), p x hx
-- Mathlib.Topology.VectorBundle.Hom
/-- Consider a `C^n` map `v : M → E₁` to a vector bundle, over a basemap `b : M → B`, and
linear maps `ϕ m : E₁ (b m) → E₂ (b m)` depending smoothly on `m`.
One can apply `ϕ m` to `v m`, and the resulting map is `C^n`.  -/
ContinuousAt.clm_bundle_apply : ∀ {𝕜 : Type u_8} {B : Type u_9} {F₁ : Type u_10} {F₂ : Type u_11} {M : Type u_13} [inst : NontriviallyNormedField 𝕜]
  {E₁ : B → Type u_14} [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] {E₂ : B → Type u_15} [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)]
  [inst_13 : TopologicalSpace B] [inst_14 : TopologicalSpace M] [inst_15 : FiberBundle F₁ E₁]
  [inst_16 : VectorBundle 𝕜 F₁ E₁] [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂] {b : M → B}
  {v : (x : M) → E₁ (b x)} {x : M} [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] {ϕ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x)},
  ContinuousAt (fun m => ⟨b m, ϕ m⟩) x →
    ContinuousAt (fun m => ⟨b m, v m⟩) x → ContinuousAt (fun m => ⟨b m, (ϕ m) (v m)⟩) x
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.StateStack.newEntries : {α β σ : Type} → Lean.ScopedEnvExtension.StateStack α β σ → List (Lean.ScopedEnvExtension.Entry α)
-- Init.Data.Ord.Array
_private.Init.Data.Ord.Array.0.Array.compareLex.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_3 ()
-- Batteries.Data.List.Lemmas
List.idxOfNth_cons_zero : ∀ {α : Type u_1} {xs : List α} {x : α} [inst : BEq α] {a : α},
  List.idxOfNth x (a :: xs) 0 = if (a == x) = true then 0 else List.idxOfNth x xs 0 + 1
-- Init.Data.Int.Linear
Int.Internal.Linear.diseq_split_cert.eq_1 : ∀ (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.diseq_split_cert p₁ p₂ p₃ =
    (p₂.beq' (p₁.addConst_k 1)).and' (p₃.beq' ((p₁.mul_k (-1)).addConst_k 1))
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- the functor is compatible with the `MorphismProperty`  -/
CategoryTheory.LocalizerMorphism.map : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (self : CategoryTheory.LocalizerMorphism W₁ W₂),
  W₁ ≤ W₂.inverseImage self.functor
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.preserves_cokernel_iso_comp_cokernel_map_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f] [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G] {X' Y' : C} (g : X' ⟶ Y')
  [inst_8 : CategoryTheory.Limits.HasCokernel g] [inst_9 : CategoryTheory.Limits.HasCokernel (G.map g)]
  [inst_10 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair g 0) G] (p : X ⟶ X')
  (q : Y ⟶ Y') (hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g) {Z : D}
  (h : CategoryTheory.Limits.cokernel (G.map g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCokernel.iso G f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
        h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.cokernel.map f g p q hpq))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCokernel.iso G g).hom h)
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instIsStableUnderShiftIsoClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] [P.IsStableUnderShift A],
  P.isoClosure.IsStableUnderShift A
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.mk : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_4} →
        {V₂ : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : Module k V₁] →
                [inst_3 : AddTorsor V₁ P₁] →
                  [inst_4 : TopologicalSpace P₁] →
                    [inst_5 : AddCommGroup V₂] →
                      [inst_6 : Module k V₂] →
                        [inst_7 : AddTorsor V₂ P₂] →
                          [inst_8 : TopologicalSpace P₂] →
                            (toAffineEquiv : P₁ ≃ᵃ[k] P₂) →
                              autoParam (Continuous toAffineEquiv.toFun)
                                  ContinuousAffineEquiv.continuous_toFun._autoParam →
                                autoParam (Continuous toAffineEquiv.invFun)
                                    ContinuousAffineEquiv.continuous_invFun._autoParam →
                                  P₁ ≃ᴬ[k] P₂