mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasSum_unique : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [inst_2 : Unique β] (f : β → α)
  (L : optParam (SummationFilter β) (SummationFilter.unconditional β)) [L.LeAtTop], HasSum f (f default) L
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.IsDPMorphism.on_span : ∀ {A : Type u_3} {B : Type u_4} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  (hI : DividedPowers I) (hJ : DividedPowers J) {f : A →+* B} {S : Set A},
  I = Ideal.span S → (∀ s ∈ S, f s ∈ J) → (∀ {n : ℕ}, ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)) → hI.IsDPMorphism hJ f
-- Init.Data.SInt.Lemmas
Int64.add_left_neg : ∀ (a : Int64), -a + a = 0
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
/-- The natural isomorphism `Γ₀ ⋙ N₁ ≅ toKaroubi (ChainComplex C ℕ)`.  -/
AlgebraicTopology.DoldKan.N₁Γ₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        AlgebraicTopology.DoldKan.Γ₀.comp AlgebraicTopology.DoldKan.N₁ ≅
          CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)
-- Init.Data.Array.Find
Array.findIdx?_take : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {p : α → Bool},
  Array.findIdx? p (xs.take i) = (Array.findIdx? p xs).bind (Option.guard fun j => decide (j < i))
-- Mathlib.Analysis.Convex.Side
/-- **Alias** of `AffineSubspace.isPreconnected_setOfPred_sOppSide`. -/
AffineSubspace.isPreconnected_setOf_sOppSide : ∀ {V : Type u_2} {P : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor V P] (s : AffineSubspace ℝ P) (x : P),
  IsPreconnected {y | s.SOppSide x y}
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `lt_neg_add_iff_add_lt`. -/
add_lt_of_lt_neg_add : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, b < -a + c → a + b < c
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumFinsuppEquivProdFinsupp_symm_inl : ∀ {α : Type u_12} {β : Type u_13} {γ : Type u_14} [inst : Zero γ] (fg : (α →₀ γ) × (β →₀ γ)) (x : α),
  (Finsupp.sumFinsuppEquivProdFinsupp.symm fg) (Sum.inl x) = fg.1 x
-- Mathlib.Analysis.Calculus.FDeriv.Pow
/-- Eta-expanded form of `HasStrictFDerivAt.pow'` -/
HasStrictFDerivAt.fun_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {f' : E →L[𝕜] 𝔸}
  {x : E},
  HasStrictFDerivAt f f' x →
    ∀ (n : ℕ),
      HasStrictFDerivAt (fun i => f i ^ n) (∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • f') x
-- Lean.Meta.Tactic.Grind.Types
/-- Inserts `e` into the list of case-split candidates if it was not inserted before.  -/
Lean.Meta.Grind.addSplitCandidate : Lean.Meta.Grind.SplitInfo → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Combinatorics.Graph.Delete
Graph.vertexSet_deleteEdges : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β), (G.deleteEdges F).vertexSet = G.vertexSet
-- Mathlib.CategoryTheory.Category.ULift
/-- The equivalence between `C` and `AsSmall C`.  -/
CategoryTheory.AsSmall.equiv : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → C ≌ CategoryTheory.AsSmall C
-- Mathlib.MeasureTheory.Group.Action
/-- Equivalent definitions of a measure invariant under an additive action of a group.

- 0: `VAddInvariantMeasure G α μ`;

- 1: for every `c : G` and a measurable set `s`, the measure of the preimage of `s` under
vector addition `(c +ᵥ ·)` is equal to the measure of `s`;

- 2: for every `c : G` and a measurable set `s`, the measure of the image `c +ᵥ s` of `s` under
vector addition `(c +ᵥ ·)` is equal to the measure of `s`;

- 3, 4: properties 2, 3 for any set, including non-measurable ones;

- 5: for any `c : G`, vector addition of `c` maps `μ` to `μ`;

- 6: for any `c : G`, vector addition of `c` is a measure-preserving map.  -/
MeasureTheory.vaddInvariantMeasure_tfae : ∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  (μ : MeasureTheory.Measure α) [MeasurableConstVAdd G α],
  [MeasureTheory.VAddInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → μ (c +ᵥ s) = μ s,
      ∀ (c : G) (s : Set α), μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), μ (c +ᵥ s) = μ s,
      ∀ (c : G), MeasureTheory.Measure.map (fun x => c +ᵥ x) μ = μ,
      ∀ (c : G), MeasureTheory.MeasurePreserving (fun x => c +ᵥ x) μ μ].TFAE
