mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_mem_Ico : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoMod hp a b ∈ Set.Ico a (a + p)
-- Mathlib.GroupTheory.OreLocalization.OreSet
OreLocalization.oreDenom.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (r : R) (s : ↥S),
  OreLocalization.oreDenom r s = OreLocalization.OreSet.oreDenom r s
-- Std.Do.PostCond
Std.Do.ExceptConds.true.eq_1 : ∀ {ps : Std.Do.PostShape}, Std.Do.ExceptConds.true = Std.Do.ExceptConds.const True
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.instQuasiCompactCoverQculift : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S)
  [inst : AlgebraicGeometry.QuasiCompactCover 𝒰.toPreZeroHypercover],
  AlgebraicGeometry.QuasiCompactCover 𝒰.qculift.toPreZeroHypercover
-- Init.Core
and_comm : ∀ {a b : Prop}, a ∧ b ↔ b ∧ a
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.forIn'.loop.match_3.splitter : {α : Type u_1} →
  (as : Array α) →
    (motive : (i : ℕ) → i ≤ as.size → Sort u_2) →
      (i : ℕ) →
        (h : i ≤ as.size) →
          ((x : 0 ≤ as.size) → motive 0 x) → ((i : ℕ) → (h : i + 1 ≤ as.size) → motive i.succ h) → motive i h
-- Mathlib.GroupTheory.IndexNormal
/-- A subgroup of index 1 is normal (does not require finiteness of G)  -/
Subgroup.normal_of_index_eq_one : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index = 1 → H.Normal
-- Lean.CoreM
Lean.Core.modifyInstLevelValueCache : (Lean.Core.InstantiateLevelCache → Lean.Core.InstantiateLevelCache) → Lean.CoreM Unit
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_natCast' : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : NatCast α] (m : ℕ),
  Matrix.diagonal ↑m = ↑m
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.iUnion_def : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I), π.iUnion = ⋃ J ∈ π, ↑J
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm 0) } = 0
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] [inst_1 : SupSet β] (f : sSupHom α β) (f' : α → β) (h : f' = ⇑f),
  f.copy f' h = f
