mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- Given some linear forms $L_1, ..., L_n, K$ over a vector space $E$, if
$\bigcap_{i=1}^n \mathrm{ker}(L_i) \subseteq \mathrm{ker}(K)$, then $K$ is in the space generated
by $L_1, ..., L_n$.  -/
mem_span_of_iInf_ker_le_ker : ∀ {ι : Type u_3} {𝕜 : Type u_4} {E : Type u_5} [inst : Field 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [Finite ι] {L : ι → E →ₗ[𝕜] 𝕜} {K : E →ₗ[𝕜] 𝕜}, ⨅ i, (L i).ker ≤ K.ker → K ∈ Submodule.span 𝕜 (Set.range L)
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_twoPow : ∀ {w : ℕ} (i j : ℕ), (BitVec.twoPow w i).getLsbD j = (decide (i < w) && decide (i = j))
-- Mathlib.Condensed.Light.TopCatAdjunction
/-- The object part of the functor `LightCondSet ⥤ TopCat`  -/
LightCondSet.toTopCat : LightCondSet → TopCat
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.trans_source : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e f : Bundle.Pretrivialization F proj), (f.symm.trans e.toPartialEquiv).source = (e.baseSet ∩ f.baseSet) ×ˢ Set.univ
-- Mathlib.Topology.Semicontinuity.Defs
UpperSemicontinuousOn.mono : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s t : Set α},
  UpperSemicontinuousOn f s → t ⊆ s → UpperSemicontinuousOn f t
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.mk.inj : ∀ {α : Type u_4} {β : Type u_5} {inst : UniformSpace α} {inst_1 : UniformSpace β} {toEquiv : α ≃ β}
  {uniformContinuous_toFun : UniformContinuous toEquiv.toFun}
  {uniformContinuous_invFun : UniformContinuous toEquiv.invFun} {toEquiv_1 : α ≃ β}
  {uniformContinuous_toFun_1 : UniformContinuous toEquiv_1.toFun}
  {uniformContinuous_invFun_1 : UniformContinuous toEquiv_1.invFun},
  { toEquiv := toEquiv, uniformContinuous_toFun := uniformContinuous_toFun,
        uniformContinuous_invFun := uniformContinuous_invFun } =
      { toEquiv := toEquiv_1, uniformContinuous_toFun := uniformContinuous_toFun_1,
        uniformContinuous_invFun := uniformContinuous_invFun_1 } →
    toEquiv = toEquiv_1
-- Mathlib.Data.Fin.Basic
Fin.size_positive' : ∀ {n : ℕ} [Nonempty (Fin n)], 0 < n
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.commute_add_nat : ∀ (f : CircleDeg1Lift) (n : ℕ), Function.Commute ⇑f fun x => x + ↑n
-- Mathlib.Data.Multiset.Replicate
Multiset.nodup_iff_pairwise : ∀ {α : Type u_3} {s : Multiset α}, s.Nodup ↔ Multiset.Pairwise (fun x1 x2 => x1 ≠ x2) s
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.exactAt_of_isSupported : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [K.IsSupported e] (i' : ι'), (∀ (i : ι), e.f i ≠ i') → K.ExactAt i'
-- Std.Tactic.BVDecide.Reflect
/-- Verify that a proof certificate is valid for a given formula.
 -/
Std.Tactic.BVDecide.Reflect.verifyCert : Std.Sat.CNF ℕ → String → Bool
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_eq_getD_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} [inst_1 : Inhabited (β a)], t.get! a = t.getD a default
-- Mathlib.Order.RelClasses
/-- Set notation form of `lt_of_le_of_lt` -/
ssubset_of_subset_of_ssubset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b c : α}, a ⊆ b → b ⊂ c → a ⊂ c
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_mapₐ : ∀ {R : Type u_3} {A : Type u_4} {B : Type u_5} {C : Type u_6} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  {I : Ideal A} (f : A →ₐ[R] B) (g : B →ₐ[R] C), Ideal.map g (Ideal.map f I) = Ideal.map (g.comp f) I
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Mul-mul-invmul version.  -/
Finset.ruzsa_triangle_inequality_mul_mul_invMul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] (A B C : Finset G),
  (A * C).card * B.card ≤ (A * B).card * (C⁻¹ * B).card
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, ∅.isEmpty = true
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.union_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₁.union t₂ = t₁ ∪ t₂
-- Mathlib.Combinatorics.SimpleGraph.Trails
SimpleGraph.Walk.IsTrail.even_countP_edges_iff : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} {p : G.Walk u v},
  p.IsTrail → ∀ (x : V), Even (List.countP (fun e => decide (x ∈ e)) p.edges) ↔ u ≠ v → x ≠ u ∧ x ≠ v