-- Mathlib.Topology.Hom.ContinuousEval
/-- Evaluation of a bundled morphism at a point is continuous in both variables.  -/
ContinuousEval.continuous_eval : ∀ {F : Type u_1} {X : outParam (Type u_2)} {Y : outParam (Type u_3)} {inst : FunLike F X Y}
  {inst_1 : TopologicalSpace F} {inst_2 : TopologicalSpace X} {inst_3 : TopologicalSpace Y}
  [self : ContinuousEval F X Y], Continuous fun fx => fx.1 fx.2
-- Mathlib.CategoryTheory.Generator.StrongGenerator
CategoryTheory.ObjectProperty.IsStrongGenerator.subobject_eq_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  P.IsStrongGenerator →
    ∀ {X : C} {A : CategoryTheory.Subobject X}, (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
CategoryTheory.Idempotents.DoldKan.Γ_map_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.IsIdempotentComplete C] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C]
  {X Y : ChainComplex C ℕ} (f : X ⟶ Y) (Δ : SimplexCategoryᵒᵖ),
  (CategoryTheory.Idempotents.DoldKan.Γ.map f).app Δ =
    (AlgebraicTopology.DoldKan.Γ₀.splitting X).desc Δ fun A =>
      CategoryTheory.CategoryStruct.comp (f.f (Opposite.unop A.fst).len)
        (((AlgebraicTopology.DoldKan.Γ₀.splitting Y).cofan Δ).inj A)
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- `charFun` is a Fourier integral for the inner product and the character `probChar`.  -/
MeasureTheory.charFun_eq_fourierIntegral : ∀ {E : Type u_2} {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [inst : SeminormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E] (t : E),
  MeasureTheory.charFun μ t = VectorFourier.fourierIntegral Real.probChar μ (innerₗ E) 1 (-t)
-- Mathlib.Algebra.Order.Module.Defs
Pi.instSMulPosStrictMono : ∀ {α : Type u_1} {ι : Type u_3} {β : ι → Type u_4} [inst : Zero α] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : PartialOrder α] [inst_3 : (i : ι) → PartialOrder (β i)] [inst_4 : (i : ι) → SMulWithZero α (β i)]
  [∀ (i : ι), SMulPosStrictMono α (β i)], SMulPosStrictMono α ((i : ι) → β i)
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
/-- The sum of the `k` initial terms of the Liouville number to base `m` is a ratio of natural
numbers where the denominator is `m ^ k!`.  -/
LiouvilleNumber.partialSum_eq_rat : ∀ {m : ℕ}, 0 < m → ∀ (k : ℕ), ∃ p, LiouvilleNumber.partialSum (↑m) k = ↑p / ↑(m ^ k.factorial)
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Cnstr.continue.injEq : ∀ (pat pat_1 : Lean.Expr),
  (Lean.Meta.Grind.EMatch.Cnstr.continue pat = Lean.Meta.Grind.EMatch.Cnstr.continue pat_1) = (pat = pat_1)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.List.forIn'_cons.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (x : ForInStep β) → ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive x
-- Mathlib.Tactic.DeriveTraversable
/-- Makes a `match` expression corresponding to the application of `casesOn` like:
```lean
match (motive := motive) indices₁, indices₂, .., (val : type.{univs} params₁ params₂ ..) with
| _, _, .., ctor₁ fields₁₁ fields₁₂ .. => rhss ctor₁ [fields₁₁, fields₁₂, ..]
| _, _, .., ctor₂ fields₂₁ fields₂₂ .. => rhss ctor₂ [fields₂₁, fields₂₂, ..]
```
This is convenient to make a definition with equation lemmas.  -/
Mathlib.Deriving.Traversable.mkCasesOnMatch : Lean.Name →
  List Lean.Level →
    List Lean.Expr →
      Lean.Expr →
        List Lean.Expr →
          Lean.Expr → (Lean.Name → List Lean.FVarId → Lean.Elab.TermElabM Lean.Expr) → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- The canonical morphism `(K.shortComplexTruncLE n₀).X₃ ⟶ K.truncGE n₁`.  -/
