mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.sc'MapIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S₁ S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex)
  (i j k : ℕ) (hij : autoParam (i + 1 = j) CategoryTheory.ComposableArrows.sc'MapIso._auto_1)
  (hjk : autoParam (j + 1 = k) CategoryTheory.ComposableArrows.sc'MapIso._auto_3)
  (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.sc'MapIso._auto_5),
  (CategoryTheory.ComposableArrows.sc'MapIso e h₁ h₂ i j k hij hjk hk).hom =
    CategoryTheory.ComposableArrows.sc'Map e.hom h₁ h₂ i j k hij hjk hk
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.instAddActionReal : AddAction ℝ UpperHalfPlane
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.ofDiameter.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ p₂ : P),
  EuclideanGeometry.Sphere.ofDiameter p₁ p₂ = { center := midpoint ℝ p₁ p₂, radius := dist p₁ p₂ / 2 }
-- Mathlib.NumberTheory.ModularForms.Basic
CuspFormClass.cuspForm : ∀ (Γ : Subgroup (GL (Fin 2) ℝ)) (k : ℤ), CuspFormClass (CuspForm Γ k) Γ k
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedGT_iff_getElem_gt_getElem_of_lt`. -/
List.SortedGT.getElem_gt_getElem_of_lt : ∀ {α : Type u_1} {l : List α} [inst : Preorder α],
  l.SortedGT → ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, j < i → l[i] < l[j]
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMapClass.map_smul : ∀ {R : outParam (Type u_14)} {M : outParam (Type u_15)} {M₂ : outParam (Type u_16)} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] {F : Type u_17}
  [inst_5 : FunLike F M M₂] [LinearMapClass F R M M₂] (f : F) (r : R) (x : M), f (r • x) = r • f x
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.combine.inj : ∀ {s t : Lean.Omega.Constraint} {c : Lean.Omega.Coeffs} {j : Lean.Elab.Tactic.Omega.Justification s c}
  {k : Lean.Elab.Tactic.Omega.Justification t c} {j_1 : Lean.Elab.Tactic.Omega.Justification s c}
  {k_1 : Lean.Elab.Tactic.Omega.Justification t c}, j.combine k = j_1.combine k_1 → j = j_1 ∧ k = k_1
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticSeverity.information : Lean.Lsp.DiagnosticSeverity
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_mul_inv : ∀ {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : Group G]
  [inst_2 : DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g h : ι → G), ⇑f ∘ (g * h⁻¹) = ⇑f ∘ g * (⇑f ∘ h)⁻¹
-- Init.Data.Nat.Dvd
Nat.mul_div_cancel' : ∀ {n m : ℕ}, n ∣ m → n * (m / n) = m
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.orthRadius_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : EuclideanGeometry.Sphere P), s.orthRadius s.center = ⊤
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentBundle.contMDiffVectorBundle : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [h : IsManifold I (n + 1) M],
  ContMDiffVectorBundle n E (TangentSpace I) I
-- Mathlib.Util.AtomM
/-- The monad that `ring` works in. This is only used for collecting atoms.  -/
Mathlib.Tactic.AtomM : Type → Type
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Mathlib.Meta.NormNum.IsNNRat.nnreal_rpow_isNNRat : ∀ (a : NNReal) (b : ℝ) (na da : ℕ),
  Mathlib.Meta.NormNum.IsNNRat a na da →
    ∀ (nr dr : ℕ),
      Mathlib.Meta.NormNum.IsNat (↑na ^ b) nr →
        Mathlib.Meta.NormNum.IsNat (↑da ^ b) dr → Mathlib.Meta.NormNum.IsNNRat (a ^ b) nr dr
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.coprod.snd.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.Limits.coprod.snd X Y = CategoryTheory.Limits.coprod.desc 0 (CategoryTheory.CategoryStruct.id Y)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry_cons_of_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
  {h₁ : Std.Internal.List.containsKey a (⟨k, v⟩ :: l) = true} (h₂ : (k == a) = false),
  Std.Internal.List.getEntry a (⟨k, v⟩ :: l) h₁ = Std.Internal.List.getEntry a l ⋯
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiffOn.prodMk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F' : Type u_11}
  [inst_11 : NormedAddCommGroup F'] [inst_12 : NormedSpace 𝕜 F'] {G' : Type u_12} [inst_13 : TopologicalSpace G']
  {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_14 : TopologicalSpace N'] [inst_15 : ChartedSpace G' N']
  {s : Set M} {n : WithTop ℕ∞} {f : M → M'} {g : M → N'},
  ContMDiffOn I I' n f s → ContMDiffOn I J' n g s → ContMDiffOn I (I'.prod J') n (fun x => (f x, g x)) s
-- Init.Data.SInt.Lemmas
Int16.ofInt_neg : ∀ (a : ℤ), Int16.ofInt (-a) = -Int16.ofInt a
-- Mathlib.Data.Multiset.ZeroCons
Multiset.card_pos : ∀ {α : Type u_1} {s : Multiset α}, 0 < s.card ↔ s ≠ 0
-- Mathlib.SetTheory.Cardinal.Aleph
/-- The Beth function is defined so that `beth 0 = ℵ₀`, `beth (succ o) = 2 ^ beth o`, and that for a
limit ordinal `o`, `beth o` is the supremum of `beth a` for `a < o`.

Assuming the generalized continuum hypothesis, which is undecidable in ZFC, we have `ℶ_ o = ℵ_ o`
for all ordinals.

For a version which starts at zero, see `Cardinal.preBeth`. 

Conventions for notations in identifiers:

 * The recommended spelling of `ℶ_` in identifiers is `beth`. -/
Cardinal.termℶ_ : Lean.ParserDescr
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsSemilinearSet.closure_finset : ∀ {M : Type u_1} [inst : AddCommMonoid M] (s : Finset M), IsSemilinearSet ↑(AddSubmonoid.closure ↑s)
-- Mathlib.Order.Hom.BoundedLattice
InfTopHomClass.toTopHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Min α] [inst_2 : Min β] [inst_3 : Top α]
  [inst_4 : Top β] [InfTopHomClass F α β], TopHomClass F α β
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- As an intermediate step to show that `μ.withDensity (v.limRatioMeas hρ) = ρ`, we show here
that `μ.withDensity (v.limRatioMeas hρ) ≤ t^2 ρ` for any `t > 1`.  -/
VitaliFamily.withDensity_le_mul : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [inst_1 : SecondCountableTopology α] [inst_2 : BorelSpace α]
  [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) {s : Set α},
  MeasurableSet s → ∀ {t : NNReal}, 1 < t → (μ.withDensity (v.limRatioMeas hρ)) s ≤ ↑t ^ 2 * ρ s
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.snd_prod : ∀ {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] (s : Multiset (M × N)),
  s.prod.2 = (Multiset.map Prod.snd s).prod
-- Mathlib.Data.List.MinMax
List.argmin_eq_some_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] {f : α → β} {l : List α} {m : α} [inst_1 : DecidableEq α],
  List.argmin f l = some m ↔ m ∈ l ∧ (∀ a ∈ l, f m ≤ f a) ∧ ∀ a ∈ l, f a ≤ f m → List.idxOf m l ≤ List.idxOf a l
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.startsWith_char_iff_exists_append : ∀ {c : Char} {s : String.Slice}, s.startsWith c = true ↔ ∃ t, s.copy = String.singleton c ++ t
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_add_mul_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (m n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R),
  (MvPowerSeries.coeff (m + n)) (φ * (MvPowerSeries.monomial n) a) = (MvPowerSeries.coeff m) φ * a
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.congr_apply_of : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] {G' : ι → Type u_5} [inst_5 : (i : ι) → AddCommMonoid (G' i)]
  [inst_6 : (i : ι) → Module R (G' i)] {f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j} (e : (i : ι) → G i ≃ₗ[R] G' i)
  (he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)) {i : ι} (g : G i),
  (Module.DirectLimit.congr e he) ((Module.DirectLimit.of R ι G f i) g) = (Module.DirectLimit.of R ι G' f' i) ((e i) g)
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
_private.Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives.0.HomotopyCategory.Plus.isRightDerivabilityStructure.instIsLocalizedEquivalencePlusInjectiveObjectInverseImageQuasiIsoMapCochainComplexPlusιIsomorphismsL : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  (HomotopyCategory.Plus.isRightDerivabilityStructure.L✝ C).IsLocalizedEquivalence
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.integral_stieltjesOfMeasurableRat : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ}
  [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (x : ℝ),
  ∫ (b : β), ↑(ProbabilityTheory.stieltjesOfMeasurableRat f ⋯ (a, b)) x ∂ν a = (κ a).real (Set.univ ×ˢ Set.Iic x)
-- Mathlib.Topology.Constructions
comap_sigmaMk_nhds : ∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] (i : ι) (x : σ i),
  Filter.comap (Sigma.mk i) (nhds ⟨i, x⟩) = nhds x
-- Lean.Declaration
Lean.mkOpaqueValEx : Lean.Name → List Lean.Name → Lean.Expr → Lean.Expr → Bool → List Lean.Name → Lean.OpaqueVal
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.NullMeasurable.comp_fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ},
  MeasureTheory.NullMeasurable f μ → MeasureTheory.NullMeasurable (fun z => f z.1) (μ.prod ν)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.left_counit_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Comonad C) (X : C) {Z : C}
  (h : self.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.δ.app X) (CategoryTheory.CategoryStruct.comp (self.ε.app (self.obj X)) h) = h
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_insert : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s : Finset β} {f : β → α}
  [inst_2 : DecidableEq β] {b : β}, (insert b s).sup f = f b ⊔ s.sup f
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The underlying `G`-equivariant linear map.  -/
Rep.Hom.hom' : {k : Type u} →
  {G : Type v} →
    [inst : Semiring k] → [inst_1 : Monoid G] → {A B : Rep.{w, u, v} k G} → A.Hom B → A.ρ.IntertwiningMap B.ρ
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → (X : AlgebraicGeometry.PresheafedSpace C) → TopologicalSpace ↑↑X
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toLinearMap_injective : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂], Function.Injective AlgEquiv.toLinearMap
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.comp_hom' : ∀ {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.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] {M N K : CategoryTheory.AddMod D A} (f : M ⟶ N) (g : N ⟶ K),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.siftedSum_le_sum_of_upperMoebius : ∀ {s : BoundingSieve} (muPlus : ℕ → ℝ),
  BoundingSieve.IsUpperMoebius muPlus →
    BoundingSieve.siftedSum ≤ ∑ d ∈ s.prodPrimes.divisors, muPlus d * BoundingSieve.multSum d
-- Mathlib.Order.Interval.Set.UnorderedInterval
AntitoneOn.mapsTo_uIcc : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Lattice β] {f : α → β} {a b : α},
  AntitoneOn f (Set.uIcc a b) → Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
-- Mathlib.Topology.Connected.PathConnected
PathConnectedSpace.mk : ∀ {X : Type u_4} [inst : TopologicalSpace X], Nonempty X → (∀ (x y : X), Joined x y) → PathConnectedSpace X
-- Mathlib.CategoryTheory.ObjectProperty.Local
CategoryTheory.MorphismProperty.isLocal_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C),
  W.isLocal Z ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → Function.Bijective fun g => CategoryTheory.CategoryStruct.comp f g
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lidOfCompatibleSMul_tmul : ∀ (R : Type u_3) (S : Type u_4) (A : Type u_6) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : Algebra S A] [inst_5 : Algebra R S] [inst_6 : TensorProduct.CompatibleSMul R S S A]
  [inst_7 : TensorProduct.CompatibleSMul S R S A] (s : S) (a : A),
  (Algebra.TensorProduct.lidOfCompatibleSMul R S A) (s ⊗ₜ[R] a) = s • a
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.linearDeriv_apply : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : DecidableEq ι] [inst_6 : Fintype ι] (f : MultilinearMap R M₁ M₂)
  (x y : (i : ι) → M₁ i), (f.linearDeriv x) y = ∑ i, f (Function.update x i (y i))
-- Mathlib.Algebra.Ring.Parity
Even.add_odd : ∀ {α : Type u_2} [inst : Semiring α] {a b : α}, Even a → Odd b → Odd (a + b)
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.mk_eq_mk : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {p q p' q' : Polynomial K},
  q ≠ 0 → q' ≠ 0 → (RatFunc.mk p q = RatFunc.mk p' q' ↔ p * q' = p' * q)
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- The based category associated to a functor `p : 𝒳 ⥤ 𝒮`.  -/
CategoryTheory.BasedCategory.ofFunctor : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {𝒳 : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] → CategoryTheory.Functor 𝒳 𝒮 → CategoryTheory.BasedCategory 𝒮
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.setLIntegral_condCDF : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (x : ℝ)
  {s : Set α},
  MeasurableSet s → ∫⁻ (a : α) in s, ENNReal.ofReal (↑(ProbabilityTheory.condCDF ρ a) x) ∂ρ.fst = ρ (s ×ˢ Set.Iic x)
-- Mathlib.Data.Finset.Disjoint
Finset.disjUnion_empty : ∀ {α : Type u_2} (s : Finset α) (h : optParam (Disjoint s ∅) ⋯), s.disjUnion ∅ h = s
-- Mathlib.Data.Num.Lemmas
Num.to_of_nat : ∀ (n : ℕ), ↑↑n = n
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.symm_apply_lt : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (e : α ≃+o β) {x : α} {y : β}, e.symm y < x ↔ y < e x
-- Mathlib.Order.OmegaCompletePartialOrder
/-- **Alias** of the reverse direction of `OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup`.

---

`ωScottContinuous f` asserts that `f` is both monotone and distributes over ωSup.  -/
OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] {f : α → β},
  (∃ (hf : Monotone f),
      ∀ (c : OmegaCompletePartialOrder.Chain α),
        f (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map { toFun := f, monotone' := hf })) →
    OmegaCompletePartialOrder.ωScottContinuous f
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_bind_getKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ((Std.Internal.List.minKey? l).bind fun k => Std.Internal.List.getKey? k l) = Std.Internal.List.minKey? l
-- Mathlib.Data.Finset.Image
/-- A `Finset` is in bijection with its image under an `Embedding`.  -/
Finset.equivMap : {α : Type u_1} → {β : Type u_2} → (f : α ↪ β) → (s : Finset α) → ↥s ≃ ↥(Finset.map f s)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instInhabitedDoElemCont.default : Lean.Elab.Do.DoElemCont
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.all : ∀ (f : Char → Bool) {s : Substring.Raw}, s.Valid → Substring.Raw.Legacy.all s f = s.toString.toList.all f
-- Aesop.Search.Expansion.Norm
Aesop.NormM.Context.options : Aesop.NormM.Context → Aesop.Options'
-- Mathlib.Order.InitialSeg
PrincipalSeg.subrelIso_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : PrincipalSeg r s) (a : α),
  f.subrelIso ⟨f.toRelEmbedding a, ⋯⟩ = a
-- Mathlib.Analysis.Calculus.FDeriv.Congr
DifferentiableAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {x : E},
  DifferentiableAt 𝕜 f x → f₁ =ᶠ[nhds x] f → DifferentiableAt 𝕜 f₁ x
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.restrict_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s : Set X}, HolderWith C r (s.domRestrict f) ↔ HolderOnWith C r f s
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- The equivalence between isomorphisms in `CompHaus` and homeomorphisms
of topological spaces.  -/
CompHausLike.isoEquivHomeo : {P : TopCat → Prop} → {X Y : CompHausLike P} → (X ≅ Y) ≃ (↑X.toTop ≃ₜ ↑Y.toTop)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.addCommGroup : {R : Type u} → {M : Type v} → [AddCommGroup R] → [AddCommGroup M] → AddCommGroup (TrivSqZeroExt R M)
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.instInhabitedChoice.default : Lean.Meta.Grind.EMatch.Choice
-- Mathlib.Data.Finsupp.SMulWithZero
Finsupp.smulCommClass : ∀ (α : Type u_1) (M : Type u_5) {R : Type u_11} {S : Type u_12} [inst : Zero M] [inst_1 : SMulZeroClass R M]
  [inst_2 : SMulZeroClass S M] [SMulCommClass R S M], SMulCommClass R S (α →₀ M)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.map_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : Matrix m n α} {f : α → β} {i : m} {j : n},
  M.map f i j = f (M i j)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (n : ℕ),
  groupHomology A n = HomologicalComplex.homology (groupHomology.inhomogeneousChains A) n
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
/-- A prelax functor between bicategories is a lax prefunctor such that `map₂` is a functor.
This structure will be extended to define `LaxFunctor` and `OplaxFunctor`.
 -/
CategoryTheory.PrelaxFunctor : (B : Type u₁) →
  [CategoryTheory.Bicategory B] →
    (C : Type u₂) → [CategoryTheory.Bicategory C] → Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.notMem_of_mem_sdiff`. -/
Set.notMem_of_mem_diff : ∀ {α : Type u_1} {s t : Set α} {x : α}, x ∈ s \ t → x ∉ t
-- Batteries.Tactic.Lint.Frontend
/-- The command `#lint` runs the linters on the current file (by default).

`#lint only someLinter` can be used to run only a single linter.  -/
Batteries.Tactic.Lint.«command#lint+-*Only___» : Lean.ParserDescr
-- Lean.DocString.Syntax
/-- A header

Headers must be correctly nested to form a tree structure. The first header in a document must
start with `#`, and subsequent headers must have at most one more `#` than the preceding header.
 -/
Lean.Doc.Syntax.header : Lean.ParserDescr
-- Mathlib.Order.Sublattice
Sublattice.comap_top : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β), Sublattice.comap f ⊤ = ⊤
-- Mathlib.Data.Set.Basic
Set.ofPred_or : ∀ {α : Type u} {p q : α → Prop}, {a | p a ∨ q a} = {a | p a} ∪ {a | q a}
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Post-composition by a uniform inducing function is
a uniform inducing function for the uniform structures of uniform convergence.

More precisely, if `f : γ → β` is uniform inducing,
then `(f ∘ ·) : (α →ᵤ γ) → (α →ᵤ β)` is uniform inducing.  -/
UniformFun.postcomp_isUniformInducing : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] [inst_1 : UniformSpace γ] {f : γ → β},
  IsUniformInducing f → IsUniformInducing (⇑UniformFun.ofFun ∘ (fun x => f ∘ x) ∘ ⇑UniformFun.toFun)
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPMVarsAnonymous : Lean.Options → Bool
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.norm_log_natCast_le_rpow_div : ∀ (n : ℕ) {ε : ℝ}, 0 < ε → ‖Complex.log ↑n‖ ≤ ↑n ^ ε / ε
-- Mathlib.FieldTheory.Extension
IntermediateField.nonempty_algHom_of_adjoin_splits : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {S : Set E},
  (∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) →
    IntermediateField.adjoin F S = ⊤ → Nonempty (E →ₐ[F] K)
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.Measure.prod_smul_right : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} {mβ : MeasurableSpace β}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {R : Type u_3} [inst : SMul R ENNReal]
  [inst_1 : IsScalarTower R ENNReal ENNReal] (c : R), μ.prod (c • ν) = c • μ.prod ν
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.instFinite : ∀ {α : Type u_1} {β : Type u_2}, Std.Iterators.Finite (Lean.PersistentHashMap.Zipper α β) Id
-- Mathlib.Order.Heyting.Basic
GeneralizedHeytingAlgebra.toLattice : {α : Type u_4} → [self : GeneralizedHeytingAlgebra α] → Lattice α
-- Mathlib.Analysis.LocallyConvex.Separation
/-- If `s` and `t` are convex, `interior s` is nonempty and disjoint from `t`, then a nonzero
continuous linear functional weakly separates `s` and `t`. The proof first separates `interior s`
from `t`, then extends the inequality from `interior s` to all of `s` using
`closure (interior s) = closure s`.  -/
geometric_hahn_banach_of_nonempty_interior : ∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {s t : Set E}
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E],
  Convex ℝ s →
    Convex ℝ t →
      Disjoint (interior s) t →
        (interior s).Nonempty → t.Nonempty → ∃ f u, f ≠ 0 ∧ (∀ a ∈ s, f a ≤ u) ∧ ∀ b ∈ t, u ≤ f b
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.toList_eq_toListModel_map : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  Std.DTreeMap.Internal.Impl.Const.toList t = List.map (fun e => (e.fst, e.snd)) t.toListModel