mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.values_emptyWithCapacity : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {c : ℕ} {β : Type v}, (Std.DHashMap.emptyWithCapacity c).values = []
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ioo_Iic_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α},
  Filter.TendstoIxxClass Set.Ioo (Filter.principal (Set.Iic a)) (Filter.principal (Set.Iio a))
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- Pullback cones to `X` are the same thing as binary fans in `Over X`.  -/
CategoryTheory.Limits.pullbackConeEquivBinaryFan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : Y ⟶ X} →
        {g : Z ⟶ X} →
          CategoryTheory.Limits.PullbackCone f g ≌
            CategoryTheory.Limits.BinaryFan (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk g)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- Auxiliary construction for showing that the free monoidal category is a groupoid. Do not use
this, use `IsIso.inv` instead.  -/
CategoryTheory.FreeMonoidalCategory.inverseAux : {C : Type u} → {X Y : CategoryTheory.FreeMonoidalCategory C} → X.Hom Y → Y.Hom X
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.Modification.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} {app : (a : B) → η.app a ⟶ θ.app a}
  {naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)) (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b)))
      CategoryTheory.Lax.LaxTrans.Modification.naturality._autoParam}
  {app_1 : (a : B) → η.app a ⟶ θ.app a}
  {naturality_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app_1 a) (G.map f))
            (θ.naturality f) =
          CategoryTheory.CategoryStruct.comp (η.naturality f)
            (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app_1 b)))
      CategoryTheory.Lax.LaxTrans.Modification.naturality._autoParam},
  { app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 } → app = app_1
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_sub : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] (m : M) (r s : R),
  MonoidAlgebra.single m (r - s) = MonoidAlgebra.single m r - MonoidAlgebra.single m s
-- Mathlib.ModelTheory.Basic
/-- Interpretation of the relation symbols  -/
FirstOrder.Language.Structure.RelMap : {L : FirstOrder.Language} → {M : Type w} → [self : L.Structure M] → {n : ℕ} → L.Relations n → (Fin n → M) → Prop
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.eq_1 : ∀ (entry : Std.Sat.AIG.Entrypoint ℕ),
  Std.Sat.AIG.toCNF entry =
    match Std.Sat.AIG.toCNF.go✝ entry.aig entry.ref.gate ⋯ (Std.Sat.AIG.toCNF.State.empty✝ entry.aig) with
    | ⟨state, property⟩ => Std.Sat.CNF.add [(entry.ref.gate, !entry.ref.invert)] (Std.Sat.AIG.toCNF.State.cnf✝ state)
-- Mathlib.Topology.Closure
Dense.eq_1 : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), Dense s = ∀ (x : X), x ∈ closure s
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.op2_rightUnitor : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitor f).op2 = CategoryTheory.Bicategory.leftUnitor f.op
-- Init.Data.String.Pattern.Basic
_private.Init.Data.String.Pattern.Basic.0.String.Slice.Pattern.SearchStep.ofSliceFrom.match_1.eq_2 : ∀ {s : String.Slice} {p : s.Pos} (motive : String.Slice.Pattern.SearchStep (s.sliceFrom p) → Sort u_1)
  (l r : (s.sliceFrom p).Pos)
  (h_1 : (l r : (s.sliceFrom p).Pos) → motive (String.Slice.Pattern.SearchStep.rejected l r))
  (h_2 : (l r : (s.sliceFrom p).Pos) → motive (String.Slice.Pattern.SearchStep.matched l r)),
  (match String.Slice.Pattern.SearchStep.matched l r with
    | String.Slice.Pattern.SearchStep.rejected l r => h_1 l r
    | String.Slice.Pattern.SearchStep.matched l r => h_2 l r) =
    h_2 l r
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemQueue.mk.inj : ∀ {kinds : Array Lean.Json.CompressWorkItemKind✝} {values : Array Lean.Json} {objectFieldKeys : Array String}
  {kinds_1 : Array Lean.Json.CompressWorkItemKind✝} {values_1 : Array Lean.Json} {objectFieldKeys_1 : Array String},
  { kinds := kinds, values := values, objectFieldKeys := objectFieldKeys } =
      { kinds := kinds_1, values := values_1, objectFieldKeys := objectFieldKeys_1 } →
    kinds = kinds_1 ∧ values = values_1 ∧ objectFieldKeys = objectFieldKeys_1
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.instEssSurjId : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.Functor.id C).EssSurj
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- The `R[X]`-module `M[X]` for an `R`-module `M`.
This is isomorphic (as an `R`-module) to `M[X]` when `M` is a ring.

