mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.OuterMeasure.Basic
/-- Let `μ` be an (outer) measure; let `s : ι → Set α` be a sequence of sets, `S = ⋃ n, s n`.
If `μ (S \ s n)` tends to zero along some nontrivial filter (usually `Filter.atTop` on `ι = ℕ`),
then `μ S = ⨆ n, μ (s n)`.  -/
MeasureTheory.measure_iUnion_of_tendsto_zero : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {ι : Type u_4}
  (μ : F) {s : ι → Set α} (l : Filter ι) [l.NeBot],
  Filter.Tendsto (fun k => μ ((⋃ n, s n) \ s k)) l (nhds 0) → μ (⋃ n, s n) = ⨆ n, μ (s n)
-- Init.Data.UInt.Lemmas
UInt32.eq_of_toBitVec_eq : ∀ {a b : UInt32}, a.toBitVec = b.toBitVec → a = b
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
instUniqueCarrierObjSSetTopCatToTopSimplexCategoryStdSimplexMkOfNatNat : Unique ↑(SSet.toTop.obj (SSet.stdSimplex.obj { len := 0 }))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.isPushout_iff_isColimit_binaryCofan_of_isThin : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [Quiver.IsThin C] {P X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y}
  {inl : X ⟶ P} {inr : Y ⟶ P},
  CategoryTheory.IsPushout f g inl inr ↔
    Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk inl inr))
-- Mathlib.Algebra.GCDMonoid.Nat
Int.nonneg_iff_normalize_eq_self : ∀ (z : ℤ), normalize z = z ↔ 0 ≤ z
-- Mathlib.RingTheory.Unramified.Basic
/-- An `R`-algebra `A` is formally unramified if `Ω[A⁄R]` is trivial.

This is equivalent to "for every `R`-algebra, every square-zero ideal
`I : Ideal B` and `f : A →ₐ[R] B ⧸ I`, there exists at most one lift `A →ₐ[R] B`".
See `Algebra.FormallyUnramified.iff_comp_injective`.  -/
Algebra.FormallyUnramified : (R : Type v) → (A : Type u) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → Prop
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
/-- The tensor product of two quadratic forms, a shorthand for dot notation.  -/
QuadraticForm.tmul : {R : Type uR} →
  {A : Type uA} →
    {M₁ : Type uM₁} →
      {M₂ : Type uM₂} →
        [inst : CommRing R] →
          [inst_1 : CommRing A] →
            [inst_2 : AddCommGroup M₁] →
              [inst_3 : AddCommGroup M₂] →
                [inst_4 : Algebra R A] →
                  [inst_5 : Module R M₁] →
                    [inst_6 : Module A M₁] →
                      [inst_7 : SMulCommClass R A M₁] →
                        [IsScalarTower R A M₁] →
                          [inst_9 : Module R M₂] →
                            [Invertible 2] →
                              QuadraticForm A M₁ → QuadraticForm R M₂ → QuadraticForm A (TensorProduct R M₁ M₂)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS.eq_def : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denoteS ctx p =
    match p with
    | Lean.Grind.CommRing.Poly.num k => Lean.Grind.CommRing.denoteSInt k
    | Lean.Grind.CommRing.Poly.add k m p =>
      Lean.Grind.CommRing.denoteSInt k * Lean.Grind.CommRing.Mon.denote ctx m + Lean.Grind.CommRing.Poly.denoteS ctx p
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.Retract.hasProjectiveDimensionLT : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (h : CategoryTheory.Retract X Y) (n : ℕ) [CategoryTheory.HasProjectiveDimensionLT Y n],
  CategoryTheory.HasProjectiveDimensionLT X n
