mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- A category has a terminal object if it has a limit over the empty diagram.
Use `hasTerminal_of_unique` to construct instances.
 -/
CategoryTheory.Limits.HasTerminal : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Prop
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.smul_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] {S : Type u_5}
  [inst_8 : DistribSMul S F] [inst_9 : SMulCommClass 𝕜₂ S F] [inst_10 : ContinuousConstSMul S F] {f : E →SWOT[σ] F}
  (c : S) (x : E), (c • f) x = c • f x
-- Lean.Parser
Lean.PrettyPrinter.Formatter.charLit.formatter : Lean.PrettyPrinter.Formatter
-- Batteries.Recycling.RBTree.Lemmas
/-- Asserts that `p` holds on all elements to the left of the hole.  -/
RBTree.RBNode.Path.AllL : {α : Type u_1} → (α → Prop) → RBTree.RBNode.Path α → Prop
-- Mathlib.AlgebraicTopology.MooreComplex
_private.Mathlib.AlgebraicTopology.MooreComplex.0.AlgebraicTopology.NormalizedMooreComplex.objX.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] (h : t.WF)
  {l : List α} {k k' fallback : α},
  compare k k' = Ordering.eq →
    k ∉ t →
      List.Pairwise (fun a b => ¬compare a b = Ordering.eq) l →
        k ∈ l → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)).getKeyD k' fallback = k
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousLinearEquiv.continuousAlternatingMapCongrLeft_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {E' : Type u_3} {F : Type u_4} {ι : Type u_6} [inst : NormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup E']
  [inst_5 : Module 𝕜 E'] [inst_6 : TopologicalSpace E'] [inst_7 : AddCommGroup F] [inst_8 : Module 𝕜 F]
  [inst_9 : TopologicalSpace F] [inst_10 : IsTopologicalAddGroup F] [inst_11 : ContinuousConstSMul 𝕜 F] (f : E ≃L[𝕜] E')
  (g : E [⋀^ι]→L[𝕜] F), f.continuousAlternatingMapCongrLeft g = g.compContinuousLinearMap ↑f.symm
-- Mathlib.Tactic.CrossRefAttribute
/-- The main parser for LMFDB identifiers: it accepts lower case words with `.` in between.
The words can also contain underscores and digits.  -/
Mathlib.CrossRef.lmfdbIdFn : Lean.Parser.ParserFn
-- Mathlib.Data.Ordmap.Invariants
Ordnode.node4L.eq_1 : ∀ {α : Type u_1} (x : Ordnode α) (x_1 x_2 : α) (x_3 : Ordnode α) (size : ℕ) (ml : Ordnode α) (y : α) (mr : Ordnode α),
  x.node4L x_1 (Ordnode.node size ml y mr) x_2 x_3 = (x.node' x_1 ml).node' y (mr.node' x_2 x_3)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.default_eq : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering}, default = ∅
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_insertManyIfNewUnit_list_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α},
  (m.insertManyIfNewUnit l).size ≤ m.size + l.length
-- Mathlib.Topology.Sober
IsGenericPoint.mem_open_set_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {S U : Set α},
  IsGenericPoint x S → IsOpen U → (x ∈ U ↔ (S ∩ U).Nonempty)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Functor.asEquivalence_counitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.IsEquivalence] (X : D),
  F.asEquivalence.counitIso.hom.app X = (F.objObjPreimageIso X).hom
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_filterMap : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl =
    Option.any (fun x => (f k x).isSome) (t.get? k)
-- Mathlib.CategoryTheory.Limits.IndYoneda
/-- Variant of `colimitHomIsoLimitYoneda` for contravariant `F`.  -/
CategoryTheory.Limits.colimitHomIsoLimitYoneda' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {I : Type v₁} →
      [inst_1 : CategoryTheory.Category.{v₂, v₁} I] →
        (F : CategoryTheory.Functor Iᵒᵖ C) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            [CategoryTheory.Limits.HasLimitsOfShape I (Type u₂)] →
              (A : C) →
                (CategoryTheory.Limits.colimit F ⟶ A) ≅
                  CategoryTheory.Limits.limit (F.rightOp.comp (CategoryTheory.yoneda.obj A))
-- Init.Data.List.Sublist
List.takeWhile_sublist : ∀ {α : Type u_1} {l : List α} (p : α → Bool), (List.takeWhile p l).Sublist l
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.ofNatCode.match_1.splitter : (motive : Bool → Bool → Sort u_1) →
  (x x_1 : Bool) →
    (Unit → motive false false) →
      (Unit → motive false true) → (Unit → motive true false) → (Unit → motive true true) → motive x x_1
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac_idempotent.injEq : ∀ (x : Lean.Grind.AC.Var) (c₁ : Lean.Meta.Grind.AC.EqCnstr) (x_1 : Lean.Grind.AC.Var)
  (c₁_1 : Lean.Meta.Grind.AC.EqCnstr),
  (Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac_idempotent x c₁ =
      Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac_idempotent x_1 c₁_1) =
    (x = x_1 ∧ c₁ = c₁_1)
-- Init.Data.Range.Polymorphic.UInt
UInt32.instIsAlwaysFinite_1 : Std.Rxo.IsAlwaysFinite UInt32
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.log_five_near_10 : |Real.log 5 - 160943791243 / 100000000000| ≤ 1 / 10 ^ 10
-- Mathlib.Algebra.Ring.Prod
/-- Combine two non-unital ring homomorphisms `f : R →ₙ+* S`, `g : R →ₙ+* T` into
`f.prod g : R →ₙ+* S × T` given by `(f.prod g) x = (f x, g x)`  -/
NonUnitalRingHom.prod : {R : Type u_1} →
  {S : Type u_3} →
    {T : Type u_5} →
      [inst : NonUnitalNonAssocSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring S] →
          [inst_2 : NonUnitalNonAssocSemiring T] → (R →ₙ+* S) → (R →ₙ+* T) → R →ₙ+* S × T
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.isIntegral : ∀ {F : Type u_1} {E : Type u_2} {inst : CommRing F} {inst_1 : Ring E} {inst_2 : Algebra F E}
  [self : IsPurelyInseparable F E], Algebra.IsIntegral F E
-- Lean.Elab.DeclModifiers
/-- Universe parameter names provided using the `universe` command and `.{...}` notation.  -/
Lean.Elab.ExpandDeclIdResult.levelNames : Lean.Elab.ExpandDeclIdResult → List Lean.Name
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ofSliceTo_le_iff : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos},
  String.Slice.Pos.ofSliceTo p ≤ q ↔ ∀ (h : q ≤ p₀), p ≤ p₀.sliceTo q h
