mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Projection
/-- The square of the distance from a point in `s` to `p₂` equals the
sum of the squares of the distances of the two points to the
`orthogonalProjection`.  -/
EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p₁ : P} (p₂ : P),
  p₁ ∈ s →
    dist p₁ p₂ * dist p₁ p₂ =
      dist p₁ ↑((EuclideanGeometry.orthogonalProjection s) p₂) *
          dist p₁ ↑((EuclideanGeometry.orthogonalProjection s) p₂) +
        dist p₂ ↑((EuclideanGeometry.orthogonalProjection s) p₂) *
          dist p₂ ↑((EuclideanGeometry.orthogonalProjection s) p₂)
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromRows_apply_inr : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (i : m₂)
  (j : n), A₁.fromRows A₂ (Sum.inr i) j = A₂ i j
-- Init.Data.List.Basic
List.append_assoc : ∀ {α : Type u} (as bs cs : List α), as ++ bs ++ cs = as ++ (bs ++ cs)
-- Mathlib.AlgebraicTopology.ModelCategory.Transport
HomotopicalAlgebra.trivialFibrations.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  HomotopicalAlgebra.trivialFibrations C = HomotopicalAlgebra.fibrations C ⊓ HomotopicalAlgebra.weakEquivalences C
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.reference : Lean.Lsp.CompletionItemKind
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
Module.basisUnique.congr_simp : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : StrongRankCondition R] (ι : Type u_2) [inst_5 : Unique ι]
  (h : Module.finrank R M = 1), Module.basisUnique ι h = Module.basisUnique ι h
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.instHashable : {w : ℕ} → Hashable (Std.Tactic.BVDecide.BVExpr w)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.Hom.mk.inj : ∀ {M N : SemiNormedGrp₁} {hom' : NormedAddGroupHom M.carrier N.carrier} {normNoninc : hom'.NormNoninc}
  {hom'_1 : NormedAddGroupHom M.carrier N.carrier} {normNoninc_1 : hom'_1.NormNoninc},
  { hom' := hom', normNoninc := normNoninc } = { hom' := hom'_1, normNoninc := normNoninc_1 } → hom' = hom'_1
-- Mathlib.Data.FunLike.IsApply
/-- `IsSubApply F α β` states for all `f g : F` and `x : α`, `(f - g) x = f x - g x`.  -/
IsSubApply : (F : Type u_1) → (α : outParam (Type u_2)) → (β : outParam (Type u_3)) → [FunLike F α β] → [Sub β] → [Sub F] → Prop
-- Init.Data.Vector.Erase
Vector.set_getElem_succ_eraseIdx_succ : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i + 1 < n),
  (xs.eraseIdx (i + 1) h).set i xs[i + 1] ⋯ = xs.eraseIdx i ⋯
-- Mathlib.Algebra.Order.Interval.Basic
Interval.addCommMonoid : {α : Type u_2} → [inst : AddCommMonoid α] → [inst_1 : Preorder α] → [IsOrderedAddMonoid α] → AddCommMonoid (Interval α)
-- Mathlib.Tactic.Simps.Basic
/-- Function elaborating `Config`.  -/
Simps.elabSimpsConfig : Lean.Syntax → optParam Simps.Config { } → optParam Bool false → Lean.CoreM Simps.Config
-- Init.While
Lean.Loop : Type
-- Lean.Meta.Tactic.Split
Lean.Meta.Split.applyMatchSplitter : Lean.MVarId → Lean.Name → Array Lean.Level → Array Lean.Expr → Array Lean.Expr → Lean.MetaM (List Lean.MVarId)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.SimprocEntry.mk.inj : ∀ {toSimprocOLeanEntry : Lean.Meta.Simp.SimprocOLeanEntry} {proc : Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc}
  {toSimprocOLeanEntry_1 : Lean.Meta.Simp.SimprocOLeanEntry}
  {proc_1 : Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc},
  { toSimprocOLeanEntry := toSimprocOLeanEntry, proc := proc } =
      { toSimprocOLeanEntry := toSimprocOLeanEntry_1, proc := proc_1 } →
    toSimprocOLeanEntry = toSimprocOLeanEntry_1 ∧ proc = proc_1
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
addInvariantVectorField_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] (c : 𝕜) (v : AddGroupLieAlgebra I G),
  addInvariantVectorField (c • v) = c • addInvariantVectorField v
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- The `degrees` of a polynomial `p` is a special case of the `weightedTotalDegree` of `p` where
the weights are singletons containing each variable.  -/
MvPolynomial.weightedTotalDegree_singleton : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (p : MvPolynomial σ R),
  MvPolynomial.weightedTotalDegree (fun i => {i}) p = p.degrees
