mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Float.Model.Format.Basic
Float.Model.Format.mk.sizeOf_spec : ∀ (mantissaBitsWithoutImplicit : ℕ) (hm : autoParam (0 < mantissaBitsWithoutImplicit) Float.Model.Format.hm._autoParam)
  (exponentBits : ℕ) (he : autoParam (0 < exponentBits) Float.Model.Format.he._autoParam),
  sizeOf
      { mantissaBitsWithoutImplicit := mantissaBitsWithoutImplicit, hm := hm, exponentBits := exponentBits, he := he } =
    1 + sizeOf mantissaBitsWithoutImplicit + sizeOf hm + sizeOf exponentBits + sizeOf he
-- Mathlib.MeasureTheory.Order.Group.Lattice
AEMeasurable.posPart : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : AddGroup α] [inst_2 : MeasurableSpace α]
  [inst_3 : MeasurableSpace β] {f : β → α} {μ : MeasureTheory.Measure β} [MeasurableSup α],
  AEMeasurable f μ → AEMeasurable (fun x => (f x)⁺) μ
-- Mathlib.Data.Fin.Basic
Fin.last_sub : ∀ {n : ℕ} (i : Fin (n + 1)), Fin.last n - i = i.rev
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_filter!_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  {f : α → β → Bool},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filter! f t).isEmpty = true ↔
      ∀ (k : α) (h : Std.DTreeMap.Internal.Impl.contains k t = true),
        f (t.getKey k h) (Std.DTreeMap.Internal.Impl.Const.get t k h) = false)
-- Mathlib.Analysis.Convex.Gauge
gauge_empty : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E], gauge ∅ = 0
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.order_ofForallLtEqZero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : LinearOrder Γ] [inst_2 : LocallyFiniteOrder Γ]
  [inst_3 : Zero Γ] (f : Γ → R), f ≠ 0 → ∀ (n : Γ) (hn : ∀ m < n, f m = 0), n ≤ (HahnSeries.ofSuppBddBelow f ⋯).order
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.instSliceableRciSlice : {α : Type u} →
  {β : α → Type v} →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.instSliceableRciSlice._auto_1) →
      Std.Rci.Sliceable (Std.DTreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.RciSlice α β)
-- Init.Prelude
/-- The global macro scope counter, used for producing fresh scope names.  -/
Lean.Macro.State.macroScope : Lean.Macro.State → Lean.MacroScope
-- Lean.Meta.WHNF
Lean.Meta.smartUnfoldingSuffix : String
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- The (unique) isomorphism between the chosen terminal object and any other terminal object.  -/
CategoryTheory.Limits.terminalIsoIsTerminal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasTerminal C] → {P : C} → CategoryTheory.Limits.IsTerminal P → (⊤_ C ≅ P)
-- Mathlib.MeasureTheory.OuterMeasure.Operations
/-- **Alias** of `FunLike.coeAddMonoidHom`. -/
MeasureTheory.OuterMeasure.coeFnAddMonoidHom : (F : Type u_1) →
  (α : Type u_2) →
    (β : Type u_3) →
      [inst : FunLike F α β] →
        [inst_1 : AddZero F] → [inst_2 : AddZeroClass β] → [IsZeroApply F α β] → [IsAddApply F α β] → F →+ α → β
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.zero_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.AddMonObj.zero = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Lean.Server.AsyncList
Lean.AsyncList.brecOn.go : {ε : Type u} →
  {α : Type v} →
    {motive_1 : Lean.AsyncList ε α → Sort u_1} →
      {motive_2 : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α)) → Sort u_1} →
        {motive_3 : Task (Except ε (Lean.AsyncList ε α)) → Sort u_1} →
          {motive_4 : Except ε (Lean.AsyncList ε α) → Sort u_1} →
            (t : Lean.AsyncList ε α) →
              ((t : Lean.AsyncList ε α) → t.below → motive_1 t) →
                ((t : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α))) → Lean.AsyncList.below_1 t → motive_2 t) →
                  ((t : Task (Except ε (Lean.AsyncList ε α))) → Lean.AsyncList.below_2 t → motive_3 t) →
                    ((t : Except ε (Lean.AsyncList ε α)) → Lean.AsyncList.below_3 t → motive_4 t) →
                      motive_1 t ×' t.below
