mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Implementation of `AddMon.equivLaxMonoidalFunctorPUnit`.  -/
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor (CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C)
        (CategoryTheory.AddMon C)
-- Mathlib.Topology.Bornology.Constructions
Bornology.cobounded_pi : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → Bornology (X i)],
  Bornology.cobounded ((i : ι) → X i) = Filter.coprodᵢ fun i => Bornology.cobounded (X i)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.map_map : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : NonUnitalNonAssocSemiring C] [inst_4 : Module R A]
  [inst_5 : Module R B] [inst_6 : Module R C] (S : NonUnitalSubalgebra R A) (g : B →ₙₐ[R] C) (f : A →ₙₐ[R] B),
  NonUnitalSubalgebra.map g (NonUnitalSubalgebra.map f S) = NonUnitalSubalgebra.map (g.comp f) S
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.trans_domCongr_domCongr : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} {O : Type u_9} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] [inst_5 : Monoid O] (e : M ≃* N)
  (f : N ≃* O),
  (MonoidAlgebra.domCongr R A e).trans (MonoidAlgebra.domCongr R A f) = MonoidAlgebra.domCongr R A (e.trans f)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.eqToHom_right : ∀ {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] {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (h : X = Y),
  (CategoryTheory.eqToHom h).right = CategoryTheory.eqToHom ⋯
-- Lean.Data.Json.Basic
Lean.Json.instCoeString : Coe String Lean.Json
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_toDual : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Ici (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Iic a
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.isFinitePlace : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (v : NumberField.FinitePlace K), NumberField.IsFinitePlace ↑v
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.toAlgEquiv_eq_coe : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A ≃ₐc[R] B), f.toAlgEquiv = f.toAlgEquiv
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_maxKey?_modify_eq_isSome : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {f : β → β},
  (t.modify k f).maxKey?.isSome = t.maxKey?.isSome
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.not_insert_eq_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, ¬m.insert k v = ∅
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.nsmul_eq_iff : ∀ {ψ θ : Real.Angle} {n : ℕ}, n ≠ 0 → (n • ψ = n • θ ↔ ∃ k, ψ = θ + ↑k • ↑(2 * Real.pi / ↑n))
-- Std.Time.DateTime.Timestamp
Std.Time.instInhabitedTimestamp.default : Std.Time.Timestamp
-- Mathlib.Algebra.Group.NatPowAssoc
Prod.instNatPowAssoc : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [NatPowAssoc M] [inst_3 : MulOneClass N]
  [inst_4 : Pow N ℕ] [NatPowAssoc N], NatPowAssoc (M × N)
-- Mathlib.Data.Bundle
Bundle.TotalSpace.toProd_symm_apply_proj : ∀ (B : Type u_4) (F : Type u_5) (x : B × F), ((Bundle.TotalSpace.toProd B F).symm x).proj = x.1
-- Lean.KeyedDeclsAttribute
/-- Recall that we cannot store `γ` into .olean files because it is a closure.
Given `OLeanEntry.declName`, we convert it into a `γ` by using the unsafe function `evalConstCheck`.  -/
Lean.KeyedDeclsAttribute.AttributeEntry.value : {γ : Type} → Lean.KeyedDeclsAttribute.AttributeEntry γ → γ
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Center C} {f g : X ⟶ Y}, f = g ↔ f.f = g.f
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.collect.processImplicitArg : Bool →
  Lean.Elab.Term.CollectPatternVars.Context →
    Lean.Elab.Term.CollectPatternVars.M Lean.Elab.Term.CollectPatternVars.Context
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_of_contains_insert : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF → ∀ {k a : α} {v : β k}, (m.insert k v).contains a = true → (k == a) = false → m.contains a = true
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsupp.eq_1 : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : Semiring S] [inst_6 : Algebra R S] [inst_7 : Module S M] [inst_8 : IsScalarTower R S M],
  finsuppTensorFinsupp R S M N ι κ =
    TensorProduct.AlgebraTensorModule.congr (finsuppLEquivDirectSum S M ι) (finsuppLEquivDirectSum R N κ) ≪≫ₗ
      ((TensorProduct.directSum R S (fun x => M) fun x => N) ≪≫ₗ
        (finsuppLEquivDirectSum S (TensorProduct R M N) (ι × κ)).symm)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- The algebra-homomorphism forgetting that a bounded continuous function is bounded.  -/
