mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Core
Fin.mk.inj : ∀ {n val : ℕ} {isLt : val < n} {val_1 : ℕ} {isLt_1 : val_1 < n}, ⟨val, isLt⟩ = ⟨val_1, isLt_1⟩ → val = val_1
-- Mathlib.Data.Finmap
Multiset.nodup_keys : ∀ {α : Type u} {β : α → Type v} {m : Multiset ((a : α) × β a)}, m.keys.Nodup ↔ m.NodupKeys
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.mk_coe_of_nndist_eq : ∀ {α : Type u_5} {β : Type u_6} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (f : α →ᵈ β)
  (h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y), Dilation.mkOfNNDistEq (⇑f) h = f
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsAddCyclic.exists_ofOrder_eq_natCard : ∀ {α : Type u_1} [inst : AddGroup α] [h : IsAddCyclic α], ∃ g, addOrderOf g = Nat.card α
-- Mathlib.Data.Finset.Density
Finset.dens_cons : ∀ {α : Type u_2} [inst : Fintype α] {s : Finset α} {a : α} (h : a ∉ s),
  (Finset.cons a s h).dens = s.dens + (↑(Fintype.card α))⁻¹
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.domMulActCongrRight_apply : ∀ {S : Type u_4} {R₁ : Type u_9} {R₁' : Type u_11} {R₂' : Type u_12} {M₁ : Type u_13} {M₁' : Type u_15}
  {M₂' : Type u_16} [inst : Semiring R₁] [inst_1 : Semiring R₁'] [inst_2 : Semiring R₂'] [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₁'] [inst_5 : AddCommMonoid M₂'] [inst_6 : Module R₁ M₁] [inst_7 : Module R₁' M₁']
  [inst_8 : Module R₂' M₂'] {σ₁'₂' : R₁' →+* R₂'} {σ₂'₁' : R₂' →+* R₁'} {σ₁₁' : R₁ →+* R₁'} {σ₁₂' : R₁ →+* R₂'}
  [inst_9 : RingHomInvPair σ₁'₂' σ₂'₁'] [inst_10 : RingHomInvPair σ₂'₁' σ₁'₂']
  [inst_11 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'] [inst_12 : Semiring S] [inst_13 : Module S M₁]
  [inst_14 : SMulCommClass R₁ S M₁] [inst_15 : RingHomCompTriple σ₁₂' σ₂'₁' σ₁₁'] (e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂')
  (a : M₁ →ₛₗ[σ₁₁'] M₁'), e₂.domMulActCongrRight a = ((LinearEquiv.refl R₁ M₁).arrowCongrAddEquiv e₂).toFun a
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_eq_some_of_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : LawfulBEq α] {k : α},
  m.contains k = true → m.getKey? k = some k
-- Mathlib.Data.FunLike.IsApply
IsMulApply.mk : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} [inst : FunLike F α β] [inst_1 : Mul β]
  [inst_2 : Mul F], (∀ (f g : F) (x : α), (f * g) x = f x * g x) → IsMulApply F α β
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Left multiplication of a row stochastic matrix by a non-negative vector
gives a non-negative vector  -/
Matrix.nonneg_vecMul_of_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] {M : Matrix n n R} {x : n → R},
  M ∈ Matrix.rowStochastic R n → (∀ (i : n), 0 ≤ x i) → ∀ (j : n), 0 ≤ Matrix.vecMul x M j
-- Mathlib.Algebra.Homology.SpectralObject.FirstPage
CategoryTheory.Abelian.SpectralObject.spectralSequence_first_page_d_eq_assoc : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : data.HasFirstPageComputation] [inst_4 : X.HasSpectralSequence data] (pq pq' : κ) (hpq : (c r₀).Rel pq pq')
  (i j k : ι) (hi : i = data.i₁ pq') (hj : j = data.i₁ pq) (hk : k = data.i₂ pq) (n n' : ℤ) (hn : n = data.deg pq)
  (hn' : autoParam (n + 1 = n') CategoryTheory.Abelian.SpectralObject.spectralSequence_first_page_d_eq._auto_1) {Z : C}
  (h : ((X.spectralSequence data).page r₀ ⋯).X pq' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((X.spectralSequence data).page r₀ ⋯).d pq pq') h =
    CategoryTheory.CategoryStruct.comp (X.spectralSequenceFirstPageXIso data pq j k hj hk n hn).hom
      (CategoryTheory.CategoryStruct.comp (X.δ (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n n' hn')
        (CategoryTheory.CategoryStruct.comp (X.spectralSequenceFirstPageXIso data pq' i j hi ⋯ n' ⋯).inv h))
-- Lean.Data.Options
Lean.instInhabitedOptionDecl : Inhabited Lean.OptionDecl
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.prod_toSubmodule : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] (S : NonUnitalSubalgebra R A) [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B]
  (S₁ : NonUnitalSubalgebra R B), (S.prod S₁).toSubmodule = S.toSubmodule.prod S₁.toSubmodule
