mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.SInt.Lemmas
Int64.ofInt_int32ToInt : ∀ (x : Int32), Int64.ofInt x.toInt = x.toInt64
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
/-- Eta-expanded form of `CurveIntegrable.neg` -/
CurveIntegrable.fun_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b}, CurveIntegrable ω γ → CurveIntegrable (fun i => -ω i) γ
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.le.match_1.eq_4 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (x : α) (y : β)
  (h_1 : (val : β) → motive none (some val)) (h_2 : Unit → motive none none) (h_3 : (val : α) → motive (some val) none)
  (h_4 : (x : α) → (y : β) → motive (some x) (some y)),
  (match some x, some y with
    | none, some val => h_1 val
    | none, none => h_2 ()
    | some val, none => h_3 val
    | some x, some y => h_4 x y) =
    h_4 x y
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.ClientInfo.mk.injEq : ∀ (name : String) (version? : Option String) (name_1 : String) (version?_1 : Option String),
  ({ name := name, version? := version? } = { name := name_1, version? := version?_1 }) =
    (name = name_1 ∧ version? = version?_1)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndep.of_subsingleton : ∀ {Ω : Type u_1} {ι : Type u_2} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [Subsingleton ι]
  {m : ι → MeasurableSpace Ω} [MeasureTheory.IsProbabilityMeasure μ], ProbabilityTheory.iIndep m μ
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- An `AddEquiv` that respects open sets is a `ContinuousAddEquiv`.  -/
AddEquiv.toContinuousAddEquiv : {G : Type u} →
  [inst : TopologicalSpace G] →
    {H : Type v} →
      [inst_1 : TopologicalSpace H] →
        [inst_2 : Add G] → [inst_3 : Add H] → (e : G ≃+ H) → (∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) → G ≃ₜ+ H
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.mkMetric'.pre.eq_1 : ∀ {X : Type u_2} [inst : EMetricSpace X] (m : Set X → ENNReal) (r : ENNReal),
  MeasureTheory.OuterMeasure.mkMetric'.pre m r =
    MeasureTheory.OuterMeasure.boundedBy (MeasureTheory.extend fun s x => m s)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_mono : ∀ {α : Type u_1} {F : Type u_5} {G : Type u_6} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G},
  (∀ (x : α), ‖f x‖ ≤ ‖g x‖) → MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_and_left : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, P ∨ Q ∧ R ⊣⊢ₛ (P ∨ Q) ∧ (P ∨ R)
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- An injective presentation of an object `X` consists of a monomorphism `f : X ⟶ J`
to some injective object `J`.
 -/
CategoryTheory.InjectivePresentation.f : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → (self : CategoryTheory.InjectivePresentation X) → X ⟶ self.J
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.count_edges_eq_one : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} {p : G.Path u v},
  ∀ e ∈ (↑p).edges, List.count e (↑p).edges = 1
-- Mathlib.Topology.Compactness.SigmaCompact
/-- The sets in the compact exhaustion form a sequence:
each set is contained in the interior of the next.  -/
CompactExhaustion.subset_interior_succ' : ∀ {X : Type u_4} [inst : TopologicalSpace X] (self : CompactExhaustion X) (n : ℕ),
  self.toFun n ⊆ interior (self.toFun (n + 1))
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.exist_mem_powersetCard_of_inf : ∀ (α : Type u_1) (n : ℕ), 0 < n → ∀ [Infinite α] (a : α), ∃ s ∈ Set.powersetCard α n, a ∈ s
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.lt_wf : WellFounded fun x1 x2 => x1 < x2
-- Init.Data.String.Extra
_private.Init.Data.String.Extra.0.String.removeNumLeadingSpaces.saveLine : ℕ → {s : String} → s.Pos → String → String
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivAt.tendsto_slope_zero_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {f' : F}
  {x v : E} [inst_5 : Preorder 𝕜],
  HasLineDerivAt 𝕜 f f' x v → Filter.Tendsto (fun t => t⁻¹ • (f (x + t • v) - f x)) (nhdsWithin 0 (Set.Iio 0)) (nhds f')
-- Mathlib.Analysis.Calculus.DSlope
dslope_sub_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : DecidableEq 𝕜] (f : 𝕜 → E) (a : 𝕜),
  dslope (fun x => (x - a) • f x) a = Function.update f a (deriv (fun x => (x - a) • f x) a)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.sInf_toAddSubmonoid : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s : Set (NonUnitalSubsemiring R)),
  (sInf s).toAddSubmonoid = ⨅ t ∈ s, t.toAddSubmonoid