-- Lean.Widget.Diff
/-- Computes the diff for `e₀` and `e₁`. If `useAfter` is `false`, `e₀, e₁` are interpreted as `after, before` instead of `before, after`. -/
_private.Lean.Widget.Diff.0.Lean.Widget.exprDiff : Lean.Expr → Lean.Expr → optParam Bool true → Lean.MetaM Lean.Widget.ExprDiff✝
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- In the trivial model with corners, the associated `PartialEquiv` is the identity.  -/
modelWithCornersSelf_partialEquiv : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (E : Type u_2) [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E], (modelWithCornersSelf 𝕜 E).toPartialEquiv = PartialEquiv.refl E
-- Aesop.Frontend.Attribute
Lean.Parser.Category.Aesop.attr_rules : Lean.Parser.Category
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.toWeightBasisInt.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : CharZero R], b.toWeightBasisInt = b.toWeightBasisInt
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- One subspace is not less than or equal to another if and only if it has a point not in the
second subspace.  -/
AffineSubspace.not_le_iff_exists : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (s₁ s₂ : AffineSubspace k P), ¬s₁ ≤ s₂ ↔ ∃ p ∈ s₁, p ∉ s₂
-- Mathlib.InformationTheory.Hamming
/-- `Hamming.ofHamming` is the identity function from the `Hamming` of a type.  -/
Hamming.ofHamming : {ι : Type u_2} → {β : ι → Type u_3} → Hamming β ≃ ((i : ι) → β i)
-- Mathlib.Order.WellQuasiOrder
WellQuasiOrderedLE.wqo : ∀ {α : Type u_3} {inst : LE α} [self : WellQuasiOrderedLE α], WellQuasiOrdered fun x1 x2 => x1 ≤ x2
-- Init.Prelude
/-- Extract the methods list from the `MacroM` state.  -/
Lean.Macro.getMethods : Lean.MacroM Lean.Macro.Methods
-- Mathlib.Order.Filter.CardinalInter
/-- For a collection of sets `s ∈ l` with cardinality below c,
their intersection belongs to `l` as well.  -/
CardinalInterFilter.cardinal_sInter_mem : ∀ {α : Type u} {l : Filter α} {c : Cardinal.{u}} [self : CardinalInterFilter l c] (S : Set (Set α)),
  Cardinal.mk ↑S < c → (∀ s ∈ S, s ∈ l) → ⋂₀ S ∈ l
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.pair_mk_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ)
  (g : α → γ) (hg : MeasureTheory.AEStronglyMeasurable g μ),
  (MeasureTheory.AEEqFun.mk f hf).pair (MeasureTheory.AEEqFun.mk g hg) =
    MeasureTheory.AEEqFun.mk (fun x => (f x, g x)) ⋯
