mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.CompactOpen
/-- The coevaluation map `Y → C(X, Y × X)` sending a point `x : Y` to the continuous function
on `X` sending `y` to `(x, y)`.  -/
ContinuousMap.coev : (X : Type u_2) → (Y : Type u_3) → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → Y → C(X, Y × X)
-- Mathlib.RingTheory.ClassGroup.Basic
FractionalIdeal.unitsMulEquivSubmodule.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P], FractionalIdeal.unitsMulEquivSubmodule = FractionalIdeal.unitsMulEquivSubmodule
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If `dist (f n) (f (n+1))` is bounded by `(C / 2) / 2^n`, then the distance from
`f n` to the limit of `f` is bounded above by `C / 2^n`.  -/
dist_le_of_le_geometric_two_of_tendsto : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {C : ℝ} {f : ℕ → α},
  (∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n) →
    ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → ∀ (n : ℕ), dist (f n) a ≤ C / 2 ^ n
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.liftMonoid_symm_coe : ∀ {α : Type u} {R : Type u_2} [inst : Monoid α] [inst_1 : Ring R] (f : FreeAbelianGroup α →+* R),
  ⇑(FreeAbelianGroup.liftMonoid.symm f) = FreeAbelianGroup.lift.symm ↑f
-- Mathlib.Algebra.Order.UpperLower
IsLowerSet.vadd_subset : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {s : Set α} {x : α},
  IsLowerSet s → x ≤ 0 → x +ᵥ s ⊆ s
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.ofList_cons : ∀ {α : Type u_1} (x : α) (xs : List α), FreeMonoid.ofList (x :: xs) = FreeMonoid.of x * FreeMonoid.ofList xs
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.C_Ψ₂Sq : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), Polynomial.C W.Ψ₂Sq = W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.ExplorationStep.lt.inj : ∀ {α : Type u} {β : α → Type v} {inst : Ord α} {k : α → Ordering} {a : α} {a_1 : k a = Ordering.lt} {a_2 : β a}
  {a_3 : List ((a : α) × β a)} {a_4 : α} {a_5 : k a_4 = Ordering.lt} {a_6 : β a_4} {a_7 : List ((a : α) × β a)},
  Std.DTreeMap.Internal.Impl.ExplorationStep.lt a a_1 a_2 a_3 =
      Std.DTreeMap.Internal.Impl.ExplorationStep.lt a_4 a_5 a_6 a_7 →
    a = a_4 ∧ a_2 ≍ a_6 ∧ a_3 = a_7
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangent.radius_le_dist_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {as : AffineSubspace ℝ P},
  s.IsTangent as → ∀ {p : P}, p ∈ as → s.radius ≤ dist p s.center
-- Lean.Structure
/-- Auxiliary state for structures defined in the current module.  -/
_private.Lean.Structure.0.Lean.StructureState : Type
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_mul_mul_comm'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommMonObj M] {Z : C}
  (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ M M M M)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)
-- Mathlib.Data.Sigma.Order
/-- Disjoint sum of orders. `⟨i, a⟩ ≤ ⟨j, b⟩` iff `i = j` and `a ≤ b`.  -/
Sigma.LE : {ι : Type u_1} → {α : ι → Type u_2} → [(i : ι) → LE (α i)] → (i : ι) × α i → (i : ι) × α i → Prop
-- Lean.Expr
/-- The constructor name for the given expression. This is used for debugging purposes.  -/
Lean.Expr.ctorName : Lean.Expr → String
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.extension_unique : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H]
  [inst_2 : T0Space H] [inst_3 : CompleteSpace H] (f : NormedAddGroupHom G H)
  {g : NormedAddGroupHom (UniformSpace.Completion G) H}, (∀ (v : G), f v = g ↑v) → f.extension = g
-- Mathlib.NumberTheory.Dioph
_private.Mathlib.NumberTheory.Dioph.0.«term_::ₒ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instCoeTC : {α : Type u} → CoeTC α (WithOne α)
-- Mathlib.Order.RelIso.Basic
/-- Given relation isomorphisms `r₁ ≃r s₁` and `r₂ ≃r s₂`, construct a relation isomorphism for the
lexicographic orders on the product.
 -/