-- Mathlib.Algebra.Group.Submonoid.Units
/-- The equivalence between the additive subgroup of additive units of
`S` and the additive submonoid of additive unit elements of `S`.  -/
AddSubgroup.ofAddUnitsTopEquiv : {M : Type u_1} → [inst : AddMonoid M] → ↥⊤.ofAddUnits ≃+ AddUnits M
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.instGroupCarrierToGrp : (G : FiniteGrp.{u_1}) → Group ↑G.toGrp
-- Lean.CoreM
Lean.Core.SavedState : Type
-- Mathlib.Data.Finset.Density
Finset.dens_sdiff_add_dens : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] (s t : Finset α), (s \ t).dens + t.dens = (s ∪ t).dens
-- Mathlib.RingTheory.Derivation.Basic
/-- If `A` is both an `R`-algebra and an `S`-algebra; `M` is both an `R`-module and an `S`-module,
then an `S`-derivation `A → M` is also an `R`-derivation if it is also `R`-linear.  -/
Derivation.restrictScalars : (R : Type u_1) →
  {A : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module A M] →
                [inst_5 : Module R M] →
                  {S : Type u_5} →
                    [inst_6 : CommSemiring S] →
                      [inst_7 : Algebra S A] →
                        [inst_8 : Module S M] → [LinearMap.CompatibleSMul A M R S] → Derivation S A M → Derivation R A M
-- Lean.Elab.Do.Basic
Lean.Elab.Do.MonadInfo.mk.sizeOf_spec : ∀ (m : Lean.Expr) (u v : Lean.Level) (cachedPUnit cachedPUnitUnit : Lean.Expr),
  sizeOf { m := m, u := u, v := v, cachedPUnit := cachedPUnit, cachedPUnitUnit := cachedPUnitUnit } =
    1 + sizeOf m + sizeOf u + sizeOf v + sizeOf cachedPUnit + sizeOf cachedPUnitUnit
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.bot_degree : ∀ {V : Type u_1} [inst : Fintype V] (v : V), ⊥.degree v = 0
-- Lean.Meta.GeneralizeTelescope
Lean.Meta.GeneralizeTelescope.Entry.type : Lean.Meta.GeneralizeTelescope.Entry → Lean.Expr
-- Mathlib.Logic.Relation
Relation.onFun_map_onFun_iff_onFun : ∀ {α : Type u_1} {β : Type u_2} {r : β → β → Prop} (f : α → β) (a₁ a₂ : α),
  Relation.Map (Function.onFun r f) f f (f a₁) (f a₂) ↔ r (f a₁) (f a₂)
-- Mathlib.CategoryTheory.Limits.Shapes.SingleObj
CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient_apply : ∀ {G : Type v} [inst : Group G] (J : CategoryTheory.Functor (CategoryTheory.SingleObj G) (Type u))
  (a : Quot J.ColimitTypeRel),
  (CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient J) a = Quot.lift (fun p => ⟦p.snd⟧) ⋯ a
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- The normal subgroups correspond to the additive congruence relations on an `AddGroup`.  -/
AddSubgroup.orderIsoAddCon : {G : Type u_1} → [inst : AddGroup G] → { N // N.Normal } ≃o AddCon G
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.instT2Space : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] [T2Space B], T2Space (A →ₜ* B)
-- Mathlib.Algebra.Order.Ring.Defs
instNoMinOrderOfNontrivial : ∀ {R : Type u} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Nontrivial R], NoMinOrder R
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.coe_apply : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (x : K), v x = ↑v x
-- Batteries.Data.PairingHeap
/-- `O(1)`. Add element `a` to the given heap `h`.  -/
Batteries.PairingHeap.insert : {α : Type u} → {le : α → α → Bool} → α → Batteries.PairingHeap α le → Batteries.PairingHeap α le
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A functor `F : C ⥤ D` reflects (small) limits if
whenever the image of a cone over some `K : J ⥤ C` under `F` is a limit cone in `D`,
the cone was already a limit cone in `C`.
Note that we do not assume a priori that `D` actually has any limits.
 -/