-- Mathlib.GroupTheory.Index
Subgroup.index_comap_of_surjective : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H : Subgroup G) {f : G' →* G},
  Function.Surjective ⇑f → (Subgroup.comap f H).index = H.index
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.mul_inv_cancel : ∀ {k : Type u_2} [inst : Field k] (φ : PowerSeries k), PowerSeries.constantCoeff φ ≠ 0 → φ * φ⁻¹ = 1
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Lattice α} {inst_1 : Lattice β} {inst_2 : BoundedOrder α}
  {inst_3 : BoundedOrder β} {toLatticeHom : LatticeHom α β} {map_top' : toLatticeHom.toFun ⊤ = ⊤}
  {map_bot' : toLatticeHom.toFun ⊥ = ⊥} {toLatticeHom_1 : LatticeHom α β} {map_top'_1 : toLatticeHom_1.toFun ⊤ = ⊤}
  {map_bot'_1 : toLatticeHom_1.toFun ⊥ = ⊥},
  { toLatticeHom := toLatticeHom, map_top' := map_top', map_bot' := map_bot' } =
      { toLatticeHom := toLatticeHom_1, map_top' := map_top'_1, map_bot' := map_bot'_1 } →
    toLatticeHom = toLatticeHom_1
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_diff_of_contains_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α], (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = true → (m₁.diff m₂).get? k = none
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.natCast_apply : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (n : ℕ) (m : α), ↑n m = n • m
-- Mathlib.Algebra.Star.Conjneg
conjneg_ne_conjneg : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R] {f g : G → R},
  conjneg f ≠ conjneg g ↔ f ≠ g
-- Mathlib.Order.Interval.Set.Basic
Set.instNoMinOrderElemIoi : ∀ (α : Type u_1) [inst : Preorder α] [DenselyOrdered α] {x : α}, NoMinOrder ↑(Set.Ioi x)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.isNormal' : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (self : OpenNormalAddSubgroup G),
  (↑self.toOpenAddSubgroup).Normal
-- Mathlib.RingTheory.Ideal.CotangentBaseChange
Ideal.tensorCotangentEquiv_tmul : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] (I : Ideal S) [inst_5 : Module.Flat R T] (t : T) (x : ↥I),
  (Ideal.tensorCotangentEquiv R T I) (t ⊗ₜ[R] I.toCotangent x) =
    t • (Ideal.map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent ⟨1 ⊗ₜ[R] ↑x, ⋯⟩
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- If `A` and `B` are isomorphic as `R`-algebras, then so are their polynomial rings  -/
Polynomial.mapAlgEquiv : {R : Type u} →
  {A : Type z} →
    {B : Type u_2} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A ≃ₐ[R] B) → Polynomial A ≃ₐ[R] Polynomial B
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- We say that `F` preserves (small) limits if it sends small
limit cones over any diagram to limit cones.  -/
CategoryTheory.Limits.PreservesColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.mk.sizeOf_spec : ∀ {R : Type u} [inst : NonAssocRing R] [inst_1 : SizeOf R] (toSubsemiring : Subsemiring R)
  (neg_mem' : ∀ {x : R}, x ∈ toSubsemiring.carrier → -x ∈ toSubsemiring.carrier),
  sizeOf { toSubsemiring := toSubsemiring, neg_mem' := neg_mem' } = 1 + sizeOf toSubsemiring
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- The characterization of weak convergence of finite measures by the usual (defining)
condition that the integrals of every continuous bounded function are continuous.  -/
MeasureTheory.FiniteMeasure.continuous_iff_forall_continuous_integral : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {X : Type u_2} [inst_3 : TopologicalSpace X] {μs : X → MeasureTheory.FiniteMeasure Ω},
  Continuous μs ↔ ∀ (f : BoundedContinuousFunction Ω ℝ), Continuous fun x => ∫ (ω : Ω), f ω ∂↑(μs x)
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.u_biInf_l : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisCoinsertion l u) {ι : Sort x} {p : ι → Prop} (f : (i : ι) → p i → β),
  u (⨅ i, ⨅ (hi : p i), l (f i hi)) = ⨅ i, ⨅ (hi : p i), f i hi
-- Mathlib.Algebra.DirectSum.Basic
/-- `setToSet β S T h` is the natural homomorphism `⨁ (i : S), β i → ⨁ (i : T), β i`,
where `h : S ⊆ T`.  -/
DirectSum.setToSet : {ι : Type v} →
  (β : ι → Type w) →
    [inst : (i : ι) → AddCommMonoid (β i)] →
      [DecidableEq ι] → (S T : Set ι) → S ⊆ T → (DirectSum ↑S fun i => β ↑i) →+ DirectSum ↑T fun i => β ↑i