RelIso.prodLexCongr : {α₁ : Type u_5} →
  {α₂ : Type u_6} →
    {β₁ : Type u_7} →
      {β₂ : Type u_8} →
        {r₁ : α₁ → α₁ → Prop} →
          {r₂ : α₂ → α₂ → Prop} →
            {s₁ : β₁ → β₁ → Prop} → {s₂ : β₂ → β₂ → Prop} → r₁ ≃r s₁ → r₂ ≃r s₂ → Prod.Lex r₁ r₂ ≃r Prod.Lex s₁ s₂
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.addSEvalprocBuiltinAttr : Lean.Name → Bool → Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc → IO Unit
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} [inst_3 : F.IsWellOrderContinuous] {j : J} (hj : Order.IsSuccLimit j)
  (s : ↑(⋯.functor.op.comp (CategoryTheory.HasLiftingProperty.transfiniteComposition.sqFunctor c p f g)).sections)
  (i : J) (hi : i < j) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom hj s) h) =
    CategoryTheory.CategoryStruct.comp (↑s (Opposite.op ⟨i, hi⟩)).f' h
-- Mathlib.MeasureTheory.Measure.Prod
/-- A measurable set `s` has `μ.prod ν` measure zero, where `ν` is an s-finite measure,
if and only if `μ`-a.e. section `{y | (x, y) ∈ s}` of `s` have `ν` measure zero.

See `measure_ae_null_of_prod_null` for the forward implication without the measurability assumption
and `measure_prod_null_of_ae_null` for the reverse implication without the s-finiteness assumption.

Note: the assumption `hs` cannot be dropped. For a counterexample, see
Walter Rudin *Real and Complex Analysis*, example (c) in section 8.9.  -/
MeasureTheory.Measure.measure_prod_null : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {s : Set (α × β)},
  MeasurableSet s → ((μ.prod ν) s = 0 ↔ (fun x => ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0)
-- Mathlib.CategoryTheory.Category.Cat.Op
CategoryTheory.Cat.opEquivalence_inverse : CategoryTheory.Cat.opEquivalence.inverse = CategoryTheory.Cat.opFunctor
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- If `g = f * h` is a Weierstrass factorization, then there is a
natural isomorphism `A[X] / (f) ≃ₐ[A] A⟦X⟧ / (g)`.  -/
PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient : {A : Type u_1} →
  [inst : CommRing A] →
    {g : PowerSeries A} →
      {f : Polynomial A} →
        {h : PowerSeries A} →
          {I : Ideal A} →
            g.IsWeierstrassFactorizationAt f h I →
              [IsAdicComplete I A] → (Polynomial A ⧸ Ideal.span {f}) ≃ₐ[A] PowerSeries A ⧸ Ideal.span {g}
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativePreorder.vle_iff_le : ∀ {R : Type u_1} {inst : Semiring R} {inst_1 : ValuativeRel R} {inst_2 : Preorder R} [self : ValuativePreorder R]
  (x y : R), x ≤ᵥ y ↔ x ≤ y
-- Init.Data.Nat.Power2.Lemmas
_private.Init.Data.Nat.Power2.Lemmas.0.Nat.isPowerOfTwo.eq_1 : ∀ (n : ℕ), n.isPowerOfTwo = ∃ k, n = 2 ^ k
-- Lean.Data.Lsp.Utf16
/-- Computes the UTF-16 offset of the `n`-th Unicode codepoint
in the substring of `s` starting at UTF-8 offset `off`.
Yes, this is actually useful. -/
Lean.String.codepointPosToUtf16PosFrom : String → ℕ → String.Pos.Raw → ℕ
-- Mathlib.Topology.EMetricSpace.Basic
/-- Expressing uniform convergence using `edist`.  -/
EMetric.tendstoUniformly_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] {ι : Type u_2} {F : ι → β → α} {f : β → α} {p : Filter ι},
  TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), edist (f x) (F n x) < ε
-- Mathlib.Algebra.Ring.TransferInstance
/-- Transfer `NonAssocRing` across an `Equiv`  -/
Equiv.nonAssocRing : {α : Type u_1} → {β : Type u_2} → α ≃ β → [NonAssocRing β] → NonAssocRing α
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isCyclic_multiplicative : ∀ {α : Type u_1} [inst : AddGroup α] [IsAddCyclic α], IsCyclic (Multiplicative α)
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.inl_desc_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr) {W : C} (h : X ⟶ W)
  (k : Y ⟶ W) (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) {Q : C},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight inl Q)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (hP.desc h k w) Q) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight h Q
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_alter_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) {hc : k ∈ m.alter k f},
  (m.alter k f).get k hc = (f (m.get? k)).get ⋯
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Set.natCard_vadd_set : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (a : G) (s : Set α),
  Nat.card ↑(a +ᵥ s) = Nat.card ↑s
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.codeBlockExpandersForUnsafe : Lean.Ident →
  Lean.Elab.TermElabM
    (Array
      (Lean.Name ×
        (Lean.StrLit →
          StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))))
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreOfNat : Lean.Expr →
  Lean.Expr →
    ℕ →
      Lean.Meta.Grind.Arith.Linear.LinExpr →
        Lean.Meta.Grind.Arith.Linear.LinExpr → Lean.Meta.Grind.Arith.Linear.EqCnstrProof