-- Mathlib.RingTheory.RootsOfUnity.Complex
IsPrimitiveRoot.arg_eq_pi_iff : ∀ {n : ℕ} {ζ : ℂ}, IsPrimitiveRoot ζ n → n ≠ 0 → (ζ.arg = Real.pi ↔ ζ = -1)
-- Mathlib.LinearAlgebra.SpecialLinearGroup
/-- The special linear group of a module.

This is only meaningful when the module is finite and free,
for otherwise, it coincides with the group of linear equivalences.  -/
SpecialLinearGroup : (R : Type u_1) → (V : Type u_2) → [inst : CommRing R] → [inst_1 : AddCommGroup V] → [Module R V] → Type (max 0 u_2)
-- Mathlib.Analysis.Complex.Schwarz
/-- Equality case in the **Schwarz Lemma**: in the setup of `norm_dslope_le_div_of_mapsTo_ball`,
if there exists a point `z₀` in the ball such that `‖dslope f c z₀‖ = R₂ / R₁`,
then the map `f` is affine with the absolute value of the slope equal to `R₂ / R₁`.

This is an existence version of `affine_of_mapsTo_ball_of_norm_dslope_eq_div` above.

TODO: once the deprecated alias `affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div` is gone,
rename this theorem to `affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div`.
 -/
Complex.affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E} {c : ℂ}
  [StrictConvexSpace ℝ E],
  DifferentiableOn ℂ f (Metric.ball c R₁) →
    Set.MapsTo f (Metric.ball c R₁) (Metric.closedBall (f c) R₂) →
      (∃ z₀ ∈ Metric.ball c R₁, ‖dslope f c z₀‖ = R₂ / R₁) →
        ∃ C, ‖C‖ = R₂ / R₁ ∧ Set.EqOn f (fun z => f c + (z - c) • C) (Metric.ball c R₁)
-- Mathlib.Data.FinEnum
/-- create a `FinEnum` instance using a surjection  -/
FinEnum.ofSurjective : {α : Type u} → {β : Type u_1} → (f : β → α) → [DecidableEq α] → [FinEnum β] → Function.Surjective f → FinEnum α
-- Mathlib.RingTheory.LocalProperties.Reduced
instIsReducedLocalization : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) [IsReduced R], IsReduced (Localization M)
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegralClosure.of_isIntegrallyClosed : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] (K : Type u_3) [inst_2 : CommRing K]
  [inst_3 : Algebra R K] [ifr : IsFractionRing R K] [IsIntegrallyClosed R] [inst_5 : Algebra S R] [inst_6 : Algebra S K]
  [IsScalarTower S R K] [Algebra.IsIntegral S R], IsIntegralClosure R S K
