mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.IsStandardSmoothOfRelativeDimension.isStandardSmooth : ∀ (n : ℕ) {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [H : Algebra.IsStandardSmoothOfRelativeDimension n R S], Algebra.IsStandardSmooth R S
-- Mathlib.CategoryTheory.FinCategory.AsType
CategoryTheory.FinCategory.instFintypeHomObjAsType : (α : Type u_1) →
  [inst : Fintype α] →
    [inst_1 : CategoryTheory.SmallCategory α] →
      [CategoryTheory.FinCategory α] → {i j : CategoryTheory.FinCategory.ObjAsType α} → Fintype (i ⟶ j)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- The 2-isomorphisms agree with the underlying 2-morphism of the lax transformation.  -/
CategoryTheory.Lax.LaxTrans.StrongCore.naturality_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η : F ⟶ G} (self : CategoryTheory.Lax.LaxTrans.StrongCore η) {a b : B}
  (f : a ⟶ b), (self.naturality f).hom = η.naturality f
-- Lean.Util.FindExpr
Lean.Expr.FindStep.visit.sizeOf_spec : sizeOf Lean.Expr.FindStep.visit = 1
-- Mathlib.Topology.TietzeExtension
/-- **Tietze extension theorem** for real-valued continuous maps.
`ℝ` is a `TietzeExtension` space.  -/
Real.instTietzeExtension : TietzeExtension ℝ
-- Mathlib.Order.Nat
Nat.instNoMaxOrder : NoMaxOrder ℕ
-- Mathlib.Algebra.Ring.Commute
Ring.lie_def : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (x y : R), ⁅x, y⁆ = x * y - y * x
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumElim_single_single : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddMonoid M] (a : α) (b : β) (m₁ m₂ : M),
  ((fun₀ | a => m₁).sumElim fun₀ | b => m₂) = (fun₀ | Sum.inl a => m₁) + fun₀ | Sum.inr b => m₂
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.algHomOfLinearMapTensorProduct_apply : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra S C] (f : TensorProduct R A B →ₗ[S] C)
  (h_mul : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂))
  (h_one : f (1 ⊗ₜ[R] 1) = 1) (x : TensorProduct R A B),
  (Algebra.TensorProduct.algHomOfLinearMapTensorProduct f h_mul h_one) x = f x
-- Mathlib.Data.Subtype
Subtype.instSetoid_mathlib : {α : Sort u_1} → [Setoid α] → (p : α → Prop) → Setoid (Subtype p)
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable.eq_1 : ∀ (α : Type u) {σ : Type v} [inst : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] (f : σ),
  Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f =
    ∀ (a : α → Bool), ¬Std.Tactic.BVDecide.LRAT.Internal.Entails.eval a f
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
/-- `bcount p s` is the multiplicity of `p` in the FactorSet `s` (with bundled `p`).  -/
Associates.bcount : {α : Type u_1} →
  [inst : CommMonoidWithZero α] → [DecidableEq (Associates α)] → { a // Irreducible a } → Associates.FactorSet α → ℕ
-- Mathlib.Algebra.Polynomial.BigOperators
/-- The leading coefficient of a product of polynomials is equal to
the product of the leading coefficients, provided that this product is nonzero.

See `Polynomial.leadingCoeff_prod` (without the `'`) for a version for integral domains,
where this condition is automatically satisfied.
 -/
Polynomial.leadingCoeff_prod' : ∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] (f : ι → Polynomial R),
  ∏ i ∈ s, (f i).leadingCoeff ≠ 0 → (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff
-- Mathlib.Algebra.Group.Ext
Group.ext_iff : ∀ {G : Type u_1} {g₁ g₂ : Group G}, g₁ = g₂ ↔ HMul.hMul = HMul.hMul
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.strongInnerAnodyneExtensions.mono : ∀ {X Y : SSet} {f : X ⟶ Y}, SSet.strongInnerAnodyneExtensions f → CategoryTheory.Mono f
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_smul_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_8} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] {f : α → ε} {c : ENNReal},
  c ≠ 0 → c ≠ ⊤ → (MeasureTheory.Integrable f (c • μ) ↔ MeasureTheory.Integrable f μ)
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- The pair `f,g` is a split pair if there is an `h : Y ⟶ Z` so that `f, g, h` forms a split
coequalizer in `C`.
 -/