-- Mathlib.CategoryTheory.Comma.Arrow
/-- The equivalence of categories `Arrow C ≌ Arrow D` induced by an equivalence `C ≌ D`.  -/
CategoryTheory.Functor.mapArrowEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (C ≌ D) → (CategoryTheory.Arrow C ≌ CategoryTheory.Arrow D)
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.toLieSubalgebra_toSubmodule : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  (LieIdeal.toLieSubalgebra R L I).toSubmodule = ↑I
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.d₂_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁ : I₁) {i₂ i₂' : I₂},
  c₂.Rel i₂ i₂' →
    ∀ (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂),
      K.d₂ c₁₂ i₁ i₂ i₁₂ =
        c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.ιTotal c₁₂ i₁ i₂' i₁₂ h')
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.isBasis_closure : ∀ {α : Type u_2} {M : Matroid α} {I : Set α}, M.Indep I → M.IsBasis I (M.closure I)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- If `κ` is a suitable cardinal for the small object argument for `I : MorphismProperty C`,
then the class `I.rlp.llp` is exactly the class of morphisms that are retracts
of transfinite compositions (of shape `κ.ord.ToType`) of pushouts of coproducts
of maps in `I`.  -/
CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [I.IsCardinalForSmallObjectArgument κ],
  I.rlp.llp =
    ((CategoryTheory.MorphismProperty.coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape
        κ.ord.ToType).retracts
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.reverse_surjective : ∀ {T : Type u_1} {N : Type u_2}, Function.Surjective ContextFreeRule.reverse
-- Mathlib.Data.Finset.NAry
Finset.image₂_image_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {s : Finset α} {t : Finset β}
  [inst_1 : DecidableEq δ] (f : α → γ → δ) (g : β → γ),
  Finset.image₂ f s (Finset.image g t) = Finset.image₂ (fun a b => f a (g b)) s t
-- Lean.Message
/-- Append the given list of messages with the given separator.  -/
Lean.MessageData.joinSep : List Lean.MessageData → Lean.MessageData → Lean.MessageData
-- Mathlib.Data.ENNReal.Real
ENNReal.toNNReal_top_mul : ∀ (a : ENNReal), (⊤ * a).toNNReal = 0
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.topologicalSpace : {ι : Type u_1} →
  (R : ι → Type u_2) →
    (A : (i : ι) → Set (R i)) →
      (𝓕 : Filter ι) →
        [(i : ι) → TopologicalSpace (R i)] → TopologicalSpace (RestrictedProduct (fun i => R i) (fun i => A i) 𝓕)
-- Mathlib.Data.PEquiv
PEquiv.mem_single_iff : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] (a₁ a₂ : α) (b₁ b₂ : β),
  b₁ ∈ (PEquiv.single a₂ b₂) a₁ ↔ a₁ = a₂ ∧ b₁ = b₂
-- Mathlib.Order.Interval.Set.Image
AntitoneOn.image_Icc_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
  AntitoneOn f (Set.Icc a b) → f '' Set.Icc a b ⊆ Set.Icc (f b) (f a)
-- Mathlib.Topology.DiscreteSubset
/-- The union of finitely many discrete closed subsets is discrete.  -/
discreteTopology_iUnion_finite : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_3} [Finite ι] {s : ι → Set X},
  (∀ (i : ι), DiscreteTopology ↑(s i)) → (∀ (i : ι), IsClosed (s i)) → DiscreteTopology ↑(⋃ i, s i)
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourierIntegral_continuousLinearMap_apply' : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type u_5} {V : Type u_6} {W : Type u_7}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : MeasurableSpace V] [BorelSpace V]
  [inst_6 : NormedAddCommGroup W] [inst_7 : NormedSpace ℝ W] {μ : MeasureTheory.Measure V} {L : V →L[ℝ] W →L[ℝ] ℝ}
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace ℝ F] {f : V → F →L[ℝ] E} {a : F} {w : W},
  MeasureTheory.Integrable f μ →
    (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) f w) a =
      VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun x => (f x) a) w
