mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.map_smul_of_tower : ∀ {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]
  (φ : A →ₗc[R] B) {R' : Type u_6} [inst_7 : SMul R' A] [inst_8 : SMul R' B] [LinearMap.CompatibleSMul A B R' R]
  (r : R') (x : A), φ (r • x) = r • φ x
-- Mathlib.Analysis.Matrix.Hermitian
/-- A matrix is Hermitian iff the corresponding linear map with an orthonormal basis is
symmetric.  -/
Matrix.isSymmetric_toLin_iff : ∀ {𝕜 : Type u_1} {n : Type u_3} {A : Matrix n n 𝕜} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {E : Type u_4} [inst_3 : NormedAddCommGroup E] [inst_4 : InnerProductSpace 𝕜 E] (b : OrthonormalBasis n 𝕜 E),
  ((Matrix.toLin b.toBasis b.toBasis) A).IsSymmetric ↔ A.IsHermitian
-- Lean.Parser.Types
Lean.Parser.CacheableParserContext.mk.injEq : ∀ (prec quotDepth : ℕ) (suppressInsideQuot : Bool) (savedPos? : Option String.Pos.Raw)
  (forbiddenTk? : Option Lean.Parser.Token) (prec_1 quotDepth_1 : ℕ) (suppressInsideQuot_1 : Bool)
  (savedPos?_1 : Option String.Pos.Raw) (forbiddenTk?_1 : Option Lean.Parser.Token),
  ({ prec := prec, quotDepth := quotDepth, suppressInsideQuot := suppressInsideQuot, savedPos? := savedPos?,
        forbiddenTk? := forbiddenTk? } =
      { prec := prec_1, quotDepth := quotDepth_1, suppressInsideQuot := suppressInsideQuot_1, savedPos? := savedPos?_1,
        forbiddenTk? := forbiddenTk?_1 }) =
    (prec = prec_1 ∧
      quotDepth = quotDepth_1 ∧
        suppressInsideQuot = suppressInsideQuot_1 ∧ savedPos? = savedPos?_1 ∧ forbiddenTk? = forbiddenTk?_1)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limit_obj_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  {H : CategoryTheory.Functor J (CategoryTheory.Functor K C)} [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  {k : K} {W : C} {f g : W ⟶ (CategoryTheory.Limits.limit H).obj k},
  f = g ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp f ((CategoryTheory.Limits.limit.π H j).app k) =
        CategoryTheory.CategoryStruct.comp g ((CategoryTheory.Limits.limit.π H j).app k)
-- Init.Data.UInt.BasicAux
UInt16.instOfNat : {n : ℕ} → OfNat UInt16 n
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mem_iUnion : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {x : ι → ℝ}, x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
Polynomial.sumIDeriv_X : Polynomial.sumIDeriv Polynomial.X = Polynomial.X + Polynomial.C 1
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
HomogeneousSubsemiring.toSubsemiring_injective : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜],
  Function.Injective HomogeneousSubsemiring.toSubsemiring
-- Mathlib.Analysis.MeanInequalities
NNReal.summable_mul_of_Lp_Lq : ∀ {ι : Type u} {f g : ι → NNReal} {p q : ℝ},
  p.HolderConjugate q → (Summable fun i => f i ^ p) → (Summable fun i => g i ^ q) → Summable fun i => f i * g i
-- Init.Data.Slice.Array.Lemmas
Array.toList_mkSlice_rcc : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  Std.Slice.toList (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = List.drop lo (List.take (hi + 1) xs.toList)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.CohomologyClass.mk_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (x : CochainComplex.HomComplex.Cocycle K L n),
  CochainComplex.HomComplex.CohomologyClass.mk (-x) = -CochainComplex.HomComplex.CohomologyClass.mk x
-- Mathlib.Topology.MetricSpace.Cover
Metric.isCover_closure : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {ε : NNReal} {s N : Set X} [ProperSpace X],
  IsClosed N → (Metric.IsCover ε (closure s) N ↔ Metric.IsCover ε s N)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulConst.go.eq_def : ∀ (k : ℤ) (a : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulConst.go k a =
    match a with
    | Lean.Grind.CommRing.Poly.num k' => Lean.Grind.CommRing.Poly.num (k * k')
    | Lean.Grind.CommRing.Poly.add k' m p =>
      Lean.Grind.CommRing.Poly.add (k * k') m (Lean.Grind.CommRing.Poly.mulConst.go k p)
-- Mathlib.Data.FunLike.Module
/-- A `FunLike` type is a `Module` if `β` is a `Module`.  -/
FunLike.module : {M : Type u_1} →
  {F : Type u_3} →
    {α : Type u_4} →
      {β : Type u_5} →
        [i : FunLike F α β] →
          [inst : Semiring M] →
            [inst_1 : AddCommMonoid β] →
              [inst_2 : Module M β] →
                [inst_3 : AddCommMonoid F] →
                  [inst_4 : SMul M F] → [IsZeroApply F α β] → [IsAddApply F α β] → [IsSMulApply M F α β] → Module M F
-- Mathlib.Algebra.Polynomial.Lifts
Polynomial.monomial_mem_lifts_and_degree_eq : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} {s : S} {n : ℕ},
  (Polynomial.monomial n) s ∈ Polynomial.lifts f →
    ∃ q, Polynomial.map f q = (Polynomial.monomial n) s ∧ q.degree = ((Polynomial.monomial n) s).degree
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
LinearEquiv.coe_ofInjectiveEndo : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V] (f : V →ₗ[K] V) (h_inj : Function.Injective ⇑f),
  ⇑(LinearEquiv.ofInjectiveEndo f h_inj) = ⇑f
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.coe_inv : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (x : ↥H), ↑x⁻¹ = (↑x)⁻¹
-- Init.Data.UInt.Bitwise
UInt16.ofBitVec_shiftRight_mod : ∀ (a : BitVec 16) (b : ℕ), { toBitVec := a >>> (b % 16) } = { toBitVec := a } >>> UInt16.ofNat b
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
/-- **Cauchy-Schwarz inequality** for finsets.

This is written in terms of sequences `f`, `g`, and `r`, where `r` is usually a stand-in for
`√(f i * g i)`. See `sum_mul_sq_le_sq_mul_sq` for the more usual form in terms of squared
sequences.  -/
Finset.sum_sq_le_sum_mul_sum_of_sq_le_mul : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [ExistsAddOfLE R] (s : Finset ι) {r f g : ι → R},
  (∀ i ∈ s, 0 ≤ f i) →
    (∀ i ∈ s, 0 ≤ g i) → (∀ i ∈ s, r i ^ 2 ≤ f i * g i) → (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Alt.mk.sizeOf_spec : ∀ (name : Lean.Name) (info : Lean.Meta.ElimAltInfo) (mvarId : Lean.MVarId),
  sizeOf { name := name, info := info, mvarId := mvarId } = 1 + sizeOf name + sizeOf info + sizeOf mvarId
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.operator.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.operator = 1
-- Mathlib.Order.BoundedOrder.Basic
bot_notMem_iff : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {s : Set α}, ⊥ ∉ s ↔ ∀ x ∈ s, ⊥ < x
-- Aesop.Tree.TreeM
Aesop.Tree.nextRappId : Aesop.Tree → Aesop.RappId
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.extendScalars_le_extendScalars_iff : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {F E E' : IntermediateField K L} (h : F ≤ E) (h' : F ≤ E'),
  IntermediateField.extendScalars h ≤ IntermediateField.extendScalars h' ↔ E ≤ E'
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_aux.shiftₗ_apply : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) (f : M → G) (y : M),
  (fwdDiff_aux.shiftₗ M G h) f y = f (y + h)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- Suppose `e` is a compatible trivialisation around `x ∈ M`, and `s` a bundle section.
Then the coefficient of `s` w.r.t. the local frame induced by `b` and `e`
equals the coefficient of "`s x` read in the trivialisation `e`" for `b i`.  -/
Bundle.Trivialization.localFrameCoeff_eq_coeff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V] {ι : Type u_7}
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_14 : MemTrivializationAtlas e] {b : Module.Basis ι 𝕜 F}
  [inst_15 : ContMDiffVectorBundle 1 F V I] {x : M} {s : (x : M) → V x},
  x ∈ e.baseSet →
    ∀ {i : ι}, (Bundle.Trivialization.localFrameCoeff I e b i x) (s x) = (b.repr (↑e ((fun x => ⟨x, s x⟩) x)).2) i
