mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.image_isVonNBounded_iff_finset_seminorm_bounded : ∀ {𝕜 : Type u_2} {E : Type u_6} {G : Type u_8} {ι : Type u_9} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [inst_3 : TopologicalSpace E] (f : G → E)
  {s : Set G},
  WithSeminorms p → (Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) (f x) < r)
-- Mathlib.Data.Finsupp.Order
Finsupp.decidableLT : {ι : Type u_1} →
  {α : Type u_3} →
    [inst : AddCommMonoid α] →
      [inst_1 : PartialOrder α] → [CanonicallyOrderedAdd α] → [DecidableLE α] → DecidableLT (ι →₀ α)
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.prop_initial : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [inst_2 : CategoryTheory.Limits.HasInitial C],
  P (⊥_ C)
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.span_range_derivation : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) = ⊤
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {X : C}
  {addMon : CategoryTheory.AddMonObj X} {X_1 : C} {addMon_1 : CategoryTheory.AddMonObj X_1},
  { X := X, addMon := addMon } = { X := X_1, addMon := addMon_1 } → X = X_1 ∧ addMon ≍ addMon_1
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- `Ext` commutes with binary biproducts on the first variable.  -/
CategoryTheory.Abelian.Ext.biprodAddEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {X₁ X₂ Y : C} →
          {n : ℕ} →
            CategoryTheory.Abelian.Ext (X₁ ⊞ X₂) Y n ≃+
              CategoryTheory.Abelian.Ext X₁ Y n × CategoryTheory.Abelian.Ext X₂ Y n
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.incidenceSetEquivNeighborSet_symm_apply_coe : ∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] (v : V) (w : ↑(G.neighborSet v)),
  ↑((G.incidenceSetEquivNeighborSet v).symm w) = s(v, ↑w)
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_pointwise_smul : ∀ {G : Type u_1} {H : Type u_2} [inst : Group H] (h : H) [inst_1 : Group G] [inst_2 : MulDistribMulAction H G]
  (J K : Subgroup G), (h • J).relIndex (h • K) = J.relIndex K
-- Init.Data.Nat.MinMax
Nat.min_le_right : ∀ (a b : ℕ), min a b ≤ b
-- Init.Data.BitVec.Bitblast
BitVec.sshiftRightRec_eq : ∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (n : ℕ),
  x.sshiftRightRec y n = x.sshiftRight' (BitVec.setWidth w₂ (BitVec.setWidth (n + 1) y))
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_add : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] {f : α → α → α} {a b : α} {a' b' c : ℕ},
  f = HAdd.hAdd →
    Mathlib.Meta.NormNum.IsNat a a' →
      Mathlib.Meta.NormNum.IsNat b b' → a'.add b' = c → Mathlib.Meta.NormNum.IsNat (f a b) c
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.kerProj_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {A : Type u_4} [inst_2 : CommRing A]
  [inst_3 : Algebra R A] [inst_4 : Algebra R S] {f : S →ₐ[R] A} (hf : Function.Surjective ⇑f),
  Function.Surjective ⇑(AdicCompletion.kerProj hf)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Two biproducts which differ by an equivalence in the indexing type,
and up to isomorphism in the factors, are isomorphic.

Unfortunately there are two natural ways to define each direction of this isomorphism
(because it is true for both products and coproducts separately).
We give the alternative definitions as lemmas below.  -/
CategoryTheory.Limits.biproduct.whiskerEquiv : {J : Type w} →
  {K : Type u_1} →
    {C : Type u} →
      [inst : CategoryTheory.Category.{v, u} C] →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
          {f : J → C} →
            {g : K → C} →
              (e : J ≃ K) →
                ((j : J) → g (e j) ≅ f j) →
                  [inst_2 : CategoryTheory.Limits.HasBiproduct f] →
                    [inst_3 : CategoryTheory.Limits.HasBiproduct g] → ⨁ f ≅ ⨁ g