-- Mathlib.Data.Finset.Basic
Equiv.piFinsetUnion.congr_simp : ∀ {ι : Type u_5} [inst : DecidableEq ι] (α : ι → Type u_4) {s t : Finset ι} (h : Disjoint s t),
  Equiv.piFinsetUnion α h = Equiv.piFinsetUnion α h
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeActionParams : Lean.FromJson Lean.Lsp.CodeActionParams
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min_le_min_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, (cmp (t.min ⋯) ((t.erase k).min he)).isLE = true
-- Mathlib.CategoryTheory.Monad.Equalizer
CategoryTheory.Comonad.beckFork_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra),
  (CategoryTheory.Comonad.beckFork X).pt = X.A
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
Subtype.preimage_ball : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {p : α → Prop} (a : { a // p a }) (r : ℝ),
  Subtype.val ⁻¹' Metric.ball (↑a) r = Metric.ball a r
-- Init.Prelude
/-- Decides whether one 8-bit unsigned integer is strictly less than another. Usually accessed via the
`DecidableLT UInt32` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if (6 : UInt32) < 7 then "yes" else "no") = "yes"`
 * `(if (5 : UInt32) < 5 then "yes" else "no") = "no"`
 * `show ¬((7 : UInt32) < 7) by decide`
 -/
UInt32.decLt : (a b : UInt32) → Decidable (a < b)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.muld_val : ∀ {d : ℤ} (x y : ℤ), Zsqrtd.sqrtd * { re := x, im := y } = { re := d * y, im := x }
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Eta-expanded form of `AEMeasurable.const_vadd` -/
AEMeasurable.fun_const_vadd : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : VAdd M X] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {g : α → X} [MeasurableConstVAdd M X],
  AEMeasurable g μ → ∀ (c : M), AEMeasurable (fun i => c +ᵥ g i) μ
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.r_sym : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] {a b : α × α},
  Lean.Grind.IntModule.OfNatModule.r α a b → Lean.Grind.IntModule.OfNatModule.r α b a
-- Mathlib.NumberTheory.ModularForms.SlashActions
ModularForm.prod_slash_sum_weights : ∀ {ι : Type u_1} {k : ι → ℤ} {g : GL (Fin 2) ℝ} {f : ι → UpperHalfPlane → ℂ} {s : Finset ι},
  SlashAction.map (∑ i ∈ s, k i) g (∏ i ∈ s, f i) =
    |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑s.card - 1) • ∏ i ∈ s, SlashAction.map (k i) g (f i)
-- Mathlib.Topology.Compactness.Compact
Filter.cocompact.eq_1 : ∀ (X : Type u_1) [inst : TopologicalSpace X], Filter.cocompact X = ⨅ s, ⨅ (_ : IsCompact s), Filter.principal sᶜ
-- Mathlib.Algebra.Category.Ring.Basic
RingEquiv.toCommSemiRingCatIso_inv : ∀ {R S : Type u} [inst : CommSemiring R] [inst_1 : CommSemiring S] (e : R ≃+* S),
  e.toCommSemiRingCatIso.inv = CommSemiRingCat.ofHom ↑e.symm
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- A monomorphism in `SimplexCategory` must increase lengths  -/
SimplexCategory.len_le_of_mono : ∀ {x y : SimplexCategory} (f : x ⟶ y) [CategoryTheory.Mono f], x.len ≤ y.len
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_mono : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} {p p' : Submodule R M},
  p ≤ p' → Submodule.map f p ≤ Submodule.map f p'
-- Mathlib.FieldTheory.SeparableClosure
/-- A separable extension has finite inseparable degree one.  -/
Algebra.IsSeparable.finInsepDegree_eq : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsSeparable F E],
  Field.finInsepDegree F E = 1
-- Mathlib.Data.List.Rotate
List.get_cyclicPermutations : ∀ {α : Type u} (l : List α) (n : Fin l.cyclicPermutations.length), l.cyclicPermutations.get n = l.rotate ↑n
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_rangeRestrict : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (f : A →A[R] B), ↑f.rangeRestrict = (↑f).rangeRestrict
-- Init.Data.Vector.Lemmas
Vector.foldl_assoc : ∀ {α : Type u_1} {n : ℕ} {op : α → α → α} [ha : Std.Associative op] {xs : Vector α n} {a₁ a₂ : α},
  Vector.foldl op (op a₁ a₂) xs = op a₁ (Vector.foldl op a₂ xs)
-- Init.Data.List.Sublist
List.sublist_or_mem_of_sublist : ∀ {α : Type u_1} {l l₁ : List α} {a : α} {l₂ : List α}, l.Sublist (l₁ ++ a :: l₂) → l.Sublist (l₁ ++ l₂) ∨ a ∈ l
-- Mathlib.Algebra.Algebra.Unitization
Unitization.isIdempotentElem_inr_iff : ∀ (R : Type u_1) {A : Type u_2} [inst : MulZeroClass R] [inst_1 : AddZeroClass A] [inst_2 : Mul A]
  [inst_3 : SMulWithZero R A] {a : A}, IsIdempotentElem ↑a ↔ IsIdempotentElem a
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.coe_neg : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [inst_2 : ContinuousNeg G],
  ⇑(Homeomorph.neg G) = Neg.neg
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapShortComplexH1_comp : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k K} (f : G →* H) (g : H →* K)
  (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C),
  groupHomology.mapShortComplexH1 (g.comp f) (CategoryTheory.CategoryStruct.comp φ ((Rep.resFunctor f).map ψ)) =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapShortComplexH1 f φ) (groupHomology.mapShortComplexH1 g ψ)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget.mk.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {outWidth w len : ℕ}
  (oldLayer oldLayer_1 : aig.RefVec (len * w)),
  oldLayer = oldLayer_1 →
    ∀ (h : outWidth = (len + 1) / 2 * w) (hlen : 0 < len),
      { w := w, len := len, oldLayer := oldLayer, h := h, hlen := hlen } =
        { w := w, len := len, oldLayer := oldLayer_1, h := h, hlen := hlen }
-- Batteries.Tactic.Alias
/-- Get the alias information for a name  -/
Batteries.Tactic.Alias.getAliasInfo : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (Option Batteries.Tactic.Alias.AliasInfo)
-- Mathlib.NumberTheory.Padics.MahlerBasis
Ring.multichoose.eq_1 : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] (r : R) (n : ℕ),
  Ring.multichoose r n = BinomialRing.multichoose r n
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.isTranscendenceBasis_of_trdeg_le : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [Nontrivial R]
  [NoZeroDivisors A] {ι : Type w} {x : ι → A},
  AlgebraicIndependent R x →
    Algebra.trdeg R A < Cardinal.aleph0 → Algebra.trdeg R A ≤ Cardinal.mk ι → IsTranscendenceBasis R x
-- Mathlib.Algebra.Ring.TransferInstance
/-- Transfer `NonUnitalSemiring` across an `Equiv`  -/
Equiv.nonUnitalSemiring : {α : Type u_1} → {β : Type u_2} → α ≃ β → [NonUnitalSemiring β] → NonUnitalSemiring α
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_eq_getKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [instBEq : BEq α] [Std.LawfulBEqOrd α] {k : α}
  [inst_3 : Inhabited α] {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered → t.getKey! k = Std.Internal.List.getKey! k t.toListModel
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.findSome?_eq_findSomeM? : ∀ {α β : Type w} {γ : Type x} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id]
  [Std.Iterators.Finite α Id] {it : Std.Iter β} {f : β → Option γ},
  it.findSome? f = (it.findSomeM? fun x => pure (f x)).run
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.self_le_max?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k kmi : α},
  (t.insert k).max?.get ⋯ = kmi → (cmp k kmi).isLE = true
-- Mathlib.Algebra.Quaternion
Quaternion.imJ_zero : ∀ {R : Type u_3} [inst : CommRing R], QuaternionAlgebra.imJ 0 = 0
-- Mathlib.Algebra.Group.Nat.Range
Finset.disjoint_range_addLeftEmbedding : ∀ (a : ℕ) (s : Finset ℕ), Disjoint (Finset.range a) (Finset.map (addLeftEmbedding a) s)
-- Mathlib.Algebra.Polynomial.OfFn
Polynomial.surjective_toFn : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), Function.Surjective ⇑(Polynomial.toFn n)
-- Mathlib.Topology.MetricSpace.Thickening
/-- **Alias** of `Metric.thickening_eq_preimage_infEDist`.

---

The (open) thickening equals the preimage of an open interval under `Metric.infEDist`.  -/
Metric.thickening_eq_preimage_infEdist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α),
  Metric.thickening δ E = (fun x => Metric.infEDist x E) ⁻¹' Set.Iio (ENNReal.ofReal δ)
-- Mathlib.Geometry.Convex.Cone.TensorProduct
/-- `maxTensorProduct` is monotone.  -/
PointedCone.maxTensorProduct_mono : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {G : Type u_2}
  [inst_3 : AddCommGroup G] [inst_4 : Module R G] {H : Type u_3} [inst_5 : AddCommGroup H] [inst_6 : Module R H]
  {C₁ C₁' : PointedCone R G} {C₂ C₂' : PointedCone R H},
  C₁ ≤ C₁' → C₂ ≤ C₂' → C₁.maxTensorProduct C₂ ≤ C₁'.maxTensorProduct C₂'
-- Init.RCases
/-- The syntax category of `rintro` patterns.  -/
Lean.Parser.Category.rintroPat : Lean.Parser.Category
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f_0_comp_chainsIso₀ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  CategoryTheory.CategoryStruct.comp ((groupHomology.chainsMap f φ).f 0) (groupHomology.chainsIso₀ B).hom =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₀ A).hom (Rep.Hom.toModuleCatHom φ)
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_mul' : ∀ {p q : ℝ}, 0 ≤ q → ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- If all elements of `s : Set A` commute pairwise and with elements of `star s`, then `adjoin R s`
is commutative.  -/
NonUnitalStarAlgebra.isMulCommutative_adjoin : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {s : Set A},
  (∀ x ∈ s, ∀ y ∈ s, x * y = y * x) →
    (∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) → IsMulCommutative ↥(NonUnitalStarAlgebra.adjoin R s)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.primesOver_finite`. -/
primesOver_finite : ∀ {A : Type u_4} [inst : CommRing A] (p : Ideal A) [hpm : p.IsMaximal] (B : Type u_5) [inst_1 : CommRing B]
  [IsDedekindDomain B] [inst_3 : Algebra A B] [IsDomain A] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B],
  (p.primesOver B).Finite
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `wbtw_vadd_const_iff`. -/
Wbtw.vadd_const : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : V} (p : P), Wbtw R x y z → Wbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
coe_set_eq_one : ∀ {G : Type u_2} [inst : Group G] {s : Subgroup G}, ↑s = 1 ↔ s = ⊥
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.exists_map_preimage_le_map_preimage : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] {i : I} {U V : (D.obj i).Opens},
  IsCompact ↑U →
    (TopologicalSpace.Opens.map (c.π.app i).base).obj U ≤ (TopologicalSpace.Opens.map (c.π.app i).base).obj V →
      ∃ j fji, (TopologicalSpace.Opens.map (D.map fji).base).obj U ≤ (TopologicalSpace.Opens.map (D.map fji).base).obj V
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.fst.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N],
  Monoid.Coprod.fst = Monoid.Coprod.lift (MonoidHom.id M) 1
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.edgeFinset_top : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V], ⊤.edgeFinset = Sym2.diagSetᶜ.toFinset
-- Std.Data.ExtDHashMap.Basic
/-- Compares two hash maps using Boolean equality on keys and values.

Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
 -/
