mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.add : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E] [SecondCountableTopology E]
  {Y : Ω → E}, ProbabilityTheory.HasGaussianLaw (fun ω => (X ω, Y ω)) P → ProbabilityTheory.HasGaussianLaw (X + Y) P
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
/-- The localization functor `HomotopyCategory C (ComplexShape.up ℤ) ⥤ DerivedCategory C`.  -/
DerivedCategory.Qh : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        CategoryTheory.Functor (HomotopyCategory C (ComplexShape.up ℤ)) (DerivedCategory C)
-- Mathlib.Analysis.Normed.Group.Lemmas
eventually_nnnorm_sub_lt : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (x₀ : E) {ε : NNReal}, 0 < ε → ∀ᶠ (x : E) in nhds x₀, ‖x - x₀‖₊ < ε
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- We have `ζ(0) = -1 / 2`.  -/
riemannZeta_zero : riemannZeta 0 = -1 / 2
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.Mod.Hom.mk'`.

---

An alternative constructor for `Hom`,
taking a morphism without a `[IsModHom]` instance, as well as the relevant
equality to put such an instance.  -/
CategoryTheory.Mod_.Hom.mk' : {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.MonObj A] →
                {M N : CategoryTheory.Mod D A} →
                  (f : M.X ⟶ N.X) →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul f =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
                            CategoryTheory.ModObj.smul)
                        CategoryTheory.Mod.Hom.mk'._auto_1 →
                      M.Hom N
-- Init.Data.List.Nat.Sum
List.sum_pos_iff_exists_pos_nat : ∀ {l : List ℕ}, 0 < l.sum ↔ ∃ x ∈ l, 0 < x
-- Mathlib.RingTheory.SimpleModule.Basic
/-- The annihilator of a semisimple module over a commutative ring is a radical ideal.  -/
IsSemisimpleModule.annihilator_isRadical : ∀ (M : Type u_4) [inst : AddCommGroup M] (R : Type u_6) [inst_1 : CommRing R] [inst_2 : Module R M]
  [IsSemisimpleModule R M], (Module.annihilator R M).IsRadical
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- The property of objects in `PartOrdEmb` that are
satisfied by `κ`-directed partially ordered types.
(Note: for partially ordered types, "`κ`-directed" and
"`κ`-filtered" are synonyms. This is implemented using the
categorical notion `IsCardinalFiltered`.)  -/
PartOrdEmb.isCardinalFiltered : (κ : Cardinal.{u}) → [Fact κ.IsRegular] → CategoryTheory.ObjectProperty PartOrdEmb
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : Option β → Option β}, k ∈ t.alter k f ↔ (f t[k]?).isSome = true
-- Std.Time.Zoned.Database.TZdb
/-- Reads a TZif file from disk and retrieves the zone rules for the specified timezone ID.
 -/
Std.Time.Database.TZdb.parseTZIfFromDisk : System.FilePath → String → IO Std.Time.TimeZone.ZoneRules
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_mul_C_eq_of_mul_eq_one : ∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R} {ai : R},
  a * ai = 1 → (p * Polynomial.C a).natDegree = p.natDegree
-- Mathlib.Analysis.AbsoluteValue.Equivalence
/-- If $v$ and $w$ are two real absolute values on a field $F$, equivalent in the sense that
$v(x) \leq v(y)$ if and only if $w(x) \leq w(y)$, then $\frac{\log (v(a))}{\log (w(a))}$ is
constant for all $0 \neq a\in F$ with $v(a) \neq 1$.
 -/
AbsoluteValue.IsEquiv.log_div_log_eq_log_div_log : ∀ {F : Type u_1} [inst : Field F] {v w : AbsoluteValue F ℝ},
  v.IsEquiv w →
    ∀ {a : F},
      a ≠ 0 → v a ≠ 1 → ∀ {b : F}, b ≠ 0 → v b ≠ 1 → Real.log (v b) / Real.log (w b) = Real.log (v a) / Real.log (w a)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.interSmaller_eq_interSmallerₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ : Std.DHashMap.Internal.Raw₀ α β)
  (m₂ : Std.DHashMap.Raw α β), m₁.interSmaller m₂ = m₁.interSmallerₘ m₂
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- **Alias** of `CategoryTheory.Functor.OplaxMonoidal.oplax_associativity`.

