mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extendXIso.eq_1 : ∀ {ι : 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.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') {i' : ι'}
  {i : ι} (h : e.f i = i'), K.extendXIso e h = HomologicalComplex.extend.XIso K ⋯
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.add_comp_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y Z : C} {X' Y' Z' : D} (eX : L.obj X ≅ X') (eY : L.obj Y ≅ Y')
  (eZ : L.obj Z ≅ Z') (f₁ f₂ : X' ⟶ Y') (g : Y' ⟶ Z') {Z_1 : D} (h : Z' ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Preadditive.add W eX eY f₁ f₂)
      (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Localization.Preadditive.add W eX eZ (CategoryTheory.CategoryStruct.comp f₁ g)
        (CategoryTheory.CategoryStruct.comp f₂ g))
      h
-- Mathlib.Topology.Order.Monotone
MonotoneOn.tendsto_nhdsWithin_Ioo_left : ∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β} {x y : α},
  (Set.Ioo y x).Nonempty →
    MonotoneOn f (Set.Ioo y x) →
      BddAbove (f '' Set.Ioo y x) → Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sSup (f '' Set.Ioo y x)))
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.lratChecker.match_3.congr_eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : List (Std.Tactic.BVDecide.LRAT.Action β α) → Sort u_3)
  (prf : List (Std.Tactic.BVDecide.LRAT.Action β α)) (h_1 : Unit → motive [])
  (h_2 :
    (id : ℕ) →
      (rupHints : Array ℕ) →
        (tail : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
          motive (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail))
  (h_3 :
    (id : ℕ) →
      (c : β) →
        (rupHints : Array ℕ) →
          (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
            motive (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf))
  (h_4 :
    (id : ℕ) →
      (c : β) →
        (pivot : Std.Sat.Literal α) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                motive (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf))
  (h_5 :
    (ids : Array ℕ) →
      (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
        motive (Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf))
  (id : ℕ) (c : β) (rupHints : Array ℕ) (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)),
  prf = Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf →
    (match prf with
      | [] => h_1 ()
      | Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail => h_2 id rupHints tail
      | Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf => h_3 id c rupHints restPrf
      | Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf =>
        h_4 id c pivot rupHints ratHints restPrf
      | Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf => h_5 ids restPrf) ≍
      h_3 id c rupHints restPrf
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousFunctions.instCoeFunElemForallOfPredContinuous : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → CoeFun ↑{f | Continuous f} fun x => α → β
-- Mathlib.Algebra.LinearRecurrence
/-- Two solutions are equal iff their initial conditions are equal.  -/
LinearRecurrence.eq_iff_eqOn_range_order : ∀ {R : Type u_1} [inst : CommSemiring R] (E : LinearRecurrence R) (u v : ℕ → R),
  E.IsSolution u → E.IsSolution v → (u = v ↔ Set.EqOn u v ↑(Finset.range E.order))
-- Lean.Parser.Attr
Lean.Parser.Attr.tactic_name.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumRingEquiv_X_inl : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (s : S₁),
  (MvPolynomial.sumRingEquiv R S₁ S₂) (MvPolynomial.X (Sum.inl s)) = MvPolynomial.X s
-- Mathlib.Order.CompleteLatticeIntervals
subset_sSup_of_not_bddAbove : ∀ {α : Type u_2} (s : Set α) [inst : Preorder α] [inst_1 : SupSet α] [inst_2 : Inhabited ↑s] {t : Set ↑s},
  ¬BddAbove t → sSup t = default
-- Batteries.Data.ByteArray
ByteArray.ofFn.eq_1 : ∀ {n : ℕ} (f : Fin n → UInt8),
  ByteArray.ofFn f = Fin.foldl n (fun acc i => acc.push (f i)) (ByteArray.emptyWithCapacity n)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.brecOn.eq : ∀ {L : FirstOrder.Language} {α : Type u'} {motive : (a : ℕ) → L.BoundedFormula α a → Sort u_1} {a : ℕ}
  (t : L.BoundedFormula α a)
  (F_1 : (a : ℕ) → (t : L.BoundedFormula α a) → FirstOrder.Language.BoundedFormula.below t → motive a t),
  FirstOrder.Language.BoundedFormula.brecOn t F_1 = F_1 a t (FirstOrder.Language.BoundedFormula.brecOn.go t F_1).2
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Preorder.mk.congr_simp : ∀ {α : Type u_2} [toLE : LE α] [toLE_1 : LE α] (e_toLE : toLE = toLE_1) [toLT : LT α] [toLT_1 : LT α]
  (e_toLT : toLT = toLT_1) (le_refl : ∀ (a : α), a ≤ a) (le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c)
  (lt_iff_le_not_ge : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a),
  { toLE := toLE, toLT := toLT, le_refl := le_refl, le_trans := le_trans, lt_iff_le_not_ge := lt_iff_le_not_ge } =
    { toLE := toLE_1, toLT := toLT_1, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }
-- Init.Dynamic
/-- A type-tagged union that can store any type with a `TypeName` instance.

This is roughly equivalent to `(α : Type) × TypeName α × α`, but without the universe bump. Use
`Dynamic.mk` to inject a value into `Dynamic` from another type, and `Dynamic.get?` to extract a
value from `Dynamic` if it has some expected type.
 -/
Dynamic : Type
-- Init.Data.Order.Classes
Std.LawfulOrderInf.mk : ∀ {α : Type u} [inst : Min α] [inst_1 : LE α], (∀ (a b c : α), a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c) → Std.LawfulOrderInf α
-- Mathlib.Algebra.Star.Unitary
Unitary.mem_iff_star_mul_self : ∀ {R : Type u_1} [inst : CommMonoid R] [inst_1 : StarMul R] {U : R}, U ∈ unitary R ↔ star U * U = 1
-- Mathlib.Topology.Sets.BaseChangeNhds
TopologicalSpace.Compacts.baseChangeOpenNhds_mono : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K L : TopologicalSpace.Compacts α} (h : K ⟶ L),
  Monotone (TopologicalSpace.Compacts.baseChangeOpenNhds h)
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.Integrable.convergenceR.congr_simp : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I I_1 : BoxIntegral.Box ι} (e_I : I = I_1)
  [inst_4 : Fintype ι] {l l_1 : BoxIntegral.IntegrationParams} (e_l : l = l_1) {f f_1 : (ι → ℝ) → E} (e_f : f = f_1)
  {vol vol_1 : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} (e_vol : vol = vol_1) (h : BoxIntegral.Integrable I l f vol)
  (ε ε_1 : ℝ),
  ε = ε_1 →
    ∀ (a a_1 : NNReal), a = a_1 → ∀ (a_2 a_3 : ι → ℝ), a_2 = a_3 → h.convergenceR ε a a_2 = ⋯.convergenceR ε_1 a_1 a_3
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.mem_valueGroup_iff_of_comm' : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : CommGroupWithZero B] (f : A →*₀ B) {y : Bˣ},
  y ∈ f.valueGroup ↔ ∃ a, f a ≠ 0 ∧ ∃ x, f x ≠ 0 ∧ f a * ↑y = f x
-- Mathlib.Topology.UniformSpace.Basic
instUniformSpaceEmpty : UniformSpace Empty
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀),
  AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso f 𝒰 i =
    CategoryTheory.Limits.pullbackSymmetry f (𝒰.affineRefinement.openCover.f i) ≪≫
      (CategoryTheory.Limits.pullbackRightPullbackFstIso (𝒰.f i.fst) f
            (((fun i => ((fun j => (𝒰.X j).affineCover) i).toPreZeroHypercover) i.fst).f i.snd)).symm ≪≫
        CategoryTheory.Limits.pullbackSymmetry
            (((fun i => ((fun j => (𝒰.X j).affineCover) i).toPreZeroHypercover) i.fst).f i.snd)
            (CategoryTheory.Limits.pullback.fst (𝒰.f i.fst) f) ≪≫
          CategoryTheory.asIso
            (CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.pullback.fst (𝒰.f i.fst) f)
              (((fun i => ((fun j => (𝒰.X j).affineCover) i).toPreZeroHypercover) i.fst).f i.snd)
              (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i.fst) ((𝒰.X i.fst).affineCover.f i.snd)
              (CategoryTheory.Limits.pullbackSymmetry (𝒰.f i.fst) f).hom
              (CategoryTheory.CategoryStruct.id (𝒰.affineRefinement.openCover.X i))
              (CategoryTheory.CategoryStruct.id (𝒰.X i.fst)) ⋯ ⋯)
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.eraseMany : {α : Type u} →
  {cmp : α → α → Ordering} → {ρ : Type u_1} → [ForIn Id ρ α] → Std.TreeSet.Raw α cmp → ρ → Std.TreeSet.Raw α cmp