BoundedContinuousFunction.toContinuousMapₐ : {α : Type u} →
  {γ : Type w} →
    (𝕜 : Type u_1) →
      [inst : NormedField 𝕜] →
        [inst_1 : TopologicalSpace α] →
          [inst_2 : NormedRing γ] → [inst_3 : NormedAlgebra 𝕜 γ] → BoundedContinuousFunction α γ →ₐ[𝕜] C(α, γ)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
/-- Auxiliary lemma showing that for any `k : ℤ` the function `z → 1/(c*z+d)^k` is
differentiable on `{z : ℂ | 0 < z.im}`.  -/
EisensteinSeries.div_linear_zpow_differentiableOn : ∀ (k : ℤ) (a : Fin 2 → ℤ), DifferentiableOn ℂ (fun z => (↑(a 0) * z + ↑(a 1)) ^ (-k)) {z | 0 < z.im}
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.front : ∀ {c : Char} {m : List Char} {s : Substring.Raw}, s.Valid → s.toString.toList = c :: m → s.front = c
-- Mathlib.Order.CountableSupClosed
CountableSupClosed.sSup_mem : ∀ {α : Type u_2} {s : Set α} [inst : CompleteLattice α],
  CountableSupClosed s → ∀ {A : Set α}, A.Countable → A.Nonempty → (∀ a ∈ A, a ∈ s) → sSup A ∈ s
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm is an absolute value: positive-definite and multiplicative, satisfying the
triangle inequality.  -/
padicNorm.instIsAbsoluteValueRat : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], IsAbsoluteValue (padicNorm p)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
ContDiff.ccos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {n : WithTop ℕ∞},
  ContDiff ℂ n f → ContDiff ℂ n fun x => Complex.cos (f x)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.hom_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒞₁ : CategoryTheory.Subobject.Classifier C),
  𝒞₁.hom 𝒞₁ = CategoryTheory.CategoryStruct.id 𝒞₁.Ω
-- Mathlib.Algebra.Homology.Augment
ChainComplex.truncateAugment_inv_f : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : ChainComplex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) (i : ℕ),
  (C.truncateAugment f w).inv.f i = CategoryTheory.CategoryStruct.id ((ChainComplex.truncate.obj (C.augment f w)).X i)
-- Mathlib.Algebra.Lie.Nilpotent
LieAlgebra.maxNilpotentIdealIsNilpotent : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [IsNoetherian R L],
  LieModule.IsNilpotent L ↥(LieAlgebra.maxNilpotentIdeal R L)
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isRevMatch_iff : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsRevMatch pat pos ↔ (s.sliceFrom pos).copy = pat
-- Mathlib.RingTheory.IdealFilter.Basic
/-- An ideal filter is Gabriel if it satisfies `IsUniform` and axiom T4.
See [nLab: Gabriel filter](https://ncatlab.org/nlab/show/Gabriel+filter).  -/
IdealFilter.IsGabriel : {A : Type u_1} → [inst : Ring A] → IdealFilter A → Prop
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.subtype.eq_1 : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} (H : S) [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G],
  ↑H = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯ }
-- Init.Data.Iterators.Basic
Std.IterM.TerminationMeasures.Finite.mk.inj : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {inst : Std.Iterator α m β} {it it_1 : Std.IterM m β},
  { it := it } = { it := it_1 } → it = it_1
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.MemSobolev.smul : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] [inst_7 : CompleteSpace F] {s : ℝ} {p : ENNReal} [hp : Fact (1 ≤ p)] (c : ℂ)
  {f : TemperedDistribution E F}, TemperedDistribution.MemSobolev s p f → TemperedDistribution.MemSobolev s p (c • f)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsLoop.eq_of_isCircuit_mem : ∀ {α : Type u_1} {M : Matroid α} {e : α} {C : Set α}, M.IsLoop e → M.IsCircuit C → e ∈ C → C = {e}
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicAt.neg` -/
MeromorphicAt.fun_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E}, MeromorphicAt f x → MeromorphicAt (fun i => -f i) x
-- Mathlib.Algebra.DirectSum.Module
/-- Direct sums of isomorphic additive groups are isomorphic.  -/
DirectSum.congrAddEquiv : {ι : Type u_2} →
  {N : ι → Type u_3} →
    [inst : (i : ι) → AddCommMonoid (N i)] →
      {P : ι → Type u_4} →
        [inst_1 : (i : ι) → AddCommMonoid (P i)] →
          ((i : ι) → N i ≃+ P i) → (DirectSum ι fun i => N i) ≃+ DirectSum ι fun i => P i
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.mul_le_one`.  -/
Left.mul_le_one : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b : α}, a ≤ 1 → b ≤ 1 → a * b ≤ 1
-- Batteries.Data.Nat.Lemmas
Nat.strongRec_eq : ∀ {motive : ℕ → Sort u_1} (ind : (n : ℕ) → ((m : ℕ) → m < n → motive m) → motive n) (t : ℕ),
  Nat.strongRec ind t = ind t fun m x => Nat.strongRec ind m
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.instNontrivialSubtypePermFinHAddNatOfNatMemSubgroup : ∀ {n : ℕ}, Nontrivial ↥(alternatingGroup (Fin (n + 3)))
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- The seminorm is given by infimum over all `c` such that the estimate
`‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ c` holds.