---

associativity of the tensorator  -/
CategoryTheory.Functor.OplaxMonoidal.associativity : ∀ {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 D}
  (F : CategoryTheory.Functor C D) [self : F.OplaxMonoidal] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) (F.obj Z))
        (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.δ F Y Z)))
-- Mathlib.Algebra.BigOperators.Expect
/-- Reorder an average.

The difference with `Finset.expect_nbij'` is that the bijection is specified as a surjective
injection, rather than by an inverse function.

The difference with `Finset.expect_bij` is that the bijection is a non-dependent function, rather
than being allowed to use membership of the domain of the average.  -/
Finset.expect_nbij : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s : Finset ι}
  {f : ι → M} {t : Finset κ} {g : κ → M} (i : ι → κ),
  (∀ a ∈ s, i a ∈ t) →
    (∀ a ∈ s, f a = g (i a)) → Set.InjOn i ↑s → Set.SurjOn i ↑s ↑t → (s.expect fun i => f i) = t.expect fun i => g i
-- Mathlib.Topology.LocallyFinite
LocallyFinite.continuousOn_iUnion : ∀ {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : ι → Set X}
  {g : X → Y},
  LocallyFinite f → (∀ (i : ι), IsClosed (f i)) → (∀ (i : ι), ContinuousOn g (f i)) → ContinuousOn g (⋃ i, f i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_empty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {a fallback : α},
  Std.DTreeMap.Internal.Impl.empty.getKeyD a fallback = fallback
-- Mathlib.GroupTheory.Nilpotent
AddGroup.nilpotencyClass_le_of_ker_le_center : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_2} [inst_1 : AddGroup H] (f : G →+ H),
  f.ker ≤ AddSubgroup.center G → ∀ [AddGroup.IsNilpotent H], AddGroup.nilpotencyClass G ≤ AddGroup.nilpotencyClass H + 1
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- Define a tempered distribution from a L^p function.  -/
MeasureTheory.Lp.toTemperedDistribution : {E : Type u_3} →
  {F : Type u_4} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℂ F] →
            [CompleteSpace F] →
              [inst_5 : MeasurableSpace E] →
                [BorelSpace E] →
                  {μ : MeasureTheory.Measure E} →
                    [hμ : μ.HasTemperateGrowth] →
                      {p : ENNReal} → [hp : Fact (1 ≤ p)] → ↥(MeasureTheory.Lp F p μ) → TemperedDistribution E F
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.of_subsingleton : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Subsingleton R], AlgebraicIndependent R x
-- Mathlib.GroupTheory.Transfer
Subgroup.mem_transferSet : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} (g : G) (q : G ⧸ H), H.transferFunction g q ∈ H.transferSet g
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getVert.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {u : V} (x : ℕ), SimpleGraph.Walk.nil.getVert x = u
-- Mathlib.Algebra.ContinuedFractions.TerminatedStable
_private.Mathlib.Algebra.ContinuedFractions.TerminatedStable.0.GenContFract.contsAux.match_1.eq_1 : ∀ {K : Type u_1} (motive : Option (GenContFract.Pair K) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (gp : GenContFract.Pair K) → motive (some gp)),
  (match none with
    | none => h_1 ()
    | some gp => h_2 gp) =
    h_1 ()
