mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.BaseChange
Localization.tensorLeftAlgEquiv_apply_one_tmul : ∀ {R : Type u_10} [inst : CommRing R] (M : Submonoid R) (S : Type u_12) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (x : Localization M),
  (Localization.tensorLeftAlgEquiv M S) (1 ⊗ₜ[R] x) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M))) x
-- Mathlib.LinearAlgebra.Projectivization.Constructions
Projectivization.cross_mk_of_ne : ∀ {F : Type u_1} [inst : Field F] [inst_1 : DecidableEq F] {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0)
  (h : Projectivization.mk F v hv ≠ Projectivization.mk F w hw),
  (Projectivization.mk F v hv).cross (Projectivization.mk F w hw) = Projectivization.mk F ((crossProduct v) w) ⋯
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- Left whiskering for morphisms  -/
CategoryTheory.Bicategory.whiskerLeft : {B : Type u} →
  [self : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : a ⟶ b) →
        {g h : b ⟶ c} → (g ⟶ h) → (CategoryTheory.CategoryStruct.comp f g ⟶ CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Topology.Germ
/-- The map `Germ (𝓝 x) E → E` into a `𝕜`-module `E` as a `𝕜`-linear map  -/
Filter.Germ.valueₗ : {X : Type u_4} →
  {𝕜 : Type u_5} →
    {E : Type u_6} →
      [inst : Semiring 𝕜] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : Module 𝕜 E] → [inst_3 : TopologicalSpace X] → {x : X} → (nhds x).Germ E →ₗ[𝕜] E
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.diagram_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C), D.diagram.right = D.U
-- Mathlib.Algebra.Group.Units.Hom
/-- The group homomorphism on units induced by a `MonoidHom`.  -/
Units.map : {M : Type u} → {N : Type v} → [inst : Monoid M] → [inst_1 : Monoid N] → (M →* N) → Mˣ →* Nˣ
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mrange_comp : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {O : Type u_5}
  [inst_2 : AddZeroClass O] (f : N →+ O) (g : M →+ N),
  AddMonoidHom.mrange (f.comp g) = AddSubmonoid.map f (AddMonoidHom.mrange g)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_5} {ε' : Type u_6}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [inst_2 : TopologicalSpace ε'] [inst_3 : ContinuousENorm ε']
  {f : α → ε} {g : α → ε'} {c : NNReal},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ) → ∀ (p : ENNReal), MeasureTheory.eLpNorm f p μ ≤ c • MeasureTheory.eLpNorm g p μ
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
CategoryTheory.Iso.toIsometryEquiv_symm : ∀ {R : Type u} [inst : CommRing R] {X Y : QuadraticModuleCat R} (e : X ≅ Y),
  e.symm.toIsometryEquiv = e.toIsometryEquiv.symm
-- Init.Data.LawfulHashable
/-- The `BEq α` and `Hashable α` instances on `α` are compatible. This means that `a == b` implies
`hash a = hash b`.

This is automatic if the `BEq` instance is lawful.
 -/
LawfulHashable : (α : Type u) → [BEq α] → [Hashable α] → Prop
-- Mathlib.Order.Sublattice
Sublattice.pi_univ_eq_bot : ∀ {κ : Type u_5} {π : κ → Type u_6} [inst : (i : κ) → Lattice (π i)] {L : (i : κ) → Sublattice (π i)} {i : κ},
  L i = ⊥ → Sublattice.pi Set.univ L = ⊥
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- The prime spectrum of `R × S` is homeomorphic
to the disjoint union of `PrimeSpectrum R` and `PrimeSpectrum S`.  -/
PrimeSpectrum.primeSpectrumProdHomeo : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] → [inst_1 : CommSemiring S] → PrimeSpectrum (R × S) ≃ₜ PrimeSpectrum R ⊕ PrimeSpectrum S
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.ext_iff : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] {f g : Π₀ (i : ι), β i}, f = g ↔ ∀ (i : ι), f i = g i
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- **Alias** of `SimpleGraph.Colorable.of_isEmpty`. -/
SimpleGraph.colorableOfIsEmpty : ∀ {V : Type u} {G : SimpleGraph V} [IsEmpty V] (n : ℕ), G.Colorable n
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_filter_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → Bool}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ((List.filter (fun p => f p.fst p.snd) l).isEmpty = false ↔
      ∃ k, ∃ (h : Std.Internal.List.containsKey k l = true), f k (Std.Internal.List.getValueCast k l h) = true)
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.str : (self : UniformSpaceCat) → UniformSpace self.carrier
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.const_eq_const_of_smul_eq_smul : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f₁ f₂ : M) (g₁ g₂ : R)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hu₁ : U ≤ PrimeSpectrum.basicOpen g₁)
  (hu₂ : U ≤ PrimeSpectrum.basicOpen g₂),
  g₁ • f₂ = g₂ • f₁ →
    AlgebraicGeometry.StructureSheaf.const f₁ g₁ U hu₁ = AlgebraicGeometry.StructureSheaf.const f₂ g₂ U hu₂
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedInf_le : ∀ {α : Type u_1} [inst : SemilatticeInf α] {s : Finset α} {a : α} [inst_1 : DecidableLE α] [inst_2 : BoundedOrder α],
  s.truncatedInf a ≤ a
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePullbackShapeOp_obj : ∀ (J : Type w) (X : CategoryTheory.Limits.WidePullbackShape J),
  (CategoryTheory.Limits.widePullbackShapeOp J).obj X = Opposite.op X
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.braiding_naturality_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y : CategoryTheory.Dial C} (f : X ⟶ Y) (Z : CategoryTheory.Dial C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id Z)) (Y.braiding Z).hom =
    CategoryTheory.CategoryStruct.comp (X.braiding Z).hom
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id Z) f)
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
/-- A (semi) normed real vector space is homeomorphic to the unit ball in the same space.
This homeomorphism sends `x : E` to `(1 + ‖x‖²)^(- ½) • x`.

