mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
HasFDerivAtFilter.restrictScalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {f : E → F} {f' : E →L[𝕜'] F}
  {L : Filter (E × E)}, HasFDerivAtFilter f f' L → HasFDerivAtFilter f (ContinuousLinearMap.restrictScalars 𝕜 f') L
-- Mathlib.Data.List.Induction
/-- A dependent recursion principle for nonempty lists. Useful for dealing with
operations like `List.head` which are not defined on the empty list.
 -/
List.recNeNil : {α : Type u_1} →
  {motive : (l : List α) → l ≠ [] → Sort u_2} →
    ((x : α) → motive [x] ⋯) →
      ((x : α) → (xs : List α) → (h : xs ≠ []) → motive xs h → motive (x :: xs) ⋯) →
        (l : List α) → (h : l ≠ []) → motive l h
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.symm.inj : ∀ {R : Type u} {inst : Rack R} {a b : Rack.PreEnvelGroup R} {hab hab_1 : Rack.PreEnvelGroupRel' R a b},
  hab.symm = hab_1.symm → hab = hab_1
-- Batteries.Data.Char.Basic
Char.val_ofNat : ∀ {n : ℕ}, n.isValidChar → (Char.ofNat n).val = UInt32.ofNat n
-- Mathlib.Data.Int.Log
/-- `zpow b` and `Int.log b` (almost) form a Galois connection.  -/
Int.zpow_le_iff_le_log : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  {b : ℕ}, 1 < b → ∀ {x : ℤ} {r : R}, 0 < r → (↑b ^ x ≤ r ↔ x ≤ Int.log b r)
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- A right extension `E : RightExtension L F` is a pointwise right Kan extension at `Y` when
`E.coneAt Y` is a limit cone.  -/
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} → L.RightExtension F → D → Type (max (max (max u_1 v_2) u_4) v_4)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.instPreservesOneHypercoversOpensOpensFunctorGrothendieckTopologyCarrierCarrierCommRingCat : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f],
  (AlgebraicGeometry.Scheme.Hom.opensFunctor f).PreservesOneHypercovers (Opens.grothendieckTopology ↥X)
    (Opens.grothendieckTopology ↥Y)
-- Mathlib.LinearAlgebra.Dimension.Constructions
rank_quotient_le : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M),
  Module.rank R (M ⧸ p) ≤ Module.rank R M
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.neg_inf : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (S T : Submodule R M), -(S ⊓ T) = -S ⊓ -T
-- Mathlib.Analysis.Calculus.FDeriv.WithLp
differentiable_piLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup H] [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : NormedSpace 𝕜 H] [Finite ι] (p : ENNReal) [Fact (1 ≤ p)] {f : H → PiLp p E},
  Differentiable 𝕜 f ↔ ∀ (i : ι), Differentiable 𝕜 fun x => (f x).ofLp i
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Fmla.subsumes_self : ∀ (f : Sat.Fmla), f.subsumes f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₁ → (t₁ ∪ t₂).getKeyD k fallback = t₂.getKeyD k fallback
-- Init.Data.UInt.Lemmas
UInt8.lt_iff_toNat_lt : ∀ {a b : UInt8}, a < b ↔ a.toNat < b.toNat
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.id_comp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (φ : A →ₐc[R] B), (BialgHom.id R B).comp φ = φ
-- Mathlib.Tactic.TacticAnalysis
/-- Run tactic code, given by a piece of syntax, in the context of a tactic info node.

Convenience abbreviation for `ContextInfo.runTacticCode`.  -/
Mathlib.TacticAnalysis.TacticNode.runTacticCode : Mathlib.TacticAnalysis.TacticNode → Lean.MVarId → Lean.Syntax → Lean.Elab.Command.CommandElabM (List Lean.MVarId)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.updateOset! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu →
    Lean.FVarId → ℕ → Lean.Compiler.LCNF.Arg pu → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