-- Init.Data.Int.LemmasAux
Int.toNat_sub' : ∀ (a : ℤ) (b : ℕ), (a - ↑b).toNat = a.toNat - b
-- Mathlib.Data.List.Count
List.count_diff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (a : α) (l₁ l₂ : List α),
  List.count a (l₁.diff l₂) = List.count a l₁ - List.count a l₂
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.instInhabitedHom : (R : Type u) → [inst : Semiring R] → (M N : CategoryTheory.Mat R) → Inhabited (M ⟶ N)
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.one_apply : ∀ {R : Type u} [inst : Monoid R] {A : Type v} [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : DistribMulAction R A]
  (a : A), 1 a = a
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.mem_iSup : ∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_4} (p : ι → AddSubmonoid M) {m : M},
  m ∈ ⨆ i, p i ↔ ∀ (N : AddSubmonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.not_infinite_mul : ∀ {x y : ℝ*}, ¬x.Infinite → ¬y.Infinite → ¬(x * y).Infinite
-- Lean.Elab.Do.Basic
Lean.Elab.Do.elabDo : Lean.Elab.Term.TermElab
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.ae_norm_ofReal_f_le_bound : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {F : ℕ → α → β} {f : α → β} {bound : α → ℝ},
  (∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a) →
    (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) →
      ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
-- Lean.Meta.Tactic.Replace
/-- Clears the value of the local definition `fvarId`. Ensures that the resulting goal state
is still type correct. Throws an error if it is a local hypothesis without a value.

Preserves the order of the local context.
 -/
Lean.MVarId.clearValue : Lean.MVarId → Lean.FVarId → Lean.MetaM Lean.MVarId
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
/-- The property of objects that are cokernels of morphisms satisfying `W`.  -/
CategoryTheory.MorphismProperty.cokernels : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.MorphismProperty C → CategoryTheory.ObjectProperty C
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RccSlice.instToIterator : {α : Type u_1} →
  {β : α → Type v} →
    [inst : Ord α] →
      Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.RccSliceData α β)) Id (Std.DTreeMap.Internal.RxcIterator α β)
        ((a : α) × β a)
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_zpow_isUnit : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a : E) {n : ℤ}, IsUnit n → ‖a ^ n‖₊ = ‖a‖₊
-- Lean.Meta.AppBuilder
_private.Lean.Meta.AppBuilder.0.Lean.Meta.mkAppMArgs.loop : Lean.Expr → Array Lean.Expr → Lean.Expr → ℕ → ℕ → Array Lean.Expr → Array Lean.MVarId → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Complex.OpenMapping
Complex.isOpenQuotientMap_pow : ∀ (n : ℕ) [NeZero n], IsOpenQuotientMap fun x => x ^ n
-- Qq.MatchImpl
Qq.Impl.PatVarDecl.mk : Option Q(Lean.Expr) → Lean.FVarId → Lean.Name → Qq.Impl.PatVarDecl
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
/-- An admissible linear change of variables of Weierstrass curves defined over a ring `R` given by
a tuple `(u, r, s, t)` for some `u` in `Rˣ` and some `r, s, t` in `R`. As a matrix, it is
$$\begin{pmatrix} u^2 & 0 & r \cr u^2s & u^3 & t \cr 0 & 0 & 1 \end{pmatrix}.$$
In other words, this is the change of variables `(X, Y) ↦ (u²X + r, u³Y + u²sX + t)`.
When `R` is a field, any two isomorphic Weierstrass equations are related by this.  -/
WeierstrassCurve.VariableChange : (R : Type u) → [CommRing R] → Type u
-- Mathlib.Topology.Algebra.Module.Complement
/-- A variant of `Submodule.IsTopCompl.isClosed`. This has the very mild advantage over
`h.symm.isClosed` that it doesn't assume `ContinuousSub M`.  -/
Submodule.IsTopCompl.isClosed' : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [T1Space ↥p], Submodule.IsTopCompl p q → IsClosed ↑q
-- Mathlib.Algebra.Torsor.Basic
Function.Surjective.addTorsor.eq_1 : ∀ {G : Type u_1} {P : Type u_2} {Q : Type u_3} [inst : AddGroup G] [inst_1 : AddTorsor G P] [inst_2 : VAdd G Q]
  [inst_3 : VSub G Q] (f : P → Q) (hf : Function.Surjective f) (smul : ∀ (c : G) (x : P), f (c +ᵥ x) = c +ᵥ f x)
  (sdiv : ∀ (x y : P), x -ᵥ y = f x -ᵥ f y),
  Function.Surjective.addTorsor f hf smul sdiv =
    { toAddAction := Function.Surjective.addAction f hf smul, toVSub := inst_3, nonempty := ⋯, vsub_vadd' := ⋯,
      vadd_vsub' := ⋯ }
-- Mathlib.Data.Fintype.Sum
Fintype.card_subtype_eq_or_eq_of_ne : ∀ {α : Type u_3} [inst : Fintype α] [inst_1 : DecidableEq α] {a b : α}, a ≠ b → Fintype.card { c // c = a ∨ c = b } = 2
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.natCast.inj : ∀ {k k_1 : ℕ}, Lean.Grind.CommRing.Expr.natCast k = Lean.Grind.CommRing.Expr.natCast k_1 → k = k_1
-- Mathlib.RingTheory.Norm.Basic
Algebra.norm_eq_of_algEquiv : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S]
  [inst_3 : Ring T] [inst_4 : Algebra R T] (e : S ≃ₐ[R] T) (x : S), (Algebra.norm R) (e x) = (Algebra.norm R) x
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.IsMarkovKernel.is_probability_measure' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsMarkovKernel κ] (a : α), MeasureTheory.IsProbabilityMeasure (κ a)
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Down.erase_mem_compression_of_mem_compression : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α} {a : α},
  s ∈ Down.compression a 𝒜 → s.erase a ∈ Down.compression a 𝒜
