mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Ray
/-- If vectors `v₁` and `v₂` are on the same ray, then they are nonnegative multiples of the same
vector. Actually, this vector can be assumed to be `v₁ + v₂`, see `SameRay.exists_eq_smul_add`.  -/
SameRay.exists_eq_smul : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {v₁ v₂ : M},
  SameRay R v₁ v₂ → ∃ u a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • u ∧ v₂ = b • u
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.le_extensionProduct_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P : CategoryTheory.ObjectProperty C} (Q : CategoryTheory.ObjectProperty C) [Q.ContainsZero], P ≤ P.extensionProduct Q
-- Mathlib.Topology.UniformSpace.Defs
uniformContinuous_id : ∀ {α : Type ua} [inst : UniformSpace α], UniformContinuous id
-- Std.Http.Internal.Char
/-- Checks if a byte represents an ASCII character (value < 128).
 -/
Std.Http.Internal.Char.isAsciiByte : UInt8 → Bool
-- Mathlib.GroupTheory.SemidirectProduct
/-- The element of N  -/
SemidirectProduct.left : {N : Type u_1} → {G : Type u_2} → [inst : Group N] → [inst_1 : Group G] → {φ : G →* MulAut N} → N ⋊[φ] G → N
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.isLongestMatchAt : ∀ {pat s : String.Slice} {stackPos needlePos : String.Pos.Raw}
  (h : String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos stackPos)
  (h' : needlePos = pat.rawEndPos),
  String.Slice.Pattern.Model.IsLongestMatchAt pat (String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.base✝ h)
    (String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.base✝ ⋯)
-- Init.Tactics
/-- A configuration item for a tactic configuration.  -/
Lean.Parser.Tactic.configItem : Lean.ParserDescr
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instStarAddMonoid : {n : Type u_2} → {A : Type u_5} → [inst : AddMonoid A] → [StarAddMonoid A] → StarAddMonoid (CStarMatrix n n A)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.filterMap_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)},
  Std.ExtDHashMap.filterMap f m = ∅ ↔ ∀ (k : α) (h : k ∈ m), f k (m.get k h) = none
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.neg : ∀ {𝕜 : 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] {f : E → F} {s : Set E},
  DiffContOnCl 𝕜 f s → DiffContOnCl 𝕜 (-f) s
-- Plausible.Testable
/-- When we assign a value to a universally quantified variable,
we record that value using this function so that our counter-examples
can be informative.  -/
Plausible.TestResult.addInfo : {p q : Prop} →
  String → (q → p) → Plausible.TestResult p → optParam (Unit ⊕' (p → q)) (PSum.inl ()) → Plausible.TestResult q
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_def' : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ H₂ : AddSubgroup G) [H₁.Normal] [H₂.Normal],
  ⁅H₁, H₂⁆ = AddSubgroup.normalClosure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
/-- The ring homomorphism from `R ⧸ I ^ m`
to `R ⧸ I ^ n` induced by the natural inclusion `I ^ n → I ^ m`.

To future contributors: Before adding lemmas related to `Ideal.factorPow`, please
check whether it can be generalized to `Ideal.factor` and whether the corresponding
(more general) lemma for `Ideal.factor` already exists.
 -/
Ideal.Quotient.factorPow : {R : Type u_1} → [inst : Ring R] → (I : Ideal R) → [inst_1 : I.IsTwoSided] → {m n : ℕ} → n ≤ m → R ⧸ I ^ m →+* R ⧸ I ^ n
-- Mathlib.Algebra.Category.BoolRing
BoolRing.coe_of : ∀ (α : Type u_1) [inst : BooleanRing α], ↑{ carrier := α, booleanRing := inst } = α
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- A cyclotomic extension splits `X ^ n - 1` if `n ∈ S`.  -/
IsCyclotomicExtension.splits_X_pow_sub_one : ∀ {n : ℕ} [NeZero n] {S : Set ℕ} (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [H : IsCyclotomicExtension S K L], n ∈ S → (Polynomial.map (algebraMap K L) (Polynomial.X ^ n - 1)).Splits
-- Batteries.Data.AssocList
Batteries.AssocList.any.eq_def : ∀ {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (x : Batteries.AssocList α β),
  Batteries.AssocList.any p x =
    match x with
    | Batteries.AssocList.nil => false
    | Batteries.AssocList.cons k v es => p k v || Batteries.AssocList.any p es
-- Mathlib.Order.Types.Arithmetic
/-- The order type of the real numbers. 

Conventions for notations in identifiers:

 * The recommended spelling of `θ` in identifiers is `theta`. -/
OrderType.theta : OrderType.{0}
-- Batteries.Data.List.Basic
List.inits.eq_2 : ∀ {α : Type u_1} (a : α) (l : List α), (a :: l).inits = [] :: List.map (fun t => a :: t) l.inits
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range' : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ),
  (Set.range τ).Countable → ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
SimpleGraph.Coloring.odd_length_iff_not_congr : ∀ {α : Type u_1} {G : SimpleGraph α} (c : G.Coloring Bool) {u v : α} (p : G.Walk u v),
  Odd p.length ↔ (¬c u = true ↔ c v = true)
-- Mathlib.Data.ZMod.Basic
Prod.snd_zmod_cast : ∀ {n : ℕ} {R : Type u_1} [inst : AddGroupWithOne R] {S : Type u_2} [inst_1 : AddGroupWithOne S] (a : ZMod n),
  a.cast.2 = a.cast
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.hf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w}
  [inst_3 : CategoryTheory.SmallCategory J] {Y : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone Y}
  (z : X ⟶ c.pt) (j : J),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pullback c.ι ((CategoryTheory.Functor.const J).map z)) j)
      (CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.f z) =
    (CategoryTheory.Limits.pullback.snd c.ι ((CategoryTheory.Functor.const J).map z)).app j