-- Mathlib.Data.Sym.Basic
SymOptionSuccEquiv.encode_of_none_mem : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] (s : Sym (Option α) n.succ) (h : none ∈ s),
  SymOptionSuccEquiv.encode s = Sum.inl (s.erase none h)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'}
  [inst_3 : CategoryTheory.Limits.HasKernel f'] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.map f f' sq.left sq.right ⋯)
      (CategoryTheory.Limits.kernelSubobjectIso f').inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).inv
      (CategoryTheory.Limits.kernelSubobjectMap sq)
-- Init.Data.List.Lemmas
List.getLast_mem_getLast? : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.getLast h ∈ l.getLast?
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.nextDen.eq_1 : ∀ {K : Type u_2} [inst : DivisionRing K] (aₙ bₙ ppredB predB : K),
  GenContFract.nextDen aₙ bₙ ppredB predB = bₙ * predB + aₙ * ppredB
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.emod.match_1.splitter : (motive : ℤ → ℤ → Sort u_1) →
  (x x_1 : ℤ) →
    ((m : ℕ) → (n : ℤ) → motive (Int.ofNat m) n) → ((m : ℕ) → (n : ℤ) → motive (Int.negSucc m) n) → motive x x_1
-- Lean.Compiler.IR.Basic
Lean.IR.LitVal.num.sizeOf_spec : ∀ (v : ℕ), sizeOf (Lean.IR.LitVal.num v) = 1 + sizeOf v
-- Mathlib.Topology.Convenient.HomSpace
Topology.ContinuousMapGeneratedBy.ev_apply : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type v'} [inst_2 : TopologicalSpace Z] [inst_3 : ∀ (i : ι), LocallyCompactSpace (X i)]
  [inst_4 : ∀ (i j : ι), Topology.IsGeneratedBy X (X i × X j)] (y : Y) (f : Topology.ContinuousMapGeneratedBy X Y Z),
  Topology.ContinuousMapGeneratedBy.ev (y, f) = f y
-- Mathlib.CategoryTheory.Shift.ShiftSequence
/-- A shift sequence for a functor `F : C ⥤ A` when `C` is equipped with a shift
by a monoid `M` involves a sequence of functor `sequence n : C ⥤ A` for all `n : M`
which behave like `shiftFunctor C n ⋙ F`.  -/
CategoryTheory.Functor.ShiftSequence : {C : Type u_1} →
  {A : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} A] →
        CategoryTheory.Functor C A →
          (M : Type u_4) →
            [inst_2 : AddMonoid M] → [CategoryTheory.HasShift C M] → Type (max (max (max (max u_1 u_3) u_4) v_1) v_3)
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformlyOn.congr_right : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι} {g : α → β},
  TendstoLocallyUniformlyOn F f p s → Set.EqOn f g s → TendstoLocallyUniformlyOn F g p s
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.mk_surjective : ∀ {X : SSet} (s : X.S), ∃ n x, s = { dim := n, simplex := x }
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesCoimageImageComparison.iso_inv_right : ∀ {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]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f] [inst_6 : CategoryTheory.Limits.HasCokernel f]
  [inst_7 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
  [inst_8 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)]
  [inst_9 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_10 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_11 :
    CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.cokernel.π f) 0) F]
  [inst_12 :
    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F]
  [inst_13 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π (F.map f))]
  [inst_14 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))],
  (CategoryTheory.Abelian.PreservesCoimageImageComparison.iso F f).inv.right =
    (CategoryTheory.Abelian.PreservesImage.iso F f).inv
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.exists_variableChange_isShortNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [Invertible 2] [Invertible 3], ∃ C, (C • W).IsShortNF
-- Mathlib.Analysis.Calculus.FDeriv.Pi
fderiv_update : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : DecidableEq ι] [inst_1 : NontriviallyNormedField 𝕜] {E : ι → Type u_3}
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (x : (i : ι) → E i) {i : ι}
  (y : E i), fderiv 𝕜 (Function.update x i) y = ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