In many cases the actual implementation is not important, so we don't mark the projection lemmas
`Homeomorph.unitBall_apply_coe` and `Homeomorph.unitBall_symm_apply` as `@[simp]`.

See also `Homeomorph.contDiff_unitBall` and `OpenPartialHomeomorph.contDiffOn_unitBall_symm`
for smoothness properties that hold when `E` is an inner-product space.  -/
Homeomorph.unitBall : {E : Type u_1} → [inst : SeminormedAddCommGroup E] → [NormedSpace ℝ E] → E ≃ₜ ↑(Metric.ball 0 1)
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.inv S.iCycles = S.moduleCatLeftHomologyData.i
-- Lean.Message
Lean.MessageData.ofLazy.inj : ∀ {f : Option Lean.PPContext → BaseIO Dynamic} {hasSyntheticSorry : Lean.MetavarContext → Bool}
  {f_1 : Option Lean.PPContext → BaseIO Dynamic} {hasSyntheticSorry_1 : Lean.MetavarContext → Bool},
  Lean.MessageData.ofLazy f hasSyntheticSorry = Lean.MessageData.ofLazy f_1 hasSyntheticSorry_1 →
    f = f_1 ∧ hasSyntheticSorry = hasSyntheticSorry_1
-- Lean.Meta.Transform
/-- Zeta-reduces only the specified free variables, applying beta reduction after substitution.
For example, if `x` has value `fun y => y + 1` and appears as `x 2`, the result is `2 + 1`.
 -/