-- Aesop.Util.EqualUpToIds
Aesop.exprsEqualUpToIds' : Lean.Expr → Lean.Expr → optParam Bool false → Lean.MetaM Bool
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientQuotientEquivQuotientAux.eq_1 : ∀ {G : Type u} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M),
  QuotientAddGroup.quotientQuotientEquivQuotientAux N M h =
    QuotientAddGroup.lift (AddSubgroup.map (QuotientAddGroup.mk' N) M) (QuotientAddGroup.map N M (AddMonoidHom.id G) h)
      ⋯
-- Mathlib.Data.EReal.Inv
/-- The absolute value from `EReal` to `ℝ≥0∞`, mapping `⊥` and `⊤` to `⊤` and
a real `x` to `|x|`.  -/
EReal.abs : EReal → ENNReal
-- Mathlib.Topology.MetricSpace.Lipschitz
/-- A function `f : α → (ι → ℝ)` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz
extension to the whole space. The same result for the space `ℓ^∞ (ι, ℝ)` over a possibly infinite
type `ι` is implemented in `LipschitzOnWith.extend_lp_infty`.  -/
LipschitzOnWith.extend_pi : ∀ {α : Type u} {ι : Type x} [inst : PseudoMetricSpace α] [inst_1 : Fintype ι] {f : α → ι → ℝ} {s : Set α} {K : NNReal},
  LipschitzOnWith K f s → ∃ g, LipschitzWith K g ∧ Set.EqOn f g s
-- Mathlib.CategoryTheory.WithTerminal.Cone
/-- The category of functors `J ⥤ Under X` can be seen as part of a comma category,
namely the comma category constructed from the identity of the category of functors
`J ⥤ C` and the functor that maps `X : C` to the constant functor `J ⥤ C`.

Given a functor `K : J ⥤ Under X`, it is mapped to a natural transformation to the
obvious functor `J ⥤ C` from the constant functor `X`.  -/
CategoryTheory.WithInitial.commaFromUnder : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {X : C} →
          CategoryTheory.Functor (CategoryTheory.Functor J (CategoryTheory.Under X))
            (CategoryTheory.Comma (CategoryTheory.Functor.const J)
              (CategoryTheory.Functor.id (CategoryTheory.Functor J C)))
-- Mathlib.RingTheory.Ideal.Pure
/-- An ideal `I` of `R` is pure if `R ⧸ I` is a flat `R`-module.  -/
Ideal.Pure : {R : Type u_1} → [inst : CommRing R] → Ideal R → Prop
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula.0.WeierstrassCurve.Projective.toAffine_slope_of_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  P 2 ≠ 0 →
    Q 2 ≠ 0 →
      P 0 * Q 2 = Q 0 * P 2 →
        P 1 * Q 2 ≠ W.negY Q * P 2 →
          W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2) =
            -(MvPolynomial.eval P) W.polynomialX / P 2 / (P 1 - W.negY P)
-- Mathlib.Data.Finset.Empty
Finset.empty_ssubset : ∀ {α : Type u_1} {s : Finset α}, ∅ ⊂ s ↔ s.Nonempty
-- Lean.Declaration
Lean.instBEqTheoremVal.beq : Lean.TheoremVal → Lean.TheoremVal → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Every coequalizer of `(f, f)` is an isomorphism.  -/
CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_self : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f : X ⟶ Y} {c : CategoryTheory.Limits.Cofork f f}
  (h : CategoryTheory.Limits.IsColimit c), CategoryTheory.IsIso c.π
-- Init.Data.List.Erase
List.eraseP_ne_nil_iff : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, List.eraseP p xs ≠ [] ↔ xs ≠ [] ∧ ∀ (x : α), p x = true → xs ≠ [x]
-- Mathlib.RingTheory.WittVector.Basic
WittVector.mk.eq_1 : ∀ (p : ℕ) {R : Type u_1} (coeff : ℕ → R), WittVector.mk p coeff = { coeff := coeff }
-- Mathlib.Combinatorics.SimpleGraph.Ends.Properties
SimpleGraph.componentComplFunctor_finite : ∀ {V : Type} (G : SimpleGraph V) [G.LocallyFinite] [Fact G.Preconnected] (K : (Finset V)ᵒᵖ),
  Finite (G.componentComplFunctor.obj K)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval.eq_7 : ∀ {w : ℕ} (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (w_3 n : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w_3)
  (h : w = w_3 * n),
  Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.replicate n expr h) =
    ⋯ ▸ BitVec.replicate n (Std.Tactic.BVDecide.BVExpr.eval assign expr)
-- Mathlib.Algebra.Lie.Rank
LieModule.isRegular_def : ∀ (R : Type u_1) {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M] [inst_9 : Module.Finite R M] [inst_10 : Module.Free R M]
  (x : L), LieModule.IsRegular R M x ↔ (LinearMap.charpoly ((LieModule.toEnd R L M) x)).coeff (LieModule.rank R L M) ≠ 0