-- Mathlib.CategoryTheory.Join.Basic
/-- Precomposing `mkFunctor F G α` with the right inclusion gives back `G`.  -/
CategoryTheory.Join.mkFunctorRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor C E) →
              (G : CategoryTheory.Functor D E) →
                (α : (CategoryTheory.Prod.fst C D).comp F ⟶ (CategoryTheory.Prod.snd C D).comp G) →
                  (CategoryTheory.Join.inclRight C D).comp (CategoryTheory.Join.mkFunctor F G α) ≅ G
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The equivalence between `IntertwiningMap`s and morphism between `X Y : Rep k G` is linear.  -/
Rep.homLinearEquiv : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] → [inst_1 : Monoid G] → (X Y : Rep.{u_1, u, v} k G) → (X ⟶ Y) ≃ₗ[k] X.ρ.IntertwiningMap Y.ρ
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.exp_int_mul_two_pi : ∀ (n : ℤ), Circle.exp (↑n * (2 * Real.pi)) = 1
-- Mathlib.Order.Directed
/-- `IsDirected α r` states that for any elements `a`, `b` there exists an element `c` such that
`r a c` and `r b c`.  -/
IsDirected : (α : Sort u_5) → (α → α → Prop) → Prop
-- Mathlib.Topology.NhdsWithin
Filter.EventuallyEq.eq_of_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s : Set α} {f g : α → β} {a : α},
  f =ᶠ[nhdsWithin a s] g → a ∈ s → f a = g a
-- Mathlib.Data.Matrix.Basic
/-- `piEquiv` as an `AlgEquiv`.  -/
Matrix.piAlgEquiv : {n : Type u_3} →
  {ι : Type u_14} →
    {β : ι → Type u_15} →
      (R : Type u_16) →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → Semiring (β i)] →
            [inst_2 : (i : ι) → Algebra R (β i)] →
              [inst_3 : Fintype n] →
                [inst_4 : DecidableEq n] → Matrix n n ((i : ι) → β i) ≃ₐ[R] (i : ι) → Matrix n n (β i)
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
/-- **Alias** of `Ideal.minimalPrimes_comap_of_surjective`. -/
Ideal.minimal_primes_comap_of_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  Function.Surjective ⇑f → ∀ {I J : Ideal S}, J ∈ I.minimalPrimes → Ideal.comap f J ∈ (Ideal.comap f I).minimalPrimes
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.EdgeDisjointTriangles.card_edgeFinset_le : ∀ {α : Type u_1} {G : SimpleGraph α} [inst : DecidableEq α] [inst_1 : Fintype α] [inst_2 : DecidableRel G.Adj],
  G.EdgeDisjointTriangles → 3 * (G.cliqueFinset 3).card ≤ G.edgeFinset.card
-- Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
factorization_eq_count : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : NormalizationMonoid α]
  [inst_3 : DecidableEq α] {n p : α},
  (factorization n) p = Multiset.count p (UniqueFactorizationMonoid.normalizedFactors n)
-- Lean.Parser.Term
Lean.Parser.Term.attrInstance.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Module.Torsion.PrimaryComponent
Ideal.primaryComponent.map_surjective : ∀ {A : Type u_1} [inst : CommRing A] [IsDedekindDomain A] {M₁ : Type u_5} {M₂ : Type u_6} [inst_2 : AddCommGroup M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₁] [inst_5 : Module A M₂],
  Module.IsTorsion A M₁ →
    ∀ (P : IsDedekindDomain.HeightOneSpectrum A) (φ : M₁ →ₗ[A] M₂),
      Function.Surjective ⇑φ → Function.Surjective ⇑(Ideal.primaryComponent.map P.asIdeal φ)