Lean.Meta.zetaDeltaFVars : Lean.Expr → Array Lean.FVarId → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.CubicDiscriminant
Cubic.equiv_symm_apply_b : ∀ {R : Type u_1} [inst : Semiring R] (f : { p // p.degree ≤ 3 }), (Cubic.equiv.symm f).b = (↑f).coeff 2
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.mapBifunctor.ι_D₂ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] (j j' : J) (i₁ : I₁) (i₂ : I₂)
  (h : c₁.π c₂ c (i₁, i₂) = j),
  CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h)
      (HomologicalComplex.mapBifunctor.D₂ K₁ K₂ F c j j') =
    HomologicalComplex.mapBifunctor.d₂ K₁ K₂ F c i₁ i₂ j'
-- Mathlib.Data.Option.NAry
/-- The image of a binary function `f : α → β → γ` as a function `Option α → Option β → Option γ`.
Mathematically this should be thought of as the image of the corresponding function `α × β → γ`.  -/
Option.map₂ : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → β → γ) → Option α → Option β → Option γ
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
MeasureTheory.Integrable.continuous_primitive : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {f : ℝ → E}
  [MeasureTheory.NullSingletonClass μ],
  MeasureTheory.Integrable f μ → ∀ (a : ℝ), Continuous fun b => ∫ (x : ℝ) in a..b, f x ∂μ
-- Mathlib.Algebra.Order.ZeroLEOne
Rat.instZeroLEOneClass : ZeroLEOneClass ℚ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.compare_maxKey_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β} {he : (t.modify k f).isEmpty = false}, cmp ((t.modify k f).maxKey he) (t.maxKey ⋯) = Ordering.eq
-- Mathlib.Data.Multiset.Pi
Multiset.card_pi : ∀ {α : Type u_1} [inst : DecidableEq α] {β : α → Type u_2} (m : Multiset α) (t : (a : α) → Multiset (β a)),
  (m.pi t).card = (Multiset.map (fun a => (t a).card) m).prod
-- Std.Data.Iterators.Producers.Repeat
/-- Internal implementation detail of the iterator library.  -/
Std.Iterators.Types.RepeatIterator.next : {α : Type u} → {f : α → α} → Std.Iterators.Types.RepeatIterator α f → α
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.interior_preimage : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ']
  [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E],
  Function.Surjective ⇑f → ∀ (s : Set F), interior (⇑f ⁻¹' s) = ⇑f ⁻¹' interior s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.equiv_iff_keys_perm : ∀ {α : Type u} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => Unit}, t₁.Equiv t₂ ↔ t₁.keys.Perm t₂.keys
-- Mathlib.CategoryTheory.Abelian.Images
/-- `f` factors through its image via the canonical morphism `p`.  -/
CategoryTheory.Abelian.image.fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {P Q : C}
  (f : P ⟶ Q) [inst_2 : CategoryTheory.Limits.HasCokernel f]
  [inst_3 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.factorThruImage f) (CategoryTheory.Abelian.image.ι f) = f
-- Mathlib.NumberTheory.LSeries.Injectivity
/-- The map `f ↦ LSeries f` is injective on functions `f` such that `f 0 = 0` and the L-series
of `f` converges somewhere.  -/
LSeries_injOn : Set.InjOn LSeries {f | f 0 = 0 ∧ LSeries.abscissaOfAbsConv f < ⊤}
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.MapFactorizationData.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      {X Y : C} →
        {f : X ⟶ Y} →
          (Z : C) →
            (i : X ⟶ Z) →
              (p : Z ⟶ Y) →
                autoParam (CategoryTheory.CategoryStruct.comp i p = f)
                    CategoryTheory.MorphismProperty.MapFactorizationData.fac._autoParam →
                  W₁ i → W₂ p → W₁.MapFactorizationData W₂ f