-- Mathlib.Data.ZMod.Basic
/-- The coercions are respectively `Nat.cast` and `ZMod.cast`.  -/
ZMod.natCast_comp_val : ∀ {n : ℕ} (R : Type u_1) [inst : Ring R] [NeZero n], Nat.cast ∘ ZMod.val = ZMod.cast
-- Mathlib.Analysis.ConstantSpeed
hasConstantSpeedOnWith_zero_iff : ∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ},
  HasConstantSpeedOnWith f s 0 ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.ofNat_ctorIdx : ∀ (x : Std.Tactic.BVDecide.LRAT.Internal.Assignment), Std.Tactic.BVDecide.LRAT.Internal.Assignment.ofNat x.ctorIdx = x
-- Mathlib.Algebra.Ring.CharZero
RingHom.charZero : ∀ {R : Type u_2} {S : Type u_3} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (ϕ : R →+* S) [CharZero S],
  CharZero R
-- Init.Data.Range.Lemmas
_private.Init.Data.Range.Lemmas.0.Std.Legacy.Range.forIn'.loop.eq_1 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] (range : Std.Legacy.Range)
  (f : (i : ℕ) → i ∈ range → β → m (ForInStep β)) (b : β) (i : ℕ) (hs : (i - range.start) % range.step = 0)
  (hl : range.start ≤ i),
  Std.Legacy.Range.forIn'.loop✝ range f b i hs hl =
    if h : i < range.stop then do
      let __do_lift ← f i ⋯ b
      match __do_lift with
        | ForInStep.done b => pure b
        | ForInStep.yield b =>
          have this := ⋯;
          Std.Legacy.Range.forIn'.loop✝ range f b (i + range.step) ⋯ ⋯
    else pure b
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.map_lowerCentralSeries_le : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (k : ℕ) {M₂ : Type w₁}
  [inst_6 : AddCommGroup M₂] [inst_7 : Module R M₂] [inst_8 : LieRingModule L M₂] [LieModule R L M₂] [LieModule R L M]
  (f : M →ₗ⁅R,L⁆ M₂), LieSubmodule.map f (LieModule.lowerCentralSeries R L M k) ≤ LieModule.lowerCentralSeries R L M₂ k
-- Mathlib.CategoryTheory.Bicategory.Free
_private.Mathlib.CategoryTheory.Bicategory.Free.0.CategoryTheory.FreeBicategory.«term𝟙» : Lean.ParserDescr
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.toArray_eq_empty_iff : ∀ {α : Type u} {r : Std.Roo α} [LE α] [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α], r.toArray = #[] ↔ ∀ (a : α), Std.PRange.succ? r.lower = some a → ¬a < r.upper
-- Mathlib.Analysis.Complex.ReImTopology
Complex.closure_setOfPred_lt_re : ∀ (a : ℝ), closure {z | a < z.re} = {z | a ≤ z.re}
-- Mathlib.NumberTheory.Real.Irrational
Irrational.add_ratCast : ∀ (q : ℚ) {x : ℝ}, Irrational x → Irrational (x + ↑q)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.zero_eq_bot : ∀ {α : Type u_1}, 0 = ⊥
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsProper.instCompScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsProper f]
  [AlgebraicGeometry.IsProper g], AlgebraicGeometry.IsProper (CategoryTheory.CategoryStruct.comp f g)
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.EvalConfigItemView.mk.sizeOf_spec : ∀ (omitFields : Array (Lean.Ident × Lean.Name)) (handlers : Array Lean.Elab.ConfigEval.EvalConfigItemHandler),
  sizeOf { omitFields := omitFields, handlers := handlers } = 1 + sizeOf omitFields + sizeOf handlers
-- Mathlib.Analysis.Complex.Exponential
Real.expMonoidHom_apply : ∀ (x : Multiplicative ℝ), Real.expMonoidHom x = Real.exp (Multiplicative.toAdd x)
-- Mathlib.Order.Std
/-- The `Max` instance of the order. This can always be automatically derived.  -/
LinearOrder.OfStdArgs.max : {α : Type u_1} →
  (self : LinearOrder.OfStdArgs α) →
    let this := self.le;
    let this := self.decidableLE;
    Max α
-- Mathlib.FieldTheory.Perfect
Polynomial.roots_X_pow_char_pow_sub_C_pow : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p n : ℕ} [inst_2 : ExpChar R p] [inst_3 : PerfectRing R p]
  {y : R} {m : ℕ},
  ((Polynomial.X ^ p ^ n - Polynomial.C y) ^ m).roots = (m * p ^ n) • {(iterateFrobeniusEquiv R p n).symm y}
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.mk.congr_simp : ∀ {d : ℤ} (x x_1 : ℤ) (e_x : x = x_1) (y y_1 : ℤ) (e_y : y = y_1) (prop : x ^ 2 - d * y ^ 2 = 1),
  Pell.Solution₁.mk x y prop = Pell.Solution₁.mk x_1 y_1 ⋯
