mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.LocalRing.Subring
/-- If a (semi)ring `R` in which every element is either invertible or a zero divisor
embeds in a local (semi)ring `S`, then `R` is local.  -/
IsLocalRing.of_injective : ∀ {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [IsLocalRing S] {f : R →+* S},
  Function.Injective ⇑f → (∀ a ∈ nonZeroDivisors R, IsUnit a) → IsLocalRing R
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.tensorHom.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ Y₁ X₂ Y₂ : CategoryTheory.Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  CategoryTheory.Center.tensorHom f g = { f := CategoryTheory.MonoidalCategoryStruct.tensorHom f.f g.f, comm := ⋯ }
-- Mathlib.Algebra.Order.Ring.InjSurj
/-- Pullback an `IsOrderedRing` under an injective map.  -/
Function.Injective.isOrderedRing : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [inst_3 : Semiring S]
  [inst_4 : PartialOrder S] (f : S → R),
  f 0 = 0 →
    f 1 = 1 →
      (∀ (x y : S), f (x + y) = f x + f y) →
        (∀ (x y : S), f (x * y) = f x * f y) → (∀ {x y : S}, f x ≤ f y ↔ x ≤ y) → IsOrderedRing S
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.infty_coeFn_intCast : ∀ {I : Type u_5} {B : I → Type u_6} [inst : (i : I) → NormedRing (B i)] [inst_1 : ∀ (i : I), NormOneClass (B i)]
  (z : ℤ), ↑↑z = ↑z
-- Mathlib.MeasureTheory.Measure.Regular
/-- If a measure `μ` admits finite spanning open sets such that the restriction of `μ` to each set
is outer regular, then the original measure is outer regular as well.  -/
MeasureTheory.Measure.FiniteSpanningSetsIn.outerRegular : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α]
  {μ : MeasureTheory.Measure α} (s : μ.FiniteSpanningSetsIn {U | IsOpen U ∧ (μ.restrict U).OuterRegular}),
  μ.OuterRegular
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Iso.hom_inv_id_triangle_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (e : A ≅ B),
  CategoryTheory.CategoryStruct.comp e.hom.hom₁ e.inv.hom₁ = CategoryTheory.CategoryStruct.id A.obj₁
-- Std.Data.HashMap.Lemmas
/-- Simpler variant of `getD_filter` when `LawfulBEq` is available.  -/
Std.HashMap.getD_filter' : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] {f : α → β → Bool}
  {k : α} {fallback : β}, (Std.HashMap.filter f m).getD k fallback = (Option.filter (f k) m[k]?).getD fallback
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ici_of_Ico : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {d : ι → α}
  {B : α},
  Filter.Tendsto d l Filter.atTop →
    ∀ [NoMaxOrder α], MeasureTheory.AECover (μ.restrict (Set.Ici B)) l fun i => Set.Ico B (d i)