-- Std.Data.ExtDHashMap.Basic
/-- Checks whether a key is present in a map, and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.ExtDHashMap.containsThenInsert : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [EquivBEq α] → [LawfulHashable α] → Std.ExtDHashMap α β → (a : α) → β a → Bool × Std.ExtDHashMap α β
-- Mathlib.Logic.Equiv.Basic
Equiv.setValue_eq : ∀ {α : Sort u_1} {β : Sort u_4} [inst : DecidableEq α] (f : α ≃ β) (a : α) (b : β), (f.setValue a b) a = b
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RiiSliceData.mk : {α : Type u} → (Std.DTreeMap.Internal.Impl α fun x => Unit) → Std.Rii α → Std.DTreeMap.Internal.Unit.RiiSliceData α
-- Mathlib.RingTheory.Localization.BaseChange
IsLocalization.bijective_linearMap_mul' : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [IsLocalization S A], Function.Bijective ⇑(LinearMap.mul' R A)
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.nsmul_coe : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddLeftMono α] (n : ℕ) (r : { x // 0 ≤ x }),
  ↑(n • r) = n • ↑r
-- Mathlib.Analysis.Polynomial.CauchyBound
Polynomial.one_le_cauchyBound : ∀ {K : Type u_1} [inst : NormedDivisionRing K] (p : Polynomial K), 1 ≤ p.cauchyBound
-- Lean.Meta.Tactic.Assert
Lean.Meta.AssertAfterResult.mk.inj : ∀ {fvarId : Lean.FVarId} {mvarId : Lean.MVarId} {subst : Lean.Meta.FVarSubst} {fvarId_1 : Lean.FVarId}
  {mvarId_1 : Lean.MVarId} {subst_1 : Lean.Meta.FVarSubst},
  { fvarId := fvarId, mvarId := mvarId, subst := subst } =
      { fvarId := fvarId_1, mvarId := mvarId_1, subst := subst_1 } →
    fvarId = fvarId_1 ∧ mvarId = mvarId_1 ∧ subst = subst_1
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
Filter.Tendsto.uniformity_sub : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {f g : ι → α × α}
  {l : Filter ι},
  Filter.Tendsto f l (uniformity α) → Filter.Tendsto g l (uniformity α) → Filter.Tendsto (f - g) l (uniformity α)
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.mrange_subtype : ∀ {M : Type u_1} [inst : MulOneClass M] (s : Submonoid M), MonoidHom.mrange s.subtype = s
-- Lean.Elab.InfoTree.Basic
/-- Instantiate the holes on the given `tree` with the assignment table.
(analogous to instantiating the metavariables in an expression)  -/
Lean.Elab.InfoTree.substitute : Lean.Elab.InfoTree → Lean.PersistentHashMap Lean.MVarId Lean.Elab.InfoTree → Lean.Elab.InfoTree
-- Mathlib.Analysis.CStarAlgebra.Spectrum
/-- Non-unital star algebra homomorphisms between C⋆-algebras are continuous linear maps.
See note [lower instance priority]  -/
NonUnitalStarAlgHom.instContinuousLinearMapClassComplex : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : NonUnitalCStarAlgebra A] [inst_1 : NonUnitalCStarAlgebra B]
  [inst_2 : FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B], ContinuousLinearMapClass F ℂ A B
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Any permutation matrix is row stochastic.  -/
Matrix.permMatrix_mem_rowStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {σ : Equiv.Perm n},
  Equiv.Perm.permMatrix R σ ∈ Matrix.rowStochastic R n
-- Mathlib.Data.PEquiv
PEquiv.bot_trans : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : β ≃. γ), ⊥.trans f = ⊥
-- Mathlib.RingTheory.Ideal.Maximal
/-- An ideal is maximal if it is maximal in the collection of proper ideals.  -/
Ideal.IsMaximal : {α : Type u} → [inst : Semiring α] → Ideal α → Prop
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.neg : ∀ {α : Type u} {β : Type v} [inst : Neg β] {f g : α → β} {l : Filter α}, f =ᶠ[l] g → -f =ᶠ[l] -g
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.ringHom_ext_iff : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {C : Type u_3} [inst_5 : Semiring C] {f g : TensorProduct R A B →+* C},
  f = g ↔
    f.comp Algebra.TensorProduct.includeLeftRingHom = g.comp Algebra.TensorProduct.includeLeftRingHom ∧
      f.comp Algebra.TensorProduct.includeRight.toRingHom = g.comp Algebra.TensorProduct.includeRight.toRingHom
