mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Groupoid
/-- The equivalence from a groupoid `C` to its opposite sending every morphism to its inverse.  -/
CategoryTheory.Groupoid.invEquivalence : (C : Type u) → [inst : CategoryTheory.Groupoid C] → C ≌ Cᵒᵖ
-- Mathlib.Order.Monotone.Defs
strictAntiOn_univ : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictAntiOn f Set.univ ↔ StrictAnti f
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.leftInvSeq_take : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ),
  cs.leftInvSeq (List.take j ω) = List.take j (cs.leftInvSeq ω)
-- Mathlib.Order.Interval.Finset.Defs
Finset.Iio_eq_Ico : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : OrderBot α] (a : α),
  Finset.Iio a = Finset.Ico ⊥ a
-- Lean.Data.Lsp.Basic
Lean.Lsp.MarkupContent.mk.sizeOf_spec : ∀ (kind : Lean.Lsp.MarkupKind) (value : String),
  sizeOf { kind := kind, value := value } = 1 + sizeOf kind + sizeOf value
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.instComonObjTensorObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        (A B : C) →
          [CategoryTheory.ComonObj A] →
            [CategoryTheory.ComonObj B] → CategoryTheory.ComonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)
-- Mathlib.Data.TypeVec
TypeVec.appendFun_comp_id : ∀ {n : ℕ} {α : TypeVec.{u} n} {β₀ β₁ β₂ : Type u} (g₀ : β₀ → β₁) (g₁ : β₁ → β₂),
  (TypeVec.id ::: g₁ ∘ g₀) = TypeVec.comp (TypeVec.id ::: g₁) (TypeVec.id ::: g₀)
-- Init.Ext
propext_iff : ∀ {a b : Prop}, a = b ↔ (a ↔ b)
-- Mathlib.Order.Filter.AtTopBot.Finite
/-- If `u` is a sequence which is unbounded above,
then it `Frequently` reaches a value strictly greater than all previous values.
 -/
Filter.frequently_high_scores : ∀ {β : Type u_4} [inst : LinearOrder β] [NoMaxOrder β] {u : ℕ → β},
  Filter.Tendsto u Filter.atTop Filter.atTop → ∃ᶠ (n : ℕ) in Filter.atTop, ∀ k < n, u k < u n
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
OrderIso.map_ciInf_set_of_directedOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompletePartialOrderInf α]
  [inst_1 : ConditionallyCompletePartialOrderInf β] (e : α ≃o β) {s : Set γ} {f : γ → α},
  DirectedOn (fun x1 x2 => x2 ≤ x1) (f '' s) → BddBelow (f '' s) → s.Nonempty → e (⨅ i, f ↑i) = ⨅ i, e (f ↑i)
-- Mathlib.NumberTheory.Divisors
Nat.map_swap_divisorsAntidiagonal : ∀ {n : ℕ}, Finset.map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal = n.divisorsAntidiagonal
-- Mathlib.RingTheory.Ideal.Basic
/-- Also see `Ideal.isSimpleOrder` for the forward direction as an instance when `R` is a
division (semi)ring.

This result actually holds for all division semirings, but we lack the predicate to state it.  -/
Ring.isField_iff_isSimpleOrder_ideal : ∀ {R : Type u_5} [inst : CommSemiring R], IsField R ↔ IsSimpleOrder (Ideal R)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- An arbitrary choice of coequalizer cocone for a parallel family `f`.
 -/
CategoryTheory.Limits.wideCoequalizer.cotrident : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} → (f : J → (X ⟶ Y)) → [CategoryTheory.Limits.HasWideCoequalizer f] → CategoryTheory.Limits.Cotrident f
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.spectrum_abs : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : TopologicalSpace A]
  [inst_3 : StarRing A] [inst_4 : PartialOrder A] [inst_5 : StarOrderedRing A] [inst_6 : Algebra 𝕜 A]
  [ContinuousFunctionalCalculus 𝕜 A p] [inst_8 : Algebra ℝ A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A]
  [T2Space A] [inst_12 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A),
  autoParam (p a) CFC.spectrum_abs._auto_1 → spectrum 𝕜 (CFC.abs a) = (fun z => ↑‖z‖) '' spectrum 𝕜 a
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.mapRange.linearEquiv_toAddEquiv : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {σ₁₂ : R →+* R₂}
  {σ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] N),
  (Finsupp.mapRange.linearEquiv f).toAddEquiv = Finsupp.mapRange.addEquiv f.toAddEquiv