We require all the module instances `Module S (PolynomialModule R M)` to factor through `R` except
`Module R[X] (PolynomialModule R M)`.
In this constraint, we have the following instances for example :
- `R` acts on `PolynomialModule R R[X]`
- `R[X]` acts on `PolynomialModule R R[X]` as `R[Y]` acting on `R[X][Y]`
- `R` acts on `PolynomialModule R[X] R[X]`
- `R[X]` acts on `PolynomialModule R[X] R[X]` as `R[X]` acting on `R[X][Y]`
- `R[X][X]` acts on `PolynomialModule R[X] R[X]` as `R[X][Y]` acting on itself

This is also the reason why `R` is included in the alias, or else there will be two different
instances of `Module R[X] (PolynomialModule R[X])`.

See https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2315065.20polynomial.20modules
for the full discussion.
 -/
PolynomialModule : (R : Type u_1) → (M : Type u_2) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [Module R M] → Type u_2
-- Mathlib.Order.Hom.Basic
/-- `Subtype.impEmbedding` as an order embedding.  -/
Subtype.orderEmbedding : {α : Type u_2} → [inst : Preorder α] → {p q : α → Prop} → (∀ (a : α), p a → q a) → { x // p x } ↪o { x // q x }
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.nnnorm_zero : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E], ‖0‖₊ = 0
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.isDPMorphism : ∀ {A : Type u_3} {B : Type u_4} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  {hI : DividedPowers I} {hJ : DividedPowers J} (f : hI.DPMorphism hJ), hI.IsDPMorphism hJ f.toRingHom
-- Init.Data.Int.Basic
Int.negSucc.injEq : ∀ (a a_1 : ℕ), (Int.negSucc a = Int.negSucc a_1) = (a = a_1)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.range_comp_le_range : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (f : A →ₐ[R] B) (g : B →ₐ[R] C), (g.comp f).range ≤ g.range
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Composition of tensor products is tensor product of compositions:
`(f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) = (f₁ ≫ g₁) ⊗ₘ (f₂ ≫ g₂)`
 -/
CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C}
  (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z₁ Z₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁ g₂) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁)
        (CategoryTheory.CategoryStruct.comp f₂ g₂))
      h
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_whiskerRight : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {L₁ L₂ : CategoryTheory.Functor A B} {R₁ R₂ : CategoryTheory.Functor B A} {L : CategoryTheory.Functor B C}
  {R : CategoryTheory.Functor C B} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj : L ⊣ R) (τ : L₂ ⟶ L₁),
  (CategoryTheory.conjugateEquiv (adj₁.comp adj) (adj₂.comp adj)) (CategoryTheory.Functor.whiskerRight τ L) =
    R.whiskerLeft ((CategoryTheory.conjugateEquiv adj₁ adj₂) τ)
-- Mathlib.MeasureTheory.Covering.DensityTheorem
/-- A version of **Lebesgue's density theorem** for a sequence of closed balls whose centers are
not required to be fixed.

See also `Besicovitch.ae_tendsto_measure_inter_div`.  -/
IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [IsUnifLocDoublingMeasure μ] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ]
  (S : Set α) (K : ℝ),
  ∀ᵐ (x : α) ∂μ.restrict S,
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Filter.Tendsto δ l (nhdsWithin 0 (Set.Ioi 0)) →
        (∀ᶠ (j : ι) in l, x ∈ Metric.closedBall (w j) (K * δ j)) →
          Filter.Tendsto (fun j => μ (S ∩ Metric.closedBall (w j) (δ j)) / μ (Metric.closedBall (w j) (δ j))) l (nhds 1)
-- Mathlib.Topology.Sober
genericPoints.component_injective : ∀ {α : Type u_1} [inst : TopologicalSpace α] [T0Space α], Function.Injective genericPoints.component
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.extendIso_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cocone F) {X : C} (f : s.pt ≅ X),
  (s.extendIso f).hom.hom = f.hom
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.foldrM_eq_foldrM_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ},
  Std.TreeMap.Raw.foldrM f init t = Array.foldrM (fun a b => f a.1 a.2 b) init t.toArray
-- Mathlib.Control.Applicative
instLawfulApplicativeConst : ∀ {α : Type u_1} [inst : Monoid α], LawfulApplicative (Functor.Const α)
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.rel_iff : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} {x y : G},
  (DoubleCoset.setoid ↑H ↑K) x y ↔ ∃ a ∈ H, ∃ b ∈ K, y = a * x * b
