mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- The inverse of a graph isomorphism.  -/
SimpleGraph.Iso.symm : {V : Type u_1} → {W : Type u_2} → {G : SimpleGraph V} → {G' : SimpleGraph W} → G ≃g G' → G' ≃g G
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.mu_eq_neg_sum_Ico_of_ne : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] {a b : α},
  a ≠ b → (IncidenceAlgebra.mu 𝕜) a b = -∑ x ∈ Finset.Ico a b, (IncidenceAlgebra.mu 𝕜) a x
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flip_f₁₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C), sq.flip.f₁₃ = sq.f₁₂
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getEntryLE! : {α : Type u} → {β : Type v} → [Ord α] → [Inhabited (α × β)] → α → (Std.DTreeMap.Internal.Impl α fun x => β) → α × β
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_right_comm : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P ∧ Q) ∧ R ⊣⊢ₛ (P ∧ R) ∧ Q
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.preFunctor_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} E]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (S : CategoryTheory.Functor C D)
  (T : CategoryTheory.Functor D E) (e : E),
  (CategoryTheory.CostructuredArrow.preFunctor S T).app e = (CategoryTheory.CostructuredArrow.pre S T e).toCatHom
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Given an equivalence of diagrams `e`, `s` is a limit cone iff `s.whisker e.functor` is.  -/
CategoryTheory.Limits.IsLimit.whiskerEquivalenceEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              {s : CategoryTheory.Limits.Cone F} →
                (e : K ≌ J) →
                  CategoryTheory.Limits.IsLimit s ≃
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Cone.whisker e.functor s)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.contDiff_sinh : ∀ {n : WithTop ℕ∞}, ContDiff ℝ n Real.sinh
-- Std.Data.DTreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the key-value pair with the largest key.
 -/
Std.DTreeMap.Const.maxEntry : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → (t : Std.DTreeMap α (fun x => β) cmp) → t.isEmpty = false → α × β
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.sup_inf_assoc_of_le_submodule : ∀ {E : Type u_2} {R : Type u_5} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup E] [inst_4 : Module R E] {C : PointedCone R E} (D : PointedCone R E) {S : Submodule R E},
  C ≤ ↑S → (C ⊔ D) ⊓ ↑S = C ⊔ D ⊓ ↑S
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.eq_bot_iff : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → (l = ⊥ ↔ ∃ i, p i ∧ s i = ∅)
-- Std.Time.Zoned.Database.Windows
/-- Represents a Time Zone Database that we get from ICU available on Windows SDK.
 -/
Std.Time.Database.WindowsDb : Type
-- Lean.Meta.Sym.Simp.SimpM
/-- No change. If `done = true`, skip remaining simplification steps for this term.  -/
Lean.Meta.Sym.Simp.Result.rfl : optParam Bool false → optParam Bool false → Lean.Meta.Sym.Simp.Result
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.coeff_mapAlgHom : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddMonoid M] (f : A →ₐ[R] B)
  (x : AddMonoidAlgebra A M) (m : M), ((AddMonoidAlgebra.mapAlgHom M f) x).coeff m = f (x.coeff m)
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
Unitization.lift_range : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A]
  [inst_2 : Module R A] [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] [inst_5 : Semiring C]
  [inst_6 : Algebra R C] (f : A →ₙₐ[R] C), (Unitization.lift f).range = Algebra.adjoin R ↑(NonUnitalAlgHom.range f)
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.j_mul_j : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (self : QuaternionAlgebra.Basis A c₁ c₂ c₃), self.j * self.j = c₃ • 1
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
minpoly.algEquiv.eq_1 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x y : L}
  (hx : IsAlgebraic K x) (h_mp : minpoly K x = minpoly K y),
  minpoly.algEquiv hx h_mp =
    (IntermediateField.adjoinRootEquivAdjoin K ⋯).symm.trans
      ((AdjoinRoot.algEquivOfEq K (minpoly K x) (minpoly K y) h_mp).trans (IntermediateField.adjoinRootEquivAdjoin K ⋯))