CochainComplex.shortComplexTruncLEX₃ToTruncGE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (K : CochainComplex C ℤ) →
        (n₀ n₁ : ℤ) →
          autoParam (n₀ + 1 = n₁) CochainComplex.shortComplexTruncLEX₃ToTruncGE._auto_1 →
            ((K.shortComplexTruncLE n₀).X₃ ⟶ K.truncGE n₁)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.takeWhile_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String},
  s.toSlice.takeWhile pat = s.takeWhile pat
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `F : ι → β → α` of functions between uniform spaces is
*uniformly equicontinuous on `S : Set β`* if, for all entourages `U ∈ 𝓤 α`, there is a relative
entourage `V ∈ 𝓤 β ⊓ 𝓟 (S ×ˢ S)` such that, whenever `x` and `y` are `V`-close, we have that,
*for all `i : ι`*, `F i x` is `U`-close to `F i y`.  -/
UniformEquicontinuousOn : {ι : Type u_1} →
  {α : Type u_6} → {β : Type u_8} → [uα : UniformSpace α] → [uβ : UniformSpace β] → (ι → β → α) → Set β → Prop
-- Mathlib.Algebra.DualNumber
/-- `ε` commutes with every element of the algebra.  -/
DualNumber.commute_eps_left : ∀ {R : Type u_1} [inst : Semiring R] (x : DualNumber R), Commute DualNumber.eps x
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
range_mem_nhds_isInteriorPoint : ∀ {𝕜 : 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] {x : M},
  I.IsInteriorPoint x → Set.range ↑I ∈ nhds (↑(extChartAt I x) x)
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- A countable product of completely pseudometrizable spaces is completely pseudometrizable.  -/
TopologicalSpace.IsCompletelyPseudoMetrizableSpace.pi_countable : ∀ {ι : Type u_3} [Countable ι] {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)]
  [∀ (i : ι), TopologicalSpace.IsCompletelyPseudoMetrizableSpace (X i)],
  TopologicalSpace.IsCompletelyPseudoMetrizableSpace ((i : ι) → X i)
-- Mathlib.Order.SuccPred.Limit
/-- See `not_isSuccPrelimit_iff_succ_eq` for a version that states that `a` is a successor of a
value other than itself.  -/
Order.mem_range_succ_of_not_isSuccPrelimit : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : SuccOrder α],
  ¬Order.IsSuccPrelimit a → a ∈ Set.range Order.succ
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
normEDS_zero : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), normEDS b c d 0 = 0
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instEssentiallySmallEssImageOfEssentiallySmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  [CategoryTheory.EssentiallySmall.{w, v, u} C] (F : CategoryTheory.Functor C D),
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v', u'} F.essImage
-- Mathlib.Algebra.Lie.Submodule
/-- Copy of a `LieSubmodule` with a new `carrier` equal to the old one. Useful to fix definitional
equalities.  -/
LieSubmodule.copy : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : LieRingModule L M] → (N : LieSubmodule R L M) → (s : Set M) → s = ↑N → LieSubmodule R L M
-- Mathlib.CategoryTheory.Sites.Over
/-- **Alias** of `BotHomClass.map_bot`. -/
CategoryTheory.Sieve.overEquiv_bot : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : Bot α} {inst_1 : Bot β}
  {inst_2 : FunLike F α β} [self : BotHomClass F α β] (f : F), f ⊥ = ⊥