-- Mathlib.Geometry.Manifold.Instances.Icc
/-- Unit vector in the tangent space to a segment, as the image of the unit vector in the real line
under the canonical projection. It is also mapped to the unit vector in the real line through
the canonical injection, see `mfderiv_subtypeVal_Icc_one`.

Note that one cannot abuse defeqs for this definition: this is *not* the same as the vector
`fun _ ↦ 1` in `EuclideanSpace ℝ (Fin 1)` through defeqs, as one of the charts of `Icc x y` is
orientation-reversing.  -/
oneTangentSpaceIcc : {x y : ℝ} → [h : Fact (x < y)] → (z : ↑(Set.Icc x y)) → TangentSpace (modelWithCornersEuclideanHalfSpace 1) z
-- Mathlib.Topology.Separation.GDelta
/-- A topological space `X` is a *perfectly normal space* provided it is normal and
closed sets are Gδ.  -/
PerfectlyNormalSpace : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.closed : ∀ {X : Type u_1} [t : TopologicalSpace X] (C : Set X) [inst : Topology.CWComplex C] [T2Space X],
  ∀ A ⊆ C,
    IsClosed A ↔ ∀ (n : ℕ) (j : Topology.RelCWComplex.cell C n), IsClosed (A ∩ Topology.RelCWComplex.closedCell n j)
-- Mathlib.NumberTheory.Divisors
Nat.nonempty_properDivisors : ∀ {n : ℕ}, n.properDivisors.Nonempty ↔ 1 < n
-- Mathlib.Topology.Algebra.UniformConvergence
instInvUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [Inv β] → Inv (UniformOnFun α β 𝔖)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_tensorObj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  { unmop := CategoryTheory.MonoidalCategoryStruct.tensorObj X Y } =
    CategoryTheory.MonoidalCategoryStruct.tensorObj { unmop := Y } { unmop := X }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Sub
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastSub : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : BitVec w)
  (assign : α → Bool) (input : aig.BinaryRefVec w),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < w),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastSub aig input).aig,
              ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastSub aig input).vec.get idx hidx }⟧ =
          (lhs - rhs).getLsbD idx
-- Mathlib.Analysis.Calculus.ContDiff.Operations
OpenPartialHomeomorph.restrContDiff_symm_apply : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (f : OpenPartialHomeomorph E F) (n : WithTop ℕ∞) (hn : n ≠ ↑⊤) (a : F),
  ↑(OpenPartialHomeomorph.restrContDiff 𝕜 f n hn).symm a = ↑f.symm a
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- If `F` has odd characteristic, then `quadraticChar F` takes the value `-1` on some unit.  -/
quadraticChar_exists_neg_one' : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
  ringChar F ≠ 2 → ∃ a, (quadraticChar F) ↑a = -1
-- Mathlib.Probability.Kernel.Posterior
ProbabilityTheory.posterior_boolKernel_apply_false : ∀ {𝓧 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} (μ ν : MeasureTheory.Measure 𝓧) [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool)
  [inst_2 : MeasureTheory.IsFiniteMeasure π],
  ∀ᵐ (x : 𝓧) ∂π.bind ⇑(ProbabilityTheory.Kernel.boolKernel μ ν),
    ((ProbabilityTheory.posterior (ProbabilityTheory.Kernel.boolKernel μ ν) π) x) {false} =
      π {false} * μ.rnDeriv (π.bind ⇑(ProbabilityTheory.Kernel.boolKernel μ ν)) x
-- Std.Data.ExtTreeSet.Basic
/-- Given a proof that such an element exists, retrieves the smallest element that is
less than the given element.
 -/
Std.ExtTreeSet.getLT : {α : Type u} →
  {cmp : α → α → Ordering} →
    [inst : Std.TransCmp cmp] → (t : Std.ExtTreeSet α cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.lt) → α
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α},
  (m.insertManyIfNewUnit l).isEmpty = (m.isEmpty && l.isEmpty)
