mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.SInt.Lemmas
ISize.toInt8_add : ∀ (a b : ISize), (a + b).toInt8 = a.toInt8 + b.toInt8
-- Lean.DocString.Parser
/-- The context within which a block should be valid.
 -/
Lean.Doc.Parser.BlockCtxt : Type
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects colimits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F : C ⥤ D` reflects
limits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.reflectsLimit_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimit K.op F.op],
  CategoryTheory.Limits.ReflectsLimit K F
-- Mathlib.CategoryTheory.EssentialImage
/-- The functor `F` factorises through its essential image, where the first functor is essentially
surjective and the second is fully faithful.
 -/
CategoryTheory.Functor.toEssImageCompι : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → F.toEssImage.comp F.essImage.ι ≅ F
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.measurableSet_generateFrom_countablePartition_iff : ∀ {α : Type u_1} [m : MeasurableSpace α] [h : MeasurableSpace.CountablyGenerated α] (n : ℕ) (s : Set α),
  MeasurableSet s ↔ ∃ S, ↑S ⊆ MeasurableSpace.countablePartition α n ∧ s = ⋃₀ ↑S
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasKernel S.g]
  [inst_3 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)],
  (CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel S).i = CategoryTheory.Limits.kernel.ι S.g
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.omega0_ne_zero : Ordinal.omega0 ≠ 0
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.dropWhile_eq_toSlice_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.ForwardPattern pat]
  [String.Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String},
  s.dropWhile pat = s.toSlice ↔ s.startsWith pat = false
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instNoZeroDivisors : ∀ {α : Type u_1} [inst : Mul α], NoZeroDivisors (WithZero α)
-- Mathlib.Order.Lattice
Prod.swap_sup : ∀ (α : Type u) (β : Type v) [inst : Max α] [inst_1 : Max β] (p q : α × β), (p ⊔ q).swap = p.swap ⊔ q.swap
-- Mathlib.Data.Num.Bitwise
/-- Add an active bit at the end of a `NzsNum`. This mimics `PosNum.bit1`.  -/
NzsNum.bit1 : NzsNum → NzsNum
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- Topology generated by a set of charts on a Type.  -/
ChartedSpaceCore.toTopologicalSpace : {H : Type u} → {M : Type u_2} → [inst : TopologicalSpace H] → ChartedSpaceCore H M → TopologicalSpace M
-- Init.SimpLemmas
Eq.mpr_not : ∀ {p q : Prop}, p = q → ¬q → ¬p
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- A locally-full and cover-dense functor `G` induces an equivalence between morphisms into a sheaf and
morphisms over the restrictions via `G`.
 -/
CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {K : CategoryTheory.GrothendieckTopology D} →
          {A : Type u_4} →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} A] →
              {G : CategoryTheory.Functor C D} →
                [G.IsCoverDense K] →
                  [G.IsLocallyFull K] →
                    {ℱ : CategoryTheory.Functor Dᵒᵖ A} →
                      {ℱ' : CategoryTheory.Sheaf K A} → (G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) ≃ (ℱ ⟶ ℱ'.obj)
-- Mathlib.Order.Types.Defs
/-- `Quotient.liftOn₂` specialized to `OrderType`.  -/
OrderType.liftOn₂ : {δ : Sort v} →
  OrderType.{u_1} →
    OrderType.{u_2} →
      (f : (α : Type u_1) → [LinearOrder α] → (β : Type u_2) → [LinearOrder β] → δ) →
        (∀ (α₁ : Type u_1) [inst : LinearOrder α₁] (β₁ : Type u_2) [inst_1 : LinearOrder β₁] (α₂ : Type u_1)
            [inst_2 : LinearOrder α₂] (β₂ : Type u_2) [inst_3 : LinearOrder β₂],
            OrderType.type α₁ = OrderType.type α₂ → OrderType.type β₁ = OrderType.type β₂ → f α₁ β₁ = f α₂ β₂) →
          δ
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- Theorem of Rudio (Wielandt, 1964, Th. 8.1)

For a preprimitive additive action, a subset which is neither empty nor full has a translate
which contains a given point and avoids another one.  -/
AddAction.IsPreprimitive.exists_mem_vadd_and_notMem_vadd : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [AddAction.IsPreprimitive G X] {A : Set X},
  A.Finite → A.Nonempty → A ≠ Set.univ → ∀ {a b : X}, a ≠ b → ∃ g, a ∈ g +ᵥ A ∧ b ∉ g +ᵥ A
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.Measure.toFiniteAux.eq_1 : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SFinite μ],
  μ.toFiniteAux = if MeasureTheory.IsFiniteMeasure μ then μ else ⋯.choose
-- Lean.Expr
/-- Return `true` if the given `BinderInfo` is an instance implicit annotation (e.g., `[Decidable α]`)  -/
Lean.BinderInfo.isInstImplicit : Lean.BinderInfo → Bool
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (t.alter k f).isEmpty = ((t.isEmpty || t.size == 1 && t.contains k) && (f (t.get? k)).isNone)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.maxD_erase_eq_of_not_compare_maxD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  t.erase k ≠ ∅ → ¬cmp k (t.maxD fallback) = Ordering.eq → (t.erase k).maxD fallback = t.maxD fallback
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst.injEq : ∀ (k₁ k₂ : ℤ) (c₁ : Lean.Meta.Grind.Arith.Linear.EqCnstr) (c₂ : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) (k₁_1 k₂_1 : ℤ)
  (c₁_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr) (c₂_1 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr),
  (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst k₁ k₂ c₁ c₂ =
      Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst k₁_1 k₂_1 c₁_1 c₂_1) =
    (k₁ = k₁_1 ∧ k₂ = k₂_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.hasForgetToFinPartOrd : CategoryTheory.HasForget₂ FinBddDistLat FinPartOrd
-- Mathlib.Data.Nat.Prime.Basic
Nat.dvd_of_forall_prime_mul_dvd : ∀ {a b : ℕ}, (∀ (p : ℕ), Nat.Prime p → p ∣ a → p * a ∣ b) → a ∣ b
-- Init.Data.List.Nat.Prod
List.prod_append_nat : ∀ {l₁ l₂ : List ℕ}, (l₁ ++ l₂).prod = l₁.prod * l₂.prod
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.eq_1 : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R],
  ClassGroup R = ((FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ ⧸ (toPrincipalIdeal R (FractionRing R)).range)
-- Init.Data.List.MinMaxOn
List.minOn_mem : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {xs : List α} {f : α → β} {h : xs ≠ []},
  List.minOn f xs h ∈ xs
-- Std.Data.ExtDTreeMap.Basic
/-- Implementation detail of the tree map  -/
Std.ExtDTreeMap.liftOn₂ : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {γ : Sort w} →
        Std.ExtDTreeMap α β cmp →
          Std.ExtDTreeMap α β cmp →
            (f : Std.DTreeMap α β cmp → Std.DTreeMap α β cmp → γ) →
              (∀ (a b c d : Std.DTreeMap α β cmp), a.Equiv c → b.Equiv d → f a b = f c d) → γ
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.eq_ones_iff_length : ∀ {n : ℕ} {c : Composition n}, c = Composition.ones n ↔ c.length = n
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₃.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 3}
  (app₀ app₀_1 : f.obj' 0 _proof_297✝ ⟶ g.obj' 0 _proof_297✝) (e_app₀ : app₀ = app₀_1)
  (app₁ app₁_1 : f.obj' 1 _proof_298✝ ⟶ g.obj' 1 _proof_298✝) (e_app₁ : app₁ = app₁_1)
  (app₂ app₂_1 : f.obj' 2 _proof_299✝ ⟶ g.obj' 2 _proof_299✝) (e_app₂ : app₂ = app₂_1)
  (app₃ app₃_1 : f.obj' 3 _proof_300✝ ⟶ g.obj' 3 _proof_300✝) (e_app₃ : app₃ = app₃_1)
  (w₀ :
    CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝) app₁ =
      CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝))
  (w₁ :
    CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_299✝) app₂ =
      CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_299✝))
  (w₂ :
    CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_300✝) app₃ =
      CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_300✝)),
  CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂ =
    CategoryTheory.ComposableArrows.homMk₃ app₀_1 app₁_1 app₂_1 app₃_1 ⋯ ⋯ ⋯
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- If a map between pseudometric spaces is a uniform inducing map then the distance between `f x`
and `f y` is controlled in terms of the distance between `x` and `y`.  -/
Metric.controlled_of_isUniformInducing : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  IsUniformInducing f →
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_findM? : ∀ {γ : Type w} [inst : Lean.Order.PartialOrder γ] {m : Type → Type} [inst_1 : Monad m]
  [inst_2 : (α : Type) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m] {α : Type} (f : γ → α → m Bool)
  (xs : Array α), Lean.Order.monotone f → Lean.Order.monotone fun x => Array.findM? (f x) xs
-- Mathlib.RingTheory.Algebraic.Basic
IsAlgebraic.ringHom_of_comp_eq : ∀ {R : Type u} {S : Type u_1} {A : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R A] {B : Type u_2} [inst_4 : Ring B] [inst_5 : Algebra S B] {FRS : Type u_3} {FAB : Type u_4}
  [inst_6 : FunLike FRS R S] [inst_7 : RingHomClass FRS R S] [inst_8 : FunLike FAB A B] [inst_9 : RingHomClass FAB A B]
  (f : FRS) (g : FAB) {a : A},
  IsAlgebraic R a → Function.Injective ⇑f → (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A) → IsAlgebraic S (g a)
-- Mathlib.Analysis.Analytic.CPolynomialDef
CPolynomialAt_congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {x : E},
  f =ᶠ[nhds x] g → (CPolynomialAt 𝕜 f x ↔ CPolynomialAt 𝕜 g x)
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNormClass.toNonarchAddGroupSeminormClass : ∀ {F : Type u_6} {α : outParam (Type u_7)} {inst : AddGroup α} {inst_1 : FunLike F α ℝ}
  [self : NonarchAddGroupNormClass F α], NonarchAddGroupSeminormClass F α
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.mk.inj : ∀ {α : Type} {state state_1 : Std.Mutex (Std.CloseableChannel.Bounded.State✝ α)},
  { state := state } = { state := state_1 } → state = state_1
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.funLike : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] → [inst_1 : SeminormedAddCommGroup V₂] → FunLike (NormedAddGroupHom V₁ V₂) V₁ V₂
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.hasRightHomology_of_epi_of_isIso_of_mono' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [S₂.HasRightHomology] [CategoryTheory.Epi φ.τ₁]
  [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃], S₁.HasRightHomology
-- Init.Data.Range.Polymorphic.UInt
UInt32.instLawfulUpwardEnumerableLT : Std.PRange.LawfulUpwardEnumerableLT UInt32
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.mk'.congr_simp : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (x x_1 : ↥X) (e_x : x = x_1) (y y_1 : ↥Y) (e_y : y = y_1)
  (h : f x = g y),
  AlgebraicGeometry.Scheme.Pullback.Triplet.mk' x y h = AlgebraicGeometry.Scheme.Pullback.Triplet.mk' x_1 y_1 ⋯
-- Mathlib.Order.Heyting.Basic
hnot_inf : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, ￢(a ⊓ b) = ￢a ⊔ ￢b
-- Mathlib.Data.Finset.Union
Finset.biUnion_subset_biUnion_of_subset_left : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Finset α} [inst : DecidableEq β] (t : α → Finset β),
  s₁ ⊆ s₂ → s₁.biUnion t ⊆ s₂.biUnion t
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.sup_primeHeight_eq_ringKrullDim : ∀ {R : Type u_1} [inst : CommRing R] [Nontrivial R], ↑(⨆ I, ⨆ (x : I.IsPrime), Ideal.primeHeight✝ I) = ringKrullDim R
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.card_box : ∀ {n d : ℕ}, (Behrend.box n d).card = d ^ n
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₁_of_lt_opow : ∀ {a : Ordinal.{u}}, a < Ordinal.omega0 ^ a → a.invVeblen₁ = 0
-- Mathlib.Data.List.Defs
/-- Given a decidable predicate `p` and a proof of existence of `a ∈ l` such that `p a`,
choose the first element with this property. This version returns `a : α`, and properties
are given by `choose_mem` and `choose_property`.  -/
List.choose : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → (l : List α) → (∃ a ∈ l, p a) → α
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_hom_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.mop =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor { unmop := X }).hom
-- Lean.Widget.InteractiveGoal
/-- Identifies the goal (ie with the unique name of the MVar that it is a goal for.)  -/
Lean.Widget.InteractiveGoal.mvarId : Lean.Widget.InteractiveGoal → Lean.MVarId
-- Mathlib.CategoryTheory.Yoneda
/-- If `F` is corepresentable, it is, modulo universe lifting, isomorphic to
`Hom(X, -)` for the corepresenting object `X`.  -/
CategoryTheory.Functor.uliftCoyonedaCoreprXIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor C (Type (max v v₁))) →
      [inst_1 : F.IsCorepresentable] → CategoryTheory.uliftCoyoneda.{v, v₁, u₁}.obj (Opposite.op F.coreprX) ≅ F
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.edgeSet_subgraphOfAdj : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (hvw : G.Adj v w), (G.subgraphOfAdj hvw).edgeSet = {s(v, w)}
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.Precylinder.op_P : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.Precylinder A),
  P.op.P = Opposite.op P.I
-- Mathlib.Topology.Homeomorph.Lemmas
IsHomeomorph.isEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → Topology.IsEmbedding f
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.forget_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Comon C), (CategoryTheory.Comon.forget C).obj A = A.X
-- Init.Data.Rat.Basic
Rat.mk'.inj : ∀ {num : ℤ} {den : ℕ} {den_nz : autoParam (den ≠ 0) Rat.den_nz._autoParam}
  {reduced : autoParam (num.natAbs.Coprime den) Rat.reduced._autoParam} {num_1 : ℤ} {den_1 : ℕ}
  {den_nz_1 : autoParam (den_1 ≠ 0) Rat.den_nz._autoParam}
  {reduced_1 : autoParam (num_1.natAbs.Coprime den_1) Rat.reduced._autoParam},
  { num := num, den := den, den_nz := den_nz, reduced := reduced } =
      { num := num_1, den := den_1, den_nz := den_nz_1, reduced := reduced_1 } →
    num = num_1 ∧ den = den_1
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.poissonPMFReal.eq_1 : ∀ (r : NNReal) (n : ℕ), ProbabilityTheory.poissonPMFReal r n = Real.exp (-↑r) * ↑r ^ n / ↑n.factorial
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.nthRoot.eq_1 : ∀ (x : ℕ), Nat.nthRoot 0 x = 1
-- Mathlib.Algebra.Ring.Invertible
pos_of_invertible_cast : ∀ {R : Type u_1} [inst : NonAssocSemiring R] [Nontrivial R] (n : ℕ) [Invertible ↑n], 0 < n
-- Init.Data.String.Basic
String.Slice.Pos.sliceTo_inj : ∀ {s : String.Slice} {p₀ pos pos' : s.Pos} {h : pos ≤ p₀} {h' : pos' ≤ p₀},
  p₀.sliceTo pos h = p₀.sliceTo pos' h' ↔ pos = pos'
-- Init.Data.Rat.Lemmas
Rat.natCast_inj : ∀ {a b : ℕ}, ↑a = ↑b ↔ a = b
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.SupportsStmt.match_1.eq_6 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5)
  (l : σ → Λ) (h_1 : (k : K) → (a : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k a q))
  (h_2 : (k : K) → (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k a q))
  (h_3 : (k : K) → (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k a q))
  (h_4 : (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q))
  (h_5 : (a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (l : σ → Λ) → motive (Turing.TM2.Stmt.goto l)) (h_7 : Unit → motive Turing.TM2.Stmt.halt),
  (match Turing.TM2.Stmt.goto l with
    | Turing.TM2.Stmt.push k a q => h_1 k a q
    | Turing.TM2.Stmt.peek k a q => h_2 k a q
    | Turing.TM2.Stmt.pop k a q => h_3 k a q
    | Turing.TM2.Stmt.load a q => h_4 a q
    | Turing.TM2.Stmt.branch a q₁ q₂ => h_5 a q₁ q₂
    | Turing.TM2.Stmt.goto l => h_6 l
    | Turing.TM2.Stmt.halt => h_7 ()) =
    h_6 l
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a b : α},
  cmp a b = Ordering.eq → Std.ExtDTreeMap.Const.get! t a = Std.ExtDTreeMap.Const.get! t b
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.divLeft_symm_apply : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α] (a : α) (a_1 : αᵒᵈ),
  (RelIso.symm (OrderIso.divLeft a)) a_1 = (OrderDual.ofDual a_1)⁻¹ * a
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_monomial : ∀ {R : Type u} {a : R} [inst : CommRing R] [inst_1 : IsDomain R],
  a ≠ 0 → ∀ (n : ℕ), ((Polynomial.monomial n) a).roots = n • {0}
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Algebra.Order.AddTorsor
instIsOrderedSMulOfIsOrderedMonoid : ∀ {G : Type u_1} [inst : CommMonoid G] [inst_1 : Preorder G] [IsOrderedMonoid G], IsOrderedSMul G G
-- Mathlib.Algebra.DirectSum.Internal
listProd_apply_eq_zero : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : AddCommMonoid ι] [inst_1 : LinearOrder ι] [IsOrderedAddMonoid ι]
  [inst_3 : DecidableEq ι] [inst_4 : Semiring R] [inst_5 : SetLike σ R] [inst_6 : AddSubmonoidClass σ R] {A : ι → σ}
  [inst_7 : SetLike.GradedMonoid A] [CanonicallyOrderedAdd ι] {l : List (DirectSum ι fun i => ↥(A i))} {m : ι},
  (∀ x ∈ l, ∀ k < m, x k = 0) → ∀ ⦃n : ι⦄, n < l.length • m → l.prod n = 0
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.IsTruncGE.mem_next : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} [self : e.IsTruncGE]
  {j : ι} {k' : ι'}, c'.Rel (e.f j) k' → ∃ k, e.f k = k'
-- Init.Data.Vector.Count
Vector.count_push_of_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {b a : α} {xs : Vector α n},
  b ≠ a → Vector.count a (xs.push b) = Vector.count a xs
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.map.congr_simp : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {L : Type u_3}
  {W : Type u_4} [inst_3 : DivisionRing L] [inst_4 : AddCommGroup W] [inst_5 : Module L W] {σ : K →+* L}
  (f f_1 : V →ₛₗ[σ] W) (e_f : f = f_1) (hf : Function.Injective ⇑f) (a a_1 : Projectivization K V),
  a = a_1 → Projectivization.map f hf a = Projectivization.map f_1 ⋯ a_1
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
Submonoid.apply_ne_one_of_mem_or_inv_mem_closure : ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S] [inst_2 : InvolutiveInv ι]
  [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι),
  (∀ i ∈ s, 1 < f (v i)) →
    ∀ (i : ι),
      v i ≠ 1 → v i⁻¹ = (v i)⁻¹ → v i ∈ Submonoid.closure (v '' s) ∨ (v i)⁻¹ ∈ Submonoid.closure (v '' s) → f (v i) ≠ 1
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.coe_injective : Function.Injective Complex.UnitDisc.coe
-- Mathlib.Data.Finset.Update
Function.updateFinset_univ : ∀ {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [inst : DecidableEq ι] [inst_1 : Fintype ι]
  {y : (i : ↥Finset.univ) → π ↑i}, Function.updateFinset x Finset.univ y = fun i => y ⟨i, ⋯⟩
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_pi_congr : ∀ {ι ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι'),
  (∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g (e i))) → Cardinal.mk ((i : ι) → f i) = Cardinal.mk ((i : ι') → g i)
-- Mathlib.Logic.Equiv.Defs
Equiv.mk.congr_simp : ∀ {α : Sort u_1} {β : Sort u_2} (toFun toFun_1 : α → β) (e_toFun : toFun = toFun_1) (invFun invFun_1 : β → α)
  (e_invFun : invFun = invFun_1) (left_inv : Function.LeftInverse invFun toFun)
  (right_inv : Function.RightInverse invFun toFun),
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
    { toFun := toFun_1, invFun := invFun_1, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
/-- The category of simplicial sets.
This is the category of contravariant functors from
`SimplexCategory` to `Type u`.  -/
SSet : Type (u + 1)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.filter_eq_toIter_filter_toIterM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} [Monad m] {f : β → Bool},
  Std.Iter.filter f it = (Std.IterM.filter f it.toIterM).toIter
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
QuotientGroup.measurableSpace : {G : Type u_6} → [inst : Group G] → [MeasurableSpace G] → (S : Subgroup G) → MeasurableSpace (G ⧸ S)
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.denote'.go.match_1.eq_3 : ∀ (motive : Lean.Grind.CommRing.Poly → Sort u_1) (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly)
  (h_1 : Unit → motive (Lean.Grind.CommRing.Poly.num 0)) (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Poly.num k))
  (h_3 :
    (k : ℤ) →
      (m : Lean.Grind.CommRing.Mon) → (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k m p)),
  (match Lean.Grind.CommRing.Poly.add k m p with
    | Lean.Grind.CommRing.Poly.num 0 => h_1 ()
    | Lean.Grind.CommRing.Poly.num k => h_2 k
    | Lean.Grind.CommRing.Poly.add k m p => h_3 k m p) =
    h_3 k m p