-- Mathlib.Order.Filter.Basic
Filter.Frequently.mono : ∀ {α : Type u} {p q : α → Prop} {f : Filter α}, (∃ᶠ (x : α) in f, p x) → (∀ (x : α), p x → q x) → ∃ᶠ (x : α) in f, q x
-- Mathlib.LinearAlgebra.Matrix.WithConv
instNonUnitalNonAssocCommSemiringWithConvMatrix : {m : Type u_1} →
  {n : Type u_2} →
    {α : Type u_3} → [NonUnitalNonAssocCommSemiring α] → NonUnitalNonAssocCommSemiring (WithConv (Matrix m n α))
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.IsInitial.to_eq_descCoconeMorphism : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsInitial c)
  (s : CategoryTheory.Limits.Cocone F), hc.to s = (c.isColimitEquivIsInitial.symm hc).descCoconeMorphism s
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.impureTypeScalarNumLit : Lean.Expr → ℕ → Lean.Compiler.LCNF.LitValue
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.inr_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β] (y : β), (OrderAddMonoidHom.inr α β) y = (0, y)
-- Mathlib.Analysis.Normed.Affine.Isometry
LinearIsometry.coe_toAffineIsometry : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : SeminormedAddCommGroup V₂] [inst_4 : NormedSpace 𝕜 V₂] (f : V →ₗᵢ[𝕜] V₂),
  ⇑f.toAffineIsometry = ⇑f
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.IsStrongPrelimit.zero : Cardinal.IsStrongPrelimit 0
-- Mathlib.RingTheory.Ideal.Operations
Ideal.zero_eq_bot : ∀ {R : Type u} [inst : Semiring R], 0 = ⊥
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.quasicoherentData_presentation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat}
  [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat] [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_4 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_5 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation)
  (x : C),
  P.quasicoherentData.presentation x =
    P.map (SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id (R.over x)))
      (CategoryTheory.Iso.refl (SheafOfModules.unit (R.over x)))
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.IsMultiplicative.pmul : ∀ {R : Type u_1} [inst : CommSemiring R] {f g : ArithmeticFunction R},
  f.IsMultiplicative → g.IsMultiplicative → (f.pmul g).IsMultiplicative
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
Topology.IsOpenEmbedding.functor_isContinuous : ∀ {X Y : TopCat} {f : X ⟶ Y} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)),
  h.functor.IsContinuous (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y)
-- Lean.Meta.Sym.Apply
Lean.Meta.Sym.ApplyResult.goals.sizeOf_spec : ∀ (mvarIds : List Lean.MVarId), sizeOf (Lean.Meta.Sym.ApplyResult.goals mvarIds) = 1 + sizeOf mvarIds
-- Mathlib.Algebra.Notation.Support
Function.support_eq_empty_iff : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] {f : ι → M}, Function.support f = ∅ ↔ f = 0
-- Mathlib.Data.Fintype.EquivFin
Infinite.of_injective : ∀ {α : Sort u_4} {β : Sort u_5} [Infinite β] (f : β → α), Function.Injective f → Infinite α
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.const_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f s → ∀ (c : ℝ), InnerProductSpace.HarmonicContOnCl (c • f) s
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso.congr_simp : ∀ {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] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (i i_1 : X.toComma ⟶ Y.toComma) (e_i : i = i_1)
  [inst_7 : CategoryTheory.IsIso i],
  CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso i =
    CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso i_1
-- Mathlib.Lean.Expr.Basic
/-- Returns true if `e` contains a name `n` where `p n` is true.  -/
Lean.Expr.containsConst : Lean.Expr → (Lean.Name → Bool) → Bool
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_iff_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {a : α},
  m.contains a = true ↔ a ∈ m
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.NullMeasurableSet.image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β)
  (μ : MeasureTheory.Measure β),
  Function.Injective f →
    (∀ (s : Set α), MeasurableSet s → MeasureTheory.NullMeasurableSet (f '' s) μ) →
      MeasureTheory.NullMeasurableSet s (MeasureTheory.Measure.comap f μ) → MeasureTheory.NullMeasurableSet (f '' s) μ
-- Mathlib.Algebra.Order.Group.Synonym
toDual_add : ∀ {α : Type u_1} [inst : Add α] (a b : α), OrderDual.toDual (a + b) = OrderDual.toDual a + OrderDual.toDual b
-- Mathlib.Data.Int.Log
Int.log_one_left : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] (r : R), Int.log 1 r = 0
-- Mathlib.Analysis.Normed.Ring.Basic
NormMulClass.mk : ∀ {α : Type u_5} [inst : Norm α] [inst_1 : Mul α], (∀ (a b : α), ‖a * b‖ = ‖a‖ * ‖b‖) → NormMulClass α
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.instContinuousSMul : ∀ {S : Type u_2} {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace S] [inst_3 : SMul S R] [inst_4 : SMul S M] [ContinuousSMul S R] [ContinuousSMul S M],
  ContinuousSMul S (TrivSqZeroExt R M)
-- Mathlib.Algebra.Order.Star.Basic
IsUnit.star_right_conjugate_nonneg_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R] {u x : R},
  IsUnit u → (0 ≤ u * x * star u ↔ 0 ≤ x)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_union_of_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₁ → k ∈ t₁ ∪ t₂