-- Lean.Elab.InfoTree.Types
Lean.Elab.MonadAutoImplicits : (Type → Type) → Type
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.map.congr_simp : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} {Y : Type u_3} [inst_2 : Fintype X]
  [inst_3 : Fintype Y] [inst_4 : IsOrderedRing S] (f f_1 : X → Y),
  f = f_1 → ∀ (s s_1 : ↑(stdSimplex S X)), s = s_1 → stdSimplex.map f s = stdSimplex.map f_1 s_1
-- Mathlib.CategoryTheory.Monad.Basic
/-- The forgetful functor from the category of comonads to the category of endofunctors.
 -/
CategoryTheory.comonadToFunctor : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.Functor (CategoryTheory.Comonad C) (CategoryTheory.Functor C C)
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.ofStar : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  [inst_2 : StarAddMonoid α] [ContinuousStar α] {f : β → α}, Summable (fun b => star (f b)) L → Summable f L
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.eq_of_le_of_domain_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {f g : E →ₛₗ.[σ] F},
  f ≤ g → f.domain = g.domain → f = g
-- Lean.Parser.Do
Lean.Parser.Term.doLetMetaExpr.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.QuaternionBasis
/-- Since `k` is redundant, it is not necessary to show `q₁.k = q₂.k` when showing `q₁ = q₂`.  -/
QuaternionAlgebra.Basis.ext : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  ⦃q₁ q₂ : QuaternionAlgebra.Basis A c₁ c₂ c₃⦄, q₁.i = q₂.i → q₁.j = q₂.j → q₁ = q₂
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.find?_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [inst_2 : Std.IteratorLoop α m m]
  [LawfulMonad m] [Std.Iterators.Finite α m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {f : β → Bool},
  it.find? f = do
    let __do_lift ← it.step
    match ↑__do_lift.inflate with
      | Std.IterStep.yield it' out => if f out = true then pure (some out) else it'.find? f
      | Std.IterStep.skip it' => it'.find? f
      | Std.IterStep.done => pure none
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.map_apply : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] (f : R →+* S) (i j : n) (g : GL n R), ↑((Matrix.GeneralLinearGroup.map f) g) i j = f (↑g i j)
-- Mathlib.Algebra.Colimit.Ring
DirectLimit.Ring.lift.congr_simp : ∀ {ι : Type u_2} [inst : Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonAssocSemiring (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)]
  [inst_6 : Nonempty ι] (P : Type u_7) [inst_7 : NonAssocSemiring P] (g g_1 : (i : ι) → G i →+* P) (e_g : g = g_1)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x),
  DirectLimit.Ring.lift G f P g Hg = DirectLimit.Ring.lift G f P g_1 ⋯
