mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.mapIdIso.eq_1 : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat),
  CategoryTheory.Pseudofunctor.CoGrothendieck.mapIdIso F =
    CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_add_right_nhdsNE : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {c a : G},
  Filter.map (fun x => x + c) (nhdsWithin a {a}ᶜ) = nhdsWithin (a + c) {a + c}ᶜ
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- A symbol above `i` that does not occur in a word in `S p i` can be inserted while
preserving strict monotonicity.  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.exists_insertNth_mem_S : ∀ {n p : ℕ} {i : Fin n} {α : Fin p → Fin n} {k : Fin n},
  α ∈ BirdDet.S✝ p i → i < k → k ∉ Set.range α → ∃ t, t.insertNth k α ∈ BirdDet.S✝ (p + 1) i
-- Mathlib.Topology.Connected.Basic
ConnectedSpace.toPreconnectedSpace : ∀ {α : Type u} {inst : TopologicalSpace α} [self : ConnectedSpace α], PreconnectedSpace α
-- Mathlib.Order.Defs.PartialOrder
/-- `CovBy a b` means that `b` covers `a`. This means that `a < b` and there is no element in
between. This is denoted `a ⋖ b`.  -/
«term_⋖_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.addLinearEquiv_symm_apply' : ∀ {R : Type u_1} [inst : Semiring R] {m n : ℕ} (PQ : ↥(Polynomial.degreeLT R m) × ↥(Polynomial.degreeLT R n)),
  ↑((Polynomial.degreeLT.addLinearEquiv R m n).symm PQ) = ↑PQ.1 + Polynomial.X ^ m * ↑PQ.2
-- Mathlib.AlgebraicGeometry.AlgClosed.Basic
AlgebraicGeometry.pointEquivClosedPoint_symm_apply_coe : ∀ {X : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] [inst_1 : IsAlgClosed K]
  (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [inst_2 : AlgebraicGeometry.LocallyOfFiniteType f]
  (x : ↑(closedPoints ↥X)),
  ↑((AlgebraicGeometry.pointEquivClosedPoint f).symm x) = AlgebraicGeometry.pointOfClosedPoint f ↑x ⋯
-- Mathlib.Geometry.RingedSpace.Basic
AlgebraicGeometry.RingedSpace.res_zero : ∀ {X : AlgebraicGeometry.RingedSpace} {U V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (hUV : U ≤ V),
  TopCat.Presheaf.restrictOpen 0 U hUV = 0
-- Init.Data.Order.Ord
/-- A typeclass for types with a transitive ordering function.  -/
Std.TransOrd : (α : Type u) → [Ord α] → Prop
-- Mathlib.Topology.Order.Basic
tendstoIccClassNhds : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] (a : α),
  Filter.TendstoIxxClass Set.Icc (nhds a) (nhds a)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.mapAlgHom_apply : ∀ {σ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {B : Type u_4} [inst_3 : Semiring B] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) (f : MvPowerSeries σ A),
  (MvPowerSeries.mapAlgHom φ) f = (MvPowerSeries.map ↑φ) f
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.sndX_inrX : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i : ι),
  ¬c.Rel i (c.next i) →
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ i)
        (HomologicalComplex.homotopyCofiber.inrX φ i) =
      CategoryTheory.CategoryStruct.id (HomologicalComplex.homotopyCofiber.X φ i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_two_pi_sub : ∀ (x : ℂ), Complex.sin (2 * ↑Real.pi - x) = -Complex.sin x
-- Mathlib.Data.ZMod.Units
ZMod.coe_int_isUnit_iff_isCoprime : ∀ (n : ℤ) (m : ℕ), IsUnit ↑n ↔ IsCoprime (↑m) n
-- Lean.Meta.Tactic.Repeat
_private.Lean.Meta.Tactic.Repeat.0.List.map_unattach.match_1.eq_1 : ∀ {α : Type u_1} {P : α → Prop} (motive : Subtype P → Sort u_2) (x : α) (h : P x)
  (h_1 : (x : α) → (h : P x) → motive ⟨x, h⟩),
  (match ⟨x, h⟩ with
    | ⟨x, h⟩ => h_1 x h) =
    h_1 x h
-- Mathlib.Order.MinMax
instCommutativeMax : ∀ {α : Type u} [inst : LinearOrder α], Std.Commutative max
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.projectiveDimension_ne_top_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C),
  CategoryTheory.projectiveDimension X ≠ ⊤ ↔ ∃ n, CategoryTheory.HasProjectiveDimensionLE X n
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
topologicalClosure_addSubgroupClosure_toAddSubmonoid : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [CompactSpace G] [inst_3 : IsTopologicalAddGroup G]
  (s : Set G), (AddSubgroup.closure s).topologicalClosure = (AddSubmonoid.closure s).topologicalClosure
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.ext_iff : ∀ {A : Type u} {inst : Ring A} {relations : Module.Relations A} {M : Type v} {inst_1 : AddCommGroup M}
  {inst_2 : Module A M} {x y : relations.Solution M}, x = y ↔ x.var = y.var