CategoryTheory.HasSplitCoequalizer : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → (X ⟶ Y) → Prop
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isSome_apply_of_contains_filterMap : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : (↑m).WF)
  (h' : (Std.DHashMap.Internal.Raw₀.filterMap f m).contains k = true), (f k (m.get k ⋯)).isSome = true
-- Mathlib.Algebra.GroupWithZero.Regular
/-- **Alias** of `IsRegular.of_ne_zero`.

---

Non-zero elements of an integral domain are regular.  -/
isRegular_of_ne_zero : ∀ {R : Type u_1} [inst : MulZeroClass R] [IsCancelMulZero R] {a : R}, a ≠ 0 → IsRegular a
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.coe_coalgHom_injective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B],
  Function.Injective CoalgHomClass.toCoalgHom
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- **Alias** of `MulHom.pi_injective`. -/
Pi.mulHom_injective : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Mul (f i)] {γ : Type w} [Nonempty I] [inst_2 : Mul γ]
  (g : (i : I) → γ →ₙ* f i), (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(MulHom.pi g)
-- Mathlib.Data.EReal.Operations
/-- See also `EReal.sub_lt_of_lt_add`.  -/
EReal.sub_lt_of_lt_add' : ∀ {a b c : EReal}, a < b + c → a - b < c
-- Mathlib.Data.Num.Lemmas
PosNum.cast_succ : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (n : PosNum), ↑n.succ = ↑n + 1
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.IterM.InternalCombinators.map : {α β γ : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      [inst : Monad n] →
        (lift : ⦃α : Type w⦄ → m α → n α) →
          [Std.Iterator α m β] → (f : β → Std.Iterators.PostconditionT n γ) → Std.IterM m β → Std.IterM n γ
-- Mathlib.SetTheory.Cardinal.Regular
/-- An inaccessible cardinal is equal to its own cofinality, see `IsInaccessible.isRegular`.  -/
Cardinal.IsInaccessible.le_cof_ord : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible → c ≤ c.ord.cof
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.tendsto_volume_totalLengthFilter_nhds_zero : Filter.Tendsto (fun E => MeasureTheory.volume (⋃ i ∈ Finset.range E.1, Set.uIoc (E.2 i).1 (E.2 i).2))
  AbsolutelyContinuousOnInterval.totalLengthFilter (nhds 0)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DHashMap.Raw.Const.getD (m₁ ∪ m₂) k fallback =
          Std.DHashMap.Raw.Const.getD m₂ k (Std.DHashMap.Raw.Const.getD m₁ k fallback)
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.lTensor_surjective_iff : ∀ {R : Type u} (M : Type v) {N : Type u_1} {P : Type u_2} [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] [Module.Invertible R M] {f : N →ₗ[R] P},
  Function.Surjective ⇑(LinearMap.lTensor M f) ↔ Function.Surjective ⇑f
-- Mathlib.Order.NonemptyFiniteChains
PartialOrder.NonemptyFiniteChains.inst : (X : Type u) → [inst : PartialOrder X] → PartialOrder (PartialOrder.NonemptyFiniteChains X)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
/-- Euler's homogeneous function theorem in projective coordinates.  -/
WeierstrassCurve.Projective.polynomial_relation : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R),
  3 * (MvPolynomial.eval P) W'.polynomial =
    P 0 * (MvPolynomial.eval P) W'.polynomialX + P 1 * (MvPolynomial.eval P) W'.polynomialY +
      P 2 * (MvPolynomial.eval P) W'.polynomialZ
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.closedBall_openSubgroup.eq_1 : ∀ (S : Type u_1) [inst : SeminormedGroup S] [inst_1 : IsUltrametricDist S] {r : ℝ} (hr : 0 < r),
  IsUltrametricDist.closedBall_openSubgroup S hr =
    { carrier := Metric.closedBall 1 r, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯, isOpen' := ⋯ }
-- Mathlib.Algebra.DirectSum.Algebra
GradedMonoid.isScalarTower_right : ∀ {ι : Type uι} (R : Type uR) (A : ι → Type uA) [inst : CommSemiring R] [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : (i : ι) → Module R (A i)] [inst_3 : AddMonoid ι] [inst_4 : DirectSum.GSemiring A] [DirectSum.GAlgebra R A],
  IsScalarTower R (GradedMonoid A) (GradedMonoid A)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.mk.sizeOf_spec : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] [inst_4 : SizeOf R] [inst_5 : SizeOf A] (toNonUnitalSubalgebra : NonUnitalSubalgebra R A)
  (star_mem' : ∀ {a : A}, a ∈ toNonUnitalSubalgebra.carrier → star a ∈ toNonUnitalSubalgebra.carrier),
  sizeOf { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := star_mem' } = 1 + sizeOf toNonUnitalSubalgebra
-- Mathlib.Data.Nat.Bitwise
Nat.testBit_ldiff : ∀ (m n k : ℕ), (m.ldiff n).testBit k = (m.testBit k && !n.testBit k)
-- Init.Data.Range.Polymorphic.NatLemmas
/-- Induction principle for proving properties of `Nat`-based ranges of the form `a...b` by
varying the lower bound.

In the `base` case, one proves that for any `a : Nat` and `b : Nat` with
`b ≤ a`, the statement holds for the empty range `a...b`.

In the `step` case, one proves that for any `a : Nat` and `b : Nat`, the
statement holds for nonempty ranges `a...b` if it holds for the smaller range
`(a + 1)...b`.

The following is an example reproving `length_toList_rco`.

```
example (a b : Nat) : (a...b).toList.length = b - a := by
  induction a, b using Nat.induct_rco_left
  case base =>
    simp only [Nat.toList_rco_eq_nil, List.length_nil, Nat.sub_eq_zero_of_le, *]
  case step =>
    simp only [Nat.toList_rco_eq_cons, List.length_cons, *]; omega
``` -/
Nat.induct_rco_left : ∀ (motive : ℕ → ℕ → Prop),
  (∀ (a b : ℕ), b ≤ a → motive a b) → (∀ (a b : ℕ), a < b → motive (a + 1) b → motive a b) → ∀ (a b : ℕ), motive a b
-- Mathlib.Algebra.Order.Sub.Basic
/-- This lemma also holds for `ENNReal`, but we need a different proof for that.  -/
tsub_lt_tsub_iff_right : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b c : α} [AddLeftReflectLE α], c ≤ a → (a - c < b - c ↔ a < b)
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.of_mul_add_left_right : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsRelPrime x (x * z + y) → IsRelPrime x y
-- Init.Data.BitVec.Bitblast
/-- If the sum of the leading zeroes of two bitvecs with bitwidth `w` is less than or equal to
(`w - 2`), then the preliminary overflow flag is true and their unsigned multiplication overflows.
The explanation is in `Efficient integer multiplication overflow detection circuits`
https://ieeexplore.ieee.org/abstract/document/987767
 -/
BitVec.resRec_of_clz_le : ∀ {w : ℕ} {x y : BitVec w} (hw : 1 < w),
  x ≠ 0#w → y ≠ 0#w → x.clz.toNat + y.clz.toNat ≤ w - 2 → x.resRec y (w - 1) ⋯ ⋯ = true
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The functor `P.Comma L R Q W ⥤ P.Comma L R Q W` induced by the identity natural transformation
on `L` is naturally isomorphic to the identity functor.  -/
CategoryTheory.MorphismProperty.Comma.mapLeftId : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                {P : CategoryTheory.MorphismProperty T} →
                  {Q : CategoryTheory.MorphismProperty A} →
                    {W : CategoryTheory.MorphismProperty B} →
                      [inst_3 : Q.IsMultiplicative] →
                        [inst_4 : W.IsMultiplicative] →
                          [Q.RespectsIso] →
                            [W.RespectsIso] →
                              CategoryTheory.MorphismProperty.Comma.mapLeft R (CategoryTheory.CategoryStruct.id L) ⋯ ≅
                                CategoryTheory.Functor.id (CategoryTheory.MorphismProperty.Comma L R P Q W)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.Real.eventually_atTop_exists_nat_between : ∀ {a b : ℝ}, a < b → 0 ≤ b → ∀ᶠ (x : ℝ) in Filter.atTop, ∃ n, a * x ≤ ↑n ∧ ↑n ≤ b * x
-- Mathlib.RingTheory.Spectrum.Prime.Defs
PrimeSpectrum.equivSubtype_symm_apply_asIdeal : ∀ (R : Type u_1) [inst : CommSemiring R] (I : { I // I.IsPrime }),
  ((RelIso.symm (PrimeSpectrum.equivSubtype R)) I).asIdeal = ↑I
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsUniformizer.iff : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] {v : Valuation A Γ}
  [hv : v.IsRankOneDiscrete] {π : A}, v.IsUniformizer π ↔ v π = ↑(Valuation.IsRankOneDiscrete.generator v)
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
CategoryTheory.IsPreFibered.exists_isCartesian : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) [p.IsPreFibered] {a : 𝒳} {R S : 𝒮},
  p.obj a = S → ∀ (f : R ⟶ S), ∃ b φ, p.IsCartesian f φ
-- Mathlib.Analysis.Normed.Group.Basic
edist_indicator : ∀ {α : Type u_2} {E : Type u_5} [inst : SeminormedAddGroup E] (s t : Set α) (f : α → E) (x : α),
  edist (s.indicator f x) (t.indicator f x) = ↑‖(symmDiff s t).indicator f x‖₊
-- Mathlib.Algebra.CubicDiscriminant
Cubic.natDegree_of_c_eq_zero' : ∀ {R : Type u_1} {d : R} [inst : Semiring R], { a := 0, b := 0, c := 0, d := d }.toPoly.natDegree = 0
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.UsedSimps.mk.injEq : ∀ (map : Lean.PHashMap Lean.Meta.Origin ℕ) (size : ℕ) (map_1 : Lean.PHashMap Lean.Meta.Origin ℕ) (size_1 : ℕ),
  ({ map := map, size := size } = { map := map_1, size := size_1 }) = (map = map_1 ∧ size = size_1)
-- Mathlib.Logic.Equiv.Defs
Equiv.cast_symm : ∀ {α β : Sort u_1} (h : α = β), Equiv.cast ⋯ = (Equiv.cast h).symm
-- Init.Data.Float.Model.Float
/-- Converts an `ISize` to a `Float.Model`, returning positive zero on zero.  -/
Float.Model.ofISize : ISize → Float.Model
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RciSliceData : (α : Type u) → (α → Type v) → [Ord α] → Type (max u v)
-- Mathlib.Order.Hom.Basic
/-- `<` is preserved by order embeddings of preorders.  -/
OrderEmbedding.ltEmbedding : {α : Type u_2} →
  {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → α ↪o β → (fun x1 x2 => x1 < x2) ↪r fun x1 x2 => x1 < x2
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_inter_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∈ m₂ → (m₁ ∩ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.Data.Nat.Factorial.Basic
Nat.mul_factorial_pred : ∀ {n : ℕ}, n ≠ 0 → n * (n - 1).factorial = n.factorial
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_smul_real_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E) (r : ℝ), inner 𝕜 x (↑r • y) = r • inner 𝕜 x y
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.induction_on₂ : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β]
  {p : UniformSpace.Completion α → UniformSpace.Completion β → Prop} (a : UniformSpace.Completion α)
  (b : UniformSpace.Completion β), IsClosed {x | p x.1 x.2} → (∀ (a : α) (b : β), p ↑a ↑b) → p a b
-- Init.Prelude
/-- Encode a hygienic name from the parsed pieces.  -/
Lean.MacroScopesView.review : Lean.MacroScopesView → Lean.Name
-- Mathlib.Topology.MetricSpace.PiNat
/-- `X` equipped with the distance coming from `∀ i, Y i` embeds in `∀ i, Y i`.  -/
Metric.PiNatEmbed.embed : {ι : Type u_2} → (X : Type u_3) → (Y : ι → Type u_4) → (f : (i : ι) → X → Y i) → Metric.PiNatEmbed X Y f → (i : ι) → Y i
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
/-- If the vertex `x` is not in the set `s`, then the induced subgraph in `G.deleteIncidenceSet x`
by `s` is equal to the induced subgraph in `G` by `s`.  -/
SimpleGraph.induce_deleteIncidenceSet_of_notMem : ∀ {V : Type u_1} (G : SimpleGraph V) {s : Set V} {x : V},
  x ∉ s → SimpleGraph.induce s (G.deleteIncidenceSet x) = SimpleGraph.induce s G
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} {T : Set α → β}
  [inst : AddMonoid β] {μ' : MeasureTheory.Measure α},
  (∀ (s : Set α), MeasurableSet s → μ s = ⊤ → μ' s = ⊤) →
    MeasureTheory.FinMeasAdditive μ T → MeasureTheory.FinMeasAdditive μ' T
-- Mathlib.RingTheory.Ideal.Quotient.Operations
AlgHom.liftOfSurjective_comp : ∀ {R : Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : CommRing C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  (f : A →ₐ[R] B) (hf : Function.Surjective ⇑f) (g : A →ₐ[R] C) (H : RingHom.ker f.toRingHom ≤ RingHom.ker g.toRingHom),
  (f.liftOfSurjective hf g H).comp f = g
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Consumer.normal.inj : ∀ {promise promise_1 : IO.Promise (Option Std.Http.Chunk)},
  Std.Http.Body.Channel.Consumer.normal✝ promise = Std.Http.Body.Channel.Consumer.normal✝ promise_1 →
    promise = promise_1
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.subst_into_smul_upcast : ∀ {α : Type u_1} [inst : AddCommGroup α] (l : ℕ) (r : α) (tl : ℕ) (zl : ℤ) (tr t : α),
  l = tl → ↑tl = zl → r = tr → Mathlib.Tactic.Abel.smulg zl tr = t → Mathlib.Tactic.Abel.smul l r = t
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instInhabitedTermElabM : {α : Type} → Inhabited (Lean.Elab.TermElabM α)
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_sum : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F},
  (∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) → deriv (∑ i ∈ u, A i) x = ∑ i ∈ u, deriv (A i) x
-- Mathlib.RingTheory.HopkinsLevitzki
IsSemiprimaryRing.finite_of_isNoetherian : ∀ (R₀ : Type u_1) (R : Type u_2) (M : Type u) [inst : Ring R₀] [inst_1 : Ring R] [inst_2 : Module R₀ R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R₀ M] [inst_5 : Module R M] [IsScalarTower R₀ R M] [IsSemiprimaryRing R]
  [inst_8 : IsScalarTower R₀ R R] [Module.Finite R₀ (R ⧸ Ring.jacobson R)] [IsNoetherian R M], Module.Finite R₀ M
-- Mathlib.FieldTheory.Perfect
iterateFrobeniusEquiv_add : ∀ (R : Type u_1) (p m n : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p],
  iterateFrobeniusEquiv R p (m + n) = (iterateFrobeniusEquiv R p n).trans (iterateFrobeniusEquiv R p m)
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.IsLocallySurjective.imageSieve_mem : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  {inst_1 : CategoryTheory.Category.{v', u'} A} {FA : A → A → Type u_1} {CA : A → Type w'}
  {inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)} {inst_3 : CategoryTheory.ConcreteCategory A FA}
  {F G : CategoryTheory.Functor Cᵒᵖ A} {f : F ⟶ G} [self : CategoryTheory.Presheaf.IsLocallySurjective J f] {U : C}
  (s : CategoryTheory.ToType (G.obj (Opposite.op U))), CategoryTheory.Presheaf.imageSieve f s ∈ J U
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- `Set.ofPred` as a `MeasurableEquiv`.  -/
MeasurableEquiv.setOfPred : {α : Type u_8} → (α → Prop) ≃ᵐ Set α
-- Mathlib.Data.Set.Operations
/-- **Alias** of `Set.mem_ofPred`. -/
Set.mem_setOf : ∀ {α : Type u} {a : α} {p : α → Prop}, a ∈ {x | p x} ↔ p a
-- Init.Data.Float.Model.Unpacked.Round
/-- The next bit after the least significant bit of the mantissa.  -/
Float.Model.UnpackedFloat.ExtendedMantissa.roundBit : Float.Model.UnpackedFloat.ExtendedMantissa → Bool
-- Lean.Parser.Do
Lean.Parser.Term.doSeqItem.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
aestronglyMeasurable_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [CompleteSpace F] [inst_4 : MeasurableSpace 𝕜] [OpensMeasurableSpace 𝕜]
  [SecondCountableTopologyEither 𝕜 F] (f : 𝕜 → F) (μ : MeasureTheory.Measure 𝕜),
  MeasureTheory.AEStronglyMeasurable (deriv f) μ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_unitOfList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.HashMap.Raw.unitOfList l).getKeyD k' fallback = k
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α},
  Std.Internal.List.getValueCast? a [] = none
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- A version of `continuousOn_cfcₙ` over `ℝ≥0` instead of `RCLike 𝕜`.  -/
continuousOn_cfcₙ_nnreal : ∀ (A : Type u_2) [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [ContinuousStar A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  {s : Set NNReal},
  IsCompact s →
    ∀ (f : NNReal → NNReal),
      autoParam (ContinuousOn f s) continuousOn_cfcₙ_nnreal._auto_1 →
        autoParam (f 0 = 0) continuousOn_cfcₙ_nnreal._auto_3 →
          ContinuousOn (fun x => cfcₙ f x) {a | 0 ≤ a ∧ quasispectrum NNReal a ⊆ s}
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.coeAddMonoidHom_apply : ∀ (M : Type u_1) [inst : AddCommMonoid M] (m : M), (DivisibleHull.coeAddMonoidHom M) m = ↑m
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.refl_symm : ∀ {α : Type u_1}, (PartialEquiv.refl α).symm = PartialEquiv.refl α
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
card_orderOf_eq_totient_aux₂ : ∀ {α : Type u_1} [inst : Group α] [inst_1 : DecidableEq α] [inst_2 : Fintype α],
  (∀ (n : ℕ), 0 < n → {a | a ^ n = 1}.card ≤ n) → ∀ {d : ℕ}, d ∣ Fintype.card α → {a | orderOf a = d}.card = d.totient
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instNeg : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : TopologicalSpace R] → [inst_3 : NegZeroClass R] → [ContinuousNeg R] → Neg (ContinuousMapZero X R)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.mk_sum : ∀ {G : Type u_1} {ι : Type u_2} [inst : AddCommGroup G] (N : AddSubgroup G) (s : Finset ι) {f : ι → G},
  ↑(s.sum f) = ∑ i ∈ s, ↑(f i)
-- Mathlib.Order.Max
NoMinOrder.not_acc : ∀ {α : Type u_1} [inst : LT α] [NoMinOrder α] (a : α), ¬Acc (fun x1 x2 => x1 < x2) a
-- Mathlib.Topology.Basic
IsClosed.isLocallyClosed : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsClosed s → IsLocallyClosed s