-- Mathlib.Algebra.Group.Subgroup.Defs
HasMemOrNegMem.mk : ∀ {S : Type u_3} {G : Type u_4} [inst : Neg G] [inst_1 : SetLike S G] {s : S},
  (∀ (a : G), a ∈ s ∨ -a ∈ s) → HasMemOrNegMem s
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- If the chromatic number of `G` is `n + 1`, then `G` is colorable in no fewer than `n + 1`
colors.  -/
SimpleGraph.chromaticNumber_eq_iff_colorable_not_colorable : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ}, G.chromaticNumber = ↑n + 1 ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
-- Mathlib.Algebra.GradedMonoid
SetLike.GradeZero.coe_one : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Monoid R] [inst_2 : AddMonoid ι]
  {A : ι → S} [inst_3 : SetLike.GradedMonoid A], ↑1 = 1
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
/-- Assuming `HasExactColimitsOfShape J C`, this lemma rephrases the exactness
of the functor `colim : (J ⥤ C) ⥤ C` by saying that if `S : ShortComplex (J ⥤ C)`
is exact, then the short complex obtained by taking the colimits is exact,
where we allow the replacement of the chosen colimit cocones of the
colimit API by arbitrary colimit cocones.  -/
CategoryTheory.Limits.colim.exact_mapShortComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.HasExactColimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)},
  S.Exact →
    ∀ {c₁ : CategoryTheory.Limits.Cocone S.X₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁)
      {c₂ : CategoryTheory.Limits.Cocone S.X₂} (hc₂ : CategoryTheory.Limits.IsColimit c₂)
      {c₃ : CategoryTheory.Limits.Cocone S.X₃} (hc₃ : CategoryTheory.Limits.IsColimit c₃) (f : c₁.pt ⟶ c₂.pt)
      (g : c₂.pt ⟶ c₃.pt)
      (hf :
        ∀ (j : J),
          CategoryTheory.CategoryStruct.comp (c₁.ι.app j) f =
            CategoryTheory.CategoryStruct.comp (S.f.app j) (c₂.ι.app j))
      (hg :
        ∀ (j : J),
          CategoryTheory.CategoryStruct.comp (c₂.ι.app j) g =
            CategoryTheory.CategoryStruct.comp (S.g.app j) (c₃.ι.app j)),
      (CategoryTheory.Limits.colim.mapShortComplex S hc₁ c₂ c₃ f g hf hg).Exact
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.equivMapOfInjective_toFun_coe : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (K : LieSubalgebra R L) (hf : Function.Injective ⇑f)
  (a : ↑↑K.toSubmodule), ↑((LieSubalgebra.equivMapOfInjective f K hf) a) = f ↑a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).size = if t.contains k = true then t.size else t.size + 1