ModuleCat.biprodIsoProd_inv_comp_fst : ∀ {R : Type u} [inst : Ring R] (M N : ModuleCat R),
  CategoryTheory.CategoryStruct.comp (M.biprodIsoProd N).inv CategoryTheory.Limits.biprod.fst =
    ModuleCat.ofHom (LinearMap.fst R ↑M ↑N)
-- Mathlib.CategoryTheory.Monoidal.Closed.Braided
CategoryTheory.ihom.instIsLeftAdjointTensorRightOfClosed : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [CategoryTheory.BraidedCategory C] (A : C) [CategoryTheory.Closed A],
  (CategoryTheory.MonoidalCategory.tensorRight A).IsLeftAdjoint
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddSemigroup : {M : Type u_1} →
  [inst : TopologicalSpace M] → [inst_1 : AddSemigroup M] → [ContinuousAdd M] → AddSemigroup (SeparationQuotient M)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.nthRoots_two_one : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R], Polynomial.nthRoots 2 1 = {-1, 1}
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_congr_r : ∀ {σs : List (Type u)} {P Q Q' : Std.Do.SPred σs}, (Q ⊣⊢ₛ Q') → P ∧ Q ⊣⊢ₛ P ∧ Q'
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- **Alias** of `BoundedContinuousFunction.coe_domRestrict`. -/
BoundedContinuousFunction.coe_restrict : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  (f : BoundedContinuousFunction α β) (s : Set α), ⇑(f.domRestrict s) = ⇑f ∘ Subtype.val
-- Mathlib.CategoryTheory.Localization.Linear
CategoryTheory.Localization.functor_linear : ∀ (R : Type w) [inst : Ring R] {C : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Preadditive D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_5 : L.IsLocalization W] [inst_6 : L.Additive] [inst_7 : CategoryTheory.Linear R C],
  CategoryTheory.Functor.Linear R L
-- Mathlib.Data.List.Lex
List.Lex.ne_iff : ∀ {α : Type u} {l₁ l₂ : List α}, l₁.length ≤ l₂.length → (List.Lex (fun x1 x2 => x1 ≠ x2) l₁ l₂ ↔ l₁ ≠ l₂)
-- Init.Data.Int.Linear
Int.Internal.Linear.le_neg : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.le_neg_cert p₁ p₂ = true →
    ¬Int.Internal.Linear.Poly.denote' ctx p₁ ≤ 0 → Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0
-- Mathlib.Algebra.Star.Unitary
Unitary.mem_iff_self_mul_star : ∀ {R : Type u_1} [inst : CommMonoid R] [inst_1 : StarMul R] {U : R}, U ∈ unitary R ↔ U * star U = 1
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.lieIdeal_eq_iSup_inf_genWeightSpace : ∀ {L : Type u_2} [inst : LieRing L] {K : Type u_4} [inst_1 : Field K] [inst_2 : LieAlgebra K L] [FiniteDimensional K L]
  (H : LieSubalgebra K L) [inst_4 : H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L),
  LieSubmodule.restr I H = ⨆ χ, LieSubmodule.restr I H ⊓ LieModule.genWeightSpace L ⇑χ
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.mem_iInf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {ι : Sort u_1} {S : ι → NonUnitalStarSubalgebra R A} {x : A},
  x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