-- Mathlib.CategoryTheory.Action.Monoidal
Action.diagonalSuccIsoTensorTrivial.eq_2 : ∀ (G : Type u) [inst : Group G] (n : ℕ),
  Action.diagonalSuccIsoTensorTrivial G n.succ =
    Action.diagonalSuccIsoTensorDiagonal G (n + 1) ≪≫
      CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.Iso.refl (Action.leftRegular G))
          (Action.diagonalSuccIsoTensorTrivial G n) ≪≫
        Action.leftRegularTensorIso G
            (CategoryTheory.MonoidalCategoryStruct.tensorObj (Action.leftRegular G) (Action.trivial G (Fin n → G))) ≪≫
          CategoryTheory.MonoidalCategory.tensorIso (CategoryTheory.Iso.refl (Action.leftRegular G))
            (Action.mkIso (Fin.insertNthEquiv (fun x => G) 0).toIso ⋯)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.mk_singleton : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : T1Space α] {x : α}, { carrier := {x}, isClosed' := ⋯ } = {x}
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_indicatorConst : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {s : Set α},
  (∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) →
    MeasureTheory.FinMeasAdditive μ T →
      ∀ (hs : MeasurableSet s) (hμs : μ s < ⊤) (x : E),
        MeasureTheory.L1.SimpleFunc.setToL1S T (MeasureTheory.Lp.simpleFunc.indicatorConst 1 hs ⋯ x) = (T s) x
-- Mathlib.Data.Set.Subsingleton
/-- A type with a set `s` whose `coe_sort` is a nontrivial type is nontrivial.
For the corresponding result for `Subtype`, see `Subtype.nontrivial_iff_exists_ne`.  -/
Set.nontrivial_of_nontrivial_coe : ∀ {α : Type u} {s : Set α}, Nontrivial ↑s → Nontrivial α
-- Std.Sync.Notify
/-- Creates a selector that waits for notifications
 -/
Std.Notify.selector : Std.Notify → Std.Async.Selector Unit
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- **Alias** of `neg_apply`. -/
SlashInvariantForm.neg_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Neg β}
  {inst_2 : Neg F} [self : IsNegApply F α β] (f : F) (x : α), (-f) x = -f x
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.closure_iUnion : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {ι : Sort u_2} (s : ι → Set R),
  NonUnitalSubsemiring.closure (⋃ i, s i) = ⨆ i, NonUnitalSubsemiring.closure (s i)
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Alt : Type
-- Mathlib.Analysis.Complex.Basic
RCLike.complexRingEquiv_symm_apply : ∀ {𝕜 : Type u_2} [inst : RCLike 𝕜] (h : RCLike.im RCLike.I = 1) (x : ℂ),
  (RCLike.complexRingEquiv h).symm x = ↑x.re + ↑x.im * RCLike.I
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.insertMany_append : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {l₁ l₂ : List ((a : α) × β a)}, m.insertMany (l₁ ++ l₂) = (m.insertMany l₁).insertMany l₂
-- Mathlib.Analysis.Normed.Module.DoubleDual
/-- The inclusion of a normed space in its double strong dual is an isometry onto its image.  -/
NormedSpace.inclusionInDoubleDualLi : (𝕜 : Type v) →
  [inst : RCLike 𝕜] →
    {E : Type u} →
      [inst_1 : SeminormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → E →ₗᵢ[𝕜] StrongDual 𝕜 (StrongDual 𝕜 E)
-- Lean.Parser.Basic
/-- `lookahead(p)` runs `p` and fails if `p` does, but it produces no parse nodes and rewinds the
position to the original state on success. So for example `lookahead("=>")` will ensure that the
next token is `"=>"`, without actually consuming this token.

This parser has arity 0 - it does not capture anything.  -/
Lean.Parser.lookahead : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Monoidal.Braided.PushoutObjObj
CategoryTheory.Functor.PushoutObjObj.flipTensor_inl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X₁ Y₁ X₂ Y₂ : C} {f₁ : X₁ ⟶ Y₁} {f₂ : X₂ ⟶ Y₂}
  (sq : (CategoryTheory.MonoidalCategory.curriedTensor C).PushoutObjObj f₁ f₂),
  sq.flipTensor.inl = CategoryTheory.CategoryStruct.comp (β_ Y₂ X₁).hom sq.inr