mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- The space of equivalence classes of almost everywhere strongly measurable functions, where two
strongly measurable functions are equivalent if they agree almost everywhere, i.e.,
they differ on a set of measure `0`.  -/
MeasureTheory.AEEqFun : (α : Type u_1) →
  (β : Type u_2) → [inst : MeasurableSpace α] → [TopologicalSpace β] → MeasureTheory.Measure α → Type (max u_1 u_2)
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_strictMono : StrictMono ENNReal.ofNNReal
-- Mathlib.Topology.PartialHomeomorph.Basic
Topology.IsEmbedding.toPartialHomeomorph.congr_simp : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f f_1 : X → Y)
  (e_f : f = f_1) (h : Topology.IsEmbedding f) [inst_2 : Nonempty X],
  Topology.IsEmbedding.toPartialHomeomorph f h = Topology.IsEmbedding.toPartialHomeomorph f_1 ⋯
-- Mathlib.NumberTheory.LSeries.Linearity
LSeries.term_smul_apply : ∀ (f : ℕ → ℂ) (c s : ℂ) (n : ℕ), LSeries.term (c • f) s n = c * LSeries.term f s n
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.neg_pure : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α] (a : α),
  -NonemptyInterval.pure a = NonemptyInterval.pure (-a)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.homothety_eq_iff_of_mul_eq_one : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] {c p q : P1} {r₁ r₂ : k},
  r₁ * r₂ = 1 → ((AffineMap.homothety c r₁) p = q ↔ (AffineMap.homothety c r₂) q = p)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- If `{Uᵢ}` covers `X`, this is the pre-`0`-hypercover of `X ×[Z] Y` given by `{Uᵢ ×[Z] Y}`.  -/
CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      (E : CategoryTheory.PreZeroHypercover X) →
        {Y Z : C} →
          (f : X ⟶ Z) →
            (g : Y ⟶ Z) →
              [inst_1 : CategoryTheory.Limits.HasPullback f g] →
                [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.f i) f) g] →
                  CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback f g)