-- Std.Data.HashSet.IteratorLemmas
Std.HashSet.toListRev_iter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m.iter.toListRev = m.toList.reverse
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_left_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Finset α), s ∪ (t ∪ u) = t ∪ (s ∪ u)
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.inclusion_obj : ∀ {X : TopCat} (x : ↑X) (U : TopologicalSpace.Opens ↑X) (p : x ∈ U),
  (TopologicalSpace.OpenNhds.inclusion x).obj ⟨U, p⟩ = U
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph1_le_mk_iff : ∀ {α : Type u_1}, Cardinal.aleph 1 ≤ Cardinal.mk α ↔ Uncountable α
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
/-- You will rarely use this typeclass directly: it is implied by the combination
`[EnoughInjectives C]` and `[Abelian C]`.  -/
CategoryTheory.HasInjectiveResolutions : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroObject C] → [CategoryTheory.Limits.HasZeroMorphisms C] → Prop
-- Mathlib.FieldTheory.Perfect
iterateFrobeniusEquiv_symm : ∀ (R : Type u_1) (p n : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p],
  (iterateFrobeniusEquiv R p n).symm = (frobeniusEquiv R p).symm ^ n
-- Mathlib.RepresentationTheory.Rep.Basic
/-- `counitIso` of the equivalence between `Action` and `Rep`.  -/
Rep.ActionToRep_RepToAction : (k : Type u) →
  (G : Type v) →
    [inst : Ring k] →
      [inst_1 : Monoid G] → (X : Rep.{w, u, v} k G) → (Rep.ActionToRep k G).obj ((Rep.RepToAction k G).obj X) ≅ X
-- Mathlib.Order.Disjoint
Codisjoint.eq_1 : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] (a b : α),
  Codisjoint a b = ∀ ⦃x : α⦄, a ≤ x → b ≤ x → ⊤ ≤ x
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.instIsClosedImmersionInclusion : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} (h : I ≤ J),
  AlgebraicGeometry.IsClosedImmersion (AlgebraicGeometry.Scheme.IdealSheafData.inclusion h)
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
_private.Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension.0.ExistsContDiffBumpBase.termμ : Lean.ParserDescr
-- Mathlib.LinearAlgebra.AffineSpace.MidpointZero
homothety_one_half : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : CharZero k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] (a b : P), (AffineMap.homothety a (1 / 2)) b = midpoint k a b
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
CategoryTheory.Limits.sigmaObjIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  {α : Type w} [inst_2 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) C]
  (f : α → CategoryTheory.Functor D C) (d : D),
  CategoryTheory.Limits.sigmaObjIso f d =
    CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation (CategoryTheory.Discrete.functor f) d ≪≫
      CategoryTheory.Limits.HasColimit.isoOfNatIso
        (CategoryTheory.Discrete.compNatIsoDiscrete f ((CategoryTheory.evaluation D C).obj d))
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.mul_def : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)] [inst_2 : (i : ι) → Module R (A i)]
  [inst_3 : ∀ (i : ι), SMulCommClass R (A i) (A i)] [inst_4 : ∀ (i : ι), IsScalarTower R (A i) (A i)]
  (x y : PiTensorProduct R fun i => A i), x * y = (PiTensorProduct.mul x) y
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapIso_inverse_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T')),
  ((CategoryTheory.CostructuredArrow.mapIso i).inverse.obj X).right = X.right