-- Mathlib.Algebra.Tropical.Basic
Tropical.instDistribTropical : {R : Type u} → [inst : LinearOrder R] → [inst_1 : Add R] → [AddLeftMono R] → [AddRightMono R] → Distrib (Tropical R)
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- An n-ary version of `Set.add_mem_add`.  -/
Set.finsetSum_mem_finsetSum : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : Finset ι) (f : ι → Set α) (g : ι → α),
  (∀ i ∈ t, g i ∈ f i) → ∑ i ∈ t, g i ∈ ∑ i ∈ t, f i
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.mem_coe : ∀ {M : Type u_1} [inst : AddZeroClass M] {c : AddCon M} {x y : M}, (x, y) ∈ ↑c ↔ (x, y) ∈ c
-- Mathlib.NumberTheory.LSeries.RiemannZeta
HurwitzZeta.expZeta_zero : HurwitzZeta.expZeta 0 = riemannZeta
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.lit.sizeOf_spec : ∀ (a : Lean.Literal), sizeOf (Lean.Meta.DiscrTree.Key.lit a) = 1 + sizeOf a
-- Mathlib.Data.Multiset.Powerset
Multiset.mem_powersetAux : ∀ {α : Type u_1} {l : List α} {s : Multiset α}, s ∈ Multiset.powersetAux l ↔ s ≤ ↑l
-- Mathlib.Logic.Function.FromTypes
Function.fromTypes_succ : ∀ {n : ℕ} (p : Fin (n + 1) → Type u) (τ : Type u),
  Function.FromTypes p τ = (Matrix.vecHead p → Function.FromTypes (Matrix.vecTail p) τ)
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.equiv_symm_toEmbedding_trans_toEmbedding : ∀ {α : Sort u_1} {β : Sort u_2} (e : α ≃ β), e.symm.toEmbedding.trans e.toEmbedding = Function.Embedding.refl β
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_right_le_size_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₂.size ≤ (t₁ ∪ t₂).size
-- Mathlib.Order.Nucleus
Nucleus.instNucleusClass : ∀ {X : Type u_1} [inst : SemilatticeInf X], NucleusClass (Nucleus X) X
-- Lean.DocString.Types
Lean.Doc.Inline.emph.inj : ∀ {i : Type u} {content content_1 : Array (Lean.Doc.Inline i)},
  Lean.Doc.Inline.emph content = Lean.Doc.Inline.emph content_1 → content = content_1
-- Lean.Parser.Do
Lean.Parser.Term.doWhile.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The tangent of an angle in a right-angled triangle as a ratio of sides, version subtracting
vectors.  -/
InnerProductGeometry.tan_angle_sub_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → Real.tan (InnerProductGeometry.angle x (x - y)) = ‖y‖ / ‖x‖
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.graphFunctor_essSurj : CategoryTheory.RelCat.graphFunctor.EssSurj
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryBiproductTriangle_mor₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryBiproductTriangle X₁ X₂).mor₃ = 0
-- Init.Data.SInt.Lemmas
Int16.toInt64_div_of_ne_left : ∀ (a b : Int16), a ≠ Int16.minValue → (a / b).toInt64 = a.toInt64 / b.toInt64
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_uIcc_castLE : ∀ {M : Type u_2} [inst : CommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n),
  ∏ i ∈ Finset.uIcc (Fin.castLE h a) (Fin.castLE h b), f i = ∏ i ∈ Finset.uIcc a b, f (Fin.castLE h i)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- The special case of the pairing integral where the pairing is just the scalar multiplication by