-- Mathlib.Order.Category.PartOrdEmb
/-- Auxiliary definition for `isColimitCocone`.  -/
PartOrdEmb.Limits.CoconePt.desc : {J : Type u} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      {F : CategoryTheory.Functor J PartOrdEmb} →
        {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))} →
          (hc : CategoryTheory.Limits.IsColimit c) →
            (s : CategoryTheory.Limits.Cocone F) → PartOrdEmb.Limits.CoconePt hc ↪o ↑s.pt
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.Λ'.normal.sizeOf_spec : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : SizeOf Γ] [inst_1 : SizeOf Λ] [inst_2 : SizeOf σ] (a : Λ),
  sizeOf (Turing.TM1to1.Λ'.normal a) = 1 + sizeOf a
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If `g` and `h` commute, then `g` fixes `(h ^ j) • x` iff `g` fixes `x`.
 -/
MulAction.smul_zpow_fixedBy_eq_of_commute : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g h : G},
  Commute g h → ∀ (j : ℤ), h ^ j • MulAction.fixedBy α g = MulAction.fixedBy α g
-- Init.Data.Int.Order
Int.zero_max_negSucc : ∀ (n : ℕ), max 0 (Int.negSucc n) = 0
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.symmetry.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [inst_2 : F.Full],
  hf'.symmetry hg = hg.lift' (hf'.snd g) (hf'.fst' g) ⋯
-- Mathlib.Algebra.Order.Ring.Basic
Odd.pow_inj : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {n : ℕ},
  Odd n → ∀ {a b : R}, a ^ n = b ^ n ↔ a = b
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.integral_withDensity : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : β → E}
  [inst_2 : ProbabilityTheory.IsSFiniteKernel κ] {a : α} {g : α → β → NNReal},
  Measurable (Function.uncurry g) → ∫ (b : β), f b ∂(κ.withDensity fun a b => ↑(g a b)) a = ∫ (b : β), g a b • f b ∂κ a
-- Lean.Meta.Canonicalizer
_private.Lean.Meta.Canonicalizer.0.Lean.Meta.Canonicalizer.mkKey.unsafe_impl_2 : Lean.Expr → Lean.Meta.Canonicalizer.State → Option UInt64
-- Mathlib.CategoryTheory.InducedCategory
/-- The forgetful functor from an induced category to the original category,
forgetting the extra data.
 -/
CategoryTheory.inducedFunctor : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v, u₂} D] →
      (F : C → D) → CategoryTheory.Functor (CategoryTheory.InducedCategory D F) D