CategoryTheory.Limits.ReflectsLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.exists_coprime_of_gcd_pos : ∀ {d : ℤ} {a : ℤ√d}, 0 < a.re.gcd a.im → ∃ b, a = ↑↑(a.re.gcd a.im) * b ∧ IsCoprime b.re b.im
-- Init.Data.List.Basic
List.empty_eq : ∀ {α : Type u}, ∅ = []
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_fract_left : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] [IsTopologicalAddGroup α] (n : ℤ),
  Filter.Tendsto Int.fract (nhdsWithin (↑n) (Set.Iio ↑n)) (nhdsWithin 1 (Set.Iio 1))
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.add_mul_succ : ∀ {a b : Ordinal.{u_4}} (c : Ordinal.{u_4}), b + a = a → (a + b) * Order.succ c = a * Order.succ c + b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_diff_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → Std.DHashMap.Raw.Const.get! (m₁.diff m₂) k = default
-- Init.Data.BitVec.Lemmas
/-- 2^i * 2^j = 2^(i + j) with bitvectors as well  -/
BitVec.twoPow_mul_twoPow_eq : ∀ {w : ℕ} (i j : ℕ), BitVec.twoPow w i * BitVec.twoPow w j = BitVec.twoPow w (i + j)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instNonUnitalRing : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : NonUnitalRing R] → [IsTopologicalRing R] → NonUnitalRing (SeparationQuotient R)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Complex.GammaSeq_eq_approx_Gamma_integral : ∀ {s : ℂ}, 0 < s.re → ∀ {n : ℕ}, n ≠ 0 → s.GammaSeq n = ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
-- Mathlib.LinearAlgebra.Dimension.Free
/-- A finite rank free module has a basis indexed by `Fin (finrank R M)`.  -/
Module.finBasis : (R : Type u) →
  (M : Type v) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          [Module.Free R M] →
            [StrongRankCondition R] → [Module.Finite R M] → Module.Basis (Fin (Module.finrank R M)) R M
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.coe_coe : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂), ⇑↑e = ⇑e
-- Init.Data.List.MinMaxIdx
List.minIdxOn.congr_simp : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] {inst_1 : DecidableLE β} [inst_2 : DecidableLE β] (f f_1 : α → β),
  f = f_1 → ∀ (xs xs_1 : List α) (e_xs : xs = xs_1) (h : xs ≠ []), List.minIdxOn f xs h = List.minIdxOn f_1 xs_1 ⋯
-- Mathlib.Algebra.Algebra.Unitization
Unitization.fst_zero : ∀ {R : Type u_3} {A : Type u_4} [inst : Zero R] [inst_1 : Zero A], (Unitization.toProd 0).1 = 0
-- Mathlib.Analysis.Normed.Algebra.Spectrum
_private.Mathlib.Analysis.Normed.Algebra.Spectrum.0.spectrum.termρ : Lean.ParserDescr
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.IsSwap.of_subtype_isSwap : ∀ {α : Type u_1} [inst : DecidableEq α] {p : α → Prop} [inst_1 : DecidablePred p] {f : Equiv.Perm (Subtype p)},
  f.IsSwap → (Equiv.Perm.ofSubtype f).IsSwap
-- Init.Control.Lawful.Basic
seqLeft_pure : ∀ {f : Type u_1 → Type u_2} {α β : Type u_1} [inst : Applicative f] [LawfulApplicative f] (x : f α) (y : β),
  x <* pure y = x