-- Mathlib.CategoryTheory.Enriched.Basic
/-- `EnrichedFunctor.forget` maps the identity enriched functor to a functor isomorphic to
`Functor.id`.  -/
CategoryTheory.EnrichedFunctor.forgetId : (W : Type v') →
  [inst : CategoryTheory.Category.{w', v'} W] →
    [inst_1 : CategoryTheory.MonoidalCategory W] →
      (C : Type u₁) →
        [inst_2 : CategoryTheory.EnrichedCategory W C] →
          (CategoryTheory.EnrichedFunctor.id W C).forget ≅
            CategoryTheory.Functor.id (CategoryTheory.ForgetEnrichment W C)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy_homEquiv_symm_apply : ∀ {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]
  {Y : CategoryTheory.Functor C V}
  (β : CategoryTheory.MonoidalCategory.externalProduct F G ⟶ (CategoryTheory.MonoidalCategory.tensor C).comp Y),
  (CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy F G).homEquiv.symm β =
    (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).descOfIsLeftKanExtension
      (CategoryTheory.MonoidalCategory.DayConvolution.unit F G) Y β
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The cosine of the angle between two vectors, multiplied by the
product of their norms.  -/
InnerProductGeometry.cos_angle_mul_norm_mul_norm : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  Real.cos (InnerProductGeometry.angle x y) * (‖x‖ * ‖y‖) = inner ℝ x y
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.stabilizer_finset_univ : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : DecidableEq α]
  [inst_3 : Fintype α], AddAction.stabilizer G Finset.univ = ⊤
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.toList_ric : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.toList_ric._auto_1) [Std.TransCmp cmp]
  {t : Std.DTreeMap α β cmp} {bound : α},
  Std.Slice.toList (Std.Ric.Sliceable.mkSlice t *...=bound) = List.filter (fun e => (cmp e.fst bound).isLE) t.toList
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.IndepFun.neg_right : ∀ {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : Ω → β} {g : Ω → β'} {_mβ : MeasurableSpace β}
  {_mβ' : MeasurableSpace β'} [inst : Neg β'] [MeasurableNeg β'],
  ProbabilityTheory.Kernel.IndepFun f g κ μ → ProbabilityTheory.Kernel.IndepFun f (-g) κ μ
-- Mathlib.Data.Sym.Sym2
Sym2.mul_mk : ∀ {M : Type u_4} [inst : CommMagma M] (a b : M), s(a, b).mul = a * b
-- Batteries.Recycling.RBTree.Basic
/-- Returns true if `t₁` and `t₂` have the same keys and values
(assuming `cmp` and `==` are compatible), ignoring the internal tree structure.
 -/
RBTree.RBMap.instBEq : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [BEq α] → [BEq β] → BEq (RBTree.RBMap α β cmp)
-- Mathlib.LinearAlgebra.RootSystem.Base
/-- The indices of the simple roots / coroots.  -/
RootPairing.Base.support : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → {P : RootPairing ι R M N} → P.Base → Finset ι
-- Mathlib.NumberTheory.SumPrimeReciprocals
/-- `HasProd` over `Nat.Primes` iff over `ℕ` extending `f` by `1`.  -/
Nat.Primes.hasProd_iff_hasProd_ite : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] (f : ℕ → M) {a : M},
  HasProd (fun p => f ↑p) a ↔ HasProd (fun n => if Nat.Prime n then f n else 1) a