-- Mathlib.Data.Rat.Cast.Defs
MonoidWithZeroHom.ofClass.congr_simp : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β]
  [inst_2 : FunLike F α β] [inst_3 : MonoidWithZeroHomClass F α β] (f f_1 : F),
  f = f_1 → MonoidWithZeroHom.ofClass f = MonoidWithZeroHom.ofClass f_1
-- Std.Sync.StreamMap
Std.AnyAsyncStream.mk : {α t : Type} → [Std.Async.IO.AsyncStream t α] → t → Std.AnyAsyncStream α
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.iInf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {W : ι → CategoryTheory.MorphismProperty C}
  [∀ (i : ι), (W i).IsMultiplicative], (⨅ i, W i).IsMultiplicative
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.HasFactorization.nonempty_mapFactorizationData : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [self : W₁.HasFactorization W₂] {X Y : C} (f : X ⟶ Y), Nonempty (W₁.MapFactorizationData W₂ f)
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.natDegree_trunc_lt : ∀ {R : Type u_1} [inst : Semiring R] (f : PowerSeries R) (n : ℕ), ((PowerSeries.trunc (n + 1)) f).natDegree < n + 1
-- Mathlib.Algebra.Group.TypeTags.Basic
ofMul_inv : ∀ {α : Type u} [inst : Inv α] (x : α), Additive.ofMul x⁻¹ = -Additive.ofMul x
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
ContinuousLinearMap.integral_comp_commSL : ∀ {X : Type u_1} {E : Type u_3} {F : Type u_4} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6}
  {𝕜' : Type u_7} [inst_1 : RCLike 𝕜] [inst_2 : RCLike 𝕜'] [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜' F] [inst_7 : NormedSpace ℝ F] {σ : 𝕜 →+* 𝕜'}
  [RingHomIsometric σ] [CompleteSpace F] [inst_10 : NormedSpace ℝ E] [CompleteSpace E],
  (∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x) →
    ∀ (L : E →SL[σ] F) {φ : X → E}, MeasureTheory.Integrable φ μ → ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Γ'.cons : Turing.PartrecToTM2.Γ'