-- Mathlib.Data.Sum.Interval
Sum.Lex.Iic_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Fintype α]
  [inst_3 : LocallyFiniteOrderBot α] [inst_4 : LocallyFiniteOrderBot β] (b : β),
  Finset.Iic (Sum.inrₗ b) = Finset.map toLex.toEmbedding (Finset.univ.disjSum (Finset.Iic b))
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
/-- If a family of sets `𝒜` is measure-dense in `X`, then it is also the case for the sets in `𝒜`
with finite measure.  -/
MeasureTheory.Measure.MeasureDense.fin_meas : ∀ {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝒜 : Set (Set X)},
  μ.MeasureDense 𝒜 → μ.MeasureDense {s | s ∈ 𝒜 ∧ μ s ≠ ⊤}
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the reverse direction of `SimpleGraph.Walk.isCircuit_mapLe`. -/
SimpleGraph.Walk.IsCircuit.mapLe : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u : V} {p : G.Walk u u},
  p.IsCircuit → (SimpleGraph.Walk.mapLe h p).IsCircuit
-- Mathlib.RingTheory.FiniteType
/-- If a set `S` generates, as algebra, `R[M]`, then the image of the union of
the supports of elements of `S` generates `R[M]`.  -/
AddMonoidAlgebra.support_gen_of_gen' : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddMonoid M] {S : Set (AddMonoidAlgebra R M)},
  Algebra.adjoin R S = ⊤ → Algebra.adjoin R (AddMonoidAlgebra.of' R M '' ⋃ f ∈ S, ↑f.coeff.support) = ⊤
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.uniformizer.congr_simp : ∀ (R : Type u_1) [inst : Semiring R] [inst_1 : ValuativeRel R] [inst_2 : ValuativeRel.IsDiscrete R],
  ValuativeRel.uniformizer R = ValuativeRel.uniformizer R
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a fallback : α} {v : β k},
  (m.insertIfNew k v).getKeyD a fallback = if (k == a) = true ∧ k ∉ m then k else m.getKeyD a fallback
-- Init.Data.FloatArray.Basic
_private.Init.Data.FloatArray.Basic.0.FloatArray.foldlMUnsafe.fold : {β : Type v} → {m : Type v → Type w} → [Monad m] → (β → Float → m β) → FloatArray → USize → USize → β → m β
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.instInhabitedOfL : {J : CategoryTheory.Limits.MulticospanShape} → [Inhabited J.L] → Inhabited (CategoryTheory.Limits.WalkingMulticospan J)
-- Mathlib.Algebra.GroupWithZero.Associated
associated_mul_unit_left_iff : ∀ {N : Type u_2} [inst : Monoid N] {a b : N} {u : Nˣ}, Associated (a * ↑u) b ↔ Associated a b
-- Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
/-- Helper lemma for the first part of the First Main Theorem: At 0, the difference between the
characteristic functions of `f` and `f⁻¹` equals `log ‖f 0‖`.
 -/