-- Mathlib.Data.Set.Sigma
Set.preimage_sigmaMap_sigma : ∀ {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} {α' : ι' → Type u_7} (f : ι → ι') (g : (i : ι) → α i → α' (f i))
  (s : Set ι') (t : (i : ι') → Set (α' i)), Sigma.map f g ⁻¹' s.sigma t = (f ⁻¹' s).sigma fun i => g i ⁻¹' t (f i)
-- Mathlib.Algebra.Order.Star.Basic
NonUnitalStarRingHom.map_le_map_of_map_star : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [StarOrderedRing R] [inst_4 : NonUnitalSemiring S] [inst_5 : PartialOrder S] [inst_6 : StarRing S] [StarOrderedRing S]
  (f : R →⋆ₙ+* S) {x y : R}, x ≤ y → f x ≤ f y
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.normalizer_inf_normalizer_le_normalizer_sup : ∀ {G : Type u_2} [inst : Group G] (H K : Subgroup G),
  Subgroup.normalizer ↑H ⊓ Subgroup.normalizer ↑K ≤ Subgroup.normalizer ↑(H ⊔ K)
-- Lean.Parser.Types
Lean.Parser.CacheableParserContext.forbiddenTk? : Lean.Parser.CacheableParserContext → Option Lean.Parser.Token
-- Mathlib.Algebra.Ring.CompTypeclasses
/-- Swap the direction of a `RingHomInvPair`. This is not an instance as it would loop, and better
instances are often available and may often be preferable to using this one. Indeed, this
declaration is not currently used in mathlib.
 -/
RingHomInvPair.symm : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] (σ₁₂ : R₁ →+* R₂) (σ₂₁ : R₂ →+* R₁)
  [RingHomInvPair σ₁₂ σ₂₁], RingHomInvPair σ₂₁ σ₁₂
-- Mathlib.Analysis.Normed.Lp.lpSpace
LipschitzWith.uniformly_bounded : ∀ {α : Type u_3} {ι : Type u_5} [inst : PseudoMetricSpace α] (g : α → ι → ℝ) {K : NNReal},
  (∀ (i : ι), LipschitzWith K fun x => g x i) → ∀ (a₀ : α), Memℓp (g a₀) ⊤ → ∀ (a : α), Memℓp (g a) ⊤
-- Mathlib.Data.Nat.Log
Nat.log.go.eq_1 : ∀ (n a : ℕ), Nat.log.go n a 0 = (n, 0)
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- We say that the action of `M` on `α` has `MeasurableConstSMul` if for each `c` the map
`x ↦ c • x` is a measurable function.  -/
MeasurableConstSMul : (M : Type u_2) → (α : Type u_3) → [SMul M α] → [MeasurableSpace α] → Prop
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_comon_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (A : CategoryTheory.Functor C D) [inst_3 : CategoryTheory.ComonObj A]
  (X : C), CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit.app X
-- Mathlib.Order.CompleteLattice.Lemmas
iSup_nat_gt_zero_eq : ∀ {α : Type u_1} [inst : CompleteLattice α] (f : ℕ → α), ⨆ i, ⨆ (_ : i > 0), f i = ⨆ i, f (i + 1)
-- Mathlib.Algebra.Group.Submonoid.Support
AddSubmonoid.IsSpanning.maximal_isPointed : ∀ {G : Type u_1} [inst : AddGroup G] {M : AddSubmonoid G}, M.IsPointed → M.IsSpanning → Maximal AddSubmonoid.IsPointed M
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prodOpEquiv_counitIso_inv_app : ∀ (C : Type u₃) [inst : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [inst_1 : CategoryTheory.Category.{v₄, u₄} D]
  (X : Cᵒᵖ × Dᵒᵖ),
  (CategoryTheory.prodOpEquiv C).counitIso.inv.app X =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.u_l_u_eq_u : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ (b : β), u (l (u b)) = u b
-- Batteries.Data.Array.Scan
Array.back_scanl : ∀ {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : Array α},
  (Array.scanl f init as).back ⋯ = Array.foldl f init as
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.continuousLinearEquivAt_apply : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : Bundle.Trivialization.IsLinear R e] (b : B)
  (hb : b ∈ e.baseSet), ⇑(Bundle.Trivialization.continuousLinearEquivAt R e b hb) = fun y => (↑e ⟨b, y⟩).2
-- Lean.Elab.Tactic.Simp
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.elabDSimpConfigCore.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Lean.Meta.DSimp.ConfigWithOptions
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.tr.match_1.eq_12 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1)
  (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 Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt 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_12 ()
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.CommMon C)
-- Mathlib.LinearAlgebra.Prod
LinearMap.prodEquiv_symm_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} (S : Type u_3) [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid M₃] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module S M₂] [inst_9 : Module S M₃]
  [inst_10 : SMulCommClass R S M₂] [inst_11 : SMulCommClass R S M₃] (f : M →ₗ[R] M₂ × M₃),
  (LinearMap.prodEquiv S).symm f = (LinearMap.fst R M₂ M₃ ∘ₗ f, LinearMap.snd R M₂ M₃ ∘ₗ f)
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.div_mul_cancel_right : ∀ {α : Type u} [inst : DivisionMonoid α] {b : α}, IsUnit b → ∀ (a : α), b / (a * b) = a⁻¹
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsIso.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  (∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P f → P (CategoryTheory.CategoryStruct.comp e.hom f)) →
    (∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), P f → P (CategoryTheory.CategoryStruct.comp f e.hom)) → P.RespectsIso
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
/-- If the spectrum of an element restricts to a smaller scalar ring, then a continuous functional
calculus over the larger scalar ring descends to the smaller one.  -/
SpectrumRestricts.starAlgHom : {R : Type u} →
  {S : Type v} →
    {A : Type w} →
      [inst : Semifield R] →
        [inst_1 : StarRing R] →
          [inst_2 : TopologicalSpace R] →
            [inst_3 : IsTopologicalSemiring R] →
              [inst_4 : ContinuousStar R] →
                [inst_5 : Semifield S] →
                  [inst_6 : StarRing S] →
                    [inst_7 : TopologicalSpace S] →
                      [inst_8 : IsTopologicalSemiring S] →
                        [inst_9 : ContinuousStar S] →
                          [inst_10 : Ring A] →
                            [inst_11 : StarRing A] →
                              [inst_12 : Algebra R S] →
                                [inst_13 : Algebra R A] →
                                  [inst_14 : Algebra S A] →
                                    [IsScalarTower R S A] →
                                      [StarModule R S] →
                                        [ContinuousSMul R S] →
                                          {a : A} →
                                            (C(↑(spectrum S a), S) →⋆ₐ[S] A) →
                                              {f : C(S, R)} → SpectrumRestricts a ⇑f → C(↑(spectrum R a), R) →⋆ₐ[R] A
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_le_iff_of_exists : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n i : ι} {ω : Ω} [WellFoundedLT ι] {m : ι},
  (∃ j ∈ Set.Icc n m, u j ω ∈ s) → (MeasureTheory.hittingBtwn u s n m ω ≤ i ↔ ∃ j ∈ Set.Icc n i, u j ω ∈ s)