-- Mathlib.Computability.Partrec
Nat.rfind_dom' : ∀ {p : ℕ →. Bool}, (Nat.rfind p).Dom ↔ ∃ n, true ∈ p n ∧ ∀ {m : ℕ}, m ≤ n → (p m).Dom
-- Mathlib.Data.Set.Basic
Set.union_union_distrib_left : ∀ {α : Type u} (s t u : Set α), s ∪ (t ∪ u) = s ∪ t ∪ (s ∪ u)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.repr_eq : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (hv : LinearIndependent R v) {l : ι →₀ R} {x : ↥(Submodule.span R (Set.range v))},
  (Finsupp.linearCombination R v) l = ↑x → hv.repr x = l
-- Lean.Elab.Match
/-- Elaborate the `match` alternative `alt` using the given `matchType`.
The array `toClear` contains variables that must be cleared before elaborating the `rhs` because
they have been generalized/refined.
 -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabMatchAltView : Array Lean.Elab.Term.Discr →
  Lean.Elab.Term.TermMatchAltView →
    Lean.Expr →
      Array Lean.FVarId →
        ExceptT Lean.Elab.Term.PatternElabException Lean.Elab.TermElabM (Lean.Meta.Match.AltLHS × Lean.Expr)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.instIsScalarTowerSubtypeMemAdjoinSingletonSetCoeRingHomAlgebraMap : ∀ {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : Field A] [inst_1 : Field B] [inst_2 : Field C]
  [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C] [inst_6 : IsScalarTower A B C] (b : B),
  IsScalarTower (↥A⟮b⟯) (↥A⟮(algebraMap B C) b⟯) C
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.mkGTNat : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.IsClosedBelow.eq_1 : ∀ (S : Set Ordinal.{u_1}) (o : Ordinal.{u_1}), Ordinal.IsClosedBelow S o = IsClosed (Subtype.val ⁻¹' S)
-- Mathlib.CategoryTheory.Sites.Point.Comap
/-- Given a continuous functor `F : C ⥤ D` between sites `(C, J)` and `(D, K)`,
and a point `Φ` of `(D, K)`, the fiber functor on sheaves of the
point `Φ.comap F hF` on `(C, J)` identifies to the composition
`F.sheafPullback A J K ⋙ Φ.sheafFiber`.  -/
CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {K : CategoryTheory.GrothendieckTopology D} →
          (Φ : K.Point) →
            (F : CategoryTheory.Functor C D) →
              [inst_2 : CategoryTheory.RepresentablyFlat F] →
                {J : CategoryTheory.GrothendieckTopology C} →
                  (hF : CategoryTheory.CoverPreserving J K F) →
                    [inst_3 : CategoryTheory.InitiallySmall (F.comp Φ.fiber).Elements] →
                      (A : Type u_3) →
                        [inst_4 : CategoryTheory.Category.{v, u_3} A] →
                          [CategoryTheory.Limits.HasProducts A] →
                            [inst_6 : F.IsContinuous J K] →
                              [inst_7 : (F.sheafPushforwardContinuous A J K).IsRightAdjoint] →
                                [inst_8 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u_3} A] →
                                  (Φ.comap F hF).sheafFiber ≅ (F.sheafPullback A J K).comp Φ.sheafFiber