Std.ExtDHashMap.Const.beq : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      {β : Type v} →
        [EquivBEq α] →
          [LawfulHashable α] → [BEq β] → (Std.ExtDHashMap α fun x => β) → (Std.ExtDHashMap α fun x => β) → Bool
-- Mathlib.Topology.Specialization
/-- Sends a topological space to its specialisation order.  -/
topToPreord : CategoryTheory.Functor TopCat Preord
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
/-- The derivative of `klFun` at `x ≠ 0` is `log x`.  -/
InformationTheory.hasDerivAt_klFun : ∀ {x : ℝ}, x ≠ 0 → HasDerivAt InformationTheory.klFun (Real.log x) x
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_measure_zero : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  μ = 0 → MeasureTheory.setToFun μ T hT f = 0
-- Mathlib.Analysis.CStarAlgebra.Projection
IsStarProjection.commute_of_le : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {p q : A},
  IsStarProjection p → IsStarProjection q → p ≤ q → Commute p q
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.glueData_openCover_map : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) (j : ι),
  (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).openCover.f j =
    AlgebraicGeometry.Scheme.LocalRepresentability.toGlued hf j
-- Mathlib.Data.Finset.Defs
Finset.ssubset_of_subset_of_ssubset : ∀ {α : Type u_1} {s₁ s₂ s₃ : Finset α}, s₁ ⊆ s₂ → s₂ ⊂ s₃ → s₁ ⊂ s₃
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYoneda_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] (X : C),
  CategoryTheory.shrinkYoneda.{w, v, u}.obj X =
    CategoryTheory.FunctorToTypes.shrink.{w, v, v, u} (CategoryTheory.yoneda.obj X)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_list_eq_aleph0 : ∀ (α : Type u) [Countable α] [Nonempty α], Cardinal.mk (List α) = Cardinal.aleph0
-- Mathlib.Data.List.Infix
List.prefix_append_drop : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₂ = l₁ ++ List.drop l₁.length l₂
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.vec_iff : ∀ {m n : ℕ} {f : List.Vector ℕ m → List.Vector ℕ n}, Nat.Partrec'.Vec f ↔ Computable f
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin.eq_1 : ∀ (x : ℝ), Real.sin x = (Complex.sin ↑x).re