mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_union : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k)
-- Init.Data.FloatArray.Basic
FloatArray.instGetElemUSizeFloatLtNatToNatSize : GetElem FloatArray USize Float fun xs i => i.toNat < xs.size
-- Lean.Environment
/-- Name of the declaration asynchronous elaboration was started for. All constants added to this
environment branch must have the name as a prefix, after erasing macro scopes and private name
prefixes.
 -/
_private.Lean.Environment.0.Lean.AsyncContext.declPrefix : Lean.AsyncContext✝ → Lean.Name
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- An equivalence of categories transfers enough injectives.  -/
CategoryTheory.EnoughInjectives.of_equivalence : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : CategoryTheory.Functor C D) [e.IsEquivalence] [CategoryTheory.EnoughInjectives D],
  CategoryTheory.EnoughInjectives C
-- Mathlib.Topology.Maps.OpenQuotient
/-- Given the following diagram with `f` inducing, `p` surjective,
`q` an open quotient map, and `g` injective. Suppose the image of `A` in `B` is stable
under the equivalence mod `q`, then the coinduced topology on `C` (from `A`)
coincides with the induced topology (from `D`).
```
A -f→ B
∣     ∣
p     q
↓     ↓
C -g→ D
```

A typical application is when `K ≤ H` are subgroups of `G`, then the quotient topology on `H/K`
is also the subspace topology from `G/K`.
 -/
coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing : ∀ {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} [inst : TopologicalSpace A] [inst_1 : TopologicalSpace B]
  [inst_2 : TopologicalSpace D] (f : A → B) (g : C → D) (p : A → C) (q : B → D),
  g ∘ p = q ∘ f →
    Topology.IsInducing f →
      Function.Surjective p →
        IsOpenQuotientMap q →
          Function.Injective g →
            q ⁻¹' q '' Set.range f ⊆ Set.range f → TopologicalSpace.coinduced p inst = TopologicalSpace.induced g inst_2
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.add : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X Y : Ω → ℝ} {cX cY : NNReal},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X cX κ ν →
    ProbabilityTheory.Kernel.HasSubgaussianMGF Y cY κ ν →
      ProbabilityTheory.Kernel.HasSubgaussianMGF (fun ω => X ω + Y ω) ((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) κ ν
-- Init.Data.Array.Lemmas
Array.all_flatten' : ∀ {α : Type u_1} {stop : ℕ} {f : α → Bool} {xss : Array (Array α)},
  stop = xss.flatten.size → xss.flatten.all f 0 stop = xss.all fun x => x.all f
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_eq_zero_of_ae : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → G}, f =ᵐ[μ] 0 → ∫ (a : α), f a ∂μ = 0
-- Batteries.Data.Char.AsciiCasing
Char.isUpper_toUpper_eq_isAlpha : ∀ (c : Char), c.toUpper.isUpper = c.isAlpha
-- Init.Data.Dyadic.Basic
Dyadic.neg_ofIntWithPrec : ∀ {i prec : ℤ}, -Dyadic.ofIntWithPrec i prec = Dyadic.ofIntWithPrec (-i) prec
-- Mathlib.Algebra.GroupWithZero.InjSurj
/-- Pull back a `SemigroupWithZero` along an injective function.
See note [reducible non-instances].  -/
Function.Injective.semigroupWithZero : {M₀ : Type u_1} →
  {M₀' : Type u_3} →
    [inst : Zero M₀'] →
      [inst_1 : Mul M₀'] →
        [inst_2 : SemigroupWithZero M₀] →
          (f : M₀' → M₀) →
            Function.Injective f → f 0 = 0 → (∀ (x y : M₀'), f (x * y) = f x * f y) → SemigroupWithZero M₀'
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
hasMFDerivAt_iff_hasFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {x : E} {f' : TangentSpace (modelWithCornersSelf 𝕜 E) x →L[𝕜] TangentSpace (modelWithCornersSelf 𝕜 E') (f x)},
  HasMFDerivAt% f x f' ↔ HasFDerivAt f f' x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.comp_whiskerRight_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {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}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' ψ'' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ')
  (η' : ψ' ⟶ ψ'') {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''}
  {Z : CategoryTheory.Limits.CatCospanTransform F G F'' G''} (h : ψ''.comp φ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight (CategoryTheory.CategoryStruct.comp η η') φ) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η' φ) h)
-- Mathlib.Algebra.Order.Archimedean.Basic
instArchimedeanNNRat : Archimedean ℚ≥0
-- Mathlib.Algebra.Category.Grp.Abelian
/-- In the category of abelian groups, every epimorphism is normal.  -/
AddCommGrpCat.normalEpi : {X Y : AddCommGrpCat} → (f : X ⟶ Y) → CategoryTheory.Epi f → CategoryTheory.NormalEpi f
-- Init.Data.List.SplitOn.Basic
_private.Init.Data.List.SplitOn.Basic.0.List.splitOnPPrepend.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (x x_1 : List α) →
      ((acc : List α) → motive [] acc) → ((a : α) → (t acc : List α) → motive (a :: t) acc) → motive x x_1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
SSet.Subcomplex.Pairing.rank'_eq : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) {y : ↑P.II} (hy : Acc P.AncestralRel y), P.rank' hy = ⨆ x, P.rank' ⋯ + 1
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.instZeroId : {M : Type u_1} →
  [inst : Monoid M] → {A : Type u_4} → [inst_1 : AddMonoid A] → [inst_2 : DistribMulAction M A] → One (A →+[M] A)
-- Mathlib.Data.Finset.Erase
Finset.ne_of_mem_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, b ∈ s.erase a → b ≠ a
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pushout.inr_codiagonal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f f)
      (CategoryTheory.Limits.pushout.codiagonal f) =
    CategoryTheory.CategoryStruct.id Y
-- Lean.DocString.Parser
Lean.Doc.Parser.InList.mk.inj : ∀ {indentation : ℕ} {type : Lean.Doc.Parser.OrderedListType ⊕ Lean.Doc.Parser.UnorderedListType} {indentation_1 : ℕ}
  {type_1 : Lean.Doc.Parser.OrderedListType ⊕ Lean.Doc.Parser.UnorderedListType},
  { indentation := indentation, type := type } = { indentation := indentation_1, type := type_1 } →
    indentation = indentation_1 ∧ type = type_1
-- Mathlib.GroupTheory.Perm.List
List.formPerm_cons_concat_apply_last : ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α) (xs : List α), (x :: (xs ++ [y])).formPerm y = x
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The chosen cone is a limit cone.
(Generally, you'll just want to use `limit.cone F`.)  -/
AddCommMonCat.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddCommMonCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] →
        CategoryTheory.Limits.IsLimit (AddCommMonCat.limitCone F)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.fst.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)), κ.fst = κ.mapOfMeasurable Prod.fst ⋯
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.State.mk.sizeOf_spec : ∀ (symbols : Array Lean.HeadIndex) (symbolSet : Std.HashSet Lean.HeadIndex) (bvarsFound : Std.HashSet ℕ),
  sizeOf { symbols := symbols, symbolSet := symbolSet, bvarsFound := bvarsFound } =
    1 + sizeOf symbols + sizeOf symbolSet + sizeOf bvarsFound
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- In a simplicial set, an edge from a vertex `x₀` to `x₁` is
a `1`-simplex with prescribed `0`-dimensional faces.  -/
SSet.Edge : {X : SSet} → X.obj (Opposite.op { len := 0 }) → X.obj (Opposite.op { len := 0 }) → Type u
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Integrable.norm_condExp_rpow_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E}
  {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ℝ},
  1 ≤ p → MeasureTheory.Integrable (fun x => ‖f x‖ ^ p) μ → (fun x => ‖μ[f | m] x‖ ^ p) ≤ᵐ[μ] μ[fun x => ‖f x‖ ^ p | m]