-- Lean.Elab.DocString
Lean.Doc.instBEqSuggestionMode.beq : Lean.Doc.SuggestionMode → Lean.Doc.SuggestionMode → Bool
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.getLast?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.u_sSup_l_image : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisCoinsertion l u) (s : Set β), u (sSup (l '' s)) = sSup s
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A split epi `f` coequalizes `(f ≫ section_ f)` and `(𝟙 X)`.
 -/
CategoryTheory.Limits.isSplitEpiCoequalizes : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.IsSplitEpi f] →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfIsSplitEpi f)
-- Mathlib.Algebra.Colimit.Ring
/-- Noncomputable field structure on the direct limit of fields.
See note [reducible non-instances].  -/
Field.DirectLimit.field : {ι : Type u_1} →
  [inst : Preorder ι] →
    (G : ι → Type u_2) →
      [Nonempty ι] →
        [IsDirectedOrder ι] →
          [inst_3 : (i : ι) → Field (G i)] →
            (f' : (i j : ι) → i ≤ j → G i →+* G j) →
              [DirectedSystem G fun x1 x2 x3 => ⇑(f' x1 x2 x3)] →
                Field (Ring.DirectLimit G fun x1 x2 x3 => ⇑(f' x1 x2 x3))
-- Mathlib.Data.Complex.Basic
Complex.ext_iff : ∀ {z w : ℂ}, z = w ↔ z.re = w.re ∧ z.im = w.im
-- Mathlib.Algebra.Group.Finsupp
Finsupp.coe_neg : ∀ {ι : Type u_1} {G : Type u_6} [inst : NegZeroClass G] (g : ι →₀ G), ⇑(-g) = -⇑g
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- Given a functor `F : C ⥤ D`, `F.op.lan : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁` is the
left Kan extension of `F ⋙ yoneda : C ⥤ Dᵒᵖ ⥤ Type v₁` along `yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁`.  -/
CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeLanOpHomCompULiftYonedaIsoULiftYonedaCompLan : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D)
  [inst_2 : ∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P],
  F.op.lan.IsLeftKanExtension (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan F).hom
-- Init.While
/-- An erased version of `repeatM.impl` that eta-expands better in the compiler.
Can be removed once `repeatM.impl` optimizes to the same code.
 -/
_private.Init.While.0.repeatM.erased : {α : Type u} → {m : Type u → Type v} → [Monad m] → {β : Type u} → [Nonempty β] → (α → m (α ⊕ β)) → α → m β
-- Mathlib.Topology.Compactness.Compact
finite_cover_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X] {U : X → Set X},
  (∀ (x : X), U x ∈ nhds x) → ∃ t, ⋃ x ∈ t, U x = Set.univ
-- Mathlib.GroupTheory.PGroup
IsPGroup.nontrivial_iff_card : ∀ {p : ℕ} {G : Type u_1} [inst : Group G],
  IsPGroup p G → ∀ [hp : Fact (Nat.Prime p)] [Finite G], Nontrivial G ↔ ∃ n > 0, Nat.card G = p ^ n
-- Mathlib.Data.Int.ConditionallyCompleteOrder
Int.csInf_empty : sInf ∅ = 0
-- Init.Data.Sum.Basic
Sum.map_inl : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : α → α') (g : β → β') (x : α),
  Sum.map f g (Sum.inl x) = Sum.inl (f x)
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- Transport evidence that a left lift is a Kan lift across an isomorphism of lifts.  -/
CategoryTheory.Bicategory.LeftLift.IsAbsKan.ofIsoAbsKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} → {g : c ⟶ a} → {s t : CategoryTheory.Bicategory.LeftLift f g} → s.IsAbsKan → (s ≅ t) → t.IsAbsKan
-- Mathlib.RingTheory.Ideal.Operations
Ideal.isCoprime_span_singleton_iff : ∀ {R : Type u} [inst : CommSemiring R] (x y : R), IsCoprime (Ideal.span {x}) (Ideal.span {y}) ↔ IsCoprime x y
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- A norm on an additive group `G` is a function `f : G → ℝ` that preserves zero, is subadditive
and such that `f (-x) = f x` and `f x = 0 → x = 0` for all `x`.  -/
AddGroupNorm : (G : Type u_6) → [AddGroup G] → Type u_6
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
/-- The boundary `∂Δ[n]` of the `n`-th standard simplex  -/
Simplicial.«term∂Δ[_]» : Lean.ParserDescr
-- Init.Data.String.Modify
/-- Replaces the character at a specified position in a string with a new character. If the position is
invalid, the string is returned unchanged.

If both the replacement character and the replaced character are 7-bit ASCII characters and the
string is not shared, then it is updated in-place and not copied.

This is a legacy function. The recommended alternative is `String.Pos.set`, combined with
`String.pos` or another means of obtaining a `String.Pos`.

Examples:
* `"abc".set ⟨1⟩ 'B' = "aBc"`
* `"abc".set ⟨3⟩ 'D' = "abc"`
* `"L∃∀N".set ⟨4⟩ 'X' = "L∃XN"`
* `"L∃∀N".set ⟨2⟩ 'X' = "L∃∀N"` because `'∃'` is a multi-byte character, so the byte index `2` is an
  invalid position.
 -/
String.Pos.Raw.set : String → String.Pos.Raw → Char → String
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor_obj_X₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)),
  (CategoryTheory.Square.fromArrowArrowFunctor.obj f).X₁ = f.left.left
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.isIso_hom_app : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.LeftExtension F) {X : C}
  (h : E.IsPointwiseLeftKanExtensionAt (L.obj X)) [L.Full] [L.Faithful],
  CategoryTheory.IsIso ((CategoryTheory.StructuredArrow.hom E).app X)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.mergeWith_eq_mergeWith! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [inst : Std.LawfulEqOrd α] {mergeFn : (a : α) → β a → β a → β a}
  {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} (h : t₁.Balanced),
  (Std.DTreeMap.Internal.Impl.mergeWith mergeFn t₁ t₂ h).impl = Std.DTreeMap.Internal.Impl.mergeWith! mergeFn t₁ t₂
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.instNeg : {R : Type u} →
  [inst : CommRing R] →
    {M : Type u_1} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {N : Type u_2} → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → Neg (M →ₚₗ[R] N)
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.val_zpow : ∀ {R : Type u_1} [inst : Field R] [inst_1 : StarRing R] (x : ↥(selfAdjoint R)) (z : ℤ), ↑(x ^ z) = ↑x ^ z
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
/-- `f z ^ g z` is analytic if `f z` is not a nonpositive real  -/
AnalyticWithinAt.cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : E → ℂ} {x : E} {s : Set E},
  AnalyticWithinAt ℂ f s x →
    AnalyticWithinAt ℂ g s x → f x ∈ Complex.slitPlane → AnalyticWithinAt ℂ (fun z => f z ^ g z) s x
