mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
/-- When `IicProdIoc` is only partially applied (i.e. `IicProdIoc a b x` but not
`IicProdIoc a b x i`) `simp [IicProdIoc]` won't unfold the definition.
This lemma allows to unfold it by writing `simp [IicProdIoc_def]`.  -/
IicProdIoc_def : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : LocallyFiniteOrder ι] [inst_2 : DecidableLE ι] {X : ι → Type u_2}
  [inst_3 : LocallyFiniteOrderBot ι] (a b : ι),
  IicProdIoc a b = fun x i => if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (τ₁ : sq₁.X₁ ⟶ sq₂.X₁)
  (τ₂ : sq₁.X₂ ⟶ sq₂.X₂) (τ₃ : sq₁.X₃ ⟶ sq₂.X₃) (τ₄ : sq₁.X₄ ⟶ sq₂.X₄)
  (comm₁₂ :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₁₂ τ₂ = CategoryTheory.CategoryStruct.comp τ₁ sq₂.f₁₂)
      CategoryTheory.Square.Hom.comm₁₂._autoParam)
  (comm₁₃ :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₁₃ τ₃ = CategoryTheory.CategoryStruct.comp τ₁ sq₂.f₁₃)
      CategoryTheory.Square.Hom.comm₁₃._autoParam)
  (comm₂₄ :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₂₄ τ₄ = CategoryTheory.CategoryStruct.comp τ₂ sq₂.f₂₄)
      CategoryTheory.Square.Hom.comm₂₄._autoParam)
  (comm₃₄ :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₃₄ τ₄ = CategoryTheory.CategoryStruct.comp τ₃ sq₂.f₃₄)
      CategoryTheory.Square.Hom.comm₃₄._autoParam)
  (τ₁_1 : sq₁.X₁ ⟶ sq₂.X₁) (τ₂_1 : sq₁.X₂ ⟶ sq₂.X₂) (τ₃_1 : sq₁.X₃ ⟶ sq₂.X₃) (τ₄_1 : sq₁.X₄ ⟶ sq₂.X₄)
  (comm₁₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₁₂ τ₂_1 = CategoryTheory.CategoryStruct.comp τ₁_1 sq₂.f₁₂)
      CategoryTheory.Square.Hom.comm₁₂._autoParam)
  (comm₁₃_1 :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₁₃ τ₃_1 = CategoryTheory.CategoryStruct.comp τ₁_1 sq₂.f₁₃)
      CategoryTheory.Square.Hom.comm₁₃._autoParam)
  (comm₂₄_1 :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₂₄ τ₄_1 = CategoryTheory.CategoryStruct.comp τ₂_1 sq₂.f₂₄)
      CategoryTheory.Square.Hom.comm₂₄._autoParam)
  (comm₃₄_1 :
    autoParam (CategoryTheory.CategoryStruct.comp sq₁.f₃₄ τ₄_1 = CategoryTheory.CategoryStruct.comp τ₃_1 sq₂.f₃₄)
      CategoryTheory.Square.Hom.comm₃₄._autoParam),
  ({ τ₁ := τ₁, τ₂ := τ₂, τ₃ := τ₃, τ₄ := τ₄, comm₁₂ := comm₁₂, comm₁₃ := comm₁₃, comm₂₄ := comm₂₄, comm₃₄ := comm₃₄ } =
      { τ₁ := τ₁_1, τ₂ := τ₂_1, τ₃ := τ₃_1, τ₄ := τ₄_1, comm₁₂ := comm₁₂_1, comm₁₃ := comm₁₃_1, comm₂₄ := comm₂₄_1,
        comm₃₄ := comm₃₄_1 }) =
    (τ₁ = τ₁_1 ∧ τ₂ = τ₂_1 ∧ τ₃ = τ₃_1 ∧ τ₄ = τ₄_1)