-- Init.Data.Int.Order
Int.mul_self_le_mul_self : ∀ {a b : ℤ}, 0 ≤ a → a ≤ b → a * a ≤ b * b
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj₃'_tensorHom : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C}
  [inst_3 : X₁.HasTensor X₂] [inst_4 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃]
  [inst_5 : Y₁.HasTensor Y₂] [inst_6 : (CategoryTheory.GradedObject.Monoidal.tensorObj Y₁ Y₂).HasTensor Y₃]
  (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ f₂) f₃ j) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (f₁ i₁) (f₂ i₂))
        (f₃ i₃))
      (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' Y₁ Y₂ Y₃ i₁ i₂ i₃ j h)
-- Mathlib.RingTheory.Flat.Basic
Module.Flat.dfinsupp_iff : ∀ {R : Type u} [inst : CommSemiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)], Module.Flat R (Π₀ (i : ι), M i) ↔ ∀ (i : ι), Module.Flat R (M i)
-- Mathlib.Order.SymmDiff
bihimp_of_ge : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ≤ b → bihimp a b = b ⇨ a
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.BimonObj.one_comul : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (M : C) [self : CategoryTheory.BimonObj M],
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one CategoryTheory.ComonObj.comul = CategoryTheory.MonObj.one
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Array.0.Std.Iterators.Types.ArrayIterator.instIterator.match_1.splitter : {m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    (motive : Std.IterStep (Std.IterM m α) α → Sort u_3) →
      (x : Std.IterStep (Std.IterM m α) α) →
        ((it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out)) →
          ((it : Std.IterM m α) → motive (Std.IterStep.skip it)) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.LinearAlgebra.DFinsupp
/-- The supremum of a family of submodules is equal to the range of `DFinsupp.lsum`; that is
every element in the `iSup` can be produced from taking a finite number of non-zero elements
of `p i`, coercing them to `N`, and summing them.  -/
Submodule.iSup_eq_range_dfinsupp_lsum : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [inst_3 : DecidableEq ι] (p : ι → Submodule R N), iSup p = ((DFinsupp.lsum ℕ) fun i => (p i).subtype).range
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.instSubsingleton : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] [Subsingleton M],
  Subsingleton (MulArchimedeanClass M)
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.instAddCommMagma : {R : Type u_1} →
  [inst : LinearOrder R] → [inst_1 : CommRing R] → [inst_2 : IsStrictOrderedRing R] → AddCommMagma (ArchimedeanClass R)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteAtFilter.filterSup : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : Filter α},
  μ.FiniteAtFilter f → μ.FiniteAtFilter g → μ.FiniteAtFilter (f ⊔ g)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instNeg : {R : Type u_1} → {a b : R} → [Neg R] → Neg (QuadraticAlgebra R a b)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.leOnePart : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : Group β] [inst_2 : Lattice β] [ContinuousSup β] [ContinuousInv β],
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun x => (f x)⁻ᵐ) μ
-- Mathlib.Topology.MetricSpace.Gluing
Metric.Sum.dist.eq_4 : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (x_2 : Y) (y : X),
  Metric.Sum.dist (Sum.inr x_2) (Sum.inl y) = dist x_2 ⋯.some + 1 + dist ⋯.some y
-- Init.Data.List.TakeDrop
List.dropWhile_cons_of_pos : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, p a = true → List.dropWhile p (a :: l) = List.dropWhile p l
-- Std.Time.Date.Unit.Year
Std.Time.Year.Era.bce.sizeOf_spec : sizeOf Std.Time.Year.Era.bce = 1
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- The norm of a bounded continuous function is the supremum of `‖f x‖`.
We use `sInf` to ensure that the definition works if `α` has no elements.  -/
BoundedContinuousFunction.norm_eq : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β), ‖f‖ = sInf {C | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C}
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.toLinearMap_injective : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {N : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N},
  Function.Injective QuadraticMap.Isometry.toLinearMap
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.fvars.anonymous : Lean.Option Bool
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Expand the square  -/
norm_add_sq_real : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * inner ℝ x y + ‖y‖ ^ 2
-- Mathlib.Data.FP.Basic
FP.instInhabitedFloat : [C : FP.FloatCfg] → Inhabited FP.Float
-- Mathlib.Algebra.Order.AddTorsor
IsOrderedVAdd.vadd_le_vadd_left : ∀ {G : Type u_3} {P : Type u_4} {inst : LE G} {inst_1 : LE P} {inst_2 : VAdd G P} [self : IsOrderedVAdd G P] (a b : P),
  a ≤ b → ∀ (c : G), c +ᵥ a ≤ c +ᵥ b
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_alterKey_eq_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  [inst_4 : Std.LawfulEqOrd α] {k : α} {f : Option (β k) → Option (β k)} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.maxKey? (Std.Internal.List.alterKey k f l) = some k ↔
      (f (Std.Internal.List.getValueCast? k l)).isSome = true ∧
        ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k' k).isLE = true)
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.natIsoFunctor_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w}
  {F : CategoryTheory.Functor C (CategoryTheory.Codiscrete A)} (X : C),
  CategoryTheory.Codiscrete.natIsoFunctor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.eval_eq_sum_degreeLTEquiv : ∀ {R : Type u} [inst : Semiring R] {n : ℕ} {p : Polynomial R} (hp : p ∈ Polynomial.degreeLT R n) (x : R),
  Polynomial.eval x p = ∑ i, (Polynomial.degreeLTEquiv R n) ⟨p, hp⟩ i * x ^ ↑i