-- Init.Data.BitVec.Lemmas
BitVec.add_left_eq_self : ∀ {w : ℕ} {x y : BitVec w}, x + y = y ↔ x = 0#w
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_linearMap_pi : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M]
  {ι : Type u_4} [Finite ι], IsNoetherian R ((ι → R) →ₗ[R] M)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_eq_toArray_roo : ∀ {m n : ℤ}, (m<...=n).toArray = (m<...n + 1).toArray
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the tangent of the opposite angle equals the
adjacent side, version subtracting vectors.  -/
Orientation.norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → ‖x‖ / (o.oangle y (y - x)).tan = ‖y‖
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.swapEquiv_inverse_obj_toTwoPointing_toProd : ∀ (X : TwoP), (TwoP.swapEquiv.inverse.obj X).toTwoPointing.toProd = (X.toTwoPointing.toProd.2, X.toTwoPointing.toProd.1)
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.instCoeMonCat.eq_1 : AddGrpCat.instCoeMonCat = { coe := (CategoryTheory.forget₂ AddGrpCat AddMonCat).obj }
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.inf'_univ_eq_ciInf : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLattice α] [inst_1 : Fintype ι] [inst_2 : Nonempty ι]
  (f : ι → α), Finset.univ.inf' ⋯ f = ⨅ i, f i
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.hasseDeriv_comp : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module R V] (k l : ℕ)
  (f : LaurentSeries V),
  (LaurentSeries.hasseDeriv R k) ((LaurentSeries.hasseDeriv R l) f) =
    (k + l).choose k • (LaurentSeries.hasseDeriv R (k + l)) f