-- Mathlib.Algebra.Exact.Basic
/-- A necessary and sufficient condition for an exact sequence to descend to a quotient.  -/
Function.Exact.exact_mapQ_iff : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P},
  Function.Exact ⇑f ⇑g →
    ∀ {p : Submodule R M} {q : Submodule R N} {r : Submodule R P} (hpq : p ≤ Submodule.comap f q)
      (hqr : q ≤ Submodule.comap g r),
      Function.Exact ⇑(p.mapQ q f hpq) ⇑(q.mapQ r g hqr) ↔ g.range ⊓ r ≤ Submodule.map g q
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.MethodsRef.toMethodsImpl : Lean.Meta.Sym.Simp.MethodsRef → Lean.Meta.Sym.Simp.Methods
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of the "multiplication table" `fun (i, j) ↦ x i * y j`
is the product of the multiplicative heights of `x` and `y`.  -/
Height.mulHeight_fun_mul_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} {ι' : Type u_3} [Finite ι]
  [Finite ι'] {x : ι → K},
  x ≠ 0 → ∀ {y : ι' → K}, y ≠ 0 → (Height.mulHeight fun a => x a.1 * y a.2) = Height.mulHeight x * Height.mulHeight y
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.hasColimitsOfShape_of_final : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  [CategoryTheory.Limits.HasColimitsOfShape C E], CategoryTheory.Limits.HasColimitsOfShape D E
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
Polynomial.IsSplittingField.IsScalarTower.splits : ∀ {F : Type u} {K : Type v} (L : Type w) [inst : Field K] [inst_1 : Field L] [inst_2 : Field F] [inst_3 : Algebra K L]
  [inst_4 : Algebra F K] [inst_5 : Algebra F L] [IsScalarTower F K L] (f : Polynomial F)
  [Polynomial.IsSplittingField K L ((Polynomial.mapAlg F K) f)], ((Polynomial.mapAlg F L) f).Splits
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.VectorsProdEqOne.rotate_length : ∀ {G : Type u_2} [inst : Group G] {n : ℕ} (v : ↑(Equiv.Perm.vectorsProdEqOne G n)),
  Equiv.Perm.VectorsProdEqOne.rotate v n = v
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {outWidth : ℕ} →
        {aig : Std.Sat.AIG α} →
          {w len : ℕ} →
            (iterNum : ℕ) →
              aig.RefVec (len * w) →
                aig.RefVec (iterNum * w) →
                  2 * (iterNum - 1) < len → outWidth = (len + 1) / 2 * w → Std.Sat.AIG.RefVecEntry α outWidth
-- Mathlib.Data.Multiset.Pi
Multiset.Pi.cons_injective : ∀ {α : Type u_1} [inst : DecidableEq α] {δ : α → Sort u_2} {a : α} {b : δ a} {s : Multiset α},
  a ∉ s → Function.Injective (Multiset.Pi.cons s a b)
-- Mathlib.Tactic.ITauto
/-- Different propositional constructors that are variants of "and" for the purposes of the
theorem prover.  -/
Mathlib.Tactic.ITauto.AndKind : Type
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toSentence.eq_4 : FirstOrder.Field.FieldAxiom.mulAssoc.toSentence =
  (((FirstOrder.Language.var ∘ Sum.inr) 0 * (FirstOrder.Language.var ∘ Sum.inr) 1 *
              (FirstOrder.Language.var ∘ Sum.inr) 2).bdEqual
          ((FirstOrder.Language.var ∘ Sum.inr) 0 *
            ((FirstOrder.Language.var ∘ Sum.inr) 1 * (FirstOrder.Language.var ∘ Sum.inr) 2))).all.all.all
-- Mathlib.Order.Max
IsTop.eq_1 : ∀ {α : Type u_1} [inst : LE α] (a : α), IsTop a = ∀ (b : α), b ≤ a
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.hom_ofHom : ∀ {R S : Type u} [inst : AddGroup R] [inst_1 : AddGroup S] (f : R →+ S), AddGrpCat.Hom.hom (AddGrpCat.ofHom f) = f
-- Init.Data.UInt.Lemmas
UInt16.lt_or_lt_of_ne : ∀ {a b : UInt16}, a ≠ b → a < b ∨ b < a
-- Lean.Structure
Lean.instInhabitedStructureResolutionOrderConflict : Inhabited Lean.StructureResolutionOrderConflict
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- When its possible to compare the two, the composition of two `IsStronglyCocartesian.map` will
also be given by a `IsStronglyCocartesian.map`. In other words, given diagrams
```
a --φ--> b        b'         b''
|        |        |          |
v        v        v          v
R --f--> S --g--> S' --g'--> S'
```
and
```
a --φ'--> b'
|         |
v         v
R --f'--> S'

```
and
```
a --φ''--> b''
|          |
v          v
R --f''--> S''
```
such that `φ` and `φ'` are strongly co-Cartesian morphisms, and such that `f' = f ≫ g` and
`f'' = f' ≫ g'`. Then composing the induced map from `b ⟶ b'` with the induced map from
`b' ⟶ b''` gives the induced map from `b ⟶ b''`.  -/
CategoryTheory.Functor.IsStronglyCocartesian.map_comp_map_assoc : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsStronglyCocartesian f φ]
  {S' S'' : 𝒮} {b' b'' : 𝒳} {f' : R ⟶ S'} {f'' : R ⟶ S''} {g : S ⟶ S'} {g' : S' ⟶ S''}
  (H : f' = CategoryTheory.CategoryStruct.comp f g) (H' : f'' = CategoryTheory.CategoryStruct.comp f' g') (φ' : a ⟶ b')
  (φ'' : a ⟶ b'') [inst_3 : p.IsStronglyCocartesian f' φ'] [inst_4 : p.IsHomLift f'' φ''] {Z : 𝒳} (h : b'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCocartesian.map p f φ H φ')
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCocartesian.map p f' φ' H' φ'') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCocartesian.map p f φ ⋯ φ'') h
-- Mathlib.Analysis.Normed.Group.Basic
add_mem_ball_iff_norm : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {a b : E} {r : ℝ}, a + b ∈ Metric.ball a r ↔ ‖b‖ < r
-- Mathlib.Topology.Algebra.Order.Group
ContinuousAt.abs : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [inst_2 : LinearOrder G] [IsOrderedAddMonoid G]
  [OrderTopology G] {X : Type u_2} [inst_5 : TopologicalSpace X] {f : X → G} {x : X},
  ContinuousAt f x → ContinuousAt (fun x => |f x|) x
-- Init.Data.Int.Basic
instCoeHTCTIntOfIntCast : {R : Type u_1} → [IntCast R] → CoeHTCT ℤ R
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- `PolynomialModule R R` is isomorphic to `R[X]` as an `R[X]` module.  -/
PolynomialModule.equivPolynomialSelf : {R : Type u_2} → [inst : CommRing R] → PolynomialModule R R ≃ₗ[Polynomial R] Polynomial R
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compMeasurePreserving_toGerm : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  {β : Type u_5} [inst_2 : MeasurableSpace β] {f : α → β} {ν : MeasureTheory.Measure β} (g : β →ₘ[ν] γ)
  (hf : MeasureTheory.MeasurePreserving f μ ν), (g.compMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f ⋯
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.lift_eq_prod_map : ∀ {α : Type u} {β : Type v} [inst : Group β] {f : α → β} {x : FreeGroup α},
  (FreeGroup.lift f) x = FreeGroup.prod ((FreeGroup.map f) x)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.instIsIsoSnd : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B)
  {x y : CategoryTheory.Limits.CategoricalPullback F G} (f : x ⟶ y) [CategoryTheory.IsIso f], CategoryTheory.IsIso f.snd
-- Mathlib.Topology.Algebra.StarSubalgebra
StarAlgebra.elemental.le_centralizer_centralizer : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : StarRing A] [inst_5 : IsSemitopologicalSemiring A] [inst_6 : ContinuousStar A]
  [inst_7 : Algebra R A] [inst_8 : StarModule R A] [T2Space A] (x : A),
  StarAlgebra.elemental R x ≤ StarSubalgebra.centralizer R ↑(StarSubalgebra.centralizer R {x})
-- Mathlib.Algebra.GradedMonoid
SetLike.mul_mem_graded : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Mul R] [inst_2 : Add ι] {A : ι → S}
  [SetLike.GradedMul A] ⦃i j : ι⦄ {gi gj : R}, gi ∈ A i → gj ∈ A j → gi * gj ∈ A (i + j)
-- Init.Data.Int.Linear
Int.Internal.Linear.abs.eq_1 : ∀ (x : ℤ), Int.Internal.Linear.abs x = Int.ofNat x.natAbs
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.comp_isOpenMap_iff' : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (h : X ≃ₜ Y) {f : Y → Z}, IsOpenMap (f ∘ ⇑h) ↔ IsOpenMap f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_le_minKeyD_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α},
      (t.erase k).isEmpty = false →
        ∀ {fallback : α}, (cmp (t.minKeyD fallback) ((t.erase k).minKeyD fallback)).isLE = true
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.structureMapLM_eq : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {i : ℕ},
  ContDiffMapSupportedIn.structureMapLM 𝕜 n i =
    ContDiffMapSupportedIn.toBoundedContinuousFunctionLM 𝕜 ∘ₗ ContDiffMapSupportedIn.iteratedFDerivLM 𝕜 n 0 i
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  (μ : MeasureTheory.ProbabilityMeasure Ω), ⇑μ.toWeakDualBCNN = μ.toFiniteMeasure.testAgainstNN
-- Lean.Level
Lean.mkLevelIMaxEx : Lean.Level → Lean.Level → Lean.Level
-- Init.Data.Nat.Basic
Nat.sub_one_sub_lt_of_lt : ∀ {a b : ℕ}, a < b → b - 1 - a < b
-- Mathlib.Tactic.ClickSuggestions.FindPremises
Mathlib.Tactic.ClickSuggestions.Choice.mk.sizeOf_spec : ∀ (rw grw app appAt : Bool),
  sizeOf { rw := rw, grw := grw, app := app, appAt := appAt } = 1 + sizeOf rw + sizeOf grw + sizeOf app + sizeOf appAt
-- Mathlib.Data.Set.Card
Set.le_ncard_of_inj_on_range : ∀ {α : Type u_1} {s : Set α} {n : ℕ} (f : ℕ → α),
  (∀ i < n, f i ∈ s) →
    (∀ i < n, ∀ j < n, f i = f j → i = j) → autoParam s.Finite Set.le_ncard_of_inj_on_range._auto_1 → n ≤ s.ncard
-- Mathlib.Topology.MetricSpace.Dilation
DilationClass.mk : ∀ {F : Type u_3} {α : outParam (Type u_4)} {β : outParam (Type u_5)} [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β] [inst_2 : FunLike F α β],
  (∀ (f : F), ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y) → DilationClass F α β
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.ext.inj : ∀ {declName declName_1 : Lean.Name},
  Lean.Meta.Grind.Entry.ext declName = Lean.Meta.Grind.Entry.ext declName_1 → declName = declName_1
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDualEquiv_apply : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) [inst_4 : Finite ι] (m : M), b.toDualEquiv m = b.toDual m
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
norm_iteratedFDerivWithin_fderivWithin : ∀ {𝕜 : 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} {x : E} {n : ℕ},
  UniqueDiffOn 𝕜 s →
    x ∈ s → ‖iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x‖ = ‖iteratedFDerivWithin 𝕜 (n + 1) f s x‖
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
/-- If the cardinality of `σ` is `n`, then `esymmAlgHom σ R n` is an isomorphism.  -/
MvPolynomial.esymmAlgEquiv : (σ : Type u_1) →
  (R : Type u_3) →
    {n : ℕ} →
      [inst : Fintype σ] →
        [inst_1 : CommRing R] →
          Fintype.card σ = n → MvPolynomial (Fin n) R ≃ₐ[R] ↥(MvPolynomial.symmetricSubalgebra σ R)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