`ℝ` on `F` and `f` is real-valued. The resulting integral is `F`-valued. -/
MeasureTheory.VectorMeasure.«term∫ᵛ_,_∂•_» : Lean.ParserDescr
-- Mathlib.RingTheory.PowerSeries.Derivative
PowerSeries.trunc_derivative' : ∀ {R : Type u_1} [inst : CommSemiring R] (f : PowerSeries R) (n : ℕ),
  (PowerSeries.trunc (n - 1)) ((PowerSeries.derivative R) f) = Polynomial.derivative ((PowerSeries.trunc n) f)
-- Mathlib.Topology.Connected.Clopen
Topology.IsCoinducing.preimage_connectedComponent : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Topology.IsCoinducing f →
    (∀ (y : β), IsConnected (f ⁻¹' {y})) → ∀ (a : α), f ⁻¹' connectedComponent (f a) = connectedComponent a
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_singleton : ∀ {α : Type u_3} [inst : PartialOrder α] {a : α}, {a}.OrdConnected
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.const.inj : ∀ {declName : Lean.Name} {nargs : ℕ} {declName_1 : Lean.Name} {nargs_1 : ℕ},
  Lean.Meta.RefinedDiscrTree.Key.const declName nargs = Lean.Meta.RefinedDiscrTree.Key.const declName_1 nargs_1 →
    declName = declName_1 ∧ nargs = nargs_1
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_iUnion_fintype : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Fintype β]
  {f : β → Set α},
  Pairwise (Function.onFun Disjoint f) →
    (∀ (i : β), MeasurableSet (f i)) →
      autoParam (∀ (i : β), μ (f i) ≠ ⊤) MeasureTheory.measureReal_iUnion_fintype._auto_1 →
        μ.real (⋃ b, f b) = ∑ p, μ.real (f p)
-- Mathlib.Order.UpperLower.Basic
isUpperSet_univ : ∀ {α : Type u_1} [inst : LE α], IsUpperSet Set.univ
-- Mathlib.RepresentationTheory.Invariants
/-- `average k G` is invariant under right multiplication by elements of `G`.
 -/
GroupAlgebra.mul_average_right : ∀ (k : Type u_1) (G : Type u_2) [inst : CommSemiring k] [inst_1 : Group G] [inst_2 : Fintype G]
  [inst_3 : Invertible ↑(Fintype.card G)] (g : G),
  GroupAlgebra.average k G * MonoidAlgebra.single g 1 = GroupAlgebra.average k G
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.posDef_iff_nonneg : ∀ {M : Type u_4} {N : Type u_5} {R₂ : Type u} [inst : CommSemiring R₂] [inst_1 : AddCommMonoid M] [inst_2 : Module R₂ M]
  [inst_3 : PartialOrder N] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {Q : QuadraticMap R₂ M N},
  Q.PosDef ↔ (∀ (x : M), 0 ≤ Q x) ∧ Q.Anisotropic
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.get_eq : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C : G.EdgeLabeling K) (x y : V) (h : G.Adj x y),
  C.get x y h = C ⟨s(x, y), h⟩
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
/-- [Stacks Tag 022D](https://stacks.math.columbia.edu/tag/022D) ((3)) -/
AlgebraicGeometry.QuasiCompactCover.instPullback₁Scheme : ∀ {S : AlgebraicGeometry.Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) [AlgebraicGeometry.QuasiCompactCover 𝒰]
  {T : AlgebraicGeometry.Scheme} (f : T ⟶ S),
  AlgebraicGeometry.QuasiCompactCover (CategoryTheory.PreZeroHypercover.pullback₁ f 𝒰)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.ofList_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (xs : List α),
  FreeAddMonoid.ofList (List.map f xs) = (FreeAddMonoid.map f) (FreeAddMonoid.ofList xs)
-- Mathlib.Control.Fold
Monoid.Foldr.ofFreeMonoid : {α β : Type u} → (α → β → β) → FreeMonoid α →* Monoid.Foldr β
-- Lean.Parser.Do
Lean.Parser.Term.optMetaFalse.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
UpperHalfPlane.gl_smul_I_eq_I_iff_of_pos : ∀ {g : GL (Fin 2) ℝ},
  0 < ↑(Matrix.GeneralLinearGroup.det g) →
    (g • UpperHalfPlane.I = UpperHalfPlane.I ↔ ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 = -↑g 1 0)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.nnrealPart_neg_eq_zero_of_nonneg : ∀ {α : Type u_2} [inst : TopologicalSpace α] {f : CompactlySupportedContinuousMap α ℝ}, 0 ≤ f → (-f).nnrealPart = 0
-- Mathlib.Order.Filter.Basic
/-- **Alias** of `Filter.EventuallyEq.of_eq`. -/
Eq.eventuallyEq : ∀ {α : Type u} {β : Type v} {l : Filter α} {f g : α → β}, f = g → f =ᶠ[l] g
-- Mathlib.RingTheory.Binomial
Ring.multichoose_two : ∀ {R : Type u_2} [inst : NonAssocSemiring R] [inst_1 : Pow R ℕ] [NatPowAssoc R] [inst_3 : BinomialRing R] (k : ℕ),
  Ring.multichoose 2 k = ↑k + 1
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter_succ'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (h : autoParam (n + i = m) CategoryTheory.SimplicialObject.σ₀Iter_succ'._auto_1) {Z : C}
  (h_1 : X.obj (Opposite.op { len := m + 1 }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.σ₀Iter (i + 1) ⋯) h_1 =
    CategoryTheory.CategoryStruct.comp (X.σ₀Iter i h) (CategoryTheory.CategoryStruct.comp (X.σ 0) h_1)
-- Mathlib.Topology.UniformSpace.Real
NNReal.ContinuousMap.canLift : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  CanLift C(X, ℝ) C(X, NNReal) ContinuousMap.coeNNRealReal.comp fun f => ∀ (x : X), 0 ≤ f x
-- Mathlib.Data.NNReal.Defs
NNReal.smul_def : ∀ {M : Type u_1} [inst : SMul ℝ M] (c : NNReal) (x : M), c • x = ↑c • x
-- Mathlib.Combinatorics.Graph.Basic
/-- `E(G)` denotes the `edgeSet` of a graph `G`.  -/
Graph.«termE(_)» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Hom.Basic
MonoidHom.comp_div : ∀ {M : Type u_2} {G : Type u_5} {H : Type u_6} [inst : MulOneClass M] [inst_1 : CommGroup G] [inst_2 : CommGroup H]
  (f : G →* H) (g h : M →* G), f.comp (g / h) = f.comp g / f.comp h
-- Lean.Level
_private.Lean.Level.0.Lean.Level.PP.parenIfFalse : Std.Format → Bool → Std.Format
-- Lean.Data.JsonRpc
Lean.JsonRpc.RequestID.num.injEq : ∀ (n n_1 : Lean.JsonNumber), (Lean.JsonRpc.RequestID.num n = Lean.JsonRpc.RequestID.num n_1) = (n = n_1)
-- Mathlib.Algebra.Ring.Parity
odd_add_one_self : ∀ {α : Type u_2} [inst : Semiring α] {a : α}, Odd (a + 1 + a)
-- Mathlib.Topology.Compactness.Lindelof
/-- The complement to a Lindelöf set belongs to a filter `f` with the countable intersection
property if each `x ∈ s` has a neighborhood `t` within `s` such that `tᶜ` belongs to `f`.  -/
IsLindelof.compl_mem_sets_of_nhdsWithin : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsLindelof s → ∀ {f : Filter X} [CountableInterFilter f], (∀ x ∈ s, ∃ t ∈ nhdsWithin x s, tᶜ ∈ f) → sᶜ ∈ f
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
/-- Line derivative of `f` at the point `x` in the direction `v`, if it exists.  Zero otherwise.

If the line derivative exists (i.e., `∃ f', HasLineDerivAt 𝕜 f f' x v`), then
`f (x + t v) = f x + t lineDeriv 𝕜 f x v + o (t)` when `t` tends to `0`.
 -/
lineDeriv : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type u_2} →
      [inst_1 : NormedAddCommGroup F] →
        [NormedSpace 𝕜 F] → {E : Type u_3} → [inst_3 : AddCommGroup E] → [Module 𝕜 E] → (E → F) → E → E → F
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- **Alias** of `ContMDiffWithinAt.curry_right`.