-- Mathlib.Data.Set.Function
Set.InjOn.right_prodMk : ∀ {α : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} {s : Set α} {f₁ : α → β₁} {f₂ : α → β₂},
  Set.InjOn f₂ s → Set.InjOn (fun x => (f₁ x, f₂ x)) s
-- Mathlib.Topology.Category.LightProfinite.AsLimit
LightProfinite.transitionMapLE.congr_simp : ∀ (S : LightProfinite) {n m : ℕ} (h : n ≤ m), S.transitionMapLE h = S.transitionMapLE h
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
AddMonoidAlgebra.toDirectSum_toAddMonoidAlgebra : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f : AddMonoidAlgebra M ι), f.toDirectSum.toAddMonoidAlgebra = f
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.instInhabitedCooperSplitPred : Inhabited Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.glue!.eq_def : ∀ {α : Type u} {β : α → Type v} (l r : Std.DTreeMap.Internal.Impl α β),
  l.glue! r =
    match l with
    | Std.DTreeMap.Internal.Impl.leaf => r
    | l@h:(Std.DTreeMap.Internal.Impl.inner sz k v l' r') =>
      match r with
      | Std.DTreeMap.Internal.Impl.leaf => l
      | r@h:(Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') =>
        if sz < sz' then
          have d := Std.DTreeMap.Internal.Impl.minView! k' v' l'' r'';
          Std.DTreeMap.Internal.Impl.balanceL! d.k d.v l d.tree
        else
          have d := Std.DTreeMap.Internal.Impl.maxView! k v l' r';
          Std.DTreeMap.Internal.Impl.balanceR! d.k d.v d.tree r
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
returning `fallback` if no such key exists.
 -/
Std.DTreeMap.getKeyGTD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → α → α
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_succ : ∀ (o : Ordinal.{u_1}), (Order.succ o).cof = 1
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsMulIndecomposable.eq_1 : ∀ {ι : Type u_1} {M : Type u_2} [inst : Monoid M] (v : ι → M) (s : Set ι) (i : ι),
  IsMulIndecomposable v s i = (i ∈ s ∧ ∀ j ∈ s, ∀ k ∈ s, v i = v j * v k → v j = 1 ∨ v k = 1)
-- Mathlib.LinearAlgebra.RootSystem.BaseExists
RootPairing.eq_baseOf_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [inst : AddCommGroup M]
  [inst_1 : AddCommGroup N] [inst_2 : Field R] [CharZero R] [inst_4 : Module R M] [inst_5 : Module R N]
  (P : RootPairing ι R M N) [P.IsRootSystem] [P.IsCrystallographic] (s : Set ι) (f : M →+ ℚ),
  (∀ i ∈ s, f (P.root i) = 1) →
    (∀ (i : ι), f (P.root i) ≠ 0) →
      (s = IsAddIndecomposable.baseOf (⇑P.root) f ↔
        LinearIndepOn R (⇑P.root) s ∧
          ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s))
-- Std.Time.Time.Unit.Second
Std.Time.Second.instNegOffset : Neg Std.Time.Second.Offset
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₂ → (t₁ ∪ t₂).getD k fallback = t₁.getD k fallback
-- Mathlib.ModelTheory.Complexity
_private.Mathlib.ModelTheory.Complexity.0.FirstOrder.Language.BoundedFormula.toPrenexImp.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → L.BoundedFormula α x → Sort u_4)
  (n : ℕ) (φ : L.BoundedFormula α (n + 1)) (ψ : L.BoundedFormula α n)
  (h_1 :
    (n : ℕ) →
      (φ : L.BoundedFormula α (n + 1)) →
        (ψ : L.BoundedFormula α n) →
          motive n ((φ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum)
            ψ)
  (h_2 : (n : ℕ) → (φ : L.BoundedFormula α (n + 1)) → (ψ : L.BoundedFormula α n) → motive n φ.all ψ)
  (h_3 : (x : ℕ) → (φ ψ : L.BoundedFormula α x) → motive x φ ψ),
  (match n, φ.all, ψ with
    | n, (φ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum, ψ =>
      h_1 n φ ψ
    | n, φ.all, ψ => h_2 n φ ψ
    | x, φ, ψ => h_3 x φ ψ) =
    h_2 n φ ψ
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
/-- The Gelfand transform as a `StarAlgEquiv` between a commutative unital C⋆-algebra over `ℂ`
and the continuous functions on its `characterSpace`.  -/
gelfandStarTransform : (A : Type u_1) → [inst : CommCStarAlgebra A] → A ≃⋆ₐ[ℂ] C(↑(WeakDual.characterSpace ℂ A), ℂ)
-- Mathlib.LinearAlgebra.Matrix.Swap
Matrix.swap_mulVec_apply : ∀ {R : Type u_1} {n : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (i j : n) (a : n → R),
  (Matrix.swap R i j).mulVec a i = a j
-- Mathlib.Topology.UniformSpace.Cauchy
CompleteSpace.mk : ∀ {α : Type u} [inst : UniformSpace α], (∀ {f : Filter α}, Cauchy f → ∃ x, f ≤ nhds x) → CompleteSpace α
-- Mathlib.Algebra.Order.Field.Power
Odd.zpow_nonpos_iff : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ},
  Odd n → (a ^ n ≤ 0 ↔ a ≤ 0)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getEntryLTD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : (a : α) × β a}, t₁.Equiv t₂ → t₁.getEntryLTD k fallback = t₂.getEntryLTD k fallback
-- Mathlib.Data.Finsupp.Defs
Finsupp.embDomain_inj : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_4} [inst : Zero M] {f : α ↪ β} {l₁ l₂ : α →₀ M},
  Finsupp.embDomain f l₁ = Finsupp.embDomain f l₂ ↔ l₁ = l₂
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.static.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenModifier.static = 1
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
AlgebraicTopology.DoldKan.Γ₂N₂_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C],
  AlgebraicTopology.DoldKan.Γ₂N₂.inv = AlgebraicTopology.DoldKan.Γ₂N₂.natTrans