-- Mathlib.Order.Heyting.Basic
GeneralizedCoheytingAlgebra.toLattice : {α : Type u_4} → [self : GeneralizedCoheytingAlgebra α] → Lattice α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- Naturality of the `prodComparison` morphism in both arguments.  -/
CategoryTheory.CartesianMonoidalCategory.prodComparison_natural : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {A B A' B' : C} (f : A ⟶ A') (g : B ⟶ B'),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
      (CategoryTheory.CartesianMonoidalCategory.prodComparison F A' B') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (F.map g))
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
/-- Tries to evaluate the polynomial `p` using the partial model/assignment built so far.
The result is `none` if the polynomial contains variables that have not been assigned.
 -/
Lean.Grind.Linarith.Poly.eval? : Lean.Grind.Linarith.Poly → Lean.Meta.Grind.Arith.Linear.LinearM (Option ℚ)
-- Std.Time.Format.Modifier
/-- `x`: Zone offset without 'Z' (e.g., +0000, -08, -0830, -08:30).
 -/
Std.Time.Modifier.x : Std.Time.OffsetX → Std.Time.Modifier
-- Mathlib.MeasureTheory.Integral.Average
/-- Average value of an `ℝ≥0∞`-valued function `f` w.r.t. a measure `μ` on a set `s`.

It is equal to `(μ s)⁻¹ * ∫⁻ x, f x ∂μ`, so it takes value zero if `s` has infinite measure. If `s`
has measure `1`, then the average of any function is equal to its integral.

For the average w.r.t. the volume, one can omit `∂volume`.  -/
MeasureTheory.«term⨍⁻_In_,_∂_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.evaluation_preservesLimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [CategoryTheory.Limits.HasLimitsOfShape J C] (k : K),
  CategoryTheory.Limits.PreservesLimitsOfShape J ((CategoryTheory.evaluation K C).obj k)
-- Mathlib.Order.Filter.Bases.Basic
Filter.disjoint_principal_right : ∀ {α : Type u_1} {f : Filter α} {s : Set α}, Disjoint f (Filter.principal s) ↔ sᶜ ∈ f
-- Mathlib.RingTheory.AdicCompletion.Basic
IsPrecomplete.mk : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  (∀ (f : ℕ → M), (∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]) → ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]) →
    IsPrecomplete I M
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.abs_sin_half : ∀ (x : ℝ), |Real.sin (x / 2)| = √((1 - Real.cos x) / 2)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.toSubmodule_inj : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {s t : NonUnitalSubalgebra R A}, s.toSubmodule = t.toSubmodule ↔ s = t
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.h_eq_diagonal : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : DecidableEq ι] (i : ↥b.support),
  RootPairing.GeckConstruction.h i = Matrix.diagonal (Sum.elim 0 fun x => ↑(P.pairingIn ℤ x ↑i))
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.instInhabitedMonadHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {T : CategoryTheory.Monad C} → Inhabited (CategoryTheory.MonadHom T T)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.map_star_eq_ofNat : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Semiring α] [inst_2 : StarRing α] {M : Matrix n n α}
  {d : ℕ} [inst_3 : d.AtLeastTwo], M.map star = OfNat.ofNat d ↔ M = OfNat.ofNat d
-- Init.Grind.Ring.Envelope
Lean.Grind.CommRing.OfCommSemiring.toQUnexpander : Lean.PrettyPrinter.Unexpander
-- Init.Data.Array.MapIdx
Array.mapIdx_singleton : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {a : α}, Array.mapIdx f #[a] = #[f 0 a]
-- Mathlib.Order.Category.Semilat
/-- Constructs an isomorphism of lattices from an order isomorphism between them.  -/
SemilatInfCat.Iso.mk : {α β : SemilatInfCat} → α.X ≃o β.X → (α ≅ β)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.CosimplicialObject C} (f g : X ⟶ Y),
  (∀ (n : SimplexCategory), f.app n = g.app n) → f = g