Note that it is usually better to use `seminorm_le_bound` or `le_seminorm` instead of this lemma.  -/
SchwartzMap.seminorm_apply : ∀ (𝕜 : Type u_2) {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {k n : ℕ} (f : SchwartzMap E F),
  (SchwartzMap.seminorm 𝕜 k n) f = sInf {c | 0 ≤ c ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ c}
-- Init.Data.List.Basic
List.headD_nil : ∀ {α : Type u} {d : α}, [].headD d = d
-- Mathlib.Topology.MetricSpace.Cover
Metric.isCover_zero : ∀ {X : Type u_1} [inst : EMetricSpace X] {s N : Set X}, Metric.IsCover 0 s N ↔ s ⊆ N
-- Mathlib.NumberTheory.Padics.Complex
/-- The valuation of `p : ℂ_[p]` is `1/p`.  -/
PadicComplex.valuation_p : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], Valued.v ↑p = 1 / ↑p
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- A submonoid `S` includes `closure s` if and only if it includes `s`.  -/
Submonoid.closure_le : ∀ {M : Type u_1} [inst : MulOneClass M] {s : Set M} {S : Submonoid M}, Submonoid.closure s ≤ S ↔ s ⊆ ↑S
-- Init.Data.List.Lemmas
List.getElem?_append_left : ∀ {α : Type u_1} {l₁ l₂ : List α} {i : ℕ}, i < l₁.length → (l₁ ++ l₂)[i]? = l₁[i]?
-- Init.Grind.ToInt
Lean.Grind.IntInterval.wrap_eq_wrap_iff : ∀ {lo hi x y : ℤ},
  (Lean.Grind.IntInterval.co lo hi).wrap x = (Lean.Grind.IntInterval.co lo hi).wrap y ↔ (x - y) % (hi - lo) = 0
-- Batteries.Data.BinomialHeap.Lemmas
Batteries.BinomialHeap.Imp.HeapNode.WF.realSize_eq : ∀ {α : Type u_1} {le : α → α → Bool} {a : α} {n : ℕ} {s : Batteries.BinomialHeap.Imp.HeapNode α},
  Batteries.BinomialHeap.Imp.HeapNode.WF le a s n → s.realSize + 1 = 2 ^ n
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- The topological Besicovitch covering theorem: there exist finitely many families of disjoint
balls covering all the centers in a package. More specifically, one can use `N` families if there
are no satellite configurations with `N+1` points.  -/
Besicovitch.exist_disjoint_covering_families : ∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} {N : ℕ} {τ : ℝ},
  1 < τ →
    IsEmpty (Besicovitch.SatelliteConfig α N τ) →
      ∀ (q : Besicovitch.BallPackage β α),
        ∃ s,
          (∀ (i : Fin N), (s i).PairwiseDisjoint fun j => Metric.closedBall (q.c j) (q.r j)) ∧
            Set.range q.c ⊆ ⋃ i, ⋃ j ∈ s i, Metric.ball (q.c j) (q.r j)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.mk.congr_simp : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (toContinuousMap toContinuousMap_1 : C(↑unitInterval × X, Y))
  (e_toContinuousMap : toContinuousMap = toContinuousMap_1)
  (map_zero_left : ∀ (x : X), toContinuousMap.toFun (0, x) = f₀ x)
  (map_one_left : ∀ (x : X), toContinuousMap.toFun (1, x) = f₁ x),
  { toContinuousMap := toContinuousMap, map_zero_left := map_zero_left, map_one_left := map_one_left } =
    { toContinuousMap := toContinuousMap_1, map_zero_left := ⋯, map_one_left := ⋯ }
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_natCast_eq_one_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ}, ‖↑n‖ = 1 ↔ p.Coprime n
-- Mathlib.Data.List.Chain
List.isChain_cons : ∀ {α : Type u_1} {R : α → α → Prop} {x : α} {l : List α},
  List.IsChain R (x :: l) ↔ (∀ y ∈ l.head?, R x y) ∧ List.IsChain R l