-- Std.Do.SPred.Laws
_private.Std.Do.SPred.Laws.0.Std.Do.SPred.entails.match_1.eq_1 : ∀ (motive : (σs : List (Type u_1)) → Std.Do.SPred σs → Std.Do.SPred σs → Sort u_2) (P Q : Std.Do.SPred [])
  (h_1 : (P Q : Std.Do.SPred []) → motive [] P Q)
  (h_2 : (σ : Type u_1) → (tail : List (Type u_1)) → (P Q : Std.Do.SPred (σ :: tail)) → motive (σ :: tail) P Q),
  (match [], P, Q with
    | [], P, Q => h_1 P Q
    | σ :: tail, P, Q => h_2 σ tail P Q) =
    h_1 P Q
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.mul.inj : ∀ {a b a_1 b_1 : Lean.Grind.CommRing.Expr}, a.mul b = a_1.mul b_1 → a = a_1 ∧ b = b_1
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.map_comp_assoc : ∀ {R : CommRingCat} {M N P : ModuleCat ↑R} (f : M ⟶ N) (g : N ⟶ P) {Z : (AlgebraicGeometry.Spec R).Modules}
  (h : AlgebraicGeometry.tilde P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.map (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.map f)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.map g) h)
-- Lean.Meta.Tactic.Grind.Types
/-- State of the clean name generator.  -/
Lean.Meta.Grind.GoalState.clean : Lean.Meta.Grind.GoalState → Lean.Meta.Grind.Clean.State
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_apply₂₂ : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α)
  (C : Matrix o l α) (D : Matrix o m α) (i : o) (j : m), Matrix.fromBlocks A B C D (Sum.inr i) (Sum.inr j) = D i j
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.isScalarTower' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul α β] [inst_1 : SMul α γ] [inst_2 : SMul β γ]
  [IsScalarTower α β γ], IsScalarTower α (Set β) (Set γ)
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_comp_inv_atTop_iff : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] {l : Filter α}
  {f : G → α}, Filter.Tendsto (fun x => f x⁻¹) Filter.atTop l ↔ Filter.Tendsto f Filter.atBot l
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.IsMarkovKernel.prod : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ]
  (η : ProbabilityTheory.Kernel α γ) [ProbabilityTheory.IsMarkovKernel η], ProbabilityTheory.IsMarkovKernel (κ.prod η)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.isEmpty_dropWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String},
  (s.dropWhile pat).isEmpty = s.all pat
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_sub_eq_toIcoDiv_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b c : α), toIcoDiv hp a (b - c) = toIcoDiv hp (a + c) b
-- Mathlib.RingTheory.Algebraic.Basic
/-- This is slightly more general than `IsAlgebraic.algebraMap` in that it
allows noncommutative intermediate rings `A`.  -/
IsAlgebraic.algHom : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u_2}
  [inst_3 : Ring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B) {a : A}, IsAlgebraic R a → IsAlgebraic R (f a)
-- Mathlib.Data.Multiset.UnionInter
Multiset.replicate_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (n : ℕ) (x : α) (s : Multiset α),
  Multiset.replicate n x ∩ s = Multiset.replicate (min n (Multiset.count x s)) x