---

Curried `C^n` functions are `C^n` in the second coordinate.  -/
ContMDiffWithinAt.along_snd : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : M → M' → N} {x : M} {y : M'} {s : Set (M × M')},
  ContMDiffWithinAt (I.prod I') J n (Function.uncurry f) s (x, y) →
    ContMDiffWithinAt I' J n (fun y => f x y) {y | (x, y) ∈ s} y
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X Y : D} {f : X ⟶ Y} (hf : F.relativelyRepresentable f) {a : C} {g : F.obj a ⟶ Y}
  {c : C} (i : F.obj c ⟶ X) (h : c ⟶ a)
  (hi : CategoryTheory.CategoryStruct.comp i f = CategoryTheory.CategoryStruct.comp (F.map h) g) [inst_2 : F.Full]
  [F.Faithful] {Z : C} (h_1 : a ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hf.lift i h hi) (CategoryTheory.CategoryStruct.comp (hf.snd g) h_1) =
    CategoryTheory.CategoryStruct.comp h h_1
-- Lean.Meta.Tactic.Assert
/-- Convert the given goal `Ctx |- target` into a goal containing `(userName : type)` after the local declaration with if `fvarId`.
It assumes `val` has type `type`, and that `type` is well-formed after `fvarId`.
Note that `val` does not need to be well-formed after `fvarId`. That is, it may contain variables that are defined after `fvarId`.  -/
Lean.MVarId.assertAfter : Lean.MVarId → Lean.FVarId → Lean.Name → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Meta.AssertAfterResult
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- Let `S / L / K` be a tower of extensions. For any two elements `y` and `x` in `S`, if `y` is a
conjugate root of `x` over `L`, then `y` is also a conjugate root of `x` over
`K`.
 -/
IsConjRoot.of_isScalarTower : ∀ {K : Type u_2} {L : Type u_3} {S : Type u_4} [inst : CommRing S] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K S] [inst_4 : Algebra K L] [inst_5 : Algebra L S] [IsDomain S] [IsScalarTower K L S] {x y : S},
  IsIntegral K x → IsConjRoot L x y → IsConjRoot K x y
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.le_iff' : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] {v w : MeasureTheory.VectorMeasure α M}, v ≤ w ↔ ∀ (i : Set α), v i ≤ w i
-- Mathlib.CategoryTheory.Functor.CurryingThree
/-- `bifunctorComp₂₃` can be described in terms of the curryfication of functors.  -/
CategoryTheory.Functor.bifunctorComp₂₃Iso : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_4} →
      {C₂₃ : Type u_5} →
        {E : Type u_9} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] →
                [inst_3 : CategoryTheory.Category.{v_5, u_5} C₂₃] →
                  [inst_4 : CategoryTheory.Category.{v_9, u_9} E] →
                    (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ E)) →
                      (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) →
                        CategoryTheory.bifunctorComp₂₃ F G₂₃ ≅
                          CategoryTheory.Functor.curry.obj
                            (CategoryTheory.Functor.curry.obj
                              ((CategoryTheory.prod.associator C₁ C₂ C₃).comp
                                (CategoryTheory.Functor.uncurry.obj
                                  ((CategoryTheory.Functor.uncurry.obj G₂₃).comp F.flip).flip)))
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
differentiableAt_jacobiTheta : ∀ {τ : ℂ}, 0 < τ.im → DifferentiableAt ℂ jacobiTheta τ
-- Mathlib.Data.NNRat.Defs
NNRat.num_divNat_den : ∀ (q : ℚ≥0), NNRat.divNat q.num q.den = q
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.instIsIsoRightAppArrowιIteration : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  (f : CategoryTheory.Arrow C),
  CategoryTheory.IsIso (CategoryTheory.Arrow.Hom.right ((CategoryTheory.SmallObject.ιIteration I κ).app f))
-- Mathlib.Data.Finset.Max
Finset.notMem_of_max_lt : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α} {a b : α}, b < a → s.max = ↑b → a ∉ s
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.Limit.map_π_apply : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F G : CategoryTheory.Functor J (Type u)}
  [inst_1 : CategoryTheory.Limits.HasLimit F] [inst_2 : CategoryTheory.Limits.HasLimit G] (α : F ⟶ G) (j : J)
  (x : CategoryTheory.Limits.limit F),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π G j))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limMap α)) x) =
    (CategoryTheory.ConcreteCategory.hom (α.app j))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) x)
-- Mathlib.Algebra.DirectSum.Module
DirectSum.sigmaLuncurry_apply : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {α : ι → Type u_1} {δ : (i : ι) → α i → Type w} [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] [inst_3 : (i : ι) → (j : α i) → Module R (δ i j)]
  (f : DirectSum ι fun i => DirectSum (α i) fun j => δ i j) (i : ι) (j : α i),
  ((DirectSum.sigmaLuncurry R) f) ⟨i, j⟩ = (f i) j