-- Lean.Compiler.IR.Basic
Lean.IR.addVarRename : Lean.IR.IndexRenaming → ℕ → ℕ → Lean.IR.IndexRenaming
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteAtFilter.inf_of_right : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : Filter α},
  μ.FiniteAtFilter g → μ.FiniteAtFilter (f ⊓ g)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.ae.neBot : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NeZero μ], (MeasureTheory.ae μ).NeBot
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabOmit : Lean.Elab.Command.CommandElab
-- Mathlib.Data.Nat.Squarefree
Nat.prod_primeFactors_sdiff_of_squarefree : ∀ {n : ℕ}, Squarefree n → ∀ {t : Finset ℕ}, t ⊆ n.primeFactors → ∏ a ∈ n.primeFactors \ t, a = n / ∏ a ∈ t, a
-- Init.SimpLemmas
forall_false : ∀ (p : False → Prop), (∀ (h : False), p h) = True
-- Std.Http.Data.Headers.Value
/-- Attempts to create a `Value` from a `String`, returning `none` if the string contains invalid characters
for HTTP header values.
 -/
Std.Http.Header.Value.ofString? : String → Option Std.Http.Header.Value
-- Init.Data.BitVec.Basic
BitVec.and_eq : ∀ {w : ℕ} (x y : BitVec w), x.and y = x &&& y
-- Mathlib.Data.Set.Prod
Set.prod_sdiff_diagonal : ∀ {α : Type u_1} (s : Set α), s ×ˢ s \ Set.diagonal α = s.offDiag
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj : ∀ (C : CategoryTheory.Cat),
  CategoryTheory.WithTerminal.prelaxfunctor.obj C = CategoryTheory.Cat.of (CategoryTheory.WithTerminal ↑C)
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprBinderInfo_mathlib.toExpr : Lean.BinderInfo → Lean.Expr
-- Mathlib.RingTheory.Valuation.Integers
Valuation.integers_nontrivial : ∀ {R : Type u} {Γ₀ : Type v} [inst : CommRing R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀),
  Nontrivial ↥v.integer ↔ Nontrivial R
-- Std.Data.DTreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the key-value pair with the smallest key.
 -/
Std.DTreeMap.minEntry : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → (t : Std.DTreeMap α β cmp) → t.isEmpty = false → (a : α) × β a
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.smul_zero : ∀ {R : Type u_1} {R' : Type u_4} [inst : CommSemiring R] [inst_1 : Monoid R'] {M : Type u_7} {N : Type u_8}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : DistribMulAction R' M] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : SMulCommClass R R' M] (r : R'), r • 0 = 0
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.OuterMeasure.ext_iff : ∀ {α : Type u_1} {μ₁ μ₂ : MeasureTheory.OuterMeasure α}, μ₁ = μ₂ ↔ ∀ (s : Set α), μ₁ s = μ₂ s
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.sub : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f g : α → β}, MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → MeasureTheory.Integrable (f - g) μ
-- Init.Data.List.Lemmas
List.append_eq_append_iff : ∀ {α : Type u_1} {ws xs ys zs : List α},
  ws ++ xs = ys ++ zs ↔ (∃ as, ys = ws ++ as ∧ xs = as ++ zs) ∨ ∃ bs, ws = ys ++ bs ∧ zs = bs ++ xs
-- Mathlib.Data.Set.Prod
/-- **Line test** for equivalences.

Let `f : α → β × γ` be a homomorphism to a product of monoids. Assume that `f` is surjective on both
factors and that the image of `f` intersects every "vertical line" `{(b, c) | c : γ}` and every
"horizontal line" `{(b, c) | b : β}` at most once. Then the image of `f` is the graph of some
equivalence `f' : β ≃ γ`.  -/
Set.exists_equiv_range_eq_graphOn_univ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β × γ},
  Function.Surjective (Prod.fst ∘ f) →
    Function.Surjective (Prod.snd ∘ f) →
      (∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) → ∃ e, Set.range f = Set.graphOn (⇑e) Set.univ
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.mem_extChartAt_ind_source : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs : SmoothBumpCovering ι I M s) (x : M)
  (hx : x ∈ s), x ∈ (extChartAt I (fs.c (fs.ind x hx))).source
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis_ne_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K),
  NumberField.mixedEmbedding.norm
      (NumberField.mixedEmbedding.mixedSpaceOfRealSpace (↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x)) ≠
    0
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_congr : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s : Set α} {f g : α → M},
  Set.EqOn f g s → s.indicator f = s.indicator g
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.coprodAssoc_symm_apply_inr_inr : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid P] (x : P),
  (MulEquiv.coprodAssoc M N P).symm (Monoid.Coprod.inr (Monoid.Coprod.inr x)) = Monoid.Coprod.inr x