-- Init.Data.SInt.Lemmas
ISize.zero_ne_one : 0 ≠ 1
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.mk_coe : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℤ_[p]), ⟨↑k, ⋯⟩ = k
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getThenInsertIfNew?_snd : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {v : β k}, (m.getThenInsertIfNew? k v).2 = m.insertIfNew k v
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanced_singleR : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (ls : ℕ) (lk : α) (lv : β lk)
  (ll lr r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced →
    r.Balanced →
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond ls r.size ∨
          Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size ls →
        ls > Std.DTreeMap.Internal.delta * r.size →
          lr.size < Std.DTreeMap.Internal.ratio * ll.size →
            (Std.DTreeMap.Internal.Impl.singleR k v lk lv ll lr r).Balanced
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.uniformContinuous_lift' : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : T0Space β] (f : α → β),
  UniformContinuous (SeparationQuotient.lift' f)
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.getSuggestions : Lean.TSyntax `tactic → Array Lean.Meta.Tactic.TryThis.Suggestion
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsRadical.radical_le_iff : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, J.IsRadical → (I.radical ≤ J ↔ I ≤ J)
-- Init.Data.SInt.Bitwise
Int64.ofBitVec_intMax : Int64.ofBitVec (BitVec.intMax 64) = Int64.maxValue
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Cat.freeMap_map : ∀ {V : Type u_1} {W : Type u_2} [inst : Quiver V] [inst_1 : Quiver W] (F : V ⥤q W) {X Y : CategoryTheory.Paths V}
  (a : Quiver.Path X Y), (CategoryTheory.Cat.freeMap F).map a = F.mapPath a
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiffWithinAt_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x : E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5}
  [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ι → E → 𝔸'},
  (∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x) → ContDiffWithinAt 𝕜 n (fun y => ∏ i ∈ t, f i y) s x
-- Mathlib.RingTheory.Spectrum.Prime.Basic
/-- Also see `PrimeSpectrum.isClosed_singleton_iff_isMaximal`  -/
PrimeSpectrum.isMax_iff : ∀ {R : Type u} [inst : CommSemiring R] {x : PrimeSpectrum R}, IsMax x ↔ x.asIdeal.IsMaximal
-- Std.Do.WP.Sound
Std.Do.WPSound.mk : ∀ {m : Type u → Type v} {ps : outParam Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WP m ps],
  (∀ {α : Type u} {x : m α} {P : α → Prop},
      (⊢ₛ (Std.Do.wp x).apply (Std.Do.PostCond.mayThrow fun a => ⌜P a⌝)) → Std.Do.Internal.Ensures P x) →
    Std.Do.WPSound m ps
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.coe_eq : ∀ (α : Type u_1) [inst : UniformSpace α], UniformSpace.Completion.coe' = SeparationQuotient.mk ∘ CauchyFilter.pureCauchy
-- Mathlib.NumberTheory.LSeries.Basic
/-- The value of the L-series of the sequence `f` at the point `s`
if it converges absolutely there, and `0` otherwise.  -/
LSeries : (ℕ → ℂ) → ℂ → ℂ
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
UniqueFactorizationMonoid.finprod_pow_count_eq_of_subsingleton_units : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : UniqueFactorizationMonoid R] [inst_2 : NormalizationMonoid R]
  [inst_3 : DecidableEq R] [Subsingleton Rˣ] {x : R},
  x ≠ 0 → ∏ᶠ (p : R), p ^ Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = x
-- Init.Data.List.Basic
List.mem_append_right : ∀ {α : Type u} {b : α} (as : List α) {bs : List α}, b ∈ bs → b ∈ as ++ bs
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF), m₁.size + m₂.size = (m₁.union m₂ ⋯ ⋯).size + (m₁.inter m₂ ⋯).size
-- Mathlib.CategoryTheory.Limits.Final
/-- Initial functors preserve cofilteredness.

This can be seen as a generalization of `IsCofiltered.of_left_adjoint` (which states that left
adjoints preserve cofilteredness), as right adjoints are always initial,
see `initial_of_adjunction`.
 -/
CategoryTheory.IsCofiltered.of_initial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Initial] [CategoryTheory.IsCofiltered C], CategoryTheory.IsCofiltered D
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleMatch.doc? : LeanSearchClient.LoogleMatch → Option String
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.faithfulSMul : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : SMulZeroClass S R] [FaithfulSMul S R],
  FaithfulSMul S (Polynomial R)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C},
  (CategoryTheory.CategoryStruct.id X).mop = CategoryTheory.CategoryStruct.id { unmop := X }
-- Init.Data.List.Sublist
List.Subset.refl : ∀ {α : Type u_1} (l : List α), l ⊆ l
-- Mathlib.CategoryTheory.Subterminal
/-- The inclusion of the subterminal objects into the original category.  -/
CategoryTheory.subterminalInclusion : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor (CategoryTheory.Subterminals C) C
-- Init.Data.BitVec.Lemmas
/-- For all bitvectors `x, y`, either `x` is unsigned less than `y`,
or is equal to `y`, or is unsigned greater than `y`.  -/
BitVec.lt_trichotomy : ∀ {w : ℕ} (x y : BitVec w), x < y ∨ x = y ∨ y < x
-- Lean.Attributes
Lean.mkAttributeImplOfEntry : Lean.AttributeExtensionOLeanEntry → IO Lean.AttributeImpl
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.toSubsemiring_strictMono : ∀ {R : Type u} [inst : NonAssocRing R], StrictMono Subring.toSubsemiring
-- Mathlib.Algebra.WithConv
WithConv.instAddCommGroup : {A : Type u_2} → [AddCommGroup A] → AddCommGroup (WithConv A)
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_add : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → (a + b).toReal = a.toReal + b.toReal
-- Mathlib.CategoryTheory.Preadditive.LeftExact
/-- A functor between preadditive categories which preserves cokernels preserves all finite
colimits.  -/
CategoryTheory.Functor.preservesFiniteColimits_of_preservesCokernels : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteCoproducts C]
  [CategoryTheory.Limits.HasCoequalizers C] [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.Limits.HasZeroObject D]
  [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F],
  CategoryTheory.Limits.PreservesFiniteColimits F
-- Mathlib.Order.Bounded
Set.bounded_lt_Ico : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Set.Bounded (fun x1 x2 => x1 < x2) (Set.Ico a b)
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.ofComposition_surj : ∀ {n : ℕ}, Function.Surjective (Nat.Partition.ofComposition n)
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.RepresentablyFlat.id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.RepresentablyFlat (CategoryTheory.Functor.id C)
-- Std.Http.Internal.IndexMultiMap
/-- Checks if a key exists in the map.
 -/
Std.Internal.IndexMultiMap.contains : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.Internal.IndexMultiMap α β → α → Bool
-- Std.Time.Zoned.Database.TzIf
/-- The number of local time types in the file.
 -/
Std.Time.TimeZone.TZif.Header.typecnt : Std.Time.TimeZone.TZif.Header → UInt32
-- Init.Data.String.Basic
String.Pos.toSlice_next : ∀ {s : String} {p : s.Pos} {h : p ≠ s.endPos}, (p.next h).toSlice = p.toSlice.next ⋯
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_aeval : ∀ {R : Type u} [inst : CommSemiring R] {A : Type u_1} [inst_1 : Semiring A] [inst_2 : Algebra R A] (p : ℕ)
  (P : Polynomial R) (r : A), (Polynomial.aeval r) ((Polynomial.expand R p) P) = (Polynomial.aeval (r ^ p)) P
-- Lean.Server.GoTo
Lean.Server.instBEqGoToKind : BEq Lean.Server.GoToKind
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.mem_ofStabilizer_iff : ∀ (G : Type u_1) [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] (a : α) {x : α},
  x ∈ SubMulAction.ofStabilizer G a ↔ x ≠ a
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.comp : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ι → Type u_10}
  {γ : ι → Type u_11} {mβ : (i : ι) → MeasurableSpace (β i)} {mγ : (i : ι) → MeasurableSpace (γ i)}
  {f : (i : ι) → Ω → β i},
  ProbabilityTheory.iIndepFun f μ →
    ∀ (g : (i : ι) → β i → γ i), (∀ (i : ι), Measurable (g i)) → ProbabilityTheory.iIndepFun (fun i => g i ∘ f i) μ
-- Mathlib.RingTheory.Finiteness.Bilinear
Submodule.FG.map₂ : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] N →ₗ[R] P) {p : Submodule R M} {q : Submodule R N},
  p.FG → q.FG → (Submodule.map₂ f p q).FG
-- Batteries.Recycling.RBTree.WF
/-- Applies `f` to the second component.
We extract this as a function so that `IsMonotone (mapSnd f)` can be an instance.
 -/
RBTree.RBMap.Imp.mapSnd : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → β → γ) → α × β → α × γ
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.add_sum_Ico_eq_sum_Icc : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {f : α → M} {a b : α} [inst_1 : PartialOrder α]
  [inst_2 : LocallyFiniteOrder α], a ≤ b → f b + ∑ x ∈ Finset.Ico a b, f x = ∑ x ∈ Finset.Icc a b, f x
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.NormalExpr.cons.sizeOf_spec : ∀ (e : Mathlib.Tactic.BicategoryLike.Mor₂) (α : Mathlib.Tactic.BicategoryLike.Structural)
  (η : Mathlib.Tactic.BicategoryLike.WhiskerLeft) (ηs : Mathlib.Tactic.BicategoryLike.NormalExpr),
  sizeOf (Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs) = 1 + sizeOf e + sizeOf α + sizeOf η + sizeOf ηs
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
/-- The pretopology defined by `P`-covers agrees with the
intersection of the pretopology of surjective families with the pretopology defined by `P`.
 -/
AlgebraicGeometry.Scheme.pretopology_eq_inf : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative],
  AlgebraicGeometry.Scheme.pretopology P = AlgebraicGeometry.Scheme.jointlySurjectivePretopology ⊓ P.pretopology
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.preimage_basicOpen_top : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (r : ↑(Y.presheaf.obj (Opposite.op ⊤))),
  (TopologicalSpace.Opens.map f.base).obj (Y.basicOpen r) =
    X.basicOpen ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f)) r)
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
ZMod.injective_stdAddChar : ∀ {N : ℕ} [inst : NeZero N], Function.Injective ⇑ZMod.stdAddChar
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intValuationDef.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v v_1 : IsDedekindDomain.HeightOneSpectrum R),
  v = v_1 → ∀ (r r_1 : R), r = r_1 → v.intValuationDef r = v_1.intValuationDef r_1
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.girth.eq_1 : ∀ {α : Type u_1} (G : SimpleGraph α), G.girth = G.egirth.toNat
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- The length of a Hamiltonian cycle is the number of vertices.  -/
SimpleGraph.Walk.IsHamiltonianCycle.length_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a} [inst_1 : Fintype α],
  p.IsHamiltonianCycle → p.length = Fintype.card α
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
/-- Variant of `sum_eq_zero_iff_forall_eq` with integer coefficients.  -/
IsPrimitiveRoot.sum_eq_zero_iff_forall_eq_int : ∀ {K : Type u_1} [inst : Field K] [CharZero K] {p : ℕ} {ζ : K},
  Nat.Prime p → IsPrimitiveRoot ζ p → ∀ (α : Fin p → ℤ), ∑ i, ↑(α i) * ζ ^ ↑i = 0 ↔ ∀ (i j : Fin p), α i = α j
-- Mathlib.LinearAlgebra.Projectivization.Collinear
Projectivization.line_unique' : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {u v : V}
  (hu : u ≠ 0) (hv : v ≠ 0),
  LinearIndependent K ![u, v] →
    ∀ (p : Submodule K V),
      Module.finrank K ↥p = 2 →
        Projectivization.mk K u hu ∈ Submodule.projectivization p →
          Projectivization.mk K v hv ∈ Submodule.projectivization p → p = Submodule.span K {u, v}
-- Mathlib.Data.Finite.Defs
/-- `Infinite α` is not `Finite`  -/
not_finite : ∀ (α : Sort u_3) [Infinite α] [Finite α], False
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
/-- A $C^{k+(α)}$ map is a $C^k$ map.  -/
ContDiffPointwiseHolderAt.contDiffAt : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {f : E → F} {a : E},
  ContDiffPointwiseHolderAt k α f a → ContDiffAt ℝ (↑k) f a
-- Init.Data.Fin.Lemmas
Fin.le_of_lt : ∀ {n : ℕ} {a b : Fin n}, a < b → a ≤ b
-- Lean.Environment
Lean.OLeanLevel.private.sizeOf_spec : sizeOf Lean.OLeanLevel.private = 1
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.stmts₁.match_1.eq_3 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → Sort u_4) (a : Γ → σ → σ)
  (q : Turing.TM1.Stmt Γ Λ σ)
  (h_1 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.move a q → motive (Turing.TM1.Stmt.move a q))
  (h_2 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Γ → σ → Γ) →
        (q : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.write a q → motive (Turing.TM1.Stmt.write a q))
  (h_3 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.load a q → motive (Turing.TM1.Stmt.load a q))
  (h_4 :
    (Q : Turing.TM1.Stmt Γ Λ σ) →
      (a : Γ → σ → Bool) →
        (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → Q = Turing.TM1.Stmt.branch a q₁ q₂ → motive (Turing.TM1.Stmt.branch a q₁ q₂))
  (h_5 : (Q : Turing.TM1.Stmt Γ Λ σ) → motive Q),
  (match Turing.TM1.Stmt.load a q with
    | Q@h:(Turing.TM1.Stmt.move a q) => h_1 Q a q h
    | Q@h:(Turing.TM1.Stmt.write a q) => h_2 Q a q h
    | Q@h:(Turing.TM1.Stmt.load a q) => h_3 Q a q h
    | Q@h:(Turing.TM1.Stmt.branch a q₁ q₂) => h_4 Q a q₁ q₂ h
    | Q => h_5 Q) =
    h_3 (Turing.TM1.Stmt.load a q) a q ⋯
-- Mathlib.Data.Finset.SMulAntidiagonal
Finset.isPWO_support_vaddAntidiagonal : ∀ {G : Type u_1} {P : Type u_2} [inst : VAdd G P] [inst_1 : PartialOrder G] [inst_2 : PartialOrder P]
  [inst_3 : IsOrderedCancelVAdd G P] {s : Set G} {t : Set P} (hs : s.IsPWO) (ht : t.IsPWO),
  {a | (Finset.VAddAntidiagonal a ⋯).Nonempty}.IsPWO
-- Init.Data.Fin.Fold
Fin.foldl_eq_foldlM : ∀ {α : Type u_1} {n : ℕ} (f : α → Fin n → α) (x : α),
  Fin.foldl n f x = (Fin.foldlM n (fun x1 x2 => pure (f x1 x2)) x).run
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
/-- A functor `F : C ⥤ H` has a pointwise left derived functor with respect to
`W : MorphismProperty C` if it has a pointwise left derived functor at `X`
for any `X : C`.  -/
CategoryTheory.Functor.HasPointwiseLeftDerivedFunctor : {C : Type u₁} →
  {H : Type u₃} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} H] →
        CategoryTheory.Functor C H → CategoryTheory.MorphismProperty C → Prop
-- Init.Data.Nat.Div.Basic
Nat.add_mul_mod_self_left : ∀ (x y z : ℕ), (x + y * z) % y = x % y
-- Init.SimpLemmas
iff_and_self : ∀ {p q : Prop}, (p ↔ q ∧ p) ↔ p → q
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.algebraMap_eq_one_iff : ∀ {R : Type u_1} (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : R),
  (algebraMap R (SymmetricAlgebra R M)) x = 1 ↔ x = 1
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α}, ∅.isEmpty = true
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveCodeProps.mk : Lean.Widget.CodeWithInfos → ProofWidgets.InteractiveCodeProps
-- Mathlib.GroupTheory.Congruence.Defs
Con.instCompleteLattice.eq_1 : ∀ {M : Type u_1} [inst : Mul M],
  Con.instCompleteLattice =
    { toSemilatticeSup := (completeLatticeOfInf (Con M) ⋯).toSemilatticeSup,
      inf := fun c d => { toSetoid := c.toSetoid ⊓ d.toSetoid, mul' := ⋯ }, inf_le_left := ⋯, inf_le_right := ⋯,
      le_inf := ⋯, toSupSet := (completeLatticeOfInf (Con M) ⋯).toSupSet, isLUB_sSup := ⋯,
      toInfSet := (completeLatticeOfInf (Con M) ⋯).toInfSet, isGLB_sInf := ⋯,
      top :=
        let __src := ⊤;
        { toSetoid := __src, mul' := ⋯ },
      le_top := ⋯,
      bot :=
        let __src := ⊥;
        { toSetoid := __src, mul' := ⋯ },
      bot_le := ⋯ }
-- Init.System.FilePath
/-- Extracts the last element of a path if it is a file or directory name.

Returns `none` if the last entry is a special name (such as `.` or `..`) or if the path is the root
directory.
 -/
System.FilePath.fileName : System.FilePath → Option String
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
/-- Given `P : ObjectProperty C`, we say that `P` is closed under subobjects,
if for any monomorphism `X ⟶ Y`, `P Y` implies `P X`.  -/
CategoryTheory.ObjectProperty.IsClosedUnderSubobjects : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.MeasureTheory.MeasurableSpace.Card
/-- If a sigma-algebra is generated by a set of sets `s` with cardinality at most the continuum,
then the sigma algebra has the same cardinality bound.  -/
MeasurableSpace.cardinal_measurableSet_le_continuum : ∀ {α : Type u} {s : Set (Set α)},
  Cardinal.mk ↑s ≤ Cardinal.continuum → Cardinal.mk ↑{t | MeasurableSet t} ≤ Cardinal.continuum
-- Std.Internal.Do.PredTrans
/-- Unfolding `pushOption` through `apply`.  -/
Std.Internal.Do.PredTrans.apply_pushOption : ∀ {α Pred : Type u} {EPred : Type v} (x : Std.Internal.Do.PredTrans Pred EPred (Option α)) (post : α → Pred)
  (epost : EPost.Cons✝ Pred EPred),
  x.pushOption.apply post epost = x.apply (Std.Internal.Do.EPost.Cons.pushOption post epost) epost.tail
-- Mathlib.Data.Fin.SuccPred
finCongr_symm_apply_coe : ∀ {n m : ℕ} (h : m = n) (k : Fin n), ↑((finCongr h).symm k) = ↑k
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_le_of_le_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {T : AddSubmonoid N} {f : F},
  S ≤ AddSubmonoid.comap f T → AddSubmonoid.map f S ≤ T
-- Mathlib.Order.CompactlyGenerated.Basic
WellFoundedLT.finite_of_sSupIndep : ∀ {α : Type u_2} [inst : CompleteLattice α] [WellFoundedLT α] {s : Set α}, sSupIndep s → s.Finite
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
/-- If `F` is a prestack for a Grothendieck topology `J` and `F` is a stack
for a covering presieve `R`, then it is also a stack for `R'` if `R ≤ R'`.  -/
CategoryTheory.Pseudofunctor.IsStackFor.of_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C}
  {R : CategoryTheory.Presieve S},
  F.IsStackFor R →
    ∀ {J : CategoryTheory.GrothendieckTopology C},
      CategoryTheory.Sieve.generate R ∈ J S →
        ∀ [F.IsPrestack J] {R' : CategoryTheory.Presieve S}, R ≤ R' → F.IsStackFor R'
-- Init.Data.Float.Model.Unpacked.Basic
Float.Model.instReprUnpackedFloat.repr : Float.Model.UnpackedFloat → ℕ → Std.Format
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.hasPushout_of_epi_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : W ⟶ X)
  [CategoryTheory.Epi h] [CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp h f) (CategoryTheory.CategoryStruct.comp h g)
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
/-- Auxiliary definition for `ExtraDegeneracy.homotopy`.  -/
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject.Augmented C} →
      X.ExtraDegeneracy →
        {n : ℕ} → Fin (n + 1) → (X.left.obj (Opposite.op { len := n }) ⟶ X.left.obj (Opposite.op { len := n + 1 }))