-- Mathlib.Analysis.Normed.Group.Basic
edist_eq_enorm_div : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (a b : E), edist a b = ‖a / b‖ₑ
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- If a valuation `v` is compatible with the valuative relation, then `ValueGroupWithZero R`
is isomorphic to the image group (with zero) of `v` as an ordered group with zero.  -/
ValuativeRel.ValueGroupWithZero.orderMonoidIso : {R : Type u_2} →
  {Γ : Type u_3} →
    [inst : Ring R] →
      [inst_1 : ValuativeRel R] →
        [inst_2 : LinearOrderedCommGroupWithZero Γ] →
          (v : Valuation R Γ) →
            [v.Compatible] → ValuativeRel.ValueGroupWithZero R ≃*o (MonoidWithZeroHom.ofClass v).ValueGroup₀
-- Mathlib.Order.CountableSupClosed
mem_countableInfClosure_iff : ∀ {α : Type u_2} {s : Set α} {a : α} [inst : Preorder α],
  a ∈ countableInfClosure s ↔ ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsGLB A a
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_pos : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] [IsStrictOrderedRing S] (n : ℕ) (s : S),
  0 < s → 0 < Polynomial.eval s (ascPochhammer S n)
-- Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent
AlgebraicGeometry.instDescendsAlongSchemeEtaleMinMorphismPropertySurjectiveFlatQuasiCompact : CategoryTheory.MorphismProperty.DescendsAlong (@AlgebraicGeometry.Etale)
  (@AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.QuasiCompact)
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.var.sizeOf_spec : ∀ (i : Int.Internal.Linear.Var), sizeOf (Int.Internal.Linear.Expr.var i) = 1 + sizeOf i
-- Init.Data.Repr
instReprAtomString : ReprAtom String
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
IsIdempotentElem.finite_spectrum : ∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] {p : A},
  IsIdempotentElem p → (spectrum 𝕜 p).Finite
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_snd_eq_one_of_mem_of_one_mem : ∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) {g : G} (h1 : 1 ∈ T),
  g ∈ S → (hST.equiv g).2 = ⟨1, h1⟩
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop.0.Std.Iterators.Types.Drop.instIterator.match_3.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.internalState.inner.Step → Sort u_3) (h : it.internalState.inner.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.HasCoeffs.of_isScalarTower : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [P.HasCoeffs R₀] {R₁ : Type u_6}
  [inst_8 : CommRing R₁] [inst_9 : Algebra R₀ R₁] [inst_10 : Algebra R₁ R] [IsScalarTower R₀ R₁ R]
  [inst_12 : Algebra R₁ S] [inst_13 : IsScalarTower R₁ R S], P.HasCoeffs R₁
-- Mathlib.Data.List.Cycle
Cycle.Chain.imp : ∀ {α : Type u_1} {s : Cycle α} {r₁ r₂ : α → α → Prop},
  (∀ (a b : α), r₁ a b → r₂ a b) → Cycle.Chain r₁ s → Cycle.Chain r₂ s
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- Order of vanishing function for elements of the fraction field defined as the extension of
`CommRing.ordMonoidWithZeroHom` to the field of fractions.
 -/
Ring.ordFrac : (R : Type u_1) →
  [inst : CommRing R] →
    [IsNoetherianRing R] →
      [Ring.KrullDimLE 1 R] →
        {K : Type u_3} →
          [inst_3 : Field K] →
            [inst_4 : Algebra R K] → [IsFractionRing R K] → [Nontrivial R] → K →*₀ WithZero (Multiplicative ℤ)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_rio_eq_zero : ∀ {n i : ℕ}, n ≤ i → (*...n).toList[i]! = 0
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- `limsup` over a general filter is measurable. See `Measurable.limsup` for the version over `ℕ`.
 -/
Measurable.limsup' : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {ι : Type u_5} {ι' : Type u_6} {f : ι → δ → α} {u : Filter ι},
  (∀ (i : ι), Measurable (f i)) →
    ∀ {p : ι' → Prop} {s : ι' → Set ι},
      u.HasCountableBasis p s → (∀ (i : ι'), (s i).Countable) → Measurable fun x => Filter.limsup (fun i => f i x) u
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromCols_mulVec_sumElim : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [inst : Semiring R] [inst_1 : Fintype n₁]
  [inst_2 : Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (v₁ : n₁ → R) (v₂ : n₂ → R),
  (A₁.fromCols A₂).mulVec (Sum.elim v₁ v₂) = A₁.mulVec v₁ + A₂.mulVec v₂
-- Batteries.Data.Nat.Lemmas
Nat.recDiagOn_succ_zero : ∀ {motive : ℕ → ℕ → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : ℕ) → motive 0 n → motive 0 (n + 1))
  (succ_zero : (m : ℕ) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : ℕ) → motive m n → motive (m + 1) (n + 1))
  (m : ℕ),
  Nat.recDiagOn (m + 1) 0 zero_zero zero_succ succ_zero succ_succ =
    succ_zero m (Nat.recDiagOn m 0 zero_zero zero_succ succ_zero succ_succ)
-- Mathlib.Order.Filter.Map
Filter.prod_map_seq_comm : ∀ {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β),
  (Filter.map Prod.mk f).seq g = (Filter.map (fun b a => (a, b)) g).seq f
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RoiSlice : (α : Type u_1) → (α → Type u_2) → [Ord α] → Type (max u_2 u_1)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_algebraMap : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] (r : ℝ),
  ((algebraMap ℝ A) r)⁺ = (algebraMap ℝ A) r⁺