-- Mathlib.Algebra.Group.Action.Faithful
instFaithfulSMulMulOpposite_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : SMul α M] [FaithfulSMul α M], FaithfulSMul α Mᵐᵒᵖ
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
/-- Fixing subgroup of iUnion is intersection  -/
fixingSubgroup_iUnion : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] {ι : Sort u_3} {s : ι → Set α},
  fixingSubgroup M (⋃ i, s i) = ⨅ i, fixingSubgroup M (s i)
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorUnivLevelPos : Type
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.instInhabitedSynthM : {α : Type} → Inhabited (Lean.Meta.SynthInstance.SynthM α)
-- Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
/-- **Alias** of `AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap`. -/
AlgebraicGeometry.isOpenImmersion_iff_stalk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.IsOpenImmersion f ↔
    Topology.IsOpenEmbedding ⇑f ∧ ∀ (x : ↥X), CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap f x)
-- Mathlib.Data.Set.Lattice.Image
Set.image2_iUnion₂_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_8} (f : α → β → γ)
  (s : (i : ι) → κ i → Set α) (t : Set β), Set.image2 f (⋃ i, ⋃ j, s i j) t = ⋃ i, ⋃ j, Set.image2 f (s i j) t
-- Init.Data.Vector.Lemmas
Vector.findSome?_toArray : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → Option β} {xs : Vector α n},
  Array.findSome? f xs.toArray = Vector.findSome? f xs
-- Mathlib.LinearAlgebra.Quotient.Pi
Submodule.piQuotientLift.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] {N : Type u_4} [inst_3 : AddCommGroup N] [inst_4 : Module R N]
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (p : (i : ι) → Submodule R (Ms i)) (q : Submodule R N)
  (f : (i : ι) → Ms i →ₗ[R] N) (hf : ∀ (i : ι), p i ≤ Submodule.comap (f i) q),
  Submodule.piQuotientLift p q f hf = (LinearMap.lsum R (fun i => Ms i ⧸ p i) R) fun i => (p i).mapQ q (f i) ⋯
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_toUSize : ∀ (n : UInt32), n.toUSize.toUInt16 = n.toUInt16
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.quasiIso_truncGEMap_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] [inst_4 : ∀ (i : ℤ), HomologicalComplex.HasHomology L i]
  (n : ℤ), QuasiIso (CochainComplex.truncGEMap φ n) ↔ ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i
-- Mathlib.NumberTheory.PrimeCounting
/-- The `n`th prime is greater or equal to `n + 2`.  -/
Nat.add_two_le_nth_prime : ∀ (n : ℕ), n + 2 ≤ Nat.nth Nat.Prime n
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.prepartition_isSubordinate : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] [inst_1 : Fintype ι] (B : BoxIntegral.Box ι) {r : ℝ} (hr : 0 < r),
  1 / ↑n ≤ r → (BoxIntegral.unitPartition.prepartition n B).IsSubordinate fun x => ⟨r, hr⟩
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.constantCoeff_smul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {S : Type u_3} [inst_1 : Semiring S] [inst_2 : Module R S]
  (φ : MvPowerSeries σ S) (a : R), MvPowerSeries.constantCoeff (a • φ) = a • MvPowerSeries.constantCoeff φ
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map f))
      ((t.eTruncLTGEIsoGELT a b).hom.app Y) =
    CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X)
      ((t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map f))
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α}, (m.insertManyIfNewUnit l)[k]! = ()
-- Lean.Environment
Lean.Kernel.instInhabitedDiagnostics : Inhabited Lean.Kernel.Diagnostics
-- Mathlib.Algebra.GroupWithZero.Action.Defs
DistribMulAction.ext : ∀ {M : Type u_12} {A : Type u_13} {inst : Monoid M} {inst_1 : AddMonoid A} {x y : DistribMulAction M A},
  SMul.smul = SMul.smul → x = y
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.rank_toZFSet : ∀ (o : Ordinal.{u_1}), o.toZFSet.rank = o
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_comp_subtype_iff : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔ LinearIndepOn R v s
-- Mathlib.RingTheory.Adjoin.Tower
exists_subalgebra_of_fg : ∀ (A : Type w) (B : Type u₁) (C : Type u_1) [inst : CommSemiring A] [inst_1 : CommSemiring B] [inst_2 : Semiring C]
  [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C] [IsScalarTower A B C],
  ⊤.FG → ⊤.FG → ∃ B₀, B₀.FG ∧ ⊤.FG
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.symm_trans : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup P] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : LieRingModule L M] [inst_9 : LieRingModule L N]
  [inst_10 : LieRingModule L P] (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P), (e₁.trans e₂).symm = e₂.symm.trans e₁.symm
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- Given `(f : B ≃ₐ[A] C)`, if `IsCyclotomicExtension S A B` then
`IsCyclotomicExtension S A C`.  -/
IsCyclotomicExtension.equiv : ∀ (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {C : Type u_1}
  [inst_3 : CommRing C] [inst_4 : Algebra A C] [h : IsCyclotomicExtension S A B] (f : B ≃ₐ[A] C),
  IsCyclotomicExtension S A C
-- Init.Data.UInt.Lemmas
UInt32.sub_neg : ∀ {a b : UInt32}, a - -b = a + b
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.empty_head : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B},
  HNNExtension.NormalWord.empty.head = 1
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.toLinearExpr : Lean.Expr → Lean.MetaM (Int.Internal.Linear.Expr × Array Lean.Expr)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- A morphism of modules is surjective if and only the morphism of exterior algebras that it
induces is surjective.  -/
ExteriorAlgebra.map_surjective_iff : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u4}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N},
  Function.Surjective ⇑(ExteriorAlgebra.map f) ↔ Function.Surjective ⇑f