ValueDistribution.characteristic_sub_characteristic_inv_at_zero : ∀ {f : ℂ → ℂ},
  Meromorphic f → ValueDistribution.characteristic f ⊤ 0 - ValueDistribution.characteristic f⁻¹ ⊤ 0 = Real.log ‖f 0‖
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImportMetaKind.noConfusionType : Sort v✝ → Lean.Lsp.LeanImportMetaKind → Lean.Lsp.LeanImportMetaKind → Sort v✝
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k a : α}, (t.erase k).get? a = if cmp k a = Ordering.eq then none else t.get? a
-- Mathlib.Topology.Sets.VietorisTopology
/-- **Alias** of `TopologicalSpace.Compacts.isOpen_setOfPred_disjoint_coe`. -/
TopologicalSpace.Compacts.isOpen_setOf_disjoint_coe : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T2Space α], IsOpen {p | Disjoint ↑p.1 ↑p.2}
-- Mathlib.Data.Setoid.Basic
/-- The third isomorphism theorem for sets.  -/
Setoid.quotientQuotientEquivQuotient : {α : Type u_1} → (r s : Setoid α) → (h : r ≤ s) → Quotient (Setoid.ker (Quot.mapRight h)) ≃ Quotient s
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_eraseKey_eq_iff_beq_minKey_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {k : α}
  {he : (Std.Internal.List.eraseKey k l).isEmpty = false},
  Std.Internal.List.minKey (Std.Internal.List.eraseKey k l) he = Std.Internal.List.minKey l ⋯ ↔
    (k == Std.Internal.List.minKey l ⋯) = false
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_inj : ∀ {K : Type u_1} [inst : RCLike K] {z w : ℝ}, ↑z = ↑w ↔ z = w
-- Mathlib.Analysis.RCLike.Lemmas
RCLike.reCLM_norm : ∀ {K : Type u_1} [inst : RCLike K], ‖RCLike.reCLM‖ = 1
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- A constructor for morphisms in `ShortComplex C` when the commutativity conditions
are not obvious.  -/
CategoryTheory.ShortComplex.homMk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (τ₁ : S₁.X₁ ⟶ S₂.X₁) →
          (τ₂ : S₁.X₂ ⟶ S₂.X₂) →
            (τ₃ : S₁.X₃ ⟶ S₂.X₃) →
              CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂ →
                CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃ → (S₁ ⟶ S₂)
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq1.toSeq.match_1.splitter : {α : Type u_1} →
  (motive : Stream'.Seq1 α → Sort u_2) →
    (x : Stream'.Seq1 α) → ((a : α) → (s : Stream'.Seq α) → motive (a, s)) → motive x
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeOpEquiv_functor_map_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} {Y X : (CategoryTheory.Limits.Cocone F)ᵒᵖ} (f : Y ⟶ X),
  (CategoryTheory.Limits.coconeOpEquiv.functor.map f).hom = f.unop.hom.op
-- Mathlib.CategoryTheory.Join.Basic
_private.Mathlib.CategoryTheory.Join.Basic.0.CategoryTheory.Join.id.match_1.eq_2 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] (motive : CategoryTheory.Join C D → Sort u_5) (x : D)
  (h_1 : (x : C) → motive (CategoryTheory.Join.left x)) (h_2 : (x : D) → motive (CategoryTheory.Join.right x)),
  (match CategoryTheory.Join.right x with
    | CategoryTheory.Join.left x => h_1 x
    | CategoryTheory.Join.right x => h_2 x) =
    h_2 x
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.single_eq_zero_iff : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → Zero (M i)] [inst_1 : DecidableEq ι] {i : ι} {x : M i},
  Pi.single i x = 0 ↔ x = 0
-- Std.Time.Format.Modifier
/-- Full form (e.g., "Tuesday")
 -/