-- Mathlib.Computability.Partrec
Computable.nat_strong_rec : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] (f : α → ℕ → σ)
  {g : α → List σ → Option σ},
  Computable₂ g → (∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)) → Computable₂ f
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.drop.eq_1 : ∀ (x : ℕ) (s : String) (b e : String.Pos.Raw),
  { str := s, startPos := b, stopPos := e }.drop x =
    { str := s, startPos := ({ str := s, startPos := b, stopPos := e }.nextn x 0).offsetBy b, stopPos := e }
-- Mathlib.Data.ULift
PLift.instIsEmpty : ∀ {α : Sort u} [IsEmpty α], IsEmpty (PLift α)
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.pf_add_c : ∀ {α : Type u_1} {a b : α} [inst : Add α], a = b → ∀ (c : α), a + c = b + c
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.weight_coweight_transpose_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (x : N₂) (f : P.Hom Q),
  f.weightMap.dualMap (Q.flip.toPerfPair x) = P.flip.toPerfPair (f.coweightMap x)
-- Lean.Meta.Tactic.Simp.Rewrite
_private.Lean.Meta.Tactic.Simp.Rewrite.0.Lean.Meta.Simp.rewrite?.diagnoseWhenNoIndex.unsafe_impl_2 : Lean.Meta.SimpTheorem → Lean.Meta.SimpTheorem → Bool
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Iso.toEquiv_id : ∀ (X : Type u), (CategoryTheory.Iso.refl X).toEquiv = Equiv.refl X
-- Mathlib.CategoryTheory.Core
CategoryTheory.coreFunctor_obj_map_iso_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Core (CategoryTheory.Functor C D)) {X Y : CategoryTheory.Core C} (f : X ⟶ Y),
  (((CategoryTheory.coreFunctor C D).obj F).map f).iso.hom = F.of.map f.iso.hom
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.toLinearMap_id : ∀ (R : Type u_1) (E₁ : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid E₁] [inst_2 : PartialOrder E₁]
  [inst_3 : Module R E₁], (PositiveLinearMap.id R E₁).toLinearMap = LinearMap.id
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt16.reduceAdd : Lean.Meta.Simp.DSimproc
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [Std.LawfulEqOrd α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : l.isEmpty = false} {km : α},
      Std.Internal.List.maxKey l he = km ↔
        Std.Internal.List.containsKey km l = true ∧
          ∀ (k : α), Std.Internal.List.containsKey k l = true → (compare k km).isLE = true