-- Mathlib.Order.Interval.Set.OrdConnected
Set.image_subtype_val_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [s.OrdConnected] (x y : ↑s), Subtype.val '' Set.Ioo x y = Set.Ioo ↑x ↑y
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_23 : HSub Std.Time.Minute.Offset Std.Time.Week.Offset Std.Time.Minute.Offset
-- Mathlib.Algebra.Ring.Int.Parity
Int.add_one_ediv_two_mul_two_of_odd : ∀ {n : ℤ}, Odd n → 1 + n / 2 * 2 = n
-- Mathlib.Data.Finset.Basic
Finset.erase_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Finset α), s.erase a ∩ t = (s ∩ t).erase a
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct
SSet.innerAnodyneExtensions.whiskerLeft : ∀ {X Y : SSet} {f : X ⟶ Y},
  SSet.innerAnodyneExtensions f →
    ∀ (Z : SSet), SSet.innerAnodyneExtensions (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- Any morphism of light profinite spaces is a closed map.  -/
LightProfinite.isClosedMap : ∀ {X Y : LightProfinite} (f : X ⟶ Y), IsClosedMap ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.RingTheory.FractionalIdeal.Extended
/-- **Alias** of `FractionalIdeal.extendedHom_coeIdeal_eq_map`. -/
FractionalIdeal.extendedHomₐ_coeIdeal_eq_map : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] (I : Ideal A), (FractionalIdeal.extendedHom L B) ↑I = ↑(Ideal.map (algebraMap A B) I)
-- Init.Data.UInt.Bitwise
USize.neg_one_and : ∀ {a : USize}, -1 &&& a = a
-- Std.Time.Format.Basic
Std.Time.Awareness.any.sizeOf_spec : sizeOf Std.Time.Awareness.any = 1
-- Init.Data.AC
_private.Init.Data.AC.0.Option.isSome.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (val : α) → motive (some val)) (h_2 : Unit → motive none),
  (match none with
    | some val => h_1 val
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Order.WithBot
WithBot.coe_unbot : ∀ {α : Type u_1} (x : WithBot α) (hx : x ≠ ⊥), ↑(x.unbot hx) = x
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.edist_toLp_snd : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (y₁ y₂ : β), edist (WithLp.toLp p (0, y₁)) (WithLp.toLp p (0, y₂)) = edist y₁ y₂
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.add_mem_add_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A} {r s : R},
  r + s ∈ spectrum R ((algebraMap R A) s + a) ↔ r ∈ spectrum R a