-- Init.Data.Int.Lemmas
Int.negSucc_mul_subNatNat : ∀ (m n k : ℕ), Int.negSucc m * Int.subNatNat n k = Int.subNatNat (m.succ * k) (m.succ * n)
-- Mathlib.FieldTheory.Relrank
/-- **Alias** of the reverse direction of `Subfield.relrank_eq_one_iff`. -/
Subfield.relrank_eq_one_of_le : ∀ {E : Type v} [inst : Field E] {A B : Subfield E}, B ≤ A → A.relrank B = 1
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.zero_mem_smul_finset : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β] {t : Finset β}
  {a : α}, 0 ∈ t → 0 ∈ a • t
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.Context : Type
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.le_sum : ∀ {ι : Type u} (f : ι → Cardinal.{max u v}) (i : ι), f i ≤ Cardinal.sum f
-- Mathlib.Algebra.Polynomial.Lifts
/-- If `p` lifts then `p.erase n` lifts.  -/
Polynomial.erase_mem_lifts : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial S} (n : ℕ),
  p ∈ Polynomial.lifts f → Polynomial.erase n p ∈ Polynomial.lifts f
-- Mathlib.Data.Finset.Insert
Finset.instNonemptyElemCoeInsert : ∀ {α : Type u_1} [inst : DecidableEq α] (i : α) (s : Finset α), Nonempty ↑↑(insert i s)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.lineDerivOpCLM_eq : ∀ (𝕜 : Type u_2) {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace ℝ F] [inst_3 : NormedSpace ℝ E] [inst_4 : RCLike 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (m : E),
  LineDeriv.lineDerivOpCLM 𝕜 (SchwartzMap E F) m = SchwartzMap.evalCLM 𝕜 E F m ∘SL SchwartzMap.fderivCLM 𝕜 E F
-- Mathlib.Geometry.Euclidean.Projection
/-- Adding a vector to a point in the given subspace, then taking the
orthogonal projection, produces the original point if the vector is a
multiple of the result of subtracting a point's orthogonal projection
from that point.  -/
EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_orthogonalProjection : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p₁ : P} (p₂ : P) (r : 𝕜) (hp : p₁ ∈ s),
  (EuclideanGeometry.orthogonalProjection s) (r • (p₂ -ᵥ ↑((EuclideanGeometry.orthogonalProjection s) p₂)) +ᵥ p₁) =
    ⟨p₁, hp⟩
-- Mathlib.Algebra.Polynomial.SpecificDegree
/-- A polynomial of degree 2 or 3 is irreducible iff it doesn't have roots.  -/
Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_three : ∀ {K : Type u_1} [inst : Field K] {p : Polynomial K}, 2 ≤ p.natDegree → p.natDegree ≤ 3 → (Irreducible p ↔ p.roots = 0)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.modByMonicHom.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] {g : Polynomial R} (hg : g.Monic),
  AdjoinRoot.modByMonicHom hg = AdjoinRoot.modByMonicHom hg
-- Mathlib.GroupTheory.Finiteness
AddSubgroup.fg_iff_mul_fg : ∀ {H : Type u_4} [inst : AddGroup H] (P : AddSubgroup H), P.FG ↔ (AddSubgroup.toSubgroup P).FG
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.mem_skeleton_iff : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] {n : ℕ∞}
  {x : X},
  x ∈ Topology.RelCWComplex.skeleton C n ↔ x ∈ D ∨ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ Topology.RelCWComplex.openCell m j
-- Lean.Meta.WrapInstance
Lean.Meta.backward.inferInstanceAs.wrap.reuseSubInstances : Lean.Option Bool
-- Mathlib.Topology.Connected.Basic
/-- The iUnion of preconnected sets indexed by a subset of a type with an archimedean successor
(like `ℕ` or `ℤ`) such that any two neighboring sets meet is preconnected.  -/
IsPreconnected.biUnion_of_chain : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] [inst_2 : SuccOrder β]
  [IsSuccArchimedean β] {s : β → Set α} {t : Set β},
  t.OrdConnected →
    (∀ n ∈ t, IsPreconnected (s n)) →
      (∀ n ∈ t, Order.succ n ∈ t → (s n ∩ s (Order.succ n)).Nonempty) → IsPreconnected (⋃ n ∈ t, s n)
-- Std.Time.DateTime.PlainDateTime
/-- Subtracts a `Month.Offset` from a `PlainDateTime`, adjusting the day to the last valid day of the
resulting month.
 -/
Std.Time.PlainDateTime.subMonthsRollOver : Std.Time.PlainDateTime → Std.Time.Month.Offset → Std.Time.PlainDateTime