-- Mathlib.Analysis.Convolution
MeasureTheory.convolution.eq_1 : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] [inst_3 : NontriviallyNormedField 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F] [inst_7 : MeasurableSpace G]
  [inst_8 : NormedSpace ℝ F] [inst_9 : Sub G] (f : G → E) (g : G → E') (L : E →L[𝕜] E' →L[𝕜] F)
  (μ : MeasureTheory.Measure G) (x : G), MeasureTheory.convolution f g L μ x = ∫ (t : G), (L (f t)) (g (x - t)) ∂μ
-- Mathlib.Data.Fin.Embedding
Fin.valEmbedding_apply : ∀ {n : ℕ}, ⇑Fin.valEmbedding = Fin.val
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (y, y + x)` sends the measure `μ × ν` to `ν × μ`.  -/
MeasureTheory.measurePreserving_prod_add_swap : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.2, z.2 + z.1)) (μ.prod ν) (ν.prod μ)
-- Mathlib.Algebra.Group.Int.Units
Int.isUnit_eq_or_eq_neg : ∀ {u v : ℤ}, IsUnit u → IsUnit v → u = v ∨ u = -v
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
      (AlgebraicGeometry.IsOpenImmersion.ΓIso f U).hom =
    Y.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mem_normalizer_iff'' : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {g : G},
  g ∈ Subgroup.normalizer ↑H ↔ ∀ (h : G), h ∈ H ↔ g⁻¹ * h * g ∈ H
-- Batteries.Data.List.Lemmas
List.getElem_filter_eq_getElem_getElem_findIdxs_sub : ∀ {i : ℕ} {α : Type u_1} {xs : List α} {p : α → Bool} (s : ℕ) (h : i < (List.filter p xs).length),
  (List.filter p xs)[i] = xs[(List.findIdxs p xs s)[i] - s]
-- Init.BinderPredicates
/-- Declare `∀ x ⊆ y, ...` as syntax for `∀ x, x ⊆ y → ...` and `∃ x ⊆ y, ...` as syntax for
`∃ x, x ⊆ y ∧ ...`  -/
Lean.«binderPred⊆_» : Lean.ParserDescr
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_inter_eq_size_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → (∀ a ∈ m₂, a ∈ m₁) → (m₁ ∩ m₂).size = m₂.size
-- Lean.Elab.Tactic.Omega.Frontend
/-- The `omega` tactic, for resolving integer and natural linear arithmetic problems.  -/
Lean.Elab.Tactic.Omega.omegaTactic : Lean.Meta.Omega.OmegaConfig → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualCoannihilator_dualAnnihilator_eq : ∀ {K : Type u_4} {V : Type u_5} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {W : Subspace K (Module.Dual K V)} [FiniteDimensional K ↥W], (Submodule.dualCoannihilator W).dualAnnihilator = W
-- Init.Data.List.Lemmas
List.replace_replicate_self : ∀ {α : Type u_1} [inst : BEq α] {n : ℕ} {b : α} [LawfulBEq α] {a : α},
  0 < n → (List.replicate n a).replace a b = b :: List.replicate (n - 1) a
-- Init.Data.Nat.Lemmas
Nat.allLTTR_eq_true : ∀ {n : ℕ} {f : (i : ℕ) → i < n → Bool}, n.allLTTR f = true ↔ ∀ (i : ℕ) (h : i < n), f i h = true
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_eq_comap_nhds_one_left : ∀ (G : Type u_1) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  uniformity G = Filter.comap (fun p => p.1⁻¹ * p.2) (nhds 1)
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mul.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.mul = H.mul
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.mem_inf : ∀ {M : Type u_1} [inst : Mul M] {p p' : Subsemigroup M} {x : M}, x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.c₄_of_char_three : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 3], W.c₄ = W.b₂ ^ 2
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- This lemma is weaker than `MeasureTheory.MemLp.integral_indicator_norm_ge_nonneg_le`
as the latter provides `0 ≤ M` and does not require the measurability of `f`.  -/
MeasureTheory.MemLp.integral_indicator_norm_ge_le : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β},
  MeasureTheory.MemLp f 1 μ →
    MeasureTheory.StronglyMeasurable f →
      ∀ {ε : ℝ}, 0 < ε → ∃ M, ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_inv_associator : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X Y Z : Rep.{u, u, v} k G},
  Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv =
    ↑(Representation.TensorProduct.assoc X.ρ Y.ρ Z.ρ).symm
-- Mathlib.Data.Matrix.DMatrix
DMatrix.instInhabited : {m : Type u_1} →
  {n : Type u_2} → {α : m → n → Type v} → [(i : m) → (j : n) → Inhabited (α i j)] → Inhabited (DMatrix m n α)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.sumElim : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : MeasurableSpace γ}
  {f : α → γ} {g : β → γ}, Measurable f → Measurable g → Measurable (Sum.elim f g)
-- Mathlib.Algebra.Order.Ring.GeomSum
geom_sum_alternating_of_le_neg_one : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {x : R},
  x + 1 ≤ 0 → ∀ (n : ℕ), if Even n then ∑ i ∈ Finset.range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ Finset.range n, x ^ i
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_succ_eval : ∀ {S : Type u_1} [inst : Ring S] (n : ℕ) (k : S),
  Polynomial.eval k (descPochhammer S (n + 1)) = Polynomial.eval k (descPochhammer S n) * (k - ↑n)
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsPrenex.relabel : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n m : ℕ} {φ : L.BoundedFormula α m},
  φ.IsPrenex → ∀ (f : α → β ⊕ Fin n), (FirstOrder.Language.BoundedFormula.relabel f φ).IsPrenex
-- Init.Data.List.Lemmas
List.mem_map_of_mem : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {a : α} {f : α → β}, a ∈ l → f a ∈ List.map f l
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_insertIfNew : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {k a : α} {fallback v : β},
      Std.DHashMap.Internal.Raw₀.Const.getD (m.insertIfNew k v) a fallback =
        if (k == a) = true ∧ m.contains k = false then v else Std.DHashMap.Internal.Raw₀.Const.getD m a fallback
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.smul_closedEBall : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [IsIsometricSMul G X] (c : G) (x : X) (r : ENNReal), c • Metric.closedEBall x r = Metric.closedEBall (c • x) r
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsNat.to_isNNRat : ∀ {α : Type u_1} [inst : Semiring α] {a : α} {n : ℕ},
  Mathlib.Meta.NormNum.IsNat a n → Mathlib.Meta.NormNum.IsNNRat a n 1
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_is_coproduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] {ι : Type u_1}
  [Finite ι] {F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C} {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsColimit c) (i : CategoryTheory.Discrete ι) {X : C}
  (g : X ⟶ ((CategoryTheory.Functor.const (CategoryTheory.Discrete ι)).obj c.pt).obj i),
  CategoryTheory.Limits.HasPullback g (c.ι.app i)
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.image_exp_Iio : ∀ (a : ℝ), Real.exp '' Set.Iio a = Set.Ioo 0 (Real.exp a)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
CategoryTheory.Square.IsPushout.of_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {sq : CategoryTheory.Square C} (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span sq.f₁₂ sq.f₁₃) F],
  (sq.map F).IsPushout → sq.IsPushout
-- Mathlib.Data.Set.Sups
Set.forall_sups_iff : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s t : Set α} {p : α → Prop},
  (∀ c ∈ s ⊻ t, p c) ↔ ∀ a ∈ s, ∀ b ∈ t, p (a ⊔ b)
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.changeLevel_eq_cast_of_dvd : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {m : ℕ} (hm : n ∣ m)
  (a : (ZMod m)ˣ), ((DirichletCharacter.changeLevel hm) χ) ↑a = χ (↑a).cast
-- Mathlib.Order.PrimeIdeal
Order.Ideal.PrimePair.mk.inj : ∀ {P : Type u_2} {inst : Preorder P} {I : Order.Ideal P} {F : Order.PFilter P} {isCompl_I_F : IsCompl ↑I ↑F}
  {I_1 : Order.Ideal P} {F_1 : Order.PFilter P} {isCompl_I_F_1 : IsCompl ↑I_1 ↑F_1},
  { I := I, F := F, isCompl_I_F := isCompl_I_F } = { I := I_1, F := F_1, isCompl_I_F := isCompl_I_F_1 } →
    I = I_1 ∧ F = F_1
-- Init.Meta.Defs
/-- Split a name literal (without the backtick) into its dot-separated components. For example,
`foo.bla.«bo.o»` ↦ `["foo", "bla", "«bo.o»"]`. If the literal cannot be parsed, return `[]`.  -/
Lean.Syntax.splitNameLit : Substring.Raw → List Substring.Raw
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
AlgebraNorm.instFunLikeReal : {R : Type u_1} →
  [inst : SeminormedCommRing R] →
    {S : Type u_2} → [inst_1 : Ring S] → [inst_2 : Algebra R S] → FunLike (AlgebraNorm R S) S ℝ
-- Init.Data.Rat.Lemmas
Rat.neg_lt_neg_iff : ∀ {a b : ℚ}, -a < -b ↔ b < a
-- Lean.Meta.Tactic.Simp.Types
/-- Construct the `Expr` `h.mp e`, from a `Simp.Result` with proof `h`.  -/
Lean.Meta.Simp.Result.mkEqMP : Lean.Meta.Simp.Result → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Topology.UniformSpace.Real
/-- Embedding of `ℝ≥0` to `ℝ` as a bundled continuous map.  -/
ContinuousMap.coeNNRealReal : C(NNReal, ℝ)
-- Mathlib.Data.Set.FiniteExhaustion
Set.FiniteExhaustion.mk.inj : ∀ {α : Type u_1} {s : Set α} {toFun : ℕ → Set α} {finite' : ∀ (n : ℕ), Finite ↑(toFun n)}
  {subset_succ' : ∀ (n : ℕ), toFun n ⊆ toFun (n + 1)} {iUnion_eq' : ⋃ n, toFun n = s} {toFun_1 : ℕ → Set α}
  {finite'_1 : ∀ (n : ℕ), Finite ↑(toFun_1 n)} {subset_succ'_1 : ∀ (n : ℕ), toFun_1 n ⊆ toFun_1 (n + 1)}
  {iUnion_eq'_1 : ⋃ n, toFun_1 n = s},
  { toFun := toFun, finite' := finite', subset_succ' := subset_succ', iUnion_eq' := iUnion_eq' } =
      { toFun := toFun_1, finite' := finite'_1, subset_succ' := subset_succ'_1, iUnion_eq' := iUnion_eq'_1 } →
    toFun = toFun_1
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.IsSymm.neg : ∀ {α : Type u_1} {n : Type u_3} [inst : Neg α] {A : Matrix n n α}, A.IsSymm → (-A).IsSymm
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.LeftHomotopyClass.mk_eq_mk_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : HomotopicalAlgebra.ModelCategory C]
  [HomotopicalAlgebra.IsCofibrant X] (f g : X ⟶ Y),
  HomotopicalAlgebra.LeftHomotopyClass.mk f = HomotopicalAlgebra.LeftHomotopyClass.mk g ↔
    HomotopicalAlgebra.LeftHomotopyRel f g
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.mk'.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {x : AddCommGroup α} {x_1 : Preorder α} {x_2 : AddCommGroup β} {x_3 : PartialOrder β}
  (f : α → β) (hf : Monotone f) (map_mul : ∀ (a b : α), f (a + b) = f a + f b),
  OrderAddMonoidHom.mk' f hf map_mul = { toAddMonoidHom := AddMonoidHom.mk' f map_mul, monotone' := hf }
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.matroid_closure_eq : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] [inst_4 : IsDomain A] {s : Set A},
  (AlgebraicIndependent.matroid R A).closure s = ↑(Subalgebra.algebraicClosure (↥(Algebra.adjoin R s)) A)
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_prod : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {ι : Type u_2} {f : ι → M} (s : Finset ι),
  (↑s).Pairwise (Function.onFun IsRelPrime f) →
    UniqueFactorizationMonoid.radical (∏ i ∈ s, f i) = ∏ i ∈ s, UniqueFactorizationMonoid.radical (f i)
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.Scheme.Hom.presieve₀_cover : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (hf : P f)
  [inst : AlgebraicGeometry.Surjective f],
  (AlgebraicGeometry.Scheme.Hom.cover f hf).presieve₀ = CategoryTheory.Presieve.singleton f
-- Mathlib.RingTheory.Valuation.Basic
Valuation.val_mrange_zero : ∀ {R : Type u_3} {Γ₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀),
  ↑0 = 0
-- Mathlib.NumberTheory.Real.Irrational
Irrational.mul_intCast : ∀ {x : ℝ}, Irrational x → ∀ {m : ℤ}, m ≠ 0 → Irrational (x * ↑m)
-- Mathlib.AlgebraicTopology.Quasicategory.Basic
/-- A simplicial set `S` is a *quasicategory* if it satisfies the following horn-filling condition:
for every `n : ℕ` and `0 < i < n`,
every map of simplicial sets `σ₀ : Λ[n, i] → S` can be extended to a map `σ : Δ[n] → S`.
 -/
SSet.Quasicategory : SSet → Prop
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.Path.cast_cons : ∀ {U : Type u_1} [inst : Quiver U] {u v w u' w' : U} (p : Quiver.Path u v) (e : v ⟶ w) (hu : u = u') (hw : w = w'),
  Quiver.Path.cast hu hw (p.cons e) = (Quiver.Path.cast hu ⋯ p).cons (Quiver.Hom.cast ⋯ hw e)
-- Mathlib.Algebra.Prime.Defs
not_irreducible_zero : ∀ {M : Type u_1} [inst : MonoidWithZero M], ¬Irreducible 0
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.inhabitedValueGroup : {K : Type u} → [inst : Field K] → (A : ValuationSubring K) → Inhabited A.ValueGroup
-- Mathlib.Algebra.Prime.Defs
Irreducible.not_dvd_unit : ∀ {M : Type u_1} [inst : CommMonoid M] {p : M} (u : Mˣ), Irreducible p → ¬p ∣ ↑u
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasSum.add_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a b : α}
  [ContinuousAdd α] {s : Set β}, HasSum (f ∘ Subtype.val) a → HasSum (f ∘ Subtype.val) b → HasSum f (a + b)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instIsScalarTower : ∀ {T : Type u_1} {S : Type u_2} {R : Type u_3} {A : Type u_4} [inst : SMul T R] [inst_1 : SMul T A] [inst_2 : SMul S R]
  [inst_3 : SMul S A] [inst_4 : SMul T S] [IsScalarTower T S R] [IsScalarTower T S A],
  IsScalarTower T S (Unitization R A)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
/-- If `f : X ⟶ Y` is iso, then `Y ⨿[X] Z ≅ Z`. This is the explicit colimit cocone.  -/
CategoryTheory.Limits.pushoutCoconeOfLeftIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} → (f : X ⟶ Y) → (g : X ⟶ Z) → [CategoryTheory.IsIso f] → CategoryTheory.Limits.PushoutCocone f g
-- Mathlib.Probability.Decision.BayesEstimator
/-- An estimator is a Bayes estimator for a prior `π` if it attains the Bayes risk for `π`.  -/
ProbabilityTheory.IsBayesEstimator : {Θ : Type u_1} →
  {𝓧 : Type u_2} →
    {𝓨 : Type u_3} →
      {mΘ : MeasurableSpace Θ} →
        {m𝓧 : MeasurableSpace 𝓧} →
          {m𝓨 : MeasurableSpace 𝓨} →
            (Θ → 𝓨 → ENNReal) →
              ProbabilityTheory.Kernel Θ 𝓧 → ProbabilityTheory.Kernel 𝓧 𝓨 → MeasureTheory.Measure Θ → Prop
-- Init.Data.Ord.Basic
instDecidableRelLe : {α : Type u_1} → [inst : Ord α] → DecidableRel LE.le
-- Lean.Compiler.IR.Basic
Lean.IR.VarId.mk : Lean.IR.Index → Lean.IR.VarId
-- Mathlib.Analysis.Real.Sqrt
/-- Variant of `sq_sqrt` without a non-negativity assumption on `x`.  -/
Real.sq_sqrt' : ∀ {x : ℝ}, √x ^ 2 = max x 0
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_pos : ∀ {r : ENNReal}, 0 < ⌊r⌋ₑ ↔ 1 ≤ r
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.image_vsub_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t : Set β}, (fun x => x.1 -ᵥ x.2) '' s ×ˢ t = s -ᵥ t
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.GradeZero.smul_eq_mul : ∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddZeroClass ι] [inst_1 : GradedMonoid.GMul A] (a b : A 0), a • b = a * b