-- Std.Async.IO
Std.Async.IO.AsyncWrite.flush : {α : Type} → (β : Type) → [self : Std.Async.IO.AsyncWrite α β] → α → Std.Async.Async Unit
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.contains_alter_of_beq_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  m.WF → (k == k') = false → (Std.DHashMap.Raw.Const.alter m k f).contains k' = m.contains k'
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.rightLeft.sizeOf_spec : sizeOf Lean.Meta.Grind.EMatchTheoremKind.rightLeft = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.homOfLE.congr_simp : ∀ {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ ≤ S₂), SSet.Subcomplex.homOfLE h = SSet.Subcomplex.homOfLE h
-- Mathlib.Topology.Order.T5
Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {a : X} {s t : Set X},
  Disjoint s (closure t) → a ∈ s → (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ nhdsWithin a (Set.Ici a)
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles._auto_1),
  (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).X₃ = X.opcycles f g n₁
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.obj_limit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j : J} (iter : Φ.Iteration j)
  (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
  iter.F.obj ⟨i, hij⟩ = CategoryTheory.Limits.colimit (CategoryTheory.SmallObject.restrictionLT iter.F hij)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.tr.match_1.eq_7 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (q₁ q₂ : Turing.PartrecToTM2.Λ')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (f : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k f q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 :
    (fs : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k)))
  (h_9 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k.cons₂))
  (h_10 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k)))
  (h_11 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k)))
  (h_12 : Unit → motive (Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt)),
  (match q₁.pred q₂ with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k f q => h_2 k f q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k) => h_8 fs k
    | Turing.PartrecToTM2.Λ'.ret k.cons₂ => h_9 k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k) => h_10 f k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k) => h_11 f k
    | Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt => h_12 ()) =
    h_7 q₁ q₂
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.mk : {α : Type u_6} → [T : TopologicalSpace α] → (σ : Type u_5) → (F : Ctop α σ) → F.toTopsp = T → Ctop.Realizer α
-- Mathlib.Geometry.Euclidean.Projection
/-- If the distance from `p₁` to its orthogonal projection equals its distance to a point in `s`,
the orthogonal projection is that point.  -/
EuclideanGeometry.dist_orthogonalProjection_eq_dist_iff_eq_of_mem : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : s.direction.HasOrthogonalProjection] {p₁ p₂ : P} (hp₂ : p₂ ∈ s),
  dist p₁ ↑((EuclideanGeometry.orthogonalProjection s) p₁) = dist p₁ p₂ ↔
    ↑((EuclideanGeometry.orthogonalProjection s) p₁) = p₂
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.indicator₀ : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} [inst_1 : Zero β],
  AEMeasurable f μ → ∀ {s : Set α}, MeasureTheory.NullMeasurableSet s μ → AEMeasurable (s.indicator f) μ
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_add_mul_of_isPrincipal_add : ∀ (a : Ordinal.{u}) {b : Ordinal.{u}},
  b ≠ 1 → Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) b → Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) (a * b)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.ofList_cons : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {k : α} {v : β} {tl : List (α × β)},
  Std.HashMap.Raw.ofList ((k, v) :: tl) = (∅.insert k v).insertMany tl
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.BilinMap.toQuadraticMap_sub : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (B₁ B₂ : LinearMap.BilinMap R M N),
  (B₁ - B₂).toQuadraticMap = B₁.toQuadraticMap - B₂.toQuadraticMap
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.outerDone_flatMap_pure : ∀ {α β α₂ γ : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterator α₂ Id γ] {f : β → Std.Iter γ}
  {it₁ : Std.Iter β},
  it₁.IsPlausibleStep Std.IterStep.done → (Std.Iter.flatMapAfter f it₁ none).IsPlausibleStep Std.IterStep.done
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.coe_rpow_def : ∀ (x : NNReal) (y : ℝ), ↑x ^ y = if x = 0 ∧ y < 0 then ⊤ else ↑(x ^ y)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.rotate_eq_nil : ∀ {V : Type u} {G : SimpleGraph V} {v u : V} [inst : DecidableEq V] {c : G.Walk v v} (h : u ∈ c.support),
  c.rotate u h = SimpleGraph.Walk.nil ↔ c = SimpleGraph.Walk.nil
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.le_degree : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ ℕ},
  d ∈ f.support → m.toSyn d ≤ m.toSyn (m.degree f)