-- Init.Data.Array.Basic
Array.instForMOfMonad : {α : Type u} → {m : Type u_1 → Type u_2} → [Monad m] → ForM m (Array α) α
-- Mathlib.Data.Sum.Order
Sum.noMaxOrder : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] [NoMaxOrder α] [NoMaxOrder β], NoMaxOrder (α ⊕ β)
-- Mathlib.FieldTheory.Finite.Basic
/-- If `R` is an algebra over a finite field `K`, the Frobenius `K`-algebra endomorphism of `R` is
given by raising every element of `R` to its `#K`-th power.  -/
FiniteField.frobeniusAlgHom : (K : Type u_1) →
  (R : Type u_2) → [inst : Field K] → [Fintype K] → [inst_2 : CommRing R] → [inst_3 : Algebra K R] → R →ₐ[K] R
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (x, y / x)` is measure-preserving.  -/
MeasureTheory.measurePreserving_prod_div : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [ν.IsMulRightInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.1, z.2 / z.1)) (μ.prod ν) (μ.prod ν)
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.setLIntegral_toKernel_univ : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → StieltjesFunction ℝ}
  [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsCondKernelCDF f κ ν) (a : α) {s : Set β},
  MeasurableSet s →
    ∫⁻ (b : β) in s, ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) (a, b)) Set.univ ∂ν a = (κ a) (s ×ˢ Set.univ)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.mul.eq_1 : ∀ (E : Type u_6) [inst : CommMonoid E] [inst_1 : TopologicalSpace E] [inst_2 : ContinuousMul E],
  ContinuousMonoidHom.mul E = { toMonoidHom := mulMonoidHom, continuous_toFun := ⋯ }
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.mk₂'_apply : ∀ {R : Type u_1} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] {M : Type u_5} {N : Type u_7} {Pₗ : Type u_11}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid Pₗ] [inst_5 : Module R M]
  [inst_6 : Module S N] [inst_7 : Module R Pₗ] [inst_8 : Module S Pₗ] [inst_9 : SMulCommClass S R Pₗ] (f : M → N → Pₗ)
  {H1 : ∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n}
  {H2 : ∀ (c : R) (m : M) (n : N), f (c • m) n = c • f m n}
  {H3 : ∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂}
  {H4 : ∀ (c : S) (m : M) (n : N), f m (c • n) = c • f m n} (m : M) (n : N),
  ((LinearMap.mk₂' R S f H1 H2 H3 H4) m) n = f m n
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.left_unitality_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.LaxMonoidal] (X : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.ε F) (F.obj X))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom) h))
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
CategoryTheory.Limits.Types.range_snd_of_isPullback : ∀ {P X Y Z : Type u} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z},
  CategoryTheory.IsPullback fst snd f g →
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom snd) =
      ⇑(CategoryTheory.ConcreteCategory.hom g) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Data.Ordmap.Ordset
_private.Mathlib.Data.Ordmap.Ordset.0.Ordnode.Bounded.match_1.eq_3 : ∀ {α : Type u_1} (motive : Ordnode α → WithBot α → WithTop α → Sort u_2) (size : ℕ) (l : Ordnode α) (x : α)
  (r : Ordnode α) (o₁ : WithBot α) (o₂ : WithTop α) (h_1 : (a b : α) → motive Ordnode.nil (some a) (some b))
  (h_2 : (x : WithBot α) → (x_1 : WithTop α) → motive Ordnode.nil x x_1)
  (h_3 :
    (size : ℕ) →
      (l : Ordnode α) →
        (x : α) → (r : Ordnode α) → (o₁ : WithBot α) → (o₂ : WithTop α) → motive (Ordnode.node size l x r) o₁ o₂),
  (match Ordnode.node size l x r, o₁, o₂ with
    | Ordnode.nil, some a, some b => h_1 a b
    | Ordnode.nil, x, x_1 => h_2 x x_1
    | Ordnode.node size l x r, o₁, o₂ => h_3 size l x r o₁ o₂) =
    h_3 size l x r o₁ o₂
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.Linear_CC'₀.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
  Profinite.NobelingProof.Linear_CC'₀ C ho =
    LocallyConstant.comapₗ ℤ { toFun := Profinite.NobelingProof.CC'₀ C ho, continuous_toFun := ⋯ }
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageDirection : Type
-- Mathlib.Probability.CDF
ProbabilityTheory.cdf_eq_real : ∀ (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (x : ℝ),
  ↑(ProbabilityTheory.cdf μ) x = μ.real (Set.Iic x)
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.right_edge : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {x y : CategoryTheory.ComposableArrows C 0}
  (e : SSet.Edge x y), CategoryTheory.ComposableArrows.right e.edge = CategoryTheory.nerveEquiv y
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.mul_vle_mul_left : ∀ {R : Type u_1} {inst : Semiring R} [self : ValuativeRel R] {x y : R}, x ≤ᵥ y → ∀ (z : R), x * z ≤ᵥ y * z
-- Mathlib.GroupTheory.Rank
AddGroup.rank_le : ∀ {G : Type u_1} [inst : AddGroup G] [h : AddGroup.FG G] {S : Finset G},
  AddSubgroup.closure ↑S = ⊤ → AddGroup.rank G ≤ S.card
-- Mathlib.LinearAlgebra.DFinsupp
/-- If `(pᵢ)ᵢ` is a family of independent submodules that generates the whole module `N`, then
`N` is isomorphic to the direct sum of the submodules.  -/
iSupIndep.linearEquiv : {ι : Type u_1} →
  {R : Type u_3} →
    {N : Type u_6} →
      [DecidableEq ι] →
        [inst : Ring R] →
          [inst_1 : AddCommGroup N] →
            [inst_2 : Module R N] → {p : ι → Submodule R N} → iSupIndep p → ⨆ i, p i = ⊤ → (Π₀ (i : ι), ↥(p i)) ≃ₗ[R] N
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_target_mem_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {y : M},
  y ∈ f.source → (f.extend I).target ∈ nhdsWithin (↑(f.extend I) y) (Set.range ↑I)
-- Init.System.IO
IO.Process.StdioConfig.mk.injEq : ∀ (stdin stdout stderr stdin_1 stdout_1 stderr_1 : IO.Process.Stdio),
  ({ stdin := stdin, stdout := stdout, stderr := stderr } =
      { stdin := stdin_1, stdout := stdout_1, stderr := stderr_1 }) =
    (stdin = stdin_1 ∧ stdout = stdout_1 ∧ stderr = stderr_1)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
SimpleGraph.chromaticNumber_pathGraph : ∀ (n : ℕ), 2 ≤ n → (SimpleGraph.pathGraph n).chromaticNumber = 2
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- Characterization of `C^n` sections of a vector bundle.  -/
Bundle.contMDiffAt_section : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] {s : (x : B) → E x} (x₀ : B),
  ContMDiffAt IB (IB.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) x₀ ↔
    ContMDiffAt IB (modelWithCornersSelf 𝕜 F) n (fun x => (↑(trivializationAt F E x₀) ⟨x, s x⟩).2) x₀
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.insert_neighborFinset_eq_univ : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableEq V] [inst_2 : DecidableRel G.Adj] (v : V),
  insert v (G.neighborFinset v) = Finset.univ ↔ G.IsUniversal v
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- The Gamma functor as a functor from schemes over `Spec R` to `R`-algebras.  -/
AlgebraicGeometry.algΓ : (R : CommRingCat) → CategoryTheory.Functor (CategoryTheory.Over (AlgebraicGeometry.Spec R)) (CommAlgCat ↑R)ᵒᵖ
-- Mathlib.Algebra.Star.LinearMap
LinearMap.intrinsicStar_eq_comp : ∀ {R : Type u_5} {E : Type u_6} {F : Type u_7} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid E]
  [inst_3 : StarAddMonoid E] [inst_4 : Module R E] [inst_5 : StarModule R E] [inst_6 : AddCommMonoid F]
  [inst_7 : StarAddMonoid F] [inst_8 : Module R F] [inst_9 : StarModule R F] (f : WithConv (E →ₗ[R] F)),
  star f = WithConv.toConv (↑(starLinearEquiv R) ∘ₛₗ f.ofConv ∘ₛₗ ↑(starLinearEquiv R))
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The induced map on finite quotients coming from a morphism to `P`.  -/
ProfiniteGrp.ProfiniteCompletion.quotientMap : {G : GrpCat} →
  {P : ProfiniteGrp.{u}} →
    (f : G ⟶ GrpCat.of ↑P.toProfinite.toTop) →
      (H : OpenNormalSubgroup ↑P.toProfinite.toTop) →
        FiniteGrp.of (↑G ⧸ (ProfiniteGrp.ProfiniteCompletion.preimage f H).toSubgroup) ⟶
          FiniteGrp.of (↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup)
-- Init.Data.String.Basic
String.Slice.Pos.ne_endPos_of_lt : ∀ {s : String.Slice} {p q : s.Pos}, p < q → p ≠ s.endPos
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAtOfComplement.instNormedAddCommGroupSmallComplement : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {F : Type u_5} →
      {H : Type u_7} →
        {G : Type u_9} →
          {E : Type u} →
            [inst : NontriviallyNormedField 𝕜] →
              [inst_1 : NormedAddCommGroup E] →
                [inst_2 : NormedSpace 𝕜 E] →
                  [inst_3 : NormedAddCommGroup E''] →
                    [inst_4 : NormedSpace 𝕜 E''] →
                      [inst_5 : NormedAddCommGroup F] →
                        [inst_6 : NormedSpace 𝕜 F] →
                          [inst_7 : TopologicalSpace H] →
                            [inst_8 : TopologicalSpace G] →
                              {I : ModelWithCorners 𝕜 E H} →
                                {J : ModelWithCorners 𝕜 E'' G} →
                                  {M : Type u_11} →
                                    {N : Type u_13} →
                                      [inst_9 : TopologicalSpace M] →
                                        [inst_10 : ChartedSpace H M] →
                                          [inst_11 : TopologicalSpace N] →
                                            [inst_12 : ChartedSpace G N] →
                                              {n : WithTop ℕ∞} →
                                                {f : M → N} →
                                                  {x : M} →
                                                    (hf : Manifold.IsSubmersionAtOfComplement F I J n f x) →
                                                      NormedAddCommGroup hf.smallComplement
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.lieSpan_eq_bot_iff : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {s : Set M}, LieSubmodule.lieSpan R L s = ⊥ ↔ ∀ m ∈ s, m = 0
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Abelian C}
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} {f₀ : S₁.L₀ ⟶ S₂.L₀} {f₁ : S₁.L₁ ⟶ S₂.L₁} {f₂ : S₁.L₂ ⟶ S₂.L₂}
  {f₃ : S₁.L₃ ⟶ S₂.L₃}
  {comm₀₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₀ S₂.v₀₁ = CategoryTheory.CategoryStruct.comp S₁.v₀₁ f₁)
      CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁._autoParam}
  {comm₁₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ S₂.v₁₂ = CategoryTheory.CategoryStruct.comp S₁.v₁₂ f₂)
      CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂._autoParam}
  {comm₂₃ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ S₂.v₂₃ = CategoryTheory.CategoryStruct.comp S₁.v₂₃ f₃)
      CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃._autoParam}
  {f₀_1 : S₁.L₀ ⟶ S₂.L₀} {f₁_1 : S₁.L₁ ⟶ S₂.L₁} {f₂_1 : S₁.L₂ ⟶ S₂.L₂} {f₃_1 : S₁.L₃ ⟶ S₂.L₃}
  {comm₀₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f₀_1 S₂.v₀₁ = CategoryTheory.CategoryStruct.comp S₁.v₀₁ f₁_1)
      CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁._autoParam}
  {comm₁₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f₁_1 S₂.v₁₂ = CategoryTheory.CategoryStruct.comp S₁.v₁₂ f₂_1)
      CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂._autoParam}
  {comm₂₃_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f₂_1 S₂.v₂₃ = CategoryTheory.CategoryStruct.comp S₁.v₂₃ f₃_1)
      CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃._autoParam},
  { f₀ := f₀, f₁ := f₁, f₂ := f₂, f₃ := f₃, comm₀₁ := comm₀₁, comm₁₂ := comm₁₂, comm₂₃ := comm₂₃ } =
      { f₀ := f₀_1, f₁ := f₁_1, f₂ := f₂_1, f₃ := f₃_1, comm₀₁ := comm₀₁_1, comm₁₂ := comm₁₂_1, comm₂₃ := comm₂₃_1 } →
    f₀ = f₀_1 ∧ f₁ = f₁_1 ∧ f₂ = f₂_1 ∧ f₃ = f₃_1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback v : β}, (m.insert k v).getD k fallback = v
-- Mathlib.Order.Types.Defs
/-- `Quotient.inductionOn` specialized to `OrderType`.  -/
OrderType.inductionOn : ∀ {C : OrderType.{u_1} → Prop} (o : OrderType.{u_1}),
  (∀ (α : Type u_1) [inst : LinearOrder α], C (OrderType.type α)) → C o
-- Init.Data.SInt.Lemmas
Int64.ofIntClamp_int16ToInt : ∀ (x : Int16), Int64.ofIntClamp x.toInt = x.toInt64
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.homogeneousComponent_eq_self : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {n : ℕ} {p : MvPolynomial σ R},
  p.IsHomogeneous n → (MvPolynomial.homogeneousComponent n) p = p
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_of_contains_erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α}, (m.erase k).contains a = true → m.contains a = true
-- Mathlib.Data.Finset.SDiff
Finset.insert_sdiff_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) (x : α), insert x s \ insert x t = s \ insert x t
-- Mathlib.Analysis.Meromorphic.Basic
/-- Analogue of the principle of isolated zeros for an analytic function: if a function is
meromorphic at `z₀`, then either it is identically zero in a punctured neighborhood of `z₀`, or it
does not vanish there at all.  -/
MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜},
  MeromorphicAt f z₀ → (∀ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = 0) ∨ ∀ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z ≠ 0
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_range_add_sub_sum_range : ∀ {G : Type u_3} [inst : AddCommGroup G] (f : ℕ → G) (n m : ℕ),
  ∑ k ∈ Finset.range (n + m), f k - ∑ k ∈ Finset.range n, f k = ∑ k ∈ Finset.range m, f (n + k)
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.mulAction_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {X Y : C}
  (σ : CategoryTheory.Aut F) (f : X ⟶ Y) (x : (F.obj X).obj),
  σ • (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f)) (σ • x)
-- Lean.Expr
/-- `.lam x t b bi` is now the preferred form.
 -/
Lean.mkLambda : Lean.Name → Lean.BinderInfo → Lean.Expr → Lean.Expr → Lean.Expr
-- Lean.Parser.Types
Lean.Parser.FirstTokens.merge : Lean.Parser.FirstTokens → Lean.Parser.FirstTokens → Lean.Parser.FirstTokens
-- Lean.LabelAttribute
/-- Helper function for `registerLabelAttr`.  -/
Lean.mkLabelExt : autoParam Lean.Name Lean.mkLabelExt._auto_1 → IO Lean.LabelExtension
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivQuotOfLEₐ_comp_mkₐ : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {I J : Ideal A}
  (h : I ≤ J),
  (↑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h)).comp (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mkₐ R I) J)) =
    Ideal.Quotient.factorₐ R h
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.XIsoOfEq_inv_naturality : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {K L : HomologicalComplex V c} (φ : K ⟶ L)
  {n n' : ι} (h : n = n'),
  CategoryTheory.CategoryStruct.comp (φ.f n') (L.XIsoOfEq h).inv =
    CategoryTheory.CategoryStruct.comp (K.XIsoOfEq h).inv (φ.f n)
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.ediam_image_le_of_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s : Set X}, HolderOnWith C r f s → ∀ {d : ENNReal}, Metric.ediam s ≤ d → Metric.ediam (f '' s) ≤ ↑C * d ^ ↑r
-- Mathlib.Data.FunLike.IsApply
IsMulApplyEqComp.mul_apply_eq_comp : ∀ {F : Type u_1} {α : outParam (Type u_2)} {inst : FunLike F α α} {inst_1 : Mul F} [self : IsMulApplyEqComp F α]
  (f g : F) (x : α), (f * g) x = f (g x)
-- Lean.Data.NameMap.Basic
Lean.NameSet.instInhabited : Inhabited Lean.NameSet
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.instHashableBVBit.hash : Std.Tactic.BVDecide.BVBit → UInt64
-- Mathlib.Topology.MetricSpace.IsometricSMul
Prod.instIsIsometricSMul : ∀ {M : Type u} {X : Type w} {Y : Type u_1} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y]
  [inst_2 : SMul M X] [IsIsometricSMul M X] [inst_4 : SMul M Y] [IsIsometricSMul M Y], IsIsometricSMul M (X × Y)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.coeff_eq_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R] {n : ℕ}, 3 < n → P.toPoly.coeff n = 0
-- Mathlib.Topology.Category.Compactum
/-- The structure map for a compactum, essentially sending an ultrafilter to its limit.  -/
Compactum.str : (X : Compactum) → Ultrafilter X.A → X.A
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The codomain of a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.HorizontalComp.tgtM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
      Mathlib.Tactic.BicategoryLike.HorizontalComp → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ}
  [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (x : ℝ) {s : Set β},
  MeasurableSet s →
    ∫⁻ (b : β) in s, ENNReal.ofReal (↑(ProbabilityTheory.stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
      (κ a) (s ×ˢ Set.Iic x)
-- Lean.Environment
/-- Environment extensions can only be registered during initialization.
Reasons:
1- Our implementation assumes the number of extensions does not change after an environment object is created.
2- We do not use any synchronization primitive to access `envExtensionsRef`.

Note that by default, extension state is *not* stored in .olean files and will not propagate across `import`s.
For that, you need to register a persistent environment extension.  -/
Lean.registerEnvExtension : {σ : Type} →
  IO σ →
    optParam (Option (Lean.ReplayFn σ)) none →
      optParam Lean.EnvExtension.AsyncMode Lean.EnvExtension.AsyncMode.mainOnly → IO (Lean.EnvExtension σ)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.pow_one_cast_of_isNat : ∀ {R : Type u_1} [inst : CommSemiring R] (a : R) (b : ℕ), Mathlib.Meta.NormNum.IsNat b 1 → a ^ b = a
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
_private.Mathlib.AlgebraicGeometry.Morphisms.FlatRank.0.AlgebraicGeometry.IsAffine.finrank_of_isPullback : ∀ {X S Y T : AlgebraicGeometry.Scheme} (f : X ⟶ S) [inst : AlgebraicGeometry.IsAffine S]
  [inst_1 : AlgebraicGeometry.IsAffine T] (f' : Y ⟶ T) (g' : Y ⟶ X) (g : T ⟶ S),
  CategoryTheory.IsPullback g' f' f g →
    ∀ [AlgebraicGeometry.Flat f] [AlgebraicGeometry.IsFinite f] (s : ↥S) (t : ↥T),
      g t = s → AlgebraicGeometry.IsAffine.finrank✝ f' t = AlgebraicGeometry.IsAffine.finrank✝ f s
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
instPartialOrderHomogeneousSubmodule_1 : {ιA : Type u_1} →
  {ιM : Type u_2} →
    {σA : Type u_3} →
      {σM : Type u_4} →
        {A : Type u_5} →
          {M : Type u_6} →
            [inst : Semiring A] →
              [inst_1 : AddCommMonoid M] →
                [inst_2 : Module A M] →
                  (𝒜 : ιA → σA) →
                    (ℳ : ιM → σM) →
                      [inst_3 : DecidableEq ιA] →
                        [inst_4 : AddMonoid ιA] →
                          [inst_5 : SetLike σA A] →
                            [inst_6 : AddSubmonoidClass σA A] →
                              [inst_7 : GradedRing 𝒜] →
                                [inst_8 : DecidableEq ιM] →
                                  [inst_9 : SetLike σM M] →
                                    [inst_10 : AddSubmonoidClass σM M] →
                                      [inst_11 : DirectSum.Decomposition ℳ] →
                                        [inst_12 : VAdd ιA ιM] →
                                          [inst_13 : SetLike.GradedSMul 𝒜 ℳ] → PartialOrder (HomogeneousSubmodule 𝒜 ℳ)