-- Mathlib.Data.NNReal.Defs
NNReal.instBot : Bot NNReal
-- Mathlib.Analysis.Calculus.Deriv.Mul
DifferentiableOn.fun_finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {s : Set 𝕜} {ι : Type u_2} {𝔸' : Type u_3}
  [inst_1 : NormedCommRing 𝔸'] [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableOn 𝕜 (f i) s) → DifferentiableOn 𝕜 (fun x => ∏ i ∈ u, f i x) s
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The expression for the horizontal composition `η ◫ ηs`.  -/
Mathlib.Tactic.BicategoryLike.MonadHorizontalComp.hConsM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadHorizontalComp m] →
    Mathlib.Tactic.BicategoryLike.WhiskerRight →
      Mathlib.Tactic.BicategoryLike.HorizontalComp → m Mathlib.Tactic.BicategoryLike.HorizontalComp
-- Mathlib.Algebra.Group.Subsemigroup.Membership
Subsemigroup.coe_iSup_of_directed : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Mul M] {S : ι → Subsemigroup M},
  Directed (fun x1 x2 => x1 ≤ x2) S → ↑(⨆ i, S i) = ⋃ i, ↑(S i)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.mulRight_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : C) [inst_2 : CategoryTheory.GrpObj A],
  CategoryTheory.GrpObj.mulRight CategoryTheory.MonObj.one = CategoryTheory.Iso.refl A
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.keys_eq_nil_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.keys = [] ↔ t = ∅
-- Mathlib.Algebra.GroupWithZero.Units.Basic
inv_pow_sub_of_lt : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {m n : ℕ} (a : G₀), n < m → a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op.eq_1 : ∀ {M : Type u_2} [inst : MulOneClass M] (x : Submonoid M),
  x.op = { carrier := MulOpposite.unop ⁻¹' ↑x, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Analysis.Distribution.Distribution
/-- Any continuous linear map `A : F →L[ℝ] G` induces a continuous linear map
`𝓓'(Ω, F) →L[ℝ] 𝓓'(Ω, G)`. On locally integrable functions, this corresponds to applying `A`
pointwise.  -/
Distribution.mapCLM : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_2} →
          [inst_2 : AddCommGroup F] →
            [inst_3 : Module ℝ F] →
              [inst_4 : TopologicalSpace F] →
                {F' : Type u_3} →
                  [inst_5 : AddCommGroup F'] →
                    [inst_6 : Module ℝ F'] →
                      [inst_7 : TopologicalSpace F'] →
                        {n : ℕ∞} →
                          [inst_8 : IsTopologicalAddGroup F] →
                            [inst_9 : ContinuousSMul ℝ F] →
                              [inst_10 : IsTopologicalAddGroup F'] →
                                [inst_11 : ContinuousSMul ℝ F'] →
                                  (F →L[ℝ] F') → Distribution Ω F n →L[ℝ] Distribution Ω F' n
-- Lean.ReservedNameAction
/-- Similar to `resolveGlobalConst`, but also executes reserved name actions.

Consider using `realizeGlobalConstWithInfo` if you want the syntax to show the resulting name's info
on hover.
 -/
Lean.realizeGlobalConst : Lean.Syntax → Lean.CoreM (List Lean.Name)
-- Mathlib.Order.Filter.Basic
Filter.eventually_or_distrib_left : ∀ {α : Type u} {f : Filter α} {p : Prop} {q : α → Prop}, (∀ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∀ᶠ (x : α) in f, q x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.binary_cofan_inr_toCocone : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q), CategoryTheory.Limits.BinaryCofan.inr c.toCocone = c.inr
-- Mathlib.Analysis.Analytic.Binomial
binomialSeries.congr_simp : ∀ {𝕂 : Type u} [inst : Field 𝕂] [inst_1 : CharZero 𝕂] (𝔸 : Type v) [inst_2 : Ring 𝔸] [inst_3 : Algebra 𝕂 𝔸]
  [inst_4 : TopologicalSpace 𝔸] [inst_5 : IsTopologicalRing 𝔸] (a a_1 : 𝕂),
  a = a_1 → ∀ (n : ℕ), binomialSeries 𝔸 a n = binomialSeries 𝔸 a_1 n
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A fork on `f g : X ⟶ Y` is determined by the morphism `ι : P ⟶ X` satisfying `ι ≫ f = ι ≫ g`.
 -/
CategoryTheory.Limits.Fork.ofι : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {P : C} →
          (ι : P ⟶ X) →
            CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g →
              CategoryTheory.Limits.Fork f g
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn'_rii : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred]
  [inst_4 : Std.PRange.Least? α] [inst_5 : Std.PRange.UpwardEnumerable α] [inst_6 : Std.Rxi.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] [inst_8 : Std.PRange.LawfulUpwardEnumerableLeast? α] {xs : Std.Rii α}
  {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Internal.Do.Invariant xs.toList β Pred)
  {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur ⋯ b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn' xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Lean.Parser.Term
Lean.Parser.Term.mdataDiagnostic.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.forget_map' : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.forget.map f)) = ⇑f
-- Mathlib.Algebra.Order.Group.End
RelIso.inv_apply_self : ∀ {α : Type u_1} {r : α → α → Prop} (e : r ≃r r) (x : α), e⁻¹ (e x) = x
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.expandAssert : Lean.Macro
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.comap_symm_apply : ∀ {V : Type u_1} {W : Type u_2} (f : V ≃ W) (G : SimpleGraph W) (w : W), (SimpleGraph.Iso.comap f G).symm w = f.symm w
-- Mathlib.GroupTheory.Sylow
Sylow.smul_le : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {P : Sylow p G} {H : Subgroup G}, ↑P ≤ H → ∀ (h : ↥H), ↑(h • P) ≤ H
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α} [inst_4 : Inhabited β], (List.map Prod.fst l).contains k = false → (Std.HashMap.Raw.ofList l)[k]! = default
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_one_sub' : ∀ {y : ℝ}, 1 - y ≠ 0 → ∀ (x : NNReal), x ^ (1 - y) = x / x ^ y
-- Plausible.DeriveShrinkable
/-- Builds a `Header` with only implicit + instance binders (no explicit target binder).
Adapted from `Plausible.mkHeaderWithOnlyImplicitBinders`.  -/
_private.Plausible.DeriveShrinkable.0.Plausible.mkShrinkableHeader : Lean.InductiveVal → Lean.Elab.TermElabM Lean.Elab.Deriving.Header
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Icc_mul_Icc_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftMono α] [MulRightMono α] (a b c d : α),
  Set.Icc a b * Set.Icc c d ⊆ Set.Icc (a * c) (b * d)
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodePi.match_3.splitter : (n : ℕ) →
  (f : Fin (n + 1) → ℕ) →
    (motive : Fin (Fin.prod fun x => f x.succ) → Sort u_1) →
      (x : Fin (Fin.prod fun x => f x.succ)) →
        ((k : ℕ) → (hk : k < Fin.prod fun x => f x.succ) → motive ⟨k, hk⟩) → motive x
-- Mathlib.Topology.Connected.Clopen
/-- If `u v : Set X` and `u ⊆ v` is clopen in `v`, then `u` is the union of the connected
components of `v` in `X` which intersect `u`.  -/
IsClopen.biUnion_connectedComponentIn : ∀ {X : Type u_3} [inst : TopologicalSpace X] {u v : Set X},
  IsClopen (Subtype.val ⁻¹' u) → u ⊆ v → u = ⋃ x ∈ u, connectedComponentIn v x
-- Mathlib.CategoryTheory.Subobject.Basic
LE.le.hom.congr_simp : ∀ {X : Type u_1} [inst : Preorder X] {x y : X} (h : x ≤ y), h.hom = h.hom
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_singleton`. -/
EMetric.hausdorffEdist_singleton : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α}, Metric.hausdorffEDist {x} {y} = edist x y
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.overMapPullback_comp_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (J.overMapPullbackComp A f (CategoryTheory.CategoryStruct.id Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (J.overMapPullbackId A Y).hom (J.overMapPullback A f))
        (J.overMapPullback A f).leftUnitor.hom) =
    (J.overMapPullbackCongr A ⋯).hom
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.foldr.match_1.eq_2 : ∀ {α : Type u_1} {β : Sort u_3} (motive : Ordnode α → β → Sort u_2) (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α)
  (z : β) (h_1 : (z : β) → motive Ordnode.nil z)
  (h_2 : (size : ℕ) → (l : Ordnode α) → (x : α) → (r : Ordnode α) → (z : β) → motive (Ordnode.node size l x r) z),
  (match Ordnode.node size l x r, z with
    | Ordnode.nil, z => h_1 z
    | Ordnode.node size l x r, z => h_2 size l x r z) =
    h_2 size l x r z
-- Mathlib.RingTheory.RingHom.Etale
RingHom.Etale.formallyUnramified : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), f.Etale → f.FormallyUnramified
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- The function `chaar` interpreted in `ℝ≥0`, as a content  -/
MeasureTheory.Measure.haar.haarContent : {G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      [IsTopologicalGroup G] → TopologicalSpace.PositiveCompacts G → MeasureTheory.Content G
-- Mathlib.RingTheory.Spectrum.Prime.Topology
MaximalSpectrum.toPiLocalizationEquiv_apply_apply : ∀ (R : Type u) [inst : CommSemiring R] [inst_1 : DiscreteTopology (PrimeSpectrum R)] (x : R) (I : MaximalSpectrum R),
  (MaximalSpectrum.toPiLocalizationEquiv R) x I = (algebraMap R (Localization.AtPrime I.asIdeal)) x
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.instHasPullbackSndHomDiscretePUnitOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) {X Y Z : T}
  (f : X ⟶ Y) (g : Y ⟶ Z) [P.HasPullbacksAlong f] [inst_2 : P.HasPullbacksAlong g] [P.IsStableUnderBaseChangeAlong g]
  (A : P.Over Q Z), CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd A.hom g) f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Std.HashMap.Raw α Unit},
  m₁.WF → m₂.WF → ∀ (l : List α), m₁.Equiv m₂ → (m₁.insertManyIfNewUnit l).Equiv (m₂.insertManyIfNewUnit l)
-- Init.Prelude
AndThen.mk : {α : Type u} → (α → (Unit → α) → α) → AndThen α
-- Mathlib.Topology.ContinuousOn
continuousOn_fst : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set (α × β)},
  ContinuousOn Prod.fst s
-- Init.Data.Slice.Array.Lemmas
Subarray.getElem_eq_getElem_array : ∀ {α : Type u_1} {i : ℕ} {xs : Subarray α} {h : i < Std.Slice.size xs}, xs[i] = xs.array[xs.start + i]
-- Mathlib.Data.PNat.Factors
PrimeMultiset.to_ofPNatMultiset : ∀ (v : Multiset ℕ+) (h : ∀ p ∈ v, p.Prime), (PrimeMultiset.ofPNatMultiset v h).toPNatMultiset = v
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
/-- Semilinear sets are closed under set difference.  -/
IsSemilinearSet.sdiff : ∀ {M : Type u_1} [inst : AddCommMonoid M] {s₁ s₂ : Set M},
  IsSemilinearSet s₁ → IsSemilinearSet s₂ → IsSemilinearSet (s₁ \ s₂)