-- Mathlib.RingTheory.Ideal.Maps
/-- The `Ideal` version of `Set.image_subset_preimage_of_inverse`.  -/
Ideal.map_le_comap_of_inverse : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  {G : Type u_2} [inst_3 : FunLike G S R] [inst_4 : RingHomClass G S R] (g : G) (I : Ideal R),
  Function.LeftInverse ⇑g ⇑f → Ideal.map f I ≤ Ideal.comap g I
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_b₆ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {A : Type v} [inst_1 : CommRing A] (f : R →+* A),
  (W.map f).b₆ = f W.b₆
-- Mathlib.Topology.MetricSpace.Gluing
/-- The predistance on the disjoint union `Σ n, X n` can be computed in any `X k` for large
enough `k`.  -/
Metric.inductiveLimitDist_eq_dist : ∀ {X : ℕ → Type u} [inst : (n : ℕ) → MetricSpace (X n)] {f : (n : ℕ) → X n → X (n + 1)},
  (∀ (n : ℕ), Isometry (f n)) →
    ∀ (x y : (n : ℕ) × X n) (m : ℕ) (hx : x.fst ≤ m) (hy : y.fst ≤ m),
      Metric.inductiveLimitDist f x y =
        dist (Nat.leRecOn hx (fun {k} => f k) x.snd) (Nat.leRecOn hy (fun {k} => f k) y.snd)
-- Mathlib.Data.Sym.Sym2
Sym2.diagSet_eq_univ_of_subsingleton : ∀ {α : Type u_1} [Subsingleton α], Sym2.diagSet = Set.univ
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- Let `{x | p x}` be a subsemigroup of a commutative monoid `M`. Let `f : M → N` be a map
submultiplicative on `{x | p x}`, i.e., `p x → p y → f (x * y) ≤ f x * f y`. Let `g i`, `i ∈ s`, be
a nonempty finite family of elements of `M` such that `∀ i ∈ s, p (g i)`. Then
`f (∏ x ∈ s, g x) ≤ ∏ x ∈ s, f (g x)`.  -/
Finset.le_prod_nonempty_of_submultiplicative_on_pred : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : CommMonoid M] [inst_1 : CommMonoid N] [inst_2 : Preorder N]
  [IsOrderedMonoid N] (f : M → N) (p : M → Prop),
  (∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) →
    (∀ (x y : M), p x → p y → p (x * y)) →
      ∀ (g : ι → M) (s : Finset ι), s.Nonempty → (∀ i ∈ s, p (g i)) → f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.functorExtension₂_obj_map_f : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (X : CategoryTheory.Functor C D)
  {X_1 Y : CategoryTheory.Idempotents.Karoubi C} (f : X_1 ⟶ Y),
  (((CategoryTheory.Idempotents.functorExtension₂ C D).obj X).map f).f = X.map f.f
-- Mathlib.Logic.Equiv.Defs
Equiv.injective_comp : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ), Function.Injective (f ∘ ⇑e) ↔ Function.Injective f
-- Mathlib.Algebra.Category.Grp.Images
/-- the universal property for the image factorisation  -/
AddCommGrpCat.image.lift : {G H : AddCommGrpCat} → {f : G ⟶ H} → (F' : CategoryTheory.Limits.MonoFactorisation f) → AddCommGrpCat.image f ⟶ F'.I
-- Mathlib.Topology.Sets.OpenCover
/-- (Pre)Irreducibility of an open set can be checked on a cover by opens
with pairwise non-empty intersections.  -/
IsPreirreducible.of_subset_iUnion : ∀ {X : Type u_1} {ι : Type u_2} [inst : TopologicalSpace X] {U : ι → TopologicalSpace.Opens X},
  Pairwise (Function.onFun (fun x1 x2 => ¬Disjoint x1 x2) U) →
    (∀ (i : ι), IsPreirreducible ↑(U i)) → ∀ {s : Set X}, IsOpen s → s ⊆ ⋃ i, ↑(U i) → IsPreirreducible s
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.empty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α], ∅.WF
-- Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
IsTranscendenceBasis.lift_cardinalMk_eq_max_lift : ∀ {F : Type u} {E : Type v} [inst : CommRing F] [Nontrivial F] [inst_2 : CommRing E] [IsDomain E] [inst_4 : Algebra F E]
  {ι : Type w} {x : ι → E} [Nonempty ι],
  IsTranscendenceBasis F x →
    Cardinal.lift.{max u w, v} (Cardinal.mk E) =
      max (max (Cardinal.lift.{max v w, u} (Cardinal.mk F)) (Cardinal.lift.{max u v, w} (Cardinal.mk ι)))
        Cardinal.aleph0