-- Mathlib.Topology.MetricSpace.Thickening
/-- The closed ball of radius `δ` centered at a point of `E` is included in the closed
thickening of `E`.  -/
Metric.closedBall_subset_cthickening : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] {x : α} {E : Set α},
  x ∈ E → ∀ (δ : ℝ), Metric.closedBall x δ ⊆ Metric.cthickening δ E
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
/-- Faithful flatness is preserved by arbitrary base change.  -/
Module.FaithfullyFlat.instTensorProduct : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Type u_1)
  [inst_3 : CommRing S] [inst_4 : Algebra R S] [Module.FaithfullyFlat R M],
  Module.FaithfullyFlat S (TensorProduct R S M)
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Splitting.instFunLike.eq_1 : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  (S : GroupExtension N E G),
  GroupExtension.Splitting.instFunLike S = { coe := fun s => (↑s.toMonoidHom).toFun, coe_injective := ⋯ }
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasPosAssignment.eq_1 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos.hasPosAssignment = true
-- Std.Http.Protocol.H1
/-- For writer-side protocol violations (e.g. fixed-length overflow), force
connection shutdown and surface a close event.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.closeOnBadMessage : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- If `‖pₙ‖ rⁿ = O(1)`, as `n → ∞`, then the radius of `p` is at least `r`.  -/
FormalMultilinearSeries.le_radius_of_isBigO : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal},
  ((fun n => ‖p n‖ * ↑r ^ n) =O[Filter.atTop] fun x => 1) → ↑r ≤ p.radius
-- Mathlib.Order.Max
nonempty_lt : ∀ {α : Type u_1} [inst : LT α] [NoMinOrder α] (a : α), Nonempty { x // x < a }
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.infinite : ∀ {X : Type u_1} [Infinite X], Infinite (OnePoint X)
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.copy_sliceFrom_endPos : ∀ {s : String.Slice}, (s.sliceFrom s.endPos).copy = ""
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableVAdd.measurable_vadd_const : ∀ {M : Type u_2} {α : Type u_3} {inst : VAdd M α} {inst_1 : MeasurableSpace M} {inst_2 : MeasurableSpace α}
  [self : MeasurableVAdd M α] (x : α), Measurable fun x_1 => x_1 +ᵥ x
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.instInhabitedOfCompactSpaceOfNonempty : {α : Type u_1} →
  [inst : TopologicalSpace α] → [CompactSpace α] → [Nonempty α] → Inhabited (TopologicalSpace.PositiveCompacts α)
-- Std.Time.Duration
Std.Time.Duration.mk.sizeOf_spec : ∀ (second : Std.Time.Second.Offset) (nano : Std.Time.Nanosecond.Span)
  (proof : second.val ≥ 0 ∧ ↑nano ≥ 0 ∨ second.val ≤ 0 ∧ ↑nano ≤ 0),
  sizeOf { second := second, nano := nano, proof := proof } = 1 + sizeOf second + sizeOf nano + sizeOf proof
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getEntryGT!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited ((a : α) × β a)] {k : α}, t₁.Equiv t₂ → t₁.getEntryGT! k = t₂.getEntryGT! k
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasCoseparator.hasCoseparator : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} [self : CategoryTheory.HasCoseparator C],
  ∃ G, CategoryTheory.IsCoseparator G
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, returning `none` if no such key exists.
 -/