-- Mathlib.RingTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg_eq_of_isFractionRing`. -/
Ideal.inertiaDeg'_eq_of_isFractionRing : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [q.LiesOver p] [p.IsPrime] [q.IsPrime] (K : Type u_4) (L : Type u_5) [inst_6 : Field K]
  [inst_7 : Field L] [inst_8 : Algebra (R ⧸ p) K] [IsFractionRing (R ⧸ p) K] [inst_10 : Algebra (S ⧸ q) L]
  [IsFractionRing (S ⧸ q) L] [inst_12 : Algebra R K] [IsScalarTower R (R ⧸ p) K] [inst_14 : Algebra S L]
  [IsScalarTower S (S ⧸ q) L] [inst_16 : Algebra R L] [IsScalarTower R S L] [inst_18 : Algebra K L]
  [IsScalarTower R K L], q.inertiaDeg R = Module.finrank K L
-- Mathlib.Data.Finsupp.Defs
Finsupp.coe_eq_zero : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {f : α →₀ M}, ⇑f = 0 ↔ f = 0
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
/-- The maximal spectrum of a local ring is a singleton.  -/
IsLocalRing.instUniqueMaximalSpectrum : {R : Type u_1} → [inst : CommSemiring R] → [IsLocalRing R] → Unique (MaximalSpectrum R)
-- Mathlib.Analysis.Complex.Asymptotics
Complex.isBigO_comp_ofReal_nhds : ∀ {f g : ℂ → ℂ} {x : ℝ}, f =O[nhds ↑x] g → (fun y => f ↑y) =O[nhds x] fun y => g ↑y
-- Init.Data.Nat.Fold
/-- Checks whether `f` returns `true` for every number strictly less than a bound.

This is a tail-recursive equivalent of `Nat.all` that's used at runtime.

Examples:
* `Nat.allTR 4 (fun i _ => i < 5) = true`
* `Nat.allTR 7 (fun i _ => i < 5) = false`
* `Nat.allTR 7 (fun i _ => i % 2 = 0) = false`
* `Nat.allTR 1 (fun i _ => i % 2 = 0) = true`
 -/
Nat.allTR : (n : ℕ) → ((i : ℕ) → i < n → Bool) → Bool
-- Mathlib.Data.Finset.Max
Finset.exists_min_image : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] (s : Finset β) (f : β → α),
  s.Nonempty → ∃ x ∈ s, ∀ x' ∈ s, f x ≤ f x'
-- Mathlib.Algebra.Notation.Prod
Prod.mk_add_mk : ∀ {M : Type u_8} {N : Type u_9} [inst : Add M] [inst_1 : Add N] (a₁ a₂ : M) (b₁ b₂ : N),
  (a₁, b₁) + (a₂, b₂) = (a₁ + a₂, b₁ + b₂)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_inj : ∀ {R : Type u} {a b : R} [inst : Semiring R], Polynomial.C a = Polynomial.C b ↔ a = b
-- Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Set.mul_zero_subset : ∀ {α : Type u_1} [inst : MulZeroClass α] (s : Set α), s * 0 ⊆ 0
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.con_neg_add_cancel : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (x : FreeAddMonoid (G ⊕ H)),
  (AddMonoid.coprodCon G H)
    (FreeAddMonoid.ofList (List.map (Sum.map Neg.neg Neg.neg) (FreeAddMonoid.toList x)).reverse + x) 0
-- Mathlib.Tactic.Module
_private.Mathlib.Tactic.Module.0.Mathlib.Tactic.Module.qNF.toNF.match_1.splitter : {u v : Lean.Level} →
  {M : Q(Type v)} →
    {R : Q(Type u)} →
      (motive : Q(«$R») × Q(«$M») → Sort u_1) →
        (x : Q(«$R») × Q(«$M»)) → ((a : Q(«$R»)) → (x : Q(«$M»)) → motive (a, x)) → motive x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.ExplorationStep.lt.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α → Ordering} (a : α) (a_1 : k a = Ordering.lt) (a_2 a_3 : β a),
  a_2 = a_3 →
    ∀ (a_4 a_5 : List ((a : α) × β a)),
      a_4 = a_5 →
        Std.DTreeMap.Internal.Impl.ExplorationStep.lt a a_1 a_2 a_4 =
          Std.DTreeMap.Internal.Impl.ExplorationStep.lt a a_1 a_3 a_5
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.lineDerivOp_zero : ∀ {V : Type u_5} {E : Type u_6} {F : Type u_7} [inst : AddCommGroup V] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : LineDeriv V E F] [LineDerivAdd V E F] (v : V), LineDeriv.lineDerivOp v 0 = 0
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.image_symm : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
  Set.image ⇑h.symm = Set.preimage ⇑h
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R], AddMonoidAlgebra.coeff 0 = 0
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
setIntegral_withDensity_eq_setIntegral_toReal_smul' : ∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] {f : X → ENNReal} (s : Set X),
  Measurable f →
    (∀ᵐ (x : X) ∂μ.restrict s, f x < ⊤) →
      ∀ (g : X → E), ∫ (x : X) in s, g x ∂μ.withDensity f = ∫ (x : X) in s, (f x).toReal • g x ∂μ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Construct a left unitor from specified limit cones.  -/
CategoryTheory.Limits.BinaryFan.leftUnitor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} →
        CategoryTheory.Limits.IsLimit s →
          {t : CategoryTheory.Limits.BinaryFan s.pt X} → CategoryTheory.Limits.IsLimit t → (t.pt ≅ X)
-- Std.Time.Time.Unit.Basic
/-- Converts a `Nanosecond.Offset` to a `Second.Offset`.
 -/
Std.Time.Second.Offset.ofNanoseconds : Std.Time.Nanosecond.Offset → Std.Time.Second.Offset
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.castLE.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} (x x_1 : ℕ) (x_2 : x ≤ x_1) (t₁ t₂ : L.Term (α ⊕ Fin x)),
  FirstOrder.Language.BoundedFormula.castLE x_2 (FirstOrder.Language.BoundedFormula.equal t₁ t₂) =
    FirstOrder.Language.BoundedFormula.equal (FirstOrder.Language.Term.relabel (Sum.map id (Fin.castLE x_2)) t₁)
      (FirstOrder.Language.Term.relabel (Sum.map id (Fin.castLE x_2)) t₂)
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.TransversalPair.mk.injEq : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (set : ℤˣ → Set G)
  (compl : ∀ (u : ℤˣ), Subgroup.IsComplement (↑(HNNExtension.toSubgroup A B u)) (set u)) (set_1 : ℤˣ → Set G)
  (compl_1 : ∀ (u : ℤˣ), Subgroup.IsComplement (↑(HNNExtension.toSubgroup A B u)) (set_1 u)),
  ({ set := set, compl := compl } = { set := set_1, compl := compl_1 }) = (set = set_1)
-- Mathlib.Algebra.Order.Ring.Finset
Finset.mul_sup₀ : ∀ {R : Type u_1} {ι : Type u_2} [inst : LinearOrder R] [inst_1 : NonUnitalNonAssocSemiring R] [CanonicallyOrderedAdd R]
  [inst_3 : OrderBot R] (s : Finset ι) (f : ι → R) (a : R), a * s.sup f = s.sup fun x => a * f x
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
SimplicialObject.opEquivalence_functor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C],
  SimplicialObject.opEquivalence.functor = SimplicialObject.opFunctor
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.eqToHom_comp_homOfLE_op_assoc : ∀ {X : Type u} [inst : Preorder X] {a b c : X} (hab : Opposite.op a = Opposite.op b) (hbc : c ≤ b) {Z : Xᵒᵖ}
  (h : Opposite.op c ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hab)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hbc).op h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE ⋯).op h
-- Std.Do.Triple.SpecLemmas
/-- Helper definition for specifying loop invariants for loops with early return.

`for ... in ...` loops with early return of type `γ` elaborate to a call like this:
```lean
forIn (β := MProd (Option γ) ...) (b := ⟨none, ...⟩) collection loopBody
```
Note that the first component of the `MProd` state tuple is the optional early return value.
It is `none` as long as there was no early return and `some r` if the loop returned early with `r`.

This function allows to specify different invariants for the loop body depending on whether the loop
terminated early or not. When there was an early return, the loop has effectively finished, which is
encoded by the additional `⌜xs.suffix = []⌝` assertion in the invariant. This assertion is vital for
successfully proving the induction step, as it contradicts with the assumption that
`xs.suffix = x::rest` of the inductive hypothesis at the start of the loop body, meaning that users
won't need to prove anything about the bogus case where the loop has returned early yet takes
another iteration of the loop body.
 -/
Std.Do.Invariant.withEarlyReturn : {β : Type (max u₁ u₂)} →
  {ps : Std.Do.PostShape} →
    {α : Type (max u₁ u₂)} →
      {xs : List α} →
        {γ : Type (max u₁ u₂)} →
          (xs.Cursor → β → Std.Do.Assertion ps) →
            (γ → β → Std.Do.Assertion ps) →
              optParam (Std.Do.ExceptConds ps) Std.Do.ExceptConds.false → Std.Do.Invariant xs (MProd (Option γ) β) ps
-- Std.Sat.AIG.Basic
Std.Sat.AIG.RefVecEntry.mk.sizeOf_spec : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] [inst_2 : DecidableEq α] {w : ℕ} [inst_3 : SizeOf α]
  (aig : Std.Sat.AIG α) (vec : aig.RefVec w), sizeOf { aig := aig, vec := vec } = 1 + sizeOf aig + sizeOf vec
-- Init.Data.Array.Lemmas
Array.foldl_induction : ∀ {α : Type u_1} {β : Type u_2} {as : Array α} (motive : ℕ → β → Prop) {init : β},
  motive 0 init →
    ∀ {f : β → α → β},
      (∀ (i : Fin as.size) (b : β), motive (↑i) b → motive (↑i + 1) (f b as[i])) →
        motive as.size (Array.foldl f init as)
-- Mathlib.Analysis.Convex.StrictConvexSpace
/-- Strict convexity is equivalent to `‖a • x + b • y‖ < 1` for all `x` and `y` of norm at most `1`
and all strictly positive `a` and `b` such that `a + b = 1`. This lemma shows that it suffices to
check this for points of norm one and some `a`, `b` such that `a + b = 1`.  -/
StrictConvexSpace.of_norm_combo_lt_one : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  (∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1) → StrictConvexSpace ℝ E
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.hasCountableCoproducts_of_hasCoproducts : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCoproducts C],
  CategoryTheory.Limits.HasCountableCoproducts C
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.le_maxKey?_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k km : α} (hc : k ∈ t), t.maxKey?.get ⋯ = km → (cmp k km).isLE = true
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- The projection on the `i`-th coordinate of `WithLp p (∀ i, α i)`, as a linear map.  -/
PiLp.projₗ : (p : ENNReal) →
  {𝕜 : Type u_1} →
    {ι : Type u_2} →
      (β : ι → Type u_4) →
        [inst : Semiring 𝕜] →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] →
            [inst_2 : (i : ι) → Module 𝕜 (β i)] → (i : ι) → PiLp p β →ₗ[𝕜] β i
-- Lean.MetavarContext
Lean.assignExp : Lean.MetavarContext → Lean.MVarId → Lean.Expr → Lean.MetavarContext
-- Init.Core
Subtype.exists_of_subtype : ∀ {α : Type u} {p : α → Prop} (a : { x // p x }), ∃ x, p x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combine.injEq : ∀ (c₁ c₂ c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combine c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combine c₁_1 c₂_1) =
    (c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Init.Prelude
/-- The notation typeclass for heterogeneous subtraction.
This enables the notation `a - b : γ` where `a : α`, `b : β`.
 -/
HSub : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.CategoryTheory.Galois.EssSurj
_private.Mathlib.CategoryTheory.Galois.EssSurj.0.CategoryTheory.PreGaloisCategory.quotientToEndObjectHom.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (V : OpenSubgroup (CategoryTheory.Aut F)) {U : OpenSubgroup (CategoryTheory.Aut F)} (h : (↑U).Normal) {A : C}
  (u u_1 :
    (CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅
      Action.FintypeCat.ofMulAction (CategoryTheory.Aut F) (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑U))),
  u = u_1 →
    CategoryTheory.PreGaloisCategory.quotientToEndObjectHom✝ V h u =
      CategoryTheory.PreGaloisCategory.quotientToEndObjectHom✝ V h u_1
-- Mathlib.Algebra.Polynomial.Basic
/-- Prefer putting constants to the left of `X ^ n`.

This lemma is the loop-avoiding `simp` version of `X_pow_mul_assoc`.  -/
Polynomial.X_pow_mul_assoc_C : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ} (r : R),
  p * Polynomial.X ^ n * Polynomial.C r = p * Polynomial.C r * Polynomial.X ^ n
-- Init.Data.SInt.Lemmas
ISize.neg_add_mul_eq_mul_not : ∀ {a b : ISize}, -(a + a * b) = a * ~~~b
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instMax.eq_1 : ∀ {G : Type u_1} [inst : Group G],
  FiniteIndexNormalSubgroup.instMax =
    {
      max := fun U V =>
        let __Subgroup := U.toSubgroup ⊔ V.toSubgroup;
        { toSubgroup := __Subgroup, isNormal' := ⋯, isFiniteIndex' := ⋯ } }
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
/-- An additive action of an additive monoid on a type `β` gives an additive action
on `Finset β`.  -/
Finset.addActionFinset : {α : Type u_2} → {β : Type u_3} → [DecidableEq β] → [inst : AddMonoid α] → [AddAction α β] → AddAction α (Finset β)
-- Mathlib.Topology.Maps.Proper.Basic
/-- The range of a proper map is closed.  -/
IsProperMap.isClosed_range : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsProperMap f → IsClosed (Set.range f)
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If the right adjoint is faithful, then each component of the counit is an epimorphism.  -/
CategoryTheory.Adjunction.counit_epi_of_R_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [R.Faithful] (X : D),
  CategoryTheory.Epi (h.counit.app X)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.instNormedSpace : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {p : ENNReal} →
        {μ : MeasureTheory.Measure α} →
          [inst : NormedAddCommGroup E] →
            {𝕜 : Type u_6} →
              [inst_1 : NormedField 𝕜] →
                [NormedSpace 𝕜 E] → [inst_3 : Fact (1 ≤ p)] → NormedSpace 𝕜 ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Topology.Order.OrderClosed
Filter.Tendsto.max_left : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f : β → α}
  {l : Filter β} {a : α}, Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun i => max (f i) a) l (nhds a)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.num : ℕ → Nat.Internal.Linear.Expr