-- Mathlib.Algebra.Lie.Solvable
LieIdeal.derivedSeries_eq_top : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (n : ℕ),
  LieAlgebra.derivedSeries R L 1 = ⊤ → LieAlgebra.derivedSeries R L n = ⊤
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Seed.coeff'.eq_1 : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] (seed : HahnEmbedding.Seed K M R) (c : FiniteArchimedeanClass M),
  seed.coeff' c = seed.coeff c ∘ₗ seed.baseDomain.subtype.submoduleComap (seed.stratum c)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddMonoid.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : AddMonoid M],
  Filter.Germ.instAddMonoid =
    { toAddSemigroup := Filter.Germ.instAddSemigroup, toZero := Filter.Germ.instZero, zero_add := ⋯, add_zero := ⋯,
      nsmul := fun n a => n • a, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- The product of the module topologies for a finite family of modules over a topological ring
is the module topology.  -/
IsModuleTopology.instPi : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R] {ι : Type u_2} [Finite ι] {A : ι → Type u_3}
  [inst_3 : (i : ι) → AddCommMonoid (A i)] [inst_4 : (i : ι) → Module R (A i)]
  [inst_5 : (i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsModuleTopology R (A i)], IsModuleTopology R ((i : ι) → A i)
-- Mathlib.Topology.Inseparable
inseparable_iff_closure_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Inseparable x y ↔ closure {x} = closure {y}
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.mk : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} →
          (Fib : 𝒮 → Type u₃) →
            (category : autoParam ((S : 𝒮) → CategoryTheory.Category.{v₃, u₃} (Fib S)) HasFibers.category._autoParam) →
              (ι : (S : 𝒮) → CategoryTheory.Functor (Fib S) 𝒳) →
                (comp_const : ∀ (S : 𝒮), (ι S).comp p = (CategoryTheory.Functor.const (Fib S)).obj S) →
                  autoParam (∀ (S : 𝒮), (CategoryTheory.Functor.Fiber.inducedFunctor ⋯).IsEquivalence)
                      HasFibers.equiv._autoParam →
                    HasFibers p
-- Init.Data.BitVec.Bitblast
/-- The remainder for `srem`, i.e. division with rounding to zero is negative
iff `x` is negative and `y` does not divide `x`.

We can eventually build fast circuits for the divisibility test `x.srem y = 0`.
 -/
BitVec.msb_srem : ∀ {w : ℕ} {x y : BitVec w}, (x.srem y).msb = (x.msb && decide (x.srem y ≠ 0))
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.map_id : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (self : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) (X : C) (Y : D),
  self.map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) =
    CategoryTheory.CategoryStruct.id (self.obj X Y)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_neg : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R) (x : R), Polynomial.eval x (-p) = -Polynomial.eval x p
-- Mathlib.Algebra.Order.Module.Defs
smul_lt_smul_of_pos_right : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero β] [SMulPosStrictMono α β], a₁ < a₂ → 0 < b → a₁ • b < a₂ • b
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coe_multilinearMap : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N), ⇑↑f = ⇑f
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_norm_conjTranspose : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] [inst_3 : StarAddMonoid α] [NormedStarGroup α] (A : Matrix m n α),
  ‖A.conjTranspose‖ = ‖A‖
-- Mathlib.Algebra.Lie.Graded
GradedLieAlgebra.toGradedBracket : ∀ {ι : Type u_1} {R : Type u_3} {L : Type u_4} {inst : DecidableEq ι} {inst_1 : AddCommMonoid ι} {inst_2 : CommRing R}
  {inst_3 : LieRing L} {inst_4 : LieAlgebra R L} {ℒ : ι → Submodule R L} [self : GradedLieAlgebra ℒ],
  SetLike.GradedBracket ℒ
-- Mathlib.Combinatorics.Enumerative.Composition
/-- When one splits a list along a composition `c`, the number of sublists thus created is
`c.length`.  -/
List.length_splitWrtComposition : ∀ {n : ℕ} {α : Type u_1} (l : List α) (c : Composition n), (l.splitWrtComposition c).length = c.length
-- Lean.Meta.Sym.IsClass
/-- Efficient version of `Meta.isClass?` for symbolic simulation. It does not use
reduction nor instantiates metavariables.
 -/