-- Mathlib.Probability.Independence.BoundedContinuousFunction
indepFun_process_of_bcf : ∀ {Ω : Type u_1} {T : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {F : T → Type u_5} {G : Type u_6}
  [inst : (t : T) → TopologicalSpace (F t)] [inst_1 : (t : T) → MeasurableSpace (F t)] [∀ (t : T), BorelSpace (F t)]
  [∀ (t : T), HasOuterApproxClosed (F t)] [inst_4 : TopologicalSpace G] [inst_5 : MeasurableSpace G] [BorelSpace G]
  [HasOuterApproxClosed G] {Y : (t : T) → Ω → F t} {Z : Ω → G} [MeasureTheory.IsZeroOrProbabilityMeasure P],
  AEMeasurable Z P →
    (∀ (t : T), AEMeasurable (Y t) P) →
      (∀ (f : BoundedContinuousFunction G ℝ) (J : Finset T) (g : BoundedContinuousFunction ((t : ↥J) → F ↑t) ℝ),
          ∫ (x : Ω), (fun ω => f (Z ω) * g fun x => Y (↑x) ω) x ∂P =
            (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (fun ω => g fun x => Y (↑x) ω) x ∂P) →
        ProbabilityTheory.IndepFun Z (fun ω t => Y t ω) P
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- `cfcHomSuperset` is continuous in the variable `a : A` when `s : Set 𝕜` is compact and `a`
varies over elements whose spectrum is contained in `s`, all of which satisfy the predicate `p`.  -/
continuous_cfcHomSuperset_left : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p]
  [ContinuousStar A] [inst_6 : TopologicalSpace X] {s : Set 𝕜},
  IsCompact s →
    ∀ (f : C(↑s, 𝕜)) (a : X → A),
      Continuous a →
        ∀ (ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s)
          (ha' : autoParam (∀ (x : X), p (a x)) continuous_cfcHomSuperset_left._auto_1),
          Continuous fun x => (cfcHomSuperset ⋯ ⋯) f
-- Mathlib.Probability.Kernel.Composition.Comp
/-- The **Chapman-Kolmogorov equation**, kernel composition version.
The `n+m`-step transition kernel is the composition of the `n`-step and `m`-step kernels.
Ref. *Meyn-Tweedie* Theorem 3.4.2, page 68  -/
ProbabilityTheory.Kernel.pow_add : ∀ {α : Type u_1} {mα : MeasurableSpace α} (κ : ProbabilityTheory.Kernel α α) (m n : ℕ),
  κ ^ (m + n) = (κ ^ m).comp (κ ^ n)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.all_eq_false_iff_exists_mem_get : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {p : α → Bool}, m.WF → (m.all p = false ↔ ∃ a, ∃ (h : a ∈ m), p (m.get a h) = false)
-- Mathlib.Algebra.Group.Prod
Units.embedProduct.eq_1 : ∀ (α : Type u_6) [inst : Monoid α],
  Units.embedProduct α = { toFun := fun x => (↑x, MulOpposite.op ↑x⁻¹), map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.EpiMono
/-- A constructor for `IsSplitMono f` taking a `SplitMono f` as an argument  -/
CategoryTheory.IsSplitMono.mk' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} (se : CategoryTheory.SplitMono f),
  CategoryTheory.IsSplitMono f
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.insertListIfNewUnit.eq_def : ∀ {α : Type u} [inst : BEq α] (l : List ((_ : α) × Unit)) (toInsert : List α),
  Std.Internal.List.insertListIfNewUnit l toInsert =
    match toInsert with
    | [] => l
    | hd :: tl => Std.Internal.List.insertListIfNewUnit (Std.Internal.List.insertEntryIfNew hd () l) tl
-- Mathlib.Data.NNRat.Defs
Rat.le_toNNRat_iff_coe_le' : ∀ {p : ℚ} {q : ℚ≥0}, 0 < q → (q ≤ p.toNNRat ↔ ↑q ≤ p)
-- Mathlib.Order.Concept
mem_lowerPolar_iff : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t : Set β} {a : α}, a ∈ lowerPolar r t ↔ ∀ ⦃b : β⦄, b ∈ t → r a b
-- Mathlib.Tactic.GRewrite.Core
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.GRewriteLemma.mk : Bool →
  Lean.Expr →
    Lean.Expr → Lean.HeadIndex × ℕ → Array (Lean.MVarId × Array Lean.LocalDecl) → Mathlib.Tactic.GRewrite.GRewriteLemma✝
-- Lean.Elab.AssertExists
/-- `AssertExists` is the structure that carries the data to check whether a declaration or an
import is meant to exist somewhere in a library.  -/
Lean.Elab.Command.AssertExists : Type
-- Mathlib.LinearAlgebra.TensorPower.Basic
/-- The canonical map from `R` to `⨂[R]^0 M` corresponding to the `algebraMap` of the tensor
algebra.  -/
TensorPower.algebraMap₀ : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → R ≃ₗ[R] TensorPower R 0 M
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → ∀ {k a : α} {v : β k}, (t.insertIfNew k v).getKey! a = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKey! a
-- Mathlib.Combinatorics.Matroid.Minor.Delete
/-- **Alias** of `Matroid.delete_delete_eq_delete_sdiff`. -/
Matroid.delete_delete_eq_delete_diff : ∀ {α : Type u_1} (M : Matroid α) (D₁ D₂ : Set α), (M.delete D₁).delete D₂ = (M.delete D₁).delete (D₂ \ D₁)
-- Init.Control.Lawful.Instances
StateT.run'_eq : ∀ {m : Type u_1 → Type u_2} {σ α : Type u_1} [inst : Monad m] (x : StateT σ m α) (s : σ),
  x.run' s = (fun x => x.1) <$> x.run s
-- Lean.Meta.AppBuilder
/-- Given `h : f = g` and `a : α`, returns a proof of `f a = g a`. -/
Lean.Meta.mkCongrFun : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Conv
/-- `first | conv | ...` runs each `conv` until one succeeds, or else fails.  -/
Lean.Parser.Tactic.Conv.first : Lean.ParserDescr
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.leftInvEquiv.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M),
  S.leftInvEquiv hS =
    { toFun := (↑S.fromCommLeftInv).toFun, invFun := fun x => ⟨↑(IsUnit.unit ⋯)⁻¹, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
      map_mul' := ⋯ }
-- Mathlib.Topology.MetricSpace.Thickening
Metric.mem_cthickening_of_dist_le : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] (x y : α) (δ : ℝ) (E : Set α),
  y ∈ E → dist x y ≤ δ → x ∈ Metric.cthickening δ E
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.toLp_eq_toLp : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} (f : MeasureTheory.SimpleFunc α E) (hf : MeasureTheory.MemLp (⇑f) p μ),
  ↑(f.toLp hf) = MeasureTheory.MemLp.toLp (⇑f) hf