-- Lean.Meta.Eqns
/-- Returns `true` iff `declName` is a definition and its type is not a proposition.
Returns `false` for matchers since their equations are handled by `Lean.Meta.Match.MatchEqs`.  -/
_private.Lean.Meta.Eqns.0.Lean.Meta.shouldGenerateEqnThms : Lean.Name → Lean.MetaM Bool
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.hom_nsum : ∀ {V W : SemiNormedGrp} (n : ℕ) (f : V ⟶ W), SemiNormedGrp.Hom.hom (n • f) = n • SemiNormedGrp.Hom.hom f
-- Mathlib.Dynamics.Transitive
/-- Let `M` be a monoid with a topologically transitive action on `α`. If `U` is a nonempty open
subset of `α` and `(m • ·) ⁻¹' U ⊆ U` for all `m : M` then `U` is dense in `α`.  -/
IsOpen.dense_of_preimage_smul_invariant : ∀ (M : Type u_1) {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Monoid M] [inst_2 : MulAction M α]
  [MulAction.IsTopologicallyTransitive M α] {U : Set α},
  IsOpen U → U.Nonempty → (∀ (m : M), (fun x => m • x) ⁻¹' U ⊆ U) → Dense U
-- Mathlib.Data.Finset.Sups
Finset.image_subset_diffs_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s t : Finset α} {b : α},
  b ∈ t → Finset.image (fun x => x \ b) s ⊆ s.diffs t
-- Mathlib.Order.Filter.Lift
Filter.lift_iInf_le : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → Filter α} {g : Set α → Filter β},
  (iInf f).lift g ≤ ⨅ i, (f i).lift g
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.closure_ssubset_closure : ∀ {α : Type u_2} {M : Matroid α} {I J : Set α}, M.Indep I → J ⊂ I → M.closure J ⊂ M.closure I
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoCycles₁_inv_comp_iCycles_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↥(groupHomology.cycles₁ A)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.iCycles A 1))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.isoCycles₁ A).inv) x) =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.i
          (groupHomology.chainsIso₁ A).inv))
      x
-- Mathlib.Tactic.Determinant.Bird.Meta
Mathlib.Tactic.Determinant.Ctx.mk.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)}
  (cα : Mathlib.Tactic.Ring.Common.Cache (Mathlib.Tactic.Determinant.commSemiringOfCommRing rα))
  (rc :
    Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.RatCoeff
      (Mathlib.Tactic.Determinant.commSemiringOfCommRing rα))
  (dimension : ℕ) (dimensionLit : Q(ℕ)) (arrayExpr : Q(Array «$α»)) (arrayEntries : Array Q(«$α»)),
  sizeOf
      { cα := cα, rc := rc, dimension := dimension, dimensionLit := dimensionLit, arrayExpr := arrayExpr,
        arrayEntries := arrayEntries } =
    1 + sizeOf cα + sizeOf rc + sizeOf dimension + sizeOf dimensionLit + sizeOf arrayExpr + sizeOf arrayEntries