Lean.Meta.Sym.isClass? : Lean.Environment → Lean.Expr → Option Lean.Name
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimitCore.mk : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {F : CategoryTheory.Functor J (Type w₀)} →
      {c : F.CoconeTypes} →
        (desc : (c' : F.CoconeTypes) → c.pt → c'.pt) →
          autoParam (∀ (c' : F.CoconeTypes) (j : J), desc c' ∘ c.ι j = c'.ι j)
              CategoryTheory.Functor.CoconeTypes.IsColimitCore.fac._autoParam →
            (∀ {T : Type w₂} {f g : c.pt → T}, (∀ (j : J), f ∘ c.ι j = g ∘ c.ι j) → f = g) → c.IsColimitCore
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- To show that a left lift `t` is a Kan lift, we need to show that for every left lift `s`
there is a unique morphism `t ⟶ s`.  -/
CategoryTheory.Bicategory.LeftLift.IsKan.mk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          {t : CategoryTheory.Bicategory.LeftLift f g} →
            (desc : (s : CategoryTheory.Bicategory.LeftLift f g) → t ⟶ s) →
              (∀ (s : CategoryTheory.Bicategory.LeftLift f g) (τ : t ⟶ s), τ = desc s) → t.IsKan
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.endsWith_eq_false_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, s.endsWith pat = false ↔ ¬String.Slice.Pattern.Model.RevMatchesAt pat s.endPos
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_sdiff_inv_smul : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) (s t : Set α),
  μ (s \ c⁻¹ • t) = μ (c • s \ t)
-- Init.Data.UInt.Basic
/-- Bitwise or for word-sized unsigned integers. Usually accessed via the `|||` operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of both input
integers are set.

This function is overridden at runtime with an efficient implementation.
 -/
USize.lor : USize → USize → USize
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.instIsUltrametricDist : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], IsUltrametricDist ℤ_[p]
-- Mathlib.CategoryTheory.Bicategory.Free
_private.Mathlib.CategoryTheory.Bicategory.Free.0.CategoryTheory.FreeBicategory.«term_≫_» : Lean.TrailingParserDescr
-- Init.Data.BitVec.Basic
/-- Bitwise complement for bitvectors. Usually accessed via the `~~~` prefix operator.

SMT-LIB name: `bvnot`.

Example:
* `~~~(0b0101#4) == 0b1010`
 -/
BitVec.not : {n : ℕ} → BitVec n → BitVec n
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.isFiniteMeasure_map : ∀ {α : Type u_1} {β : Type u_2} [mβ : MeasurableSpace β] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure μ] (f : α → β), MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.map f μ)
-- Mathlib.Algebra.Ring.Regular
/-- **Alias** of `IsRegular.of_ne_zero'`. -/
isRegular_of_ne_zero' : ∀ {α : Type u_1} [inst : NonUnitalNonAssocRing α] [NoZeroDivisors α] {k : α}, k ≠ 0 → IsRegular k
-- Lean.Elab.App
/-- State of the `elab_as_elim` elaboration procedure.  -/
Lean.Elab.Term.ElabElim.State : Type
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.MkSimpContextResult.simprocs : Lean.Elab.Tactic.MkSimpContextResult → Lean.Meta.Simp.SimprocsArray
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
DifferentiableAt.arctan : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → DifferentiableAt ℝ (fun x => Real.arctan (f x)) x
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- If a cycle `p` is Hamiltonian then the graph has finitely many vertices.  -/
SimpleGraph.Walk.IsHamiltonianCycle.finite : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a}, p.IsHamiltonianCycle → Finite α
-- Mathlib.GroupTheory.Congruence.Hom
AddCon.mapOfSurjective.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_4} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [inst_3 : AddHomClass F M N] {c : AddCon M} (f : F) (h : AddCon.ker f ≤ c) (hf : Function.Surjective ⇑f),
  AddCon.mapOfSurjective f h hf = { toSetoid := c.mapOfSurjective (⇑f) h hf, add' := ⋯ }
-- Mathlib.Tactic.FieldSimp
/-- Given a product of powers, split as a quotient: the positive powers divided by (the negations
of) the negative powers.  -/
Mathlib.Tactic.FieldSimp.qNF.split : {v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (l : Mathlib.Tactic.FieldSimp.qNF M) →
        Lean.MetaM
          ((l_n : Mathlib.Tactic.FieldSimp.qNF M) ×
            (l_d : Mathlib.Tactic.FieldSimp.qNF M) ×
              have a := l_d.toNF;
              have a_1 := l_n.toNF;
              have a_2 := l.toNF;
              Q(«$a_2».eval = «$a_1».eval / «$a».eval))
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.instAddCancelMonoid : {α : Type u_1} → AddCancelMonoid (FreeAddMonoid α)
-- Lean.Elab.Tactic.Doc
Lean.Elab.Tactic.Doc.elabTacticExtension : Lean.Elab.Command.CommandElab
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.ofAlgHom_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R B] (f : A →ₐ[R] B)
  (counit_comp : (Bialgebra.counitAlgHom R B).comp f = Bialgebra.counitAlgHom R A)
  (map_comp_comul :
    (Algebra.TensorProduct.map f f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp f)
  (a : A), (BialgHom.ofAlgHom f counit_comp map_comp_comul) a = f a
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_eq_getKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [instBEq : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α β}, t.Ordered → t.getKey? k = Std.Internal.List.getKey? k t.toListModel
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to0.trAux.match_1.eq_4 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → σ → Sort u_4) (p : Γ → σ → Bool)
  (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) (v : σ)
  (h_1 : (d : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.move d q) v)
  (h_2 : (a : Γ → σ → Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.write a q) v)
  (h_3 : (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.load a q) v)
  (h_4 : (p : Γ → σ → Bool) → (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.branch p q₁ q₂) v)
  (h_5 : (l : Γ → σ → Λ) → (v : σ) → motive (Turing.TM1.Stmt.goto l) v) (h_6 : (v : σ) → motive Turing.TM1.Stmt.halt v),
  (match Turing.TM1.Stmt.branch p q₁ q₂, v with
    | Turing.TM1.Stmt.move d q, v => h_1 d q v
    | Turing.TM1.Stmt.write a q, v => h_2 a q v
    | Turing.TM1.Stmt.load a q, v => h_3 a q v
    | Turing.TM1.Stmt.branch p q₁ q₂, v => h_4 p q₁ q₂ v
    | Turing.TM1.Stmt.goto l, v => h_5 l v
    | Turing.TM1.Stmt.halt, v => h_6 v) =
    h_4 p q₁ q₂ v
-- Init.Data.Array.Subarray
Std.Slice.Internal.SubarrayData.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (array : Array α) (start stop : ℕ) (start_le_stop : start ≤ stop)
  (stop_le_array_size : stop ≤ array.size),
  sizeOf
      { array := array, start := start, stop := stop, start_le_stop := start_le_stop,
        stop_le_array_size := stop_le_array_size } =
    1 + sizeOf array + sizeOf start + sizeOf stop + sizeOf start_le_stop + sizeOf stop_le_array_size
-- Mathlib.NumberTheory.Dioph
/-- Diophantine functions are closed under subtraction.  -/
Dioph.sub_dioph : ∀ {α : Type} {f g : (α → ℕ) → ℕ}, Dioph.DiophFn f → Dioph.DiophFn g → Dioph.DiophFn fun v => f v - g v
-- Mathlib.Tactic.Linarith.Frontend
/-- `cfg.updateReducibility reduce_default` will change the transparency setting of `cfg` to
`default` if `reduce_default` is true. In this case, it also sets the discharger to `ring!`,
since this is typically needed when using stronger unification.
 -/
Mathlib.Tactic.Linarith.LinarithConfig.updateReducibility : Mathlib.Tactic.Linarith.LinarithConfig → Bool → Mathlib.Tactic.Linarith.LinarithConfig
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.assignExprIfUnassigned : ℕ → Lean.Expr → Lean.Meta.Sym.UnifyM✝ Unit
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_neg : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1]
  [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2] [inst_5 : Module k V2] (f : P1 →ᵃ[k] V2),
  ⇑(-f) = -⇑f