-- Mathlib.Algebra.DirectSum.Module
DirectSum.range_lmap : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {N : ι → Type u_1} [inst_3 : (i : ι) → AddCommMonoid (N i)]
  [inst_4 : (i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i),
  (DirectSum.lmap f).range = Submodule.comap (DirectSum.coeFnLinearMap R) (Submodule.pi Set.univ fun i => (f i).range)
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.inertiaDegIn_mul_inertiaDegIn : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (p : Ideal A)
  (P : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] (G : Type u_3) [inst_3 : Group G] [Finite G]
  [inst_5 : MulSemiringAction G B] [IsGaloisGroup G A B] (C : Type u_4) [inst_7 : CommRing C] [inst_8 : Algebra A C]
  [inst_9 : Algebra B C] [Nonempty ↑(P.primesOver C)] [IsScalarTower A B C] (GAC : Type u_5) [inst_12 : Group GAC]
  [Finite GAC] [inst_14 : MulSemiringAction GAC C] [IsGaloisGroup GAC A C] (GBC : Type u_6) [inst_16 : Group GBC]
  [Finite GBC] [inst_18 : MulSemiringAction GBC C] [IsGaloisGroup GBC B C],
  p.inertiaDegIn B * P.inertiaDegIn C = p.inertiaDegIn C
-- Init.Data.String.Basic
String.rawEndPos_push : ∀ {s : String} {c : Char}, (s.push c).rawEndPos = s.rawEndPos + c
-- Lean.Parser.Basic
Lean.Parser.notFollowedByFn : Lean.Parser.ParserFn → String → Lean.Parser.ParserFn
-- Init.Data.List.Range
List.range_succ_eq_map : ∀ {n : ℕ}, List.range (n + 1) = 0 :: List.map Nat.succ (List.range n)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.map_extend_nhdsWithin_eq_image : ∀ {𝕜 : 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} {s : Set M} {y : M},
  y ∈ f.source →
    Filter.map (↑(f.extend I)) (nhdsWithin y s) =
      nhdsWithin (↑(f.extend I) y) (↑(f.extend I) '' ((f.extend I).source ∩ s))
-- Mathlib.NumberTheory.LSeries.Convolution
/-- The L-series of the convolution product `f ⍟ g` of two sequences `f` and `g`
is summable when both L-series are summable.  -/
LSeriesSummable.convolution : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (LSeries.convolution f g) s
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minView!.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (l : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r')),
  l = Std.DTreeMap.Internal.Impl.leaf →
    (match l with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k' v' l' r' => h_2 size k' v' l' r') ≍
      h_1 ()
-- Mathlib.Topology.MetricSpace.Infsep
Set.Nontrivial.einfsep_ne_top : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α}, s.Nontrivial → s.einfsep ≠ ⊤
-- Mathlib.Topology.EMetricSpace.Basic
lebesgue_number_lemma_of_emetric : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α} {ι : Sort u_2} {c : ι → Set α},
  IsCompact s → (∀ (i : ι), IsOpen (c i)) → s ⊆ ⋃ i, c i → ∃ δ > 0, ∀ x ∈ s, ∃ i, Metric.eball x δ ⊆ c i
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_ratCast : ∀ {K : Type u_1} [inst : RCLike K] (n : ℚ), ↑↑n = ↑n