-- Mathlib.Order.Lattice
left_or_right_lt_sup : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ≠ b → a < a ⊔ b ∨ b < a ⊔ b
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidIso.withZero_symm_apply_apply : ∀ {G : Type u_6} {H : Type u_7} [inst : Group G] [inst_1 : PartialOrder G] [inst_2 : Group H] [inst_3 : PartialOrder H]
  (e : WithZero G ≃*o WithZero H) (x : G), (OrderMonoidIso.withZero.symm e) x = WithZero.unzero ⋯
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- A natural transformation of bifunctors induces a map on chosen coends.  -/
CategoryTheory.Limits.chosenCoend.map : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} J] →
        {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
          [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C] →
            {G : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
              (F ⟶ G) → (CategoryTheory.Limits.chosenCoend F ⟶ CategoryTheory.Limits.chosenCoend G)
-- Mathlib.Algebra.Homology.LocalCohomology
/-- Local cohomology along a composition of diagrams.  -/
localCohomology.diagramComp : {R : Type (max u v v')} →
  [inst : CommRing R] →
    {D : Type v} →
      [inst_1 : CategoryTheory.SmallCategory D] →
        {E : Type v'} →
          [inst_2 : CategoryTheory.SmallCategory E] →
            (I' : CategoryTheory.Functor E D) →
              (I : CategoryTheory.Functor D (Ideal R)) →
                (i : ℕ) → localCohomology.diagram (I'.comp I) i ≅ I'.op.comp (localCohomology.diagram I i)
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.coe_toHom : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f : L.ElementaryEmbedding M N}, ⇑f.toHom = ⇑f
-- Mathlib.Topology.DiscreteSubset
Topology.IsEmbedding.image_mem_codiscreteWithin : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsEmbedding f → ∀ {s t : Set X}, f '' s ∈ Filter.codiscreteWithin (f '' t) ↔ s ∈ Filter.codiscreteWithin t
-- Batteries.Classes.Order
Std.TransCmp.ge_trans : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] {x y z : α},
  cmp x y ≠ Ordering.lt → cmp y z ≠ Ordering.lt → cmp x z ≠ Ordering.lt
-- Mathlib.RingTheory.Ideal.Colon
/-- `N.colon P` is the ideal of all elements `r : R` such that `r • P ⊆ N`.
We treat it as an infix in lemma names.  -/
Submodule.colon : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → Set M → Ideal R
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sin_antiperiodic : Function.Antiperiodic Real.Angle.sin ↑Real.pi
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.getElem?_toArray_eq : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst : Std.Rxi.IsAlwaysFinite α] {i : ℕ}, r.toArray[i]? = Std.PRange.succMany? (i + 1) r.lower
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- The cofork which describes the counit of the adjunction: the morphism from the coequalizer of
this pair to this morphism is the counit.
 -/
CategoryTheory.Monad.MonadicityInternal.counitCofork : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {G : CategoryTheory.Functor D C} →
          {F : CategoryTheory.Functor C D} →
            (adj : F ⊣ G) →
              (B : D) →
                CategoryTheory.Limits.Cofork (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B)))
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.ins.eq_1 : ∀ {α : Type u_1} (x : RBTree.RBNode α), RBTree.RBNode.Path.root.ins x = x.setBlack
-- Lean.Level
/-- Returns true if and only if `l` evaluates to zero for all instantiations of parameters and
meta-variables.
 -/
Lean.Level.isAlwaysZero : Lean.Level → Bool
-- Mathlib.Data.NNReal.Defs
/-- A `DistribMulAction` over `ℝ` restricts to a `DistribMulAction` over `ℝ≥0`.  -/
NNReal.instDistribMulActionOfReal : {M : Type u_1} → [inst : AddMonoid M] → [DistribMulAction ℝ M] → DistribMulAction NNReal M
-- Mathlib.Analysis.Convex.Continuous
ConcaveOn.locallyLipschitzOn_interior : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {C : Set E} {f : E → ℝ}
  [FiniteDimensional ℝ E], ConcaveOn ℝ C f → LocallyLipschitzOn (interior C) f
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivWithinAt.mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {z : M} {F' : Type u_21}
  [inst_6 : NormedCommRing F'] [inst_7 : NormedAlgebra 𝕜 F'] {p q : M → F'} {p' q' : TangentSpace I z →L[𝕜] F'},
  HasMFDerivAt[s] p z p' → HasMFDerivAt[s] q z q' → HasMFDerivAt[s] (p * q) z (p z • q' + q z • p')
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
/-- The `SymmetricAlgebra` of a free module over a commutative semiring with no zero-divisors has
no zero-divisors.  -/
SymmetricAlgebra.instNoZeroDivisors : ∀ {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [NoZeroDivisors R] [Module.Free R M], NoZeroDivisors (SymmetricAlgebra R M)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_alter_eq_add_one : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      k ∉ t →
        (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true → (Std.DTreeMap.Raw.Const.alter t k f).size = t.size + 1
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShift.rightUnitor : ∀ {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] {F₁ : CategoryTheory.Functor C D} (A : Type u_5)
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A], CategoryTheory.NatTrans.CommShift F₁.rightUnitor.hom A
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.ConcreteCategory.ext_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C}
  {f g : X ⟶ Y},
  (∀ (x : CC X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.Topology.UniformSpace.Closeds
UniformSpace.hausdorff.isClosedEmbedding_singleton : ∀ {α : Type u_1} [inst : UniformSpace α] [T0Space α], Topology.IsClosedEmbedding fun x => {x}
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `not_isMulTorsionFree_of_isMulTorsion`.

---

A nontrivial torsion abelian group is not torsion-free.  -/
not_isMulTorsionFree_of_isTorsion : ∀ {G : Type u_1} [inst : CommGroup G] [Nontrivial G], IsMulTorsion G → ¬IsMulTorsionFree G
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Small
CategoryTheory.StructuredArrow.instSmallOfLocallySmall : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} [Small.{w, u₁} C] [CategoryTheory.LocallySmall.{w, v₂, u₂} D],
  Small.{w, max u₁ v₂} (CategoryTheory.StructuredArrow S T)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Measurable.iSup_Prop : ∀ {δ : Type u_4} {mδ : MeasurableSpace δ} {α : Type u_5} {mα : MeasurableSpace α}
  [inst : ConditionallyCompleteLattice α] (p : Prop) {f : δ → α}, Measurable f → Measurable fun b => ⨆ (_ : p), f b
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
/-- When `ϕ x` is a continuous linear map that changes vectors in charts around `f x` to vectors
in charts around `g x`, `inTangentCoordinates I I' f g ϕ x₀ x` is a coordinate change of
this continuous linear map that makes sense from charts around `f x₀` to charts around `g x₀`
by composing it with appropriate coordinate changes.
Note that the type of `ϕ` is more accurately
`Π x : N, TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)`.
We are unfolding `TangentSpace` in this type so that Lean recognizes that the type of `ϕ` doesn't
actually depend on `f` or `g`.

This is the underlying function of the trivializations of the hom of (pullbacks of) tangent spaces.
 -/
inTangentCoordinates : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    (I : ModelWithCorners 𝕜 E H) →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          (I' : ModelWithCorners 𝕜 E' H') →
                            {M : Type u_6} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        [IsManifold I 1 M] →
                                          [IsManifold I' 1 M'] →
                                            {N : Type u_9} → (N → M) → (N → M') → (N → E →L[𝕜] E') → N → N → E →L[𝕜] E'
-- Mathlib.CategoryTheory.Category.PartialFun
partialFunEquivPointed_functor_obj_point : ∀ (X : PartialFun), (partialFunEquivPointed.functor.obj X).point = none
-- Mathlib.Data.List.Nodup
List.Nodup.erase_get : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {l : List α},
  l.Nodup → ∀ (i : Fin l.length), l.erase (l.get i) = l.eraseIdx ↑i
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.b₄_of_char_two : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 2], W.b₄ = W.a₁ * W.a₃
-- Mathlib.Data.List.Sublists
/-- Auxiliary function to construct the list of all sublists of a given length. Given an
integer `n`, a list `l`, a function `f` and an auxiliary list `L`, it returns the list made of
`f` applied to all sublists of `l` of length `n`, concatenated with `L`.  -/
List.sublistsLenAux : {α : Type u} → {β : Type v} → ℕ → List α → (List α → β) → List β → List β
-- Mathlib.Algebra.Polynomial.Laurent
Polynomial.toLaurent_X : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.toLaurent Polynomial.X = LaurentPolynomial.T 1
-- Mathlib.Tactic.NormNum.Pow
/-- The `norm_num` extension which identifies expressions of the form `a ^ b`,
such that `norm_num` successfully recognises both `a` and `b`, with `b : ℤ`.  -/
Mathlib.Meta.NormNum.evalZPow : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_mul_monomial : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (m s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R),
  MvPolynomial.coeff (m + s) (p * (MvPolynomial.monomial s) r) = MvPolynomial.coeff m p * r
-- Mathlib.Analysis.Complex.Hadamard
/-- Alternative version of `norm_le_sSupNormIm` with a strict inequality and a positive `ε`.  -/
Complex.HadamardThreeLines.norm_lt_sSupNormIm_eps : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E),
  ∀ ε > 0,
    ∀ z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1,
      BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1) →
        ‖f z‖ < ε + Complex.HadamardThreeLines.sSupNormIm f z.re