-- Mathlib.Algebra.Group.ForwardDiff
Polynomial.fwdDiff_iter_degree_add_one_eq_zero : ∀ {R : Type u_3} [inst : CommRing R] (P : Polynomial R),
  ((fwdDiff 1)^[P.natDegree + 1] fun x => Polynomial.eval x P) = 0
-- Mathlib.RingTheory.Regular.RegularSequence
/-- A simplified version of `IsWeaklyRegular.recIterModByRegular` where the
motive is not allowed to depend on the proof of `IsWeaklyRegular`.  -/
RingTheory.Sequence.IsWeaklyRegular.ndrecIterModByRegular : {R : Type u_1} →
  [inst : CommRing R] →
    {motive : (M : Type v) → [inst_1 : AddCommGroup M] → [Module R M] → List R → Sort u_7} →
      ((M : Type v) → [inst_1 : AddCommGroup M] → [inst : Module R M] → motive M []) →
        ({M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] →
                (r : R) →
                  (rs : List R) →
                    IsSMulRegular M r →
                      RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) rs →
                        motive (QuotSMulTop r M) rs → motive M (r :: rs)) →
          {M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] → {rs : List R} → RingTheory.Sequence.IsWeaklyRegular M rs → motive M rs
-- Batteries.Lean.PersistentHashSet
/-- Returns `true` if `f` returns `true` for any element of the set.
 -/
Lean.PersistentHashSet.anyM : {α : Type u_1} →
  [inst : BEq α] →
    [inst_1 : Hashable α] → {m : Type → Type u_2} → [Monad m] → Lean.PersistentHashSet α → (α → m Bool) → m Bool
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.addSimpTheorem : Lean.Meta.SimpTheorems → Lean.Meta.SimpTheorem → Lean.Meta.SimpTheorems
-- Mathlib.Data.List.Intervals
/-- For any natural numbers n, a, and b, one of the following holds:
1. n < a
2. n ≥ b
3. n ∈ Ico a b
 -/
List.Ico.trichotomy : ∀ (n a b : ℕ), n < a ∨ b ≤ n ∨ n ∈ List.Ico a b
-- Mathlib.Data.Real.ConjExponents
/-- Nonnegative real numbers `p q : ℝ≥0` are **Hölder conjugate** if they are positive and satisfy
the equality `p⁻¹ + q⁻¹ = 1`. This is an abbreviation for `NNReal.HolderTriple p q 1`. This
condition shows up in many theorems in analysis, notably related to `L^p` norms.

It is equivalent that `1 < p` and `p⁻¹ + q⁻¹ = 1`. See `NNReal.holderConjugate_iff`.  -/
NNReal.HolderConjugate : NNReal → NNReal → Prop
-- Mathlib.Data.List.AList
AList.mk.inj : ∀ {α : Type u} {β : α → Type v} {entries : List (Sigma β)} {nodupKeys : entries.NodupKeys} {entries_1 : List (Sigma β)}
  {nodupKeys_1 : entries_1.NodupKeys},
  { entries := entries, nodupKeys := nodupKeys } = { entries := entries_1, nodupKeys := nodupKeys_1 } →
    entries = entries_1
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.one_def : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoidWithOne (A i)] [inst_2 : (i : ι) → Module R (A i)], 1 = (PiTensorProduct.tprod R) 1