-- Init.Data.SInt.Bitwise
Bool.toBitVec_toInt64 : ∀ {b : Bool}, b.toInt64.toBitVec = BitVec.setWidth 64 (BitVec.ofBool b)
-- Mathlib.RingTheory.RootsOfUnity.Complex
Complex.isPrimitiveRoot_exp_rat_of_even_num : ∀ (q : ℚ), Even q.num → IsPrimitiveRoot (Complex.exp (↑Real.pi * Complex.I * ↑q)) q.den
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.contains_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a b : α}, (a == b) = true → m.contains a = m.contains b
-- Init.Data.BitVec.Basic
/-- Checks whether subtraction of `x` and `y` results in *unsigned* overflow.

SMT-Lib name: `bvusubo`.
 -/
BitVec.usubOverflow : {w : ℕ} → BitVec w → BitVec w → Bool
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso_inv_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  [inst_4 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C}
  (i : CategoryTheory.Limits.IsInitial I) {W : C},
  (CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isInitialIso X i).inv.right = ⋯.isoPullback.hom
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_mem_mul : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] {M N : Submodule R A} {m n : A}, m ∈ M → n ∈ N → m * n ∈ M * N
-- Lean.Parser.Command
/-- `with_weak_namespace <id> <cmd>` changes the current namespace to `<id>` for the duration of
executing command `<cmd>`, without causing scoped things to go out of scope.