-- Mathlib.Topology.Sober
isGenericPoint_iff_specializes : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {S : Set α}, IsGenericPoint x S ↔ ∀ (y : α), x ⤳ y ↔ y ∈ S
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.center_toNonUnitalSubalgebra : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : IsScalarTower R A A] [inst_5 : SMulCommClass R A A],
  (NonUnitalStarSubalgebra.center R A).toNonUnitalSubalgebra = NonUnitalSubalgebra.center R A
-- Mathlib.Probability.Process.Adapted
MeasureTheory.StronglyAdapted.stronglyMeasurable : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i} {i : ι},
  MeasureTheory.StronglyAdapted f u → MeasureTheory.StronglyMeasurable (u i)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The TM1 model is a simplification and extension of TM0
(Post-Turing model) in the direction of Wang B-machines. The machine's
internal state is extended with a (finite) store `σ` of variables
that may be accessed and updated at any time.
A machine is given by a `Λ` indexed set of procedures or functions.
Each function has a body which is a `Stmt`, which can either be a
`move` or `write` command, a `branch` (if statement based on the
current tape value), a `load` (set the variable value),
a `goto` (call another function), or `halt`. Note that here
most statements do not have labels; `goto` commands can only
go to a new function. All commands have access to the variable value
and current tape value.  -/
Turing.TM1.Stmt : Type u_1 → Type u_2 → Type u_3 → Type (max (max u_1 u_2) u_3)
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsTransitive.powerset : ∀ {x : ZFSet.{u}}, x.IsTransitive → x.powerset.IsTransitive
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_inter_eq_size_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], (∀ a ∈ m₂, a ∈ m₁) → (m₁ ∩ m₂).size = m₂.size
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.flippingIso_hom_toFunctor_obj_map_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X Y : D} (f : X ⟶ Y) (j : C),
  ((CategoryTheory.flippingIso.hom.toFunctor.obj F).map f).app j = (F.obj j).map f
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderivWithin_eq_mfderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M},
  UniqueMDiffAt[s] x → MDiffAt f x → mfderiv[s] f x = mfderiv% f x
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.coprodPUnit.eq_1 : ∀ (M : Type u_1) [inst : AddMonoid M], AddEquiv.coprodPUnit M = AddMonoid.Coprod.fst.toAddEquiv AddMonoid.Coprod.inl ⋯ ⋯
-- Mathlib.Algebra.Homology.DerivedCategory.KInjective
CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKInjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (K L : CochainComplex C ℤ)
  (n : ℤ)
  [inst_2 :
    CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L]
  [L.IsKInjective], Function.Bijective CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom
-- Mathlib.Combinatorics.Quiver.Schreier
/-- Transport the scalar multiplication to the Schreier graph vertices.  -/
Quiver.SchreierGraph.schreierGraphSMul : (V : Type u_1) → {M : Type u_2} → [inst : SMul M V] → {S : Type u_3} → (ι : S → M) → SMul M (Quiver.SchreierGraph V ι)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_insertList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α}
  (not_contains : (List.map Sigma.fst toInsert).contains k = false)
  {h : Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) = true},
  Std.Internal.List.getValueCast k (Std.Internal.List.insertList l toInsert) h = Std.Internal.List.getValueCast k l ⋯
-- Mathlib.Order.Notation
/-- Syntax typeclass for Heyting negation `￢`.

The difference between `Compl` and `HNot` is that the former belongs to Heyting algebras,
while the latter belongs to co-Heyting algebras. They are both pseudo-complements, but `compl`
underestimates while `HNot` overestimates. In Boolean algebras, they are equal.
See `hnot_eq_compl`.
 -/
HNot : Type u_1 → Type u_1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} → {aig : Std.Sat.AIG α} → {len : ℕ} → aig.RefVec (len * w) → 0 < len → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_fun_sum_right' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ}
  {s : Finset ι} [MeasureTheory.IsFiniteMeasure μ],
  (∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) →
    MeasureTheory.MemLp Y 2 μ →
      ProbabilityTheory.covariance Y (fun ω => ∑ i ∈ s, X i ω) μ = ∑ i ∈ s, ProbabilityTheory.covariance Y (X i) μ
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.mulLeft.eq_1 : ∀ {G : Type u_5} [inst : Group G] (a : G), Equiv.mulLeft a = (toUnits a).mulLeft
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.one_not_equiv_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] [IsDomain β] (abv : β → α) [inst_5 : IsAbsoluteValue abv], ¬CauSeq.const abv 1 ≈ CauSeq.const abv 0
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.smul_mem_pointwise_smul_iff₀ : ∀ {M : Type u_1} {R : Type u_2} [inst : GroupWithZero M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] {a : M},
  a ≠ 0 → ∀ (S : Subring R) (x : R), a • x ∈ a • S ↔ x ∈ S
-- Mathlib.Data.List.Chain
List.isChain_cons_of_isChain_cons_pmap : ∀ {α : Type u_1} {β : Type u_2} {R : α → α → Prop} {S : β → β → Prop} {p : α → Prop} (f : (a : α) → p a → β)
  {l : List α} (hl₁ : ∀ a ∈ l, p a) {a : α} (ha : p a),
  List.IsChain S (f a ha :: List.pmap f l hl₁) →
    (∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b) → List.IsChain R (a :: l)
-- Init.Data.Slice.Array.Lemmas
_private.Init.Data.Slice.Array.Lemmas.0.Std.IterStep.successor.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Std.IterStep α β → Sort u_3) (it : α) (out : β)
  (h_1 : (it : α) → (out : β) → motive (Std.IterStep.yield it out)) (h_2 : (it : α) → motive (Std.IterStep.skip it))
  (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it out with
    | Std.IterStep.yield it out => h_1 it out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_1 it out
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.OLeanEntry.key : Lean.KeyedDeclsAttribute.OLeanEntry → Lean.KeyedDeclsAttribute.Key
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.map_symm : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂) (s : AffineSubspace k P₂),
  AffineSubspace.map (↑e.symm) s = AffineSubspace.comap (↑e) s
-- Init.Data.List.MinMaxOn
List.maxOn_eq_of_maxOn?_eq_some : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} {x : α}
  (h : List.maxOn? f xs = some x), List.maxOn f xs ⋯ = x
-- Mathlib.Probability.Distributions.Binomial
/-- The binomial probability distribution with parameter `p` valued in the semiring `R`.  -/
ProbabilityTheory.«termBin(_,_,_)» : Lean.ParserDescr