-- Mathlib.Order.Hom.CompleteLattice
/-- Reinterpret a complete lattice homomorphism as a complete lattice homomorphism between the dual
lattices.  -/
CompleteLatticeHom.dual : {α : Type u_2} →
  {β : Type u_3} →
    [inst : CompleteLattice α] → [inst_1 : CompleteLattice β] → CompleteLatticeHom α β ≃ CompleteLatticeHom αᵒᵈ βᵒᵈ
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullbackIsoProdSubtype_hom_apply : ∀ {X Y Z : TopCat} {f : X ⟶ Z} {g : Y ⟶ Z} (x : ↑(CategoryTheory.Limits.pullback f g)),
  (CategoryTheory.ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype f g).hom) x =
    ⟨((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) x,
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g)) x),
      ⋯⟩
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Context.mk : Lean.Meta.Sym.DSimp.Config → Lean.Meta.Sym.DSimp.Context
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- The square
```
  Y --inr--> X ⊞ Y
  |            |
  0           fst
  |            |
  v            v
  0 ---0-----> X
```
is a pullback square.
 -/
CategoryTheory.IsPullback.inr_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.IsPullback CategoryTheory.Limits.biprod.inr 0 CategoryTheory.Limits.biprod.fst 0
-- Mathlib.Probability.ConditionalProbability
/-- The conditional probability measure of measure `μ` on `{ω | X ω ∈ s}`.

It is `μ` restricted to `{ω | X ω ∈ s}` and scaled by the inverse of `μ {ω | X ω ∈ s}`
(to make it a probability measure): `(μ {ω | X ω ∈ s})⁻¹ • μ.restrict {ω | X ω ∈ s}`.  -/
ProbabilityTheory.«term__[|_In_]» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- Any additive free group is isomorphic to "the" additive free group.  -/
IsFreeAddGroup.toFreeAddGroup : (G : Type u_1) → [inst : AddGroup G] → [inst_1 : IsFreeAddGroup G] → G ≃+ FreeAddGroup (IsFreeAddGroup.Generators G)
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_eq_self_of_superset : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s t : Set α} {f : α → M},
  s.mulIndicator f = f → s ⊆ t → t.mulIndicator f = f
-- Mathlib.Algebra.Group.Defs
isDedekindFiniteMonoid_iff : ∀ (M : Type u_2) [inst : MulOne M], IsDedekindFiniteMonoid M ↔ ∀ {a b : M}, a * b = 1 → b * a = 1
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
/-- under suitable mild assumptions on `𝕜`, the character space is a closed set in
`WeakDual 𝕜 A`.  -/
WeakDual.CharacterSpace.isClosed : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommRing 𝕜] [NoZeroDivisors 𝕜] [inst_2 : TopologicalSpace 𝕜]
  [inst_3 : ContinuousAdd 𝕜] [inst_4 : ContinuousConstSMul 𝕜 𝕜] [inst_5 : TopologicalSpace A] [inst_6 : Semiring A]
  [inst_7 : Algebra 𝕜 A] [Nontrivial 𝕜] [T2Space 𝕜] [ContinuousMul 𝕜], IsClosed (WeakDual.characterSpace 𝕜 A)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toList_rcc_eq_fallback : ∀ {m n fallback : ℤ} {i : ℕ}, (n + 1 - m).toNat ≤ i → (m...=n).toList.getD i fallback = fallback
-- Batteries.Data.Array.Lemmas
/-- **Alias** of `Array.getElem_insertIdx_self`. -/
Array.getElem_insertIdx_eq : ∀ {α : Type u} {xs : Array α} {x : α} {i : ℕ} (w : i ≤ xs.size), (xs.insertIdx i x w)[i] = x