This is in contrast to `namespace <id>` which pushes a new scope and deactivates scoped entries
from the previous namespace. `with_weak_namespace` modifies the existing scope's namespace,
so scoped extensions remain active.

This is primarily useful for defining syntax extensions that should be scoped to a different
namespace than the current one.
 -/
Lean.Parser.Command.withWeakNamespace : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.op_X₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C), sq.op.X₄ = Opposite.op sq.X₁
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.var : Lean.FVarId → Lean.Meta.Match.Pattern
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap`.

---

Preparatory lemma for `inducedOrderRingHom`.  -/
LinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap : ∀ {α : Type u_2} {β : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α},
  0 < a →
    ∀ b ∈ LinearOrderedField.cutMap β (a * a),
      b ≤
        ConditionallyCompleteLinearOrderedField.inducedMap α β a *
          ConditionallyCompleteLinearOrderedField.inducedMap α β a
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.norm.go.eq_def : ∀ (p r : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.norm.go p r =
    match p with
    | [] => r
    | (k, v) :: p => Nat.Internal.Linear.Poly.norm.go p (Nat.Internal.Linear.Poly.insert k v r)
-- Mathlib.Algebra.GCDMonoid.Basic
neg_gcd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : HasDistribNeg α] [inst_2 : NormalizedGCDMonoid α] {a b : α},
  gcd (-a) b = gcd a b
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.OptionT.bind.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) →
    (__do_lift : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive __do_lift
-- Mathlib.Analysis.Complex.Tietze
Set.instTietzeExtensionUnitClosedBall : ∀ {𝕜 : Type v} [inst : RCLike 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [FiniteDimensional 𝕜 E], TietzeExtension ↑(Metric.closedBall 0 1)
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- Given a diagram
```
a --φ--> b        b'
|        |        |
v        v        v
R --f--> S --g--> S'
```
such that `φ` is strongly co-Cartesian, and morphisms `φ' : a ⟶ b'`, `ψ : b ⟶ b'` such that
`g ≫ ψ = φ'`. Then `ψ` is the map induced by the universal property.  -/
CategoryTheory.Functor.IsStronglyCocartesian.map_uniq : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsStronglyCocartesian f φ]
  {S' : 𝒮} {b' : 𝒳} {g : S ⟶ S'} {f' : R ⟶ S'} (hf' : f' = CategoryTheory.CategoryStruct.comp f g) (φ' : a ⟶ b')
  [inst_3 : p.IsHomLift f' φ'] (ψ : b ⟶ b') [p.IsHomLift g ψ],
  CategoryTheory.CategoryStruct.comp φ ψ = φ' → ψ = CategoryTheory.Functor.IsStronglyCocartesian.map p f φ hf' φ'