Std.DTreeMap.Raw.getKeyLE? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → Option α
-- Init.Data.List.Zip
/-- See also `List.zipWith_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths.  -/
List.zipWith_replicate' : ∀ {α : Type u_1} {β : Type u_2} {α_1 : Type u_3} {f : α → β → α_1} {a : α} {b : β} {n : ℕ},
  List.zipWith f (List.replicate n a) (List.replicate n b) = List.replicate n (f a b)
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
List.Nat.antidiagonalTuple_two : ∀ (n : ℕ), List.Nat.antidiagonalTuple 2 n = List.map (fun i => ![i.1, i.2]) (List.Nat.antidiagonal n)
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
/-- The category of quadratic modules; modules with an associated quadratic form  -/
QuadraticModuleCat : (R : Type u) → [CommRing R] → Type (max u (v + 1))
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.structureInstances.flatten : Lean.Option Bool
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheorem.mk : Array Lean.Name →
  Lean.Expr →
    ℕ →
      List Lean.Expr →
        List Lean.HeadIndex →
          Lean.Meta.Grind.Origin →
            Lean.Meta.Grind.EMatchTheoremKind →
              Bool → List Lean.Meta.Grind.EMatchTheoremConstraint → Lean.Meta.Grind.EMatchTheorem
-- Mathlib.Data.DFinsupp.Defs
/-- `x.piecewise y s` is the finitely supported function equal to `x` on the set `s`,
and to `y` on its complement.  -/
DFinsupp.piecewise : {ι : Type u} →
  {β : ι → Type v} →
    [inst : (i : ι) → Zero (β i)] →
      (Π₀ (i : ι), β i) → (Π₀ (i : ι), β i) → (s : Set ι) → [(i : ι) → Decidable (i ∈ s)] → Π₀ (i : ι), β i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdFstIsoProd.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Y Z] [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Z]
  [inst_3 : CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst],
  CategoryTheory.Limits.pullbackProdFstIsoProd f Z =
    {
      hom :=
        CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f CategoryTheory.Limits.prod.fst)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f CategoryTheory.Limits.prod.fst)
            CategoryTheory.Limits.prod.snd),
      inv :=
        CategoryTheory.Limits.pullback.lift CategoryTheory.Limits.prod.fst
          (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id Z)) ⋯,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- the third morphism of a triangle  -/
CategoryTheory.Pretriangulated.Triangle.mor₃ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      (self : CategoryTheory.Pretriangulated.Triangle C) → self.obj₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj self.obj₁
-- Batteries.CodeAction.Attr
Batteries.CodeAction.mkTacticSeqCodeAction.unsafe_1 : Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Batteries.CodeAction.TacticSeqCodeAction
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.toLin_restrict_range_dualCoannihilator_eq_orthogonal : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (B : LinearMap.BilinForm K V) (W : Subspace K V), (LinearMap.domRestrict B W).range.dualCoannihilator = B.orthogonal W
-- Mathlib.Topology.Maps.Basic
/-- A continuous surjective open map is a quotient map.  -/
IsOpenMap.isQuotientMap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → Continuous f → Function.Surjective f → Topology.IsQuotientMap f
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.SpecialLinearGroup.mapGL.eq_1 : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (S : Type u_1)
  [inst_3 : CommRing S] [inst_4 : Algebra R S],
  Matrix.SpecialLinearGroup.mapGL S =
    Matrix.SpecialLinearGroup.toGL.comp (Matrix.SpecialLinearGroup.map (algebraMap R S))
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.ProjectivePresentation.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      (p : C) →
        [projective : CategoryTheory.Projective p] →
          (f : p ⟶ X) → [epi : CategoryTheory.Epi f] → CategoryTheory.ProjectivePresentation X
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_inter_of_contains_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α},
        m₂.contains k = true →
          Std.DHashMap.Internal.Raw₀.Const.get? (m₁.inter m₂) k = Std.DHashMap.Internal.Raw₀.Const.get? m₁ k
-- Mathlib.Combinatorics.Matroid.Basic
_private.Mathlib.Combinatorics.Matroid.Basic.0.Matroid.ground_sdiff_subset_ground : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.E \ X ⊆ M.E
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_filter_eq_size_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → β → Bool}, (Std.HashMap.filter f m).size = m.size ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) m[k] = true
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.continuous_map : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  (pkg' : AbstractCompletion.{vβ, uβ} β) (f : α → β), Continuous (pkg.map pkg' f)
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
/-- The degree `[E : D]` of the inertia field `E` over the decomposition field `D` equals the
inertia degree of `p` in `B`.
 -/
IsInertiaField.rank_decompositionField : ∀ (A : Type u_1) (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] {p : Ideal A} (P : Ideal B) [P.LiesOver p]
  [FiniteDimensional K L] [inst_8 : MulSemiringAction Gal(L/K) B] [IsGaloisGroup Gal(L/K) A B] [IsDedekindDomain A]
  [IsDedekindDomain B] [Module.Finite A B] [Module.IsTorsionFree A B] [Ring.HasFiniteQuotients A] [P.IsMaximal]
  (D : Type u_5) [inst_16 : Field D] [inst_17 : Algebra D L] [IsDecompositionField K L P D] (E : Type u_6)
  [inst_19 : Field E] [inst_20 : Algebra E L] [IsInertiaField K L P E] [IsGalois K L] [inst_23 : Algebra K D]
  [inst_24 : Algebra K E] [inst_25 : Algebra D E] [IsScalarTower K D E] [IsScalarTower K E L] [IsScalarTower K D L],
  p ≠ ⊥ → Module.finrank D E = p.inertiaDegIn B
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.prod_ne_zero_of_subset_normalizedFactors : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : NormalizationMonoid α]
  [Nontrivial α] {a : α} {m : Multiset α}, m ⊆ UniqueFactorizationMonoid.normalizedFactors a → m.prod ≠ 0
-- Lean.Meta.Match.SolveOverlap
/-- A custom, approximated, and quick `contradiction` tactic.
It only finds contradictions of the form `(h₁ : p)` and `(h₂ : ¬ p)` where
`p`s are structurally equal. The procedure is not quadratic like `contradiction`.

We use it to improve the performance of `proveSubgoalLoop` at `mkSplitterProof`.
We will eventually have to write more efficient proof automation for this module.
The new proof automation should exploit the structure of the generated goals and avoid general purpose tactics
such as `contradiction`.
 -/
_private.Lean.Meta.Match.SolveOverlap.0.Lean.MVarId.contradictionQuick : Lean.MVarId → Lean.MetaM Bool
-- Lean.Parser.Do
Lean.Parser.Term.doMatchExprAlts.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.IsSymmetric.conj_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] {T : E →ₗ[𝕜] E},
  T.IsSymmetric → ∀ (S : E →ₗ[𝕜] F), (S ∘ₗ T ∘ₗ LinearMap.adjoint S).IsSymmetric
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.trans_toLinearMap : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [inst : CommSemiring R] [inst_1 : Semiring A₁]
  [inst_2 : Semiring A₂] [inst_3 : Semiring A₃] [inst_4 : Algebra R A₁] [inst_5 : Algebra R A₂] [inst_6 : Algebra R A₃]
  (f : A₁ ≃ₐ[R] A₂) (g : A₂ ≃ₐ[R] A₃), (f.trans g).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap
-- Mathlib.Algebra.QuadraticAlgebra.Defs
instDecidableEqQuadraticAlgebra.decEq : {R : Type u_1} → {a b : R} → [DecidableEq R] → (x x_1 : QuadraticAlgebra R a b) → Decidable (x = x_1)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.toArray_toList : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → m.toList.toArray = m.toArray
-- Mathlib.RingTheory.Localization.Module
Module.Basis.ofIsLocalizedModule_repr_apply : ∀ {R : Type u_1} (Rₛ : Type u_2) [inst : CommSemiring R] (S : Submonoid R) [inst_1 : CommSemiring Rₛ]
  [inst_2 : Algebra R Rₛ] [inst_3 : IsLocalization S Rₛ] {M : Type u_3} {Mₛ : Type u_4} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid Mₛ] [inst_7 : Module R Mₛ] [inst_8 : Module Rₛ Mₛ]
  [inst_9 : IsScalarTower R Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [inst_10 : IsLocalizedModule S f] {ι : Type u_5}
  (b : Module.Basis ι R M) (m : M) (i : ι),
  ((Module.Basis.ofIsLocalizedModule Rₛ S f b).repr (f m)) i = (algebraMap R Rₛ) ((b.repr m) i)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.Iterators.Types.TakeWhile.instIterator.match_3.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} →
          (it : Std.IterM m β) →
            (motive : it.internalState.inner.Step → Sort u_3) →
              (x : it.internalState.inner.Step) →
                ((it' : Std.IterM m β) →
                    (out : β) →
                      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
                        motive ⟨Std.IterStep.yield it' out, h⟩) →
                  ((it' : Std.IterM m β) →
                      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) →
                        motive ⟨Std.IterStep.skip it', h⟩) →
                    ((h : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) →
                      motive x
-- Mathlib.NumberTheory.Chebyshev
/-- A sum over prime powers may be written as a double sum over exponents and then primes.  -/
Chebyshev.sum_PrimePow_eq_sum_sum' : ∀ {R : Type u_1} [inst : AddCommMonoid R] (f : ℕ → R) {x : ℝ},
  0 ≤ x →
    ∀ {N : ℕ},
      ⌊Real.log x / Real.log 2⌋₊ ≤ N →
        ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊ with IsPrimePow n, f n =
          ∑ k ∈ Finset.Icc 1 N, ∑ p ∈ Finset.Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)
-- Mathlib.Data.Nat.Size
Nat.lt_size : ∀ {m n : ℕ}, m < n.size ↔ 2 ^ m ≤ n
-- Mathlib.Tactic.IrreducibleDef
Lean.Elab.Command.irredDefLemma : Lean.ParserDescr
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.map.congr_simp : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {B : Type u_4} {τ : Type u_5} [inst_6 : CommRing B] [inst_7 : SetLike τ B]
  [inst_8 : AddSubgroupClass τ B] {ℬ : ι → τ} [inst_9 : GradedRing ℬ] {P : Submonoid A} {Q : Submonoid B}
  (g g_1 : 𝒜 →+*ᵍ ℬ) (e_g : g = g_1) (comap_le : P ≤ Submonoid.comap g Q),
  HomogeneousLocalization.map g comap_le = HomogeneousLocalization.map g_1 ⋯
-- Mathlib.Analysis.SpecialFunctions.Exponential
hasStrictDerivAt_exp_smul_const : ∀ {𝕂 : Type u_1} {𝔸 : Type u_3} [inst : RCLike 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸]
  (x : 𝔸) (t : 𝕂), HasStrictDerivAt (fun u => NormedSpace.exp (u • x)) (NormedSpace.exp (t • x) * x) t
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.isRegularEpi_of_EffectiveEpi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B X : C} (f : X ⟶ B)
  [CategoryTheory.Limits.HasPullback f f] [CategoryTheory.EffectiveEpi f], CategoryTheory.IsRegularEpi f
-- Mathlib.Topology.QuasiSeparated
/-- A topological space is quasi-separated if the intersections of any pairs of compact open
subsets are still compact.  -/
QuasiSeparatedSpace : (α : Type u_3) → [TopologicalSpace α] → Prop
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x x' : ↥X) (hxx' : x = x'),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x) (X.presheaf.stalkCongr ⋯).hom =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x')
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionAssocIso : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (x : Dᵒᵖ) (x_1 x_2 : Cᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso x x_1 x_2 =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (Opposite.unop x) (Opposite.unop x_1)
          (Opposite.unop x_2)).symm.op
-- Mathlib.Combinatorics.SimpleGraph.Partition
SimpleGraph.Partition.default_def : ∀ {V : Type u} {G : SimpleGraph V}, default = G.selfColoring.toPartition
-- Mathlib.Topology.Order.OrderClosed
IsClosed.epigraph : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
  [inst_2 : TopologicalSpace β] {f : β → α} {s : Set β},
  IsClosed s → ContinuousOn f s → IsClosed {p | p.1 ∈ s ∧ f p.1 ≤ p.2}
-- Lean.Data.PersistentArray
Lean.PersistentArray.collectStats : {α : Type u} → Lean.PersistentArrayNode α → Lean.PersistentArray.Stats → ℕ → Lean.PersistentArray.Stats
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
/-- If a family of maps `g` is contained in another family `g'` (up to isomorphisms),
if `f : X₁ ⟶ X₂` is a morphism, and `X₂` is obtained from `X₁` by attaching cells
of the form `g`, then it is also obtained by attaching cells of the form `g'`.  -/
HomotopicalAlgebra.AttachCells.reindexCellTypes : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} →
        {g : (a : α) → A a ⟶ B a} →
          {X₁ X₂ : C} →
            {f : X₁ ⟶ X₂} →
              HomotopicalAlgebra.AttachCells g f →
                {α' : Type t'} →
                  {A' B' : α' → C} →
                    (g' : (i' : α') → A' i' ⟶ B' i') →
                      (a : α → α') →
                        ((i : α) → CategoryTheory.Arrow.mk (g i) ≅ CategoryTheory.Arrow.mk (g' (a i))) →
                          HomotopicalAlgebra.AttachCells g' f
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extendId_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cocone F),
  s.extendId.hom.hom = CategoryTheory.CategoryStruct.id s.pt
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instHashableCanonArgKey : Hashable Lean.Meta.Grind.CanonArgKey
-- Mathlib.Topology.Clopen
IsClopen.preimage : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set Y},
  IsClopen s → ∀ {f : X → Y}, Continuous f → IsClopen (f ⁻¹' s)
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, returning `none` if no such key exists.
 -/
Std.DTreeMap.getKeyLE? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → Option α
-- Mathlib.Control.Bitraversable.Instances
LawfulBitraversable.flip : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] [LawfulBitraversable t], LawfulBitraversable (flip t)
-- Mathlib.Algebra.Category.MonCat.Adjunctions
MonCat.adjoinOne_obj_coe : ∀ (S : Semigrp), ↑(MonCat.adjoinOne.obj S) = WithOne ↑S
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLE?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.getEntryLE? k = Std.DTreeMap.Internal.Impl.getEntryLE?.go k none
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_one : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M],
  UniqueFactorizationMonoid.radical 1 = 1
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.UnsatAt.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig aig_1 : Std.Sat.AIG α) (e_aig : aig = aig_1)
  (start start_1 : ℕ) (e_start : start = start_1) (invert invert_1 : Bool),
  invert = invert_1 → ∀ (h : start < aig.decls.size), aig.UnsatAt start invert h = aig_1.UnsatAt start_1 invert_1 ⋯
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.isEqv.eq_1 : ∀ {α : Type u} (xs ys : Array α) (p : α → α → Bool),
  xs.isEqv ys p = if h : xs.size = ys.size then xs.isEqvAux ys h p xs.size ⋯ else false