-- Init.SizeOf
SizeOf.mk : {α : Sort u} → (α → ℕ) → SizeOf α
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt8.reduceMul : Lean.Meta.Simp.DSimproc
-- Mathlib.Control.Bifunctor
/-- Bifunctor. This typeclass asserts that a lawless `Bifunctor` is lawful.  -/
LawfulBifunctor : (F : Type u₀ → Type u₁ → Type u₂) → [Bifunctor F] → Prop
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.instFourierSMul : ∀ (𝕜 : Type u_1) [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℂ E]
  [inst_3 : NormedSpace 𝕜 E] [inst_4 : SMulCommClass ℂ 𝕜 E] {V : Type u_3} [inst_5 : NormedAddCommGroup V]
  [inst_6 : InnerProductSpace ℝ V] [inst_7 : FiniteDimensional ℝ V] [inst_8 : MeasurableSpace V]
  [inst_9 : BorelSpace V], FourierSMul 𝕜 (SchwartzMap V E) (SchwartzMap V E)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
/-- **Alias** of `SimpleGraph.Walk.edges_dropUntil_subset_edges`. -/
SimpleGraph.Walk.edges_dropUntil_subset : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk v w) (h : u ∈ p.support),
  (p.dropUntil u h).edges ⊆ p.edges
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.add : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Add M] {m : MeasurableSpace α} {f g : α → M}
  {μ : MeasureTheory.Measure α} [MeasurableAdd₂ M], AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (f + g) μ
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.inr_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) {Z_1 : C} (h : CategoryTheory.Limits.cokernel (CategoryTheory.CategoryStruct.comp f g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.π f g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp f g)) h
-- Mathlib.Order.Defs.PartialOrder
lt_or_eq_of_le' : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b ≤ a → b < a ∨ a = b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
/-- The `n`-th Chebyshev polynomial of the second kind evaluates on `cosh θ` to the
value `sinh ((n + 1) * θ) / sinh θ`.  -/
Polynomial.Chebyshev.U_complex_cosh : ∀ (θ : ℂ) (n : ℤ),
  Polynomial.eval (Complex.cosh θ) (Polynomial.Chebyshev.U ℂ n) * Complex.sinh θ = Complex.sinh ((↑n + 1) * θ)
-- Lean.PrettyPrinter.Delaborator.Basic
/-- The number of `delab` steps so far. Used by `pp.maxSteps` to stop delaboration.  -/
Lean.PrettyPrinter.Delaborator.State.steps : Lean.PrettyPrinter.Delaborator.State → ℕ
-- Init.Data.Format.Basic
/-- Emits a newline followed by `indent` columns of indentation.
 -/
Std.Format.MonadPrettyFormat.pushNewline : {m : Type → Type} → [self : Std.Format.MonadPrettyFormat m] → ℕ → m Unit
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
/-- The formula `y(P₁)(x(P₂) - x(P₃)) + y(P₂)(x(P₃) - x(P₁)) + y(P₃)(x(P₁) - x(P₂)) = 0`,
assuming that `P₁ + P₂ + P₃ = O`.  -/
WeierstrassCurve.Affine.cyclic_sum_Y_mul_X_sub_X : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ : F} (y₁ y₂ : F),
  x₁ ≠ x₂ →
    have x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂);
    y₁ * (x₂ - x₃) + y₂ * (x₃ - x₁) + W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂) = 0
-- Mathlib.Data.List.Induction
List.bidirectionalRec_nil : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (singleton : (a : α) → motive [a])
  (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))),
  List.bidirectionalRec nil singleton cons_append [] = nil
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.add_nsmul : ∀ {M : Type u_2} [inst : AddMonoid M] {a b : M}, AddCommute a b → ∀ (n : ℕ), n • (a + b) = n • a + n • b
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.instAddHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier : (X : TopCat) → (R : TopCommRingCat) → Add (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.instIsCentralScalar : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)] [inst_1 : (i : ι) → SMul Mᵐᵒᵖ (α i)]
  [∀ (i : ι), IsCentralScalar M (α i)], IsCentralScalar M ((i : ι) × α i)