-- Mathlib.Analysis.InnerProductSpace.CanonicalTensor
/-- Representation of the canonical covariant tensor in terms of an orthonormal basis.  -/
InnerProductSpace.canonicalCovariantTensor_eq_sum : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {ι : Type u_2} [inst_3 : Fintype ι] (v : OrthonormalBasis ι ℝ E),
  InnerProductSpace.canonicalCovariantTensor E = ∑ i, v i ⊗ₜ[ℝ] v i
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.instIsLocallyNoetherianToScheme : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} [AlgebraicGeometry.IsLocallyNoetherian X],
  AlgebraicGeometry.IsLocallyNoetherian ↑U
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.sinZeta.eq_1 : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.sinZeta a s = HurwitzZeta.completedSinZeta a s / (s + 1).Gammaℝ
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
extDerivWithin_apply : ∀ {𝕜 : 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] {n : ℕ}
  {ω : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E},
  DifferentiableWithinAt 𝕜 ω s x →
    UniqueDiffWithinAt 𝕜 s x →
      ∀ (v : Fin (n + 1) → E),
        (extDerivWithin ω s x) v = ∑ i, (-1) ^ ↑i • (fderivWithin 𝕜 (fun x => (ω x) (i.removeNth v)) s x) (v i)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roo_eq_cons_iff : ∀ {xs : List ℤ} {m n a : ℤ}, (m<...n).toList = a :: xs ↔ m + 1 = a ∧ m + 1 < n ∧ ((m + 1)<...n).toList = xs
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.tan_add_pi : ∀ (θ : Real.Angle), (θ + ↑Real.pi).tan = θ.tan
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.mul : ℝ → ℝ → ℝ
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.ker_toNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f],
  AlgebraicGeometry.Scheme.Hom.ker (AlgebraicGeometry.Scheme.Hom.toNormalization f) = ⊥
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.measure_Iio_pos : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X] {m : MeasurableSpace X}
  (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [NoMinOrder X] (a : X), 0 < μ (Set.Iio a)
-- Mathlib.CategoryTheory.Grothendieck
/-- Let `F, F' : C ⥤ Cat` be functor, `G : D ≌ C` an equivalence and `α : F ⟶ F'` a natural
transformation.

Left-whiskering `α` by `G` and then taking the Grothendieck construction is, up to isomorphism,
the same as taking the Grothendieck construction of `α` and using the equivalences `pre F G`
and `pre F' G` to match the expected type:

```
Grothendieck (G.functor ⋙ F) ≌ Grothendieck F ⥤ Grothendieck F' ≌ Grothendieck (G.functor ⋙ F')
```
 -/
CategoryTheory.Grothendieck.mapWhiskerLeftIsoConjPreMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} D] →
        {F F' : CategoryTheory.Functor C CategoryTheory.Cat} →
          (G : D ≌ C) →
            (α : F ⟶ F') →
              CategoryTheory.Grothendieck.map (G.functor.whiskerLeft α) ≅
                (CategoryTheory.Grothendieck.preEquivalence F G).functor.comp
                  ((CategoryTheory.Grothendieck.map α).comp (CategoryTheory.Grothendieck.preEquivalence F' G).inverse)
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.instIsAffine : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine S],
  AlgebraicGeometry.IsAffine (AlgebraicGeometry.AffineSpace n S)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
ContinuousAt.logb : ∀ {α : Type u_1} {b : ℝ} [inst : TopologicalSpace α] {f : α → ℝ} {a : α},
  ContinuousAt f a → f a ≠ 0 → ContinuousAt (fun x => Real.logb b (f x)) a
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- "Semicontinuity of the `lp` norm": If all sufficiently large elements of a sequence in `lp E p`
have `lp` norm `≤ C`, then the pointwise limit, if it exists, also has `lp` norm `≤ C`.  -/
lp.norm_le_of_tendsto : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {ι : Type u_5}
  {l : Filter ι} [l.NeBot] [_i : Fact (1 ≤ p)] {C : ℝ} {F : ι → ↥(lp E p)},
  (∀ᶠ (k : ι) in l, ‖F k‖ ≤ C) → ∀ {f : ↥(lp E p)}, Filter.Tendsto (id fun i => ↑(F i)) l (nhds ↑f) → ‖f‖ ≤ C
-- Lean.Parser.Term
Lean.Parser.Term.funStrictImplicitBinder : Lean.Parser.Parser
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.eq_top_iff' : ∀ {M : Type u_1} [inst : Mul M] (S : Subsemigroup M), S = ⊤ ↔ ∀ (x : M), x ∈ S
-- Mathlib.Order.Filter.ENNReal
ENNReal.limsup_eq_zero_iff : ∀ {α : Type u_1} {f : Filter α} [CountableInterFilter f] {u : α → ENNReal}, Filter.limsup u f = 0 ↔ u =ᶠ[f] 0
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedLT_iff_strictMono_get`. -/
List.SortedLT.strictMono_get : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedLT → StrictMono l.get
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBumpBase.mk.inj : ∀ {E : Type u_3} {inst : NormedAddCommGroup E} {inst_1 : NormedSpace ℝ E} {toFun : ℝ → E → ℝ}
  {mem_Icc : ∀ (R : ℝ) (x : E), toFun R x ∈ Set.Icc 0 1} {symmetric : ∀ (R : ℝ) (x : E), toFun R (-x) = toFun R x}
  {smooth : ContDiffOn ℝ (↑⊤) (Function.uncurry toFun) (Set.Ioi 1 ×ˢ Set.univ)}
  {eq_one : ∀ (R : ℝ), 1 < R → ∀ (x : E), ‖x‖ ≤ 1 → toFun R x = 1}
  {support : ∀ (R : ℝ), 1 < R → Function.support (toFun R) = Metric.ball 0 R} {toFun_1 : ℝ → E → ℝ}
  {mem_Icc_1 : ∀ (R : ℝ) (x : E), toFun_1 R x ∈ Set.Icc 0 1}
  {symmetric_1 : ∀ (R : ℝ) (x : E), toFun_1 R (-x) = toFun_1 R x}
  {smooth_1 : ContDiffOn ℝ (↑⊤) (Function.uncurry toFun_1) (Set.Ioi 1 ×ˢ Set.univ)}
  {eq_one_1 : ∀ (R : ℝ), 1 < R → ∀ (x : E), ‖x‖ ≤ 1 → toFun_1 R x = 1}
  {support_1 : ∀ (R : ℝ), 1 < R → Function.support (toFun_1 R) = Metric.ball 0 R},
  { toFun := toFun, mem_Icc := mem_Icc, symmetric := symmetric, smooth := smooth, eq_one := eq_one,
        support := support } =
      { toFun := toFun_1, mem_Icc := mem_Icc_1, symmetric := symmetric_1, smooth := smooth_1, eq_one := eq_one_1,
        support := support_1 } →
    toFun = toFun_1
-- Aesop.Tree.Data
Aesop.GoalUnsafe.mk : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Aesop.GoalUnsafe
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_mul_cancel_of_imp : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, (b = 0 → a = 0) → a / b * b = a
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.toProd_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  Function.Surjective ⇑AddMonoid.Coprod.toProd
-- Mathlib.NumberTheory.ClassNumber.Finite
/-- The main theorem: the class group of an integral closure `S` of `R` in a
finite extension `L` of `K = Frac(R)` is finite if there is an admissible
absolute value.

See also `ClassGroup.fintypeOfAdmissibleOfAlgebraic` where `L` is an
algebraic extension of `R`, that includes some extra assumptions.
 -/
ClassGroup.fintypeOfAdmissibleOfFinite : {R : Type u_1} →
  {S : Type u_2} →
    (K : Type u_3) →
      (L : Type u_4) →
        [inst : EuclideanDomain R] →
          [inst_1 : CommRing S] →
            [inst_2 : IsDomain S] →
              [inst_3 : Field K] →
                [inst_4 : Field L] →
                  [inst_5 : Algebra R K] →
                    [IsFractionRing R K] →
                      [inst_7 : Algebra K L] →
                        [FiniteDimensional K L] →
                          [Algebra.IsSeparable K L] →
                            [algRL : Algebra R L] →
                              [IsScalarTower R K L] →
                                [inst_11 : Algebra R S] →
                                  [inst_12 : Algebra S L] →
                                    [ist : IsScalarTower R S L] →
                                      {abv : AbsoluteValue R ℤ} →
                                        abv.IsAdmissible →
                                          [Infinite R] →
                                            [DecidableEq R] → [IsIntegralClosure S R L] → Fintype (ClassGroup S)
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
AnalyticOn.im_ofReal : ∀ {f : ℂ → ℂ} {s : Set ℝ}, AnalyticOn ℂ f (Complex.ofReal '' s) → AnalyticOn ℝ (fun x => (f ↑x).im) s
-- Mathlib.Algebra.Polynomial.Expand
/-- Expand the polynomial by a factor of p, so `∑ aₙ xⁿ` becomes `∑ aₙ xⁿᵖ`.  -/
Polynomial.expand : (R : Type u) → [inst : CommSemiring R] → ℕ → Polynomial R →ₐ[R] Polynomial R
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.image_preimage_le : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj ((TopologicalSpace.Opens.map f.base).obj U) ≤ U
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbit_eq_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {a b : α},
  MulAction.orbit G a = MulAction.orbit G b ↔ a ∈ MulAction.orbit G b
-- Mathlib.Analysis.Meromorphic.Basic
/-- `MeromorphicOn` is invariant under translation, special case where the set is a closed ball.  -/
MeromorphicOn.meromorphicOn_closedBall_comp_sub_const_iff_meromorphicOn_closedBall : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {R : ℝ},
  MeromorphicOn (f ∘ fun x => x - c) (Metric.closedBall c R) ↔ MeromorphicOn f (Metric.closedBall 0 R)
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.Hom.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {G : CategoryTheory.Comonad C} {A B : G.Coalgebra}
  {x y : A.Hom B}, x.f = y.f → x = y
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_insertMany_list_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)}, (t.insertMany l).size ≤ t.size + l.length
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_eq_subtypeClosure : ∀ {α : Type u_2} (M : Matroid α) (X : Set α), M.closure X = ↑(M.subtypeClosure ⟨X ∩ M.E, ⋯⟩)
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicAt.const_smul` -/
MeromorphicAt.fun_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_4} [inst_3 : NormedRing R] [inst_4 : Module R E] [IsBoundedSMul R E]
  [SMulCommClass 𝕜 R E] {x : 𝕜} {f : 𝕜 → E}, MeromorphicAt f x → ∀ (c : R), MeromorphicAt (fun i => c • f i) x
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The morphism in the fiber over the domain.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.fiber : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} →
      {X Y : F.CoGrothendieck} → (self : X.Hom Y) → X.fiber ⟶ (F.map self.base.op.toLoc).toFunctor.obj Y.fiber
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
hasSum_pnat_iff : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℕ → G} {a : G},
  HasSum (fun x => f ↑x) a ↔ HasSum f (a + f 0)
-- Init.Data.AC
Lean.Data.AC.Context.evalList_append : ∀ {α : Sort u_1} (ctx : Lean.Data.AC.Context α) (l r : List ℕ),
  l ≠ [] →
    r ≠ [] →
      Lean.Data.AC.evalList α ctx (l.append r) = ctx.op (Lean.Data.AC.evalList α ctx l) (Lean.Data.AC.evalList α ctx r)