-- Init.Grind.AC
Lean.Grind.AC.Seq.brecOn.eq : ∀ {motive : Lean.Grind.AC.Seq → Sort u} (t : Lean.Grind.AC.Seq)
  (F_1 : (t : Lean.Grind.AC.Seq) → Lean.Grind.AC.Seq.below t → motive t),
  Lean.Grind.AC.Seq.brecOn t F_1 = F_1 t (Lean.Grind.AC.Seq.brecOn.go t F_1).2
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `le_div_iff₀'` for a version with multiplication on the other side.  -/
le_div_iff₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b c : G₀},
  0 < c → (a ≤ b / c ↔ a * c ≤ b)
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.Context : Type
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.forget_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Center C), (CategoryTheory.Center.forget C).obj X = X.fst
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
/-- The topology on the small affine étale site is the topology induced by `Spec` from
the small étale site.  -/
AlgebraicGeometry.Scheme.AffineEtale.topology : (S : AlgebraicGeometry.Scheme) → CategoryTheory.GrothendieckTopology S.AffineEtale
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
/-- A `X`-continuous map `g : Y → Z` induces a continuous map
between the types `Y` and `Z` equipped with the `X`-generated topology.  -/
Topology.ContinuousGeneratedBy.continuousMap : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Y : Type v} →
        [inst_1 : TopologicalSpace Y] →
          {Z : Type v'} →
            [inst_2 : TopologicalSpace Z] →
              {g : Y → Z} →
                Topology.ContinuousGeneratedBy X g →
                  C(Topology.WithGeneratedByTopology X Y, Topology.WithGeneratedByTopology X Z)
-- Std.Data.ByteSlice
instSliceableByteArrayNatByteSlice : Std.Rcc.Sliceable ByteArray ℕ ByteSlice
-- Mathlib.Combinatorics.HalesJewett
/-- Consider a line in `ι → η → α` as a `η`-dimensional subspace in `ι × η → α`.  -/
Combinatorics.Line.toSubspace : {η : Type u_1} → {α : Type u_2} → {ι : Type u_3} → Combinatorics.Line (η → α) ι → Combinatorics.Subspace η α (ι × η)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.succ_pos : ∀ (c : Cardinal.{u_1}), 0 < Order.succ c
-- Mathlib.Topology.Closure
IsClosed.closure_subset : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → closure s ⊆ s
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreesLE_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.degreesLE R σ 0 = 1
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- Given a family of schemes with morphisms to `X` satisfying `P` that jointly
cover `X`, `Cover.mkOfCovers` is an associated `P`-cover of `X`.  -/
AlgebraicGeometry.Scheme.Cover.mkOfCovers : {X : AlgebraicGeometry.Scheme} →
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
    (J : Type u_1) →
      (obj : J → AlgebraicGeometry.Scheme) →
        (map : (j : J) → obj j ⟶ X) →
          (∀ (x : ↥X), ∃ j y, (map j) y = x) →
            autoParam (∀ (j : J), P (map j)) AlgebraicGeometry.Scheme.Cover.mkOfCovers._auto_1 →
              AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (k : α) (f : Option β → Option β), (t₁.alter k f).Equiv (t₂.alter k f)
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
TopCat.Presheaf.IsSheaf.isSheafOpensLeCover : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} {F : TopCat.Presheaf C X} {ι : Type u_2}
  (U : ι → TopologicalSpace.Opens ↑X),
  F.IsSheaf →
    Nonempty
      (CategoryTheory.Limits.IsLimit
        (CategoryTheory.Functor.mapCone F (TopCat.Presheaf.SheafCondition.opensLeCoverCocone U).op))
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.coeff_update_ne : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (f : SkewMonoidAlgebra M α) {a a' : α} (b : M),
  a' ≠ a → (f.update a b).coeff a' = f.coeff a'
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ext_iff : ∀ {R : Type u_1} {inst : Semiring R} {x y : ValuativeRel R}, x = y ↔ ValuativeRel.vle = ValuativeRel.vle
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflQuiver.homOfEq_id : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {X X' : V} (hX : X = X'),
  Quiver.homOfEq (CategoryTheory.ReflQuiver.id X) hX hX = CategoryTheory.ReflQuiver.id X'
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleRange_last : ∀ (n : ℕ), (Fin.last n).cycleRange = finRotate (n + 1)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.containsThenInsertIfNew_snd : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.containsThenInsertIfNew k v).2 = m.insertIfNew k v
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_minKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).minKey?.isSome = true