-- Mathlib.InformationTheory.Hamming
Hamming.ofHamming_zero : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : (i : ι) → Zero (β i)], Hamming.ofHamming 0 = 0
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
/-- Analytic functions on ℂ are harmonic.  -/
AnalyticAt.harmonicAt : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] {f : ℂ → F} {x : ℂ} [CompleteSpace F],
  AnalyticAt ℂ f x → InnerProductSpace.HarmonicAt f x
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.readMCtx₂ : Aesop.EqualUpToIdsM Lean.MetavarContext
-- Mathlib.RingTheory.PowerBasis
PowerBasis.liftEquiv_apply_coe : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (f : S →ₐ[A] S'), ↑(pb.liftEquiv f) = f pb.gen
-- Std.Data.HashSet.Lemmas
Std.HashSet.insertMany_list_equiv_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {l : List α},
  (m.insertMany l).Equiv (List.foldl (fun acc a => acc.insert a) m l)
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.toTree.go : Lean.Syntax → Lean.Elab.TermElabM FBinopElab.Tree✝
-- Mathlib.Geometry.Manifold.Notation
/-- Attempt to find a model from a `TotalSpace` first by seeing if it is the total space of a
tangent bundle, and otherwise by finding a model with corners on its base.  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findModelInner.fromTotalSpace : Lean.Expr → Lean.Elab.TermElabM Manifold.Elab.FindModelResult
-- Init.Data.SInt.Basic
/-- Converts a natural number to a 64-bit signed integer, wrapping around to negative numbers on
overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `Int64.ofNat 127 = 127`
 * `Int64.ofNat 2_147_483_648 = 2_147_483_648`
 * `Int64.ofNat 9_223_372_036_854_775_807 = 9_223_372_036_854_775_807`
 * `Int64.ofNat 9_223_372_036_854_775_808 = -9_223_372_036_854_775_808`
 * `Int64.ofNat 18_446_744_073_709_551_618 = 0`
 -/
Int64.ofNat : ℕ → Int64
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorHom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [inst_3 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)]
  {X₁ Y₁ X₂ Y₂ : P.FullSubcategory} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom =
    CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.coe_toAddMonoidHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A →ₗc[R] B), ⇑↑f = ⇑f
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.subtypeRestr_symm_eqOn : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {U : TopologicalSpace.Opens X} (hU : Nonempty ↥U),
  Set.EqOn (↑e.symm) (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) (e.subtypeRestr hU).target
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.forget_reflects_isos : (CategoryTheory.forget AddGrpCat).ReflectsIsomorphisms
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.seq_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α (β → γ))
  (g : MeasureTheory.SimpleFunc α β) (a : α), (f.seq g) a = f a (g a)
-- Mathlib.Order.GaloisConnection.Basic
sInf_image2_eq_sSup_sInf : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β},
  (∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ u₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) →
    (∀ (a : α), GaloisConnection (u₂ a) (u a)) → sInf (Set.image2 u s t) = u (sSup s) (sInf t)