CategoryTheory.Abelian.Ext.smul_comp : ∀ {R : Type t} [inst : Ring R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : CategoryTheory.HasExt C]
  {X Y Z : C} {a b : ℕ} (α : CategoryTheory.Abelian.Ext X Y a) (β : CategoryTheory.Abelian.Ext Y Z b) {c : ℕ}
  (h : a + b = c) (r : R), (r • α).comp β h = r • α.comp β h
-- Mathlib.LinearAlgebra.RootSystem.Basic
/-- Even though the roots may not span, coroots are distinguished by their pairing with the
roots. The proof depends crucially on the fact that there are finitely-many roots.

Modulo trivial generalisations, this statement is exactly Lemma 1.1.4 on page 87 of SGA 3 XXI.  -/
RootPairing.injOn_dualMap_subtype_span_root_coroot : ∀ {ι : 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) [Finite ι]
  [IsAddTorsionFree M],
  Set.InjOn (⇑((Submodule.span R (Set.range ⇑P.root)).subtype.dualMap ∘ₗ P.flip)) (Set.range ⇑P.coroot)
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_le_self : ∀ {G : Type u_1} [inst : AddGroup G] (S : AddSubgroup G) (n : ℕ), S.lowerCentralSeries n ≤ S
-- Mathlib.Topology.Homotopy.HSpaces
unitInterval.continuous_qRight : Continuous unitInterval.qRight
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- If `F₁` and `F₂` are functors `J ⥤ C`, `G : K ⥤ J`, and
`F₁'` and `F₂'` are functors `K ⥤ C` that are respectively
isomorphic to `G ⋙ F₁` and `G ⋙ F₂`, then this is the
induced morphism `enrichedHom V F₁ F₂ ⟶ enrichedHom V F₁' F₂'` in `V`
when `C` is a category enriched in `V`.  -/
CategoryTheory.Enriched.FunctorCategory.precompEnrichedHom' : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          {J : Type u₃} →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              {K : Type u₄} →
                [inst_4 : CategoryTheory.Category.{v₄, u₄} K] →
                  [inst_5 : CategoryTheory.EnrichedOrdinaryCategory V C] →
                    {F₁ F₂ : CategoryTheory.Functor J C} →
                      (G : CategoryTheory.Functor K J) →
                        [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₂] →
                          {F₁' F₂' : CategoryTheory.Functor K C} →
                            [inst_7 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁' F₂'] →
                              (G.comp F₁ ≅ F₁') →
                                (G.comp F₂ ≅ F₂') →
                                  (CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₂ ⟶
                                    CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁' F₂')
-- Mathlib.Topology.MetricSpace.ShrinkingLemma
/-- Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover
of a proper metric space by open balls can be shrunk to a new cover by open balls so that each of
the new balls has strictly smaller radius than the old one.  -/
exists_iUnion_ball_eq_radius_lt : ∀ {α : Type u} {ι : Type v} [inst : MetricSpace α] [ProperSpace α] {c : ι → α} {r : ι → ℝ},
  (∀ (x : α), {i | x ∈ Metric.ball (c i) (r i)}.Finite) →
    ⋃ i, Metric.ball (c i) (r i) = Set.univ → ∃ r', ⋃ i, Metric.ball (c i) (r' i) = Set.univ ∧ ∀ (i : ι), r' i < r i
-- Mathlib.Probability.Moments.ComplexMGF
ProbabilityTheory.integrableExpSet.eq_1 : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.integrableExpSet X μ = {t | MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ}
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.instSemiringObjForgetRingHomCarrier : {R : SemiRingCat} → Semiring ((CategoryTheory.forget SemiRingCat).obj R)
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.Gamma1_to_Gamma0_mem : ∀ {N : ℕ} (A : ↥(CongruenceSubgroup.Gamma0 N)),
  A ∈ CongruenceSubgroup.Gamma1' N ↔ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
-- Mathlib.Topology.Category.TopPair
/-- The proof that the homotopies fit into a commutative square with the maps of the pairs.  -/
TopPair.Homotopy.w_assoc : ∀ {X Y : TopPair} {f g : X ⟶ Y} (self : TopPair.Homotopy f g) {Z : TopCat} (h : TopPair.fst ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight TopPair.map TopCat.I)
      (CategoryTheory.CategoryStruct.comp self.fst.h h) =
    CategoryTheory.CategoryStruct.comp self.snd.h (CategoryTheory.CategoryStruct.comp TopPair.map h)
-- Mathlib.Algebra.Order.Round
abs_sub_round_div_natCast_eq : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] {m n : ℕ},
  |↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(min (m % n) (n - m % n)) / ↑n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a : α}
  {fallback : β}, t.isEmpty = true → Std.DTreeMap.Const.getD t a fallback = fallback
-- Lean.Util.ReplaceLevel
Lean.Expr.ReplaceLevelImpl.cache : USize → Lean.Expr → Lean.Expr → Lean.Expr.ReplaceLevelImpl.ReplaceM Lean.Expr
-- Mathlib.RingTheory.Flat.Basic
Module.Flat.out : ∀ {R : Type u} {M : Type v} {inst : CommSemiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
  [self : Module.Flat R M] ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] [Module.Finite R P]
  (N : Submodule R P), N.FG → Function.Injective ⇑(LinearMap.rTensor M N.subtype)
-- Mathlib.Order.SuccPred.Basic
PredOrder.ext_iff : ∀ {α : Type u_3} {inst : Preorder α} {x y : PredOrder α}, x = y ↔ PredOrder.pred = PredOrder.pred
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.Homotopic.refl : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} (f : ↑(GenLoop N X x)), GenLoop.Homotopic f f
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.page_X : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r : ℤ) (hr : r₀ ≤ r) (pq : κ),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.page X data r hr).X pq =
    CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX X data r pq ⋯