-- Mathlib.Data.PEquiv
/-- Create a `PEquiv` which sends `a` to `b` and `b` to `a`, but is otherwise `none`.  -/
PEquiv.single : {α : Type u} → {β : Type v} → [DecidableEq α] → [DecidableEq β] → α → β → α ≃. β
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.mapBifunctorMap_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6}
  (p : I × J → K)
  [inst_3 :
    ∀ (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂),
      (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p]
  {X₁ X₂ : CategoryTheory.GradedObject I C₁} (φ : X₁ ⟶ X₂) (Y : CategoryTheory.GradedObject J C₂) (i : K),
  ((CategoryTheory.GradedObject.mapBifunctorMap F p).map φ).app Y i =
    CategoryTheory.GradedObject.mapBifunctorMapMap F p φ (CategoryTheory.CategoryStruct.id Y) i
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.totallyBounded_subsets_of_totallyBounded : ∀ {α : Type u_1} [inst : UniformSpace α] {t : Set α}, TotallyBounded t → TotallyBounded {K | ↑K ⊆ t}
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_sdiff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  s₂ ⊆ s₁ → MeasureTheory.NullMeasurableSet s₂ μ → μ s₂ ≠ ⊤ → μ (s₁ \ s₂) = μ s₁ - μ s₂
-- Mathlib.Algebra.Quaternion
/-- Quaternion conjugate.  -/
QuaternionAlgebra.instStarQuaternionAlgebra : {R : Type u_3} → {c₁ c₂ c₃ : R} → [CommRing R] → Star (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toLinearMap_smul : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] {S₂ : Type u_9}
  [inst_8 : DistribSMul S₂ M₂] [inst_9 : SMulCommClass R₂ S₂ M₂] [inst_10 : ContinuousConstSMul S₂ M₂] (c : S₂)
  (f : M₁ →SL[σ₁₂] M₂), ↑(c • f) = c • ↑f
-- Mathlib.Tactic.Linter.TextBased
Mathlib.Linter.TextBased.instInhabitedStyleError.default : Mathlib.Linter.TextBased.StyleError✝
-- Mathlib.Analysis.Convex.Combination
/-- The convex hull of an affine basis is the intersection of the half-spaces defined by the
corresponding barycentric coordinates.  -/
AffineBasis.convexHull_eq_nonneg_coord : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] {ι : Type u_8} (b : AffineBasis ι R E),
  (convexHull R) (Set.range ⇑b) = {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- `p` is a Taylor series of `f` up to `⊤` if and only if `p.shift` is a Taylor series up to `⊤`
for `p 1`, which is a derivative of `f`.  -/
hasFTaylorSeriesUpToOn_top_iff_right : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {N : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  ↑⊤ ≤ N →
    (HasFTaylorSeriesUpToOn N f p s ↔
      (∀ x ∈ s, (p x 0).curry0 = f x) ∧
        (∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x) ∧
          HasFTaylorSeriesUpToOn N (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift) s)
-- Mathlib.Topology.Connected.Basic
IsPreconnected.subset_left_of_subset_union : ∀ {α : Type u} [inst : TopologicalSpace α] {s u v : Set α},
  IsOpen u → IsOpen v → Disjoint u v → s ⊆ u ∪ v → (s ∩ u).Nonempty → IsPreconnected s → s ⊆ u
-- Mathlib.Data.List.Lattice
List.sublist_suffix_of_union : ∀ {α : Type u_1} [inst : DecidableEq α] (l₁ l₂ : List α), ∃ t, t.Sublist l₁ ∧ t ++ l₂ = l₁ ∪ l₂
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Trident.mkHom.congr_simp : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {s t : CategoryTheory.Limits.Trident f} (k k_1 : s.pt ⟶ t.pt) (e_k : k = k_1)
  (w : CategoryTheory.CategoryStruct.comp k t.ι = s.ι),
  CategoryTheory.Limits.Trident.mkHom k w = CategoryTheory.Limits.Trident.mkHom k_1 ⋯
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_top : ∀ {R : Type u_2} [inst : NonAssocSemiring R], ⊤.op = ⊤
-- Mathlib.GroupTheory.GroupAction.OfQuotient
MulAction.quotient_out_smul_fixedPoints : ∀ {G : Type u_1} [inst : Group G] {A : Type u_2} [inst_1 : MulAction G A] {H : Subgroup G} [inst_2 : H.Normal]
  (g : G ⧸ H) (a : ↑(MulAction.fixedPoints (↥H) A)), Quotient.out g • a = g • a
-- Mathlib.Algebra.Algebra.Hom
/-- Promote a `LinearMap` to an `AlgHom` by supplying proofs about the behavior on `1` and `*`.  -/
AlgHom.ofLinearMap : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] → (f : A →ₗ[R] B) → f 1 = 1 → (∀ (x y : A), f (x * y) = f x * f y) → A →ₐ[R] B
-- Mathlib.Control.LawfulFix
Part.Fix.approxChain.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)),
  Part.Fix.approxChain f = { toFun := Part.Fix.approx ⇑f, monotone' := ⋯ }
-- Init.Data.Float.Model.Unpacked.Operations.OfNat
/-- Converts an `Int8` to an `UnpackedFloat`, returning positive zero on zero.  -/
Float.Model.UnpackedFloat.ofInt8 : Float.Model.Format → Int8 → Float.Model.UnpackedFloat
-- Mathlib.CategoryTheory.Sites.LocallySurjective
/-- If `φ : F₁ ⟶ F₂` is a morphism of sheaves, this is an abbreviation for
`Presheaf.IsLocallySurjective J φ.val`.  -/
CategoryTheory.Sheaf.IsLocallySurjective : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          {FA : A → A → Type u_1} →
            {CA : A → Type w'} →
              [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
                [CategoryTheory.ConcreteCategory A FA] → {F₁ F₂ : CategoryTheory.Sheaf J A} → (F₁ ⟶ F₂) → Prop
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.Hom.ext_iff : ∀ {M N : SemiNormedGrp} {x y : M.Hom N}, x = y ↔ x.hom' = y.hom'
-- Init.Data.Range.Polymorphic.UInt
UInt32.upwardEnumerableLE_ofBitVec : ∀ {x y : BitVec 32},
  Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y
-- Mathlib.Algebra.BigOperators.Finprod
AddMonoidHom.map_finsum : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {f : α → M}
  (g : M →+ N), Function.HasFiniteSupport f → g (∑ᶠ (i : α), f i) = ∑ᶠ (i : α), g (f i)
-- Init.Data.List.ToArray
List.find?_toArray : ∀ {α : Type u_1} (f : α → Bool) (l : List α), Array.find? f l.toArray = List.find? f l
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
_private.Mathlib.SetTheory.Ordinal.CantorNormalForm.0.Ordinal.CNF.rec.eq_def : ∀ (b : Ordinal.{u_2}) {C : Ordinal.{u_2} → Sort u_1} (H0 : C 0)
  (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ Ordinal.log b o) → C o) (o : Ordinal.{u_2}),
  Ordinal.CNF.rec b H0 H o = if h : o = 0 then ⋯ ▸ H0 else H o h (Ordinal.CNF.rec b H0 H (o % b ^ Ordinal.log b o))
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- The type of `I`-adic Cauchy sequences.  -/
AdicCompletion.AdicCauchySequence : {R : Type u_1} → [inst : CommRing R] → Ideal R → (M : Type u_4) → [inst_1 : AddCommGroup M] → [Module R M] → Type u_4
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.instStrictPatternModelForallCharBool : ∀ {p : Char → Bool}, String.Slice.Pattern.Model.StrictPatternModel p
-- Aesop.Util.Basic
Aesop.runTacticSyntaxAsMetaM : Lean.Syntax → List Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If the second of three points is weakly between the other two, and not equal to the first,
the angle at the first point (reversed) is zero.  -/
Wbtw.angle₃₁₂_eq_zero_of_ne : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, Wbtw ℝ p₁ p₂ p₃ → p₂ ≠ p₁ → EuclideanGeometry.angle p₃ p₁ p₂ = 0
-- Lean.Meta.Tactic.Simp.RegisterCommand
Lean.Parser.Command.registerSimpAttr : Lean.ParserDescr
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Martingale.sub : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f g : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E],
  MeasureTheory.Martingale f ℱ μ → MeasureTheory.Martingale g ℱ μ → MeasureTheory.Martingale (f - g) ℱ μ
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpoint_singleton_mem_interior_faceOpposite : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  (i : Fin (n + 1)), s.touchpoint {i} i ∈ (s.faceOpposite i).interior