-- Mathlib.NumberTheory.Real.Irrational
irrational_mul_ratCast_iff : ∀ {q : ℚ} {x : ℝ}, Irrational (x * ↑q) ↔ q ≠ 0 ∧ Irrational x
-- Mathlib.Analysis.Normed.Operator.Conformal
IsConformalMap.ne_zero : ∀ {R : Type u_1} {N : Type u_3} {M' : Type u_5} [inst : NormedField R] [inst_1 : SeminormedAddCommGroup N]
  [inst_2 : NormedSpace R N] [inst_3 : NormedAddCommGroup M'] [inst_4 : NormedSpace R M'] [Nontrivial M']
  {f' : M' →L[R] N}, IsConformalMap f' → f' ≠ 0
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.tr.match_1.eq_2 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (k : Turing.PartrecToTM2.K')
  (f : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') (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 Turing.PartrecToTM2.Λ'.push k f 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_2 k f q
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.π_comp_H1Iso_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.π A 1) (groupCohomology.H1Iso A).hom =
    CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₁ A).hom
      (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData.π
-- Mathlib.CategoryTheory.ComposableArrows.Basic
_private.Mathlib.CategoryTheory.ComposableArrows.Basic.0.CategoryTheory.ComposableArrows.Mk₁.map.match_1.eq_2 : ∀ (motive : (x x_1 : Fin 2) → x ≤ x_1 → Sort u_1) (isLt : 0 < 2) (isLt_1 : 1 < 2) (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩)
  (h_1 : (isLt isLt_2 : 0 < 2) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_2⟩ x)
  (h_2 : (isLt : 0 < 2) → (isLt_2 : 1 < 2) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_2⟩ x)
  (h_3 : (isLt isLt_2 : 1 < 2) → (x : ⟨1, isLt⟩ ≤ ⟨1, isLt_2⟩) → motive ⟨1, isLt⟩ ⟨1, isLt_2⟩ x),
  (match ⟨0, isLt⟩, ⟨1, isLt_1⟩, x with
    | ⟨0, isLt⟩, ⟨0, isLt_2⟩, x => h_1 isLt isLt_2 x
    | ⟨0, isLt⟩, ⟨1, isLt_2⟩, x => h_2 isLt isLt_2 x
    | ⟨1, isLt⟩, ⟨1, isLt_2⟩, x => h_3 isLt isLt_2 x) =
    h_2 isLt isLt_1 x
-- Mathlib.FieldTheory.Separable
Algebra.IsSeparable.isSeparable' : ∀ {F : Type u_1} {K : Type u_3} {inst : CommRing F} {inst_1 : Ring K} {inst_2 : Algebra F K}
  [self : Algebra.IsSeparable F K] (x : K), IsSeparable F x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsFunctor_obj_d : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (i j : ℕ),
  ((groupCohomology.cochainsFunctor k G).obj A).d i j =
    CochainComplex.of.d (fun n => ModuleCat.of k ((Fin n → G) → ↑A)) (fun n => inhomogeneousCochains.d A n) i j
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.coreprW_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v₁))
  [inst_1 : F.IsCorepresentable] (X : C) (f : F.coreprX ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (F.coreprW.hom.app X)) f =
    (CategoryTheory.ConcreteCategory.hom (F.map f)) F.coreprx
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_mod : ∀ (a b : BitVec 16), { toBitVec := a % b } = { toBitVec := a } % { toBitVec := b }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β k}, a ∈ t.insert k v ↔ cmp k a = Ordering.eq ∨ a ∈ t
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List α} {k : α}, (t.insertMany l).contains k = (t.contains k || l.contains k)
-- Mathlib.Topology.Separation.Basic
pure_le_nhds_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {a b : X}, pure a ≤ nhds b ↔ a = b
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.mgf_le : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {X : Ω → ℝ} {c : NNReal}
  {κ : ProbabilityTheory.Kernel Ω' Ω}
  {ν : autoParam (MeasureTheory.Measure Ω') ProbabilityTheory.Kernel.HasSubgaussianMGF._auto_1},
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν →
    ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), ProbabilityTheory.mgf X (κ ω') t ≤ Real.exp (↑c * t ^ 2 / 2)
-- Mathlib.Data.Num.ZNum
ZNum.of_nat_toZNumNeg : ∀ (n : ℕ), (↑n).toZNumNeg = -↑n
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃ObjObj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} (C₃ : Type u_3) {D₁ : Type u_4} {D₂ : Type u_5} (D₃ : Type u_6)
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) {X Y : CategoryTheory.Functor C₃ D₃} (τ₃ : X ⟶ Y),
  (CategoryTheory.Functor.whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂).map τ₃ =
    CategoryTheory.Functor.whiskeringLeft₃ObjObjMap E F₁ F₂ τ₃
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
AlgebraicGeometry.instUniversallyInjectiveOfMonoScheme : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.Mono f], AlgebraicGeometry.UniversallyInjective f
-- Lean.Parser.Term
Lean.Parser.Term.byTactic.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Normed.Group.Real
NNReal.instNNNorm : NNNorm NNReal
-- Init.Data.List.Lemmas
List.eq_nil_iff_forall_not_mem : ∀ {α : Type u_1} {l : List α}, l = [] ↔ ∀ (a : α), a ∉ l
-- Lean.Meta.Basic
Lean.Meta.mkFreshExprMVarWithId : Lean.MVarId →
  optParam (Option Lean.Expr) none →
    optParam Lean.MetavarKind Lean.MetavarKind.natural → optParam Lean.Name Lean.Name.anonymous → Lean.MetaM Lean.Expr
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.bddAbove_image : ∀ (f : Cardinal.{u} → Cardinal.{max u v}) {s : Set Cardinal.{u}}, BddAbove s → BddAbove (f '' s)
-- Mathlib.Tactic.NormNum.Pow
/-- Unfolds the assertion.  -/
Mathlib.Meta.NormNum.IsNatPowT.run' : ∀ {p : Prop} {a b c : ℕ}, Mathlib.Meta.NormNum.IsNatPowT p a b c → p → a.pow b = c