-- Mathlib.Analysis.LocallyConvex.AbsConvex
absConvex_convexClosedHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] [inst_4 : TopologicalSpace E] {s : Set E}, AbsConvex 𝕜 ((closedAbsConvexHull 𝕜) s)
-- Mathlib.Analysis.Normed.Group.Uniform
LocallyLipschitz.div : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {f g : α → E},
  LocallyLipschitz f → LocallyLipschitz g → LocallyLipschitz fun x => f x / g x
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →ₗ[𝕜] E), T.IsSymmetric = ∀ (x y : E), inner 𝕜 (T x) y = inner 𝕜 x (T y)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Heterobasic version of `TensorProduct.mk`:

The canonical bilinear map `M →[A] N →[R] M ⊗[R] N`.  -/
TensorProduct.AlgebraTensorModule.mk : (R : Type uR) →
  [inst : CommSemiring R] →
    (A : Type u_1) →
      (M : Type u_2) →
        (N : Type u_3) →
          [inst_1 : Semiring A] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : Module R M] →
                [inst_4 : Module A M] →
                  [inst_5 : SMulCommClass R A M] →
                    [inst_6 : AddCommMonoid N] → [inst_7 : Module R N] → M →ₗ[A] N →ₗ[R] TensorProduct R M N
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.blsub_id : ∀ (o : Ordinal.{u}), (o.blsub fun x x_1 => x) = o
-- Init.Data.Iterators.PostconditionMonad
/-- Lifts a monadic value from `m { a : α // P a }` to a value `PostconditionT m α`.
 -/
Std.Iterators.PostconditionT.liftWithProperty : {α : Type w} → {m : Type w → Type w'} → {P : α → Prop} → m { α // P α } → Std.Iterators.PostconditionT m α
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : CategoryTheory.Cat) {X Y Z : CategoryTheory.Join C ↑D}
  (a : X.Hom Y) (a_1 : Y.Hom Z), CategoryTheory.CategoryStruct.comp a a_1 = CategoryTheory.Join.comp a a_1
-- Lean.Message
/-- The content of the message.  -/
Lean.BaseMessage.data : {α : Type u} → Lean.BaseMessage α → α
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- Equivalence expressing that two morphisms are homotopic iff
their difference is homotopic to zero.  -/
CategoryTheory.ShortComplex.Homotopy.equivSubZero : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ₁ φ₂ : S₁ ⟶ S₂) →
          CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ ≃ CategoryTheory.ShortComplex.Homotopy (φ₁ - φ₂) 0
-- Init.Internal.Order.Basic
Lean.Order.ind_not : ∀ {α : Sort u_1} [inst : Lean.Order.PartialOrder α] (f₁ : α → Prop),
  Lean.Order.monotone f₁ → Lean.Order.monotone fun x => ¬f₁ x
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_mul_X : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {x : R},
  Polynomial.eval x (p * Polynomial.X) = Polynomial.eval x p * x