Std.Time.Text.full : Std.Time.Text
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.ofHom_apply : ∀ {X Y : Type u} [inst : CommMonoid X] [inst_1 : CommMonoid Y] (f : X →* Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (CommMonCat.ofHom f)) x = f x
-- Mathlib.RingTheory.Spectrum.Prime.Topology
IsLocalRing.closedPoint_mem_iff : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : IsLocalRing R] (U : TopologicalSpace.Opens (PrimeSpectrum R)),
  IsLocalRing.closedPoint R ∈ U ↔ U = ⊤
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.image_const_add_Ioi : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b : M), (fun x => a + x) '' Set.Ioi b = Set.Ioi (a + b)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.eq_normEq0_cert.eq_1 : ∀ (c : ℕ) (p₁ p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.eq_normEq0_cert c p₁ p₂ p = (p₁.beq' (Lean.Grind.CommRing.Poly.num ↑c) && p.beq' (p₂.normEq0 c))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_eq_some_get!_of_contains : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)], m.contains a = true → m.get? a = some (m.get! a)
-- Init.Core
Std.IdempotentOp.mk : ∀ {α : Sort u} {op : α → α → α}, (∀ (x : α), op x x = x) → Std.IdempotentOp op
-- Mathlib.Data.Int.Init
Int.lt_div_iff_of_dvd_of_pos : ∀ {a b c : ℤ}, 0 < c → c ∣ b → (a < b / c ↔ c * a < b)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k} {fallback : α},
      (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).maxKeyD fallback =
        t.maxKey?.elim k fun k' => if compare k' k = Ordering.lt then k else k'
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
scalarSMulCLE_apply : ∀ (H : Type u_1) [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] (c : ℂˣ) (x : H),
  (scalarSMulCLE H c) x = c • x
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} {h : k' ∈ m.modify k f},
  (m.modify k f).getKey k' h = if (k == k') = true then k else m.getKey k' ⋯
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The map from the global sections `Γ(X)` to the sections on the (preimage of) a basic open.  -/
AlgebraicGeometry.LocallyRingedSpace.toToΓSpecMapBasicOpen : (X : AlgebraicGeometry.LocallyRingedSpace) →
  (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))) →
    X.presheaf.obj (Opposite.op ⊤) ⟶ X.presheaf.obj (Opposite.op (X.toΓSpecMapBasicOpen r))
-- Mathlib.Geometry.Euclidean.NinePointCircle
Affine.Simplex.ninePointCircle_restrict : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (S : AffineSubspace ℝ P)
  (hS : affineSpan ℝ (Set.range s.points) ≤ S),
  (s.restrict S hS).ninePointCircle = { center := ⟨s.ninePointCircle.center, ⋯⟩, radius := s.ninePointCircle.radius }
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn.match_1.splitter : (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1) →
  (x : Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
    (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos) →
      (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg) →
        (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both) →
          (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned) → motive x
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mk_eq_one : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Invertible R M] [Module.Free R M], CommRing.Pic.mk R M = 1
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Complex.Gamma_ofNat_eq_factorial : ∀ (n : ℕ) [inst : (n + 1).AtLeastTwo], Complex.Gamma (OfNat.ofNat (n + 1)) = ↑n.factorial
-- Mathlib.Analysis.RCLike.Basic
/-- The real part in an `RCLike` field, as a linear map.  -/
RCLike.reLm : {K : Type u_1} → [inst : RCLike K] → K →ₗ[ℝ] ℝ
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.stepAux.match_1.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ]
  (motive : Turing.TM1.Stmt Γ Λ σ → σ → Turing.Tape Γ → Sort u_4) (a : Γ → σ → Γ) (q : Turing.TM1.Stmt Γ Λ σ) (v : σ)
  (T : Turing.Tape Γ)
  (h_1 :
    (d : Turing.Dir) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.move d q) v T)
  (h_2 :
    (a : Γ → σ → Γ) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.write a q) v T)
  (h_3 :
    (s : Γ → σ → σ) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.load s q) v T)
  (h_4 :
    (p : Γ → σ → Bool) →
      (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.branch p q₁ q₂) v T)
  (h_5 : (l : Γ → σ → Λ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.goto l) v T)
  (h_6 : (v : σ) → (T : Turing.Tape Γ) → motive Turing.TM1.Stmt.halt v T),
  (match Turing.TM1.Stmt.write a q, v, T with
    | Turing.TM1.Stmt.move d q, v, T => h_1 d q v T
    | Turing.TM1.Stmt.write a q, v, T => h_2 a q v T
    | Turing.TM1.Stmt.load s q, v, T => h_3 s q v T
    | Turing.TM1.Stmt.branch p q₁ q₂, v, T => h_4 p q₁ q₂ v T
    | Turing.TM1.Stmt.goto l, v, T => h_5 l v T
    | Turing.TM1.Stmt.halt, v, T => h_6 v T) =
    h_2 a q v T