mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.gluing_t' : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).t' i j k = AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- Conjugation by a unit preserves the spectrum, inverse on right.  -/
spectrum.units_conjugate : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A} {u : Aˣ},
  spectrum R (↑u * a * ↑u⁻¹) = spectrum R a
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.adjoinRootAlgEquiv_apply_root : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f), h.adjoinRootAlgEquiv (AdjoinRoot.root f) = h.root
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_apply_self : ∀ {α : Type u_2} (f : Equiv.Perm α) [inst : DecidableRel f.SameCycle] (x : α), (f.cycleOf x) x = f x
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.iCycles_δ_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.iCycles_δ._auto_1) {Z : C}
  (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.iCycles f g n₀) (CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Tactic.LinearCombination.Lemmas
/-- Given an (in)equality, look up the lemma to left-multiply it by a constant.  If relevant, also
take into account the degree of positivity which can be proved of the constant: strict or
non-strict.  -/
Mathlib.Ineq.mulRelConstData : Mathlib.Ineq.WithStrictness → Lean.Name
-- Mathlib.GroupTheory.OrderOfElement
/-- If `gcd(|G|,n)=1` then the `n`th power map is a bijection  -/
powCoprime : {n : ℕ} → {G : Type u_6} → [Group G] → (Nat.card G).Coprime n → G ≃ G
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.quot_neg : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (x : CommRingCat.Colimits.Prequotient F),
  Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) x.neg =
    -have this := Quot.mk (⇑(CommRingCat.Colimits.colimitSetoid F)) x;
      this
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic.0.ProbabilityTheory.HasIndepIncrements.indepFun_sub_sub.match_1_1.congr_eq_3 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (x : ℕ) → motive x) (x_1 : ℕ),
  x = x_1 →
    (x_1 = 0 → False) →
      (x_1 = 1 → False) →
        (match x with
          | 0 => h_1 ()
          | 1 => h_2 ()
          | x => h_3 x) ≍
          h_3 x_1
-- Mathlib.Algebra.Group.Basic
leftInverse_neg_add_add_right : ∀ {G : Type u_3} [inst : AddGroup G] (c : G), Function.LeftInverse (fun x => -c + x) fun x => c + x
-- Mathlib.Data.Set.Card
Function.Injective.encard_range : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ENat.card α ≤ (Set.range f).encard
-- Mathlib.Algebra.Group.Nat.Units
/-- Alias of `isAddUnit_iff_eq_zero` for discoverability.  -/
Nat.isAddUnit_iff : ∀ {n : ℕ}, IsAddUnit n ↔ n = 0
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mul_subset_mul_right : ∀ {α : Type u_2} [inst : Mul α] {s₁ s₂ t : Set α}, s₁ ⊆ s₂ → s₁ * t ⊆ s₂ * t
-- Mathlib.Algebra.Homology.Localization
/-- The homology functor on `HomologicalComplexUpToQuasiIso C c` is induced by
the homology functor on `HomologicalComplex C c`.  -/
HomologicalComplexUpToQuasiIso.homologyFunctorFactors : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {ι : Type u_2} →
      (c : ComplexShape ι) →
        [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_2 : CategoryTheory.CategoryWithHomology C] →
            [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization] →
              (i : ι) →
                HomologicalComplexUpToQuasiIso.Q.comp (HomologicalComplexUpToQuasiIso.homologyFunctor C c i) ≅
                  HomologicalComplex.homologyFunctor C c i
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.constAddMonoidHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddZeroClass Y] (y : Y),
  LocallyConstant.constAddMonoidHom y = LocallyConstant.const X y
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.condExp_ae_eq_integral_condDistrib : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} [inst_5 : NormedSpace ℝ F]
  [CompleteSpace F],
  Measurable X →
    AEMeasurable Y μ →
      ∀ {f : Ω → F},
        MeasureTheory.StronglyMeasurable f →
          MeasureTheory.Integrable (fun a => f (Y a)) μ →
            μ[fun a => f (Y a) | MeasurableSpace.comap X mβ] =ᵐ[μ] fun a =>
              ∫ (y : Ω), f y ∂(ProbabilityTheory.condDistrib Y X μ) (X a)
-- Mathlib.Topology.Algebra.GroupWithZero
map_mul_left_nhds₀ : ∀ {G₀ : Type u_3} [inst : TopologicalSpace G₀] [inst_1 : GroupWithZero G₀] [SeparatelyContinuousMul G₀] {a : G₀},
  a ≠ 0 → ∀ (b : G₀), Filter.map (fun x => a * x) (nhds b) = nhds (a * b)
-- Mathlib.Data.Complex.Basic
/-- `mulAux` is an auxiliary definition for defining multiplication and scalar multiplication on `ℂ`
in such a way that `real_smul {x : ℝ} {z : ℂ} : x • z = x * z` holds definitionally.
This makes sure that `Module.restrictScalars ℝ ℂ ℂ = Complex.instModule` definitionally.
 -/
Complex.mulAux : {R : Type u_1} → [SMul R ℝ] → R → ℝ → ℂ → ℂ
-- Mathlib.RingTheory.Extension.Basic
/-- The kernel of an extension.  -/
Algebra.Extension.ker : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : Algebra.Extension R S) → Ideal P.Ring
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.wasCancelled : Lean.Server.RequestCancellationToken → BaseIO Bool
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.equivIccQuot.congr_simp : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜] (p a : 𝕜)
  [hp : Fact (0 < p)] [inst_3 : Archimedean 𝕜], AddCircle.equivIccQuot p a = AddCircle.equivIccQuot p a
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
CuspForm.toModularFormₗ_eq_coe : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [inst : Γ.HasDetOne] (f : CuspForm Γ k),
  CuspForm.toModularFormₗ f = ModularFormClass.modularForm f
-- Init.Data.String.Lemmas.Iterate
String.Slice.Model.revPositionsFrom_startPos : ∀ {s : String.Slice}, String.Slice.Model.revPositionsFrom s.startPos = []
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.inf_idem : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (a : CauSeq α abs),
  a ⊓ a = a
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.good : {α : Type u_1} → (α → Prop) → Option α → Prop
-- Init.Data.Nat.Lemmas
/-- Shift left on successor with multiple moved to outside.  -/
Nat.shiftLeft_succ : ∀ (m n : ℕ), m <<< (n + 1) = 2 * m <<< n
-- Batteries.Recycling.RBTree.Basic
/-- A node consists of a value `v`, a subtree `l` of smaller items,
and a subtree `r` of larger items. The color `c` is either `red` or `black`
and participates in the red-black balance invariant (see `Balanced`).  -/
RBTree.RBNode.node : {α : Type u} → RBTree.RBColor → RBTree.RBNode α → α → RBTree.RBNode α → RBTree.RBNode α
-- Mathlib.CategoryTheory.GuitartExact.Opposite
CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence_unitIso : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  {X₃ : C₃ᵒᵖ} {X₂ : C₂ᵒᵖ} (g : B.op.obj X₃ ⟶ R.op.obj X₂),
  (w.structuredArrowRightwardsOpEquivalence g).unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (w.op.StructuredArrowRightwards g)ᵒᵖ)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.constantCoeff_map : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (φ : MvPolynomial σ R), MvPolynomial.constantCoeff ((MvPolynomial.map f) φ) = f (MvPolynomial.constantCoeff φ)
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
/-- Sum of iterated derivatives of a polynomial, as a linear map

This definition does not allow different weights for the derivatives. It is likely that it could be
extended to allow them, but this was not needed for the initial use case (the integration by parts
of the integral $I_i$ in the
[Lindemann-Weierstrass](https://en.wikipedia.org/wiki/Lindemann%E2%80%93Weierstrass_theorem)
theorem).
 -/
Polynomial.sumIDeriv : {R : Type u_1} → [inst : Semiring R] → Polynomial R →ₗ[R] Polynomial R
-- Lean.Parser.Term
Lean.Parser.Term.motive.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_eq_sum_sq' : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] (s t : Finset α),
  s.addEnergy t = ∑ a ∈ s + t, {xy ∈ s ×ˢ t | xy.1 + xy.2 = a}.card ^ 2
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.nsmul_atBot : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] {l : Filter α}
  {f : α → M}, Filter.Tendsto f l Filter.atBot → ∀ {n : ℕ}, 0 < n → Filter.Tendsto (fun x => n • f x) l Filter.atBot
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_inv_id_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cyclesIsoH_hom_inv_id._auto_1) {Z : C}
  (h : X.cycles (CategoryTheory.CategoryStruct.id i₀) f n₀ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.cyclesIsoH f n₀ n₁ hn₁).hom
      (CategoryTheory.CategoryStruct.comp (X.toCycles (CategoryTheory.CategoryStruct.id i₀) f f ⋯ n₀) h) =
    h
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivAt.comp_hasDerivWithinAt_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' y : 𝕜'},
  HasDerivAt h₂ h₂' y → HasDerivWithinAt h h' s x → y = h x → HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getGE?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getGE? k = t₂.getGE? k
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰)
  [inst_5 :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.Limits.PreservesColimitsOfShape J
        (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))]
  [inst_6 : Quiver.IsThin 𝒰.I₀] [inst_7 : Small.{u, u_2} 𝒰.I₀] [inst_8 : AlgebraicGeometry.IsZariskiLocalAtTarget P]
  (a : J) (i : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.obj a).hom (𝒰.f i))
      (d.gluedCocone.ι.app a).left =
    CategoryTheory.CategoryStruct.comp ((d.cocone i).ι.app a).left
      (CategoryTheory.Limits.colimit.ι d.relativeGluingData.functor i)
-- Mathlib.Data.Rat.Lemmas
Rat.sub_den_dvd_lcm : ∀ (q₁ q₂ : ℚ), (q₁ - q₂).den ∣ q₁.den.lcm q₂.den
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.instAddSemigroup.eq_1 : ∀ {α : Type u} [inst : Add α],
  AddMagma.FreeAddSemigroup.instAddSemigroup =
    { add := fun x y => Quot.liftOn₂ x y (fun x y => Quot.mk (AddMagma.AssocRel α) (x + y)) ⋯ ⋯, add_assoc := ⋯ }
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.toThinSkeleton_faithful : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [Quiver.IsThin C],
  (CategoryTheory.toThinSkeleton C).Faithful
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
IsPurelyInseparable.HasExponent.has_exponent : ∀ {K : Type u_2} {L : Type u_3} {inst : CommRing K} {inst_1 : Ring L} {inst_2 : Algebra K L}
  [self : IsPurelyInseparable.HasExponent K L], ∃ e, ∀ (a : L), a ^ ringExpChar K ^ e ∈ (algebraMap K L).range
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.lift_def : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] {C : Sort u_9}
  (ih : (i : ι) → F i → C) (compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x))
  (x : (i : ι) × F i), DirectLimit.lift f ih compat ⟦x⟧ = ih x.fst x.snd
-- Init.Data.Array.Count
Array.count_singleton_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α}, Array.count a #[a] = 1
-- Mathlib.RingTheory.Localization.BaseChange
Localization.tensorLeftAlgEquiv.eq_1 : ∀ {R : Type u_10} [inst : CommRing R] (M : Submonoid R) (S : Type u_12) [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Localization.tensorLeftAlgEquiv M S =
    (Localization.algEquiv (Algebra.algebraMapSubmonoid S M) (TensorProduct R S (Localization M))).symm
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Option.isSome.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((val : α) → motive (some val)) → (Unit → motive none) → motive x
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.vadd.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {α : Type u_3} [inst_1 : VAdd α Y],
  LocallyConstant.vadd = { vadd := fun n f => LocallyConstant.map (fun x => n +ᵥ x) f }
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.congr_preservesLimitsOfShape : ∀ (J : Type u_1) (C : Type u_3) {K : Type u_5} {K' : Type u_6} [inst : CategoryTheory.Category.{v_1, u_5} K]
  [inst_1 : CategoryTheory.Category.{v_2, u_6} K'] [inst_2 : CategoryTheory.Category.{v_3, u_1} J]
  [inst_3 : CategoryTheory.Category.{v_5, u_3} C] (e : K ≌ K'),
  CategoryTheory.ObjectProperty.preservesLimitsOfShape K = CategoryTheory.ObjectProperty.preservesLimitsOfShape K'
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_inv : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] (F : CategoryTheory.Functor C H)
  [inst_3 : L.HasPointwiseLeftKanExtension F] [inst_4 : L.HasLeftKanExtension F] (X : D)
  (f : CategoryTheory.CostructuredArrow L X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L X).comp F) f)
      (L.leftKanExtensionObjIsoColimit F X).inv =
    CategoryTheory.CategoryStruct.comp ((L.leftKanExtensionUnit F).app f.left) ((L.leftKanExtension F).map f.hom)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε], 0 < q → MeasureTheory.eLpNorm' 0 q μ = 0
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_subsingleton`.

---

The diameter of a subsingleton vanishes.  -/
Set.Subsingleton.ediam_eq : ∀ {X : Type u_2} {s : Set X} [inst : PseudoEMetricSpace X], s.Subsingleton → Metric.ediam s = 0
-- Init.Data.SInt.Lemmas
Int16.toInt64_toInt32 : ∀ (n : Int16), n.toInt32.toInt64 = n.toInt64
-- Mathlib.Data.PFun
PFun.dom_toSubtype : ∀ {α : Type u_1} {β : Type u_2} (p : β → Prop) (f : α → β), (PFun.toSubtype p f).Dom = {a | p (f a)}
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerRight_naturality_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.StrongTrans F G) {a b c : B} {a' : C} (f : a ⟶ b)
  (g : b ⟶ c) (h : G.obj c ⟶ a'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.comp f g)).hom h)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.comp f g)) h).hom
        (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.mapComp f g) h))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (η.app c)) h)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (η.app c)).hom
          h)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) (η.app c))
              h).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft (F.map f)
              (CategoryTheory.Bicategory.whiskerRight (η.naturality g).hom h))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (η.app b) (G.map g))
                  h).inv
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.whiskerRight
                  (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (G.map g)).inv h)
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.whiskerRight
                    (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom (G.map g)) h)
                  (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.Bicategory.whiskerRight
                      (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (G.map g)).hom h)
                    (CategoryTheory.Bicategory.associator (η.app a)
                        (CategoryTheory.CategoryStruct.comp (G.map f) (G.map g)) h).hom)))))))
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.cos_arg : ∀ {x : ℂ}, x ≠ 0 → Real.cos x.arg = x.re / ‖x‖
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mk_natCast : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NatCast R] (n : ℕ), SeparationQuotient.mk ↑n = ↑n
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_le_of_le_div : ∀ {a b c : ENNReal}, a ≤ b / c → a * c ≤ b
-- Mathlib.Data.Set.Disjoint
Disjoint.inter_left : ∀ {α : Type u_1} {s t : Set α} (u : Set α), Disjoint s t → Disjoint (s ∩ u) t
-- Mathlib.Order.CompleteLattice.Defs
le_iSup_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteSemilatticeSup α] {a : α} {s : ι → α},
  a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_lt_self : ∀ {n : ℕ}, 1 < n → n.sqrt < n
-- Mathlib.Topology.Instances.Matrix
Summable.matrix_transpose : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : AddCommMonoid R] [inst_1 : TopologicalSpace R]
  {L : SummationFilter X} {f : X → Matrix m n R}, Summable f L → Summable (fun x => (f x).transpose) L
-- Mathlib.Topology.Algebra.StarSubalgebra
/-- The topological closure of the star subalgebra generated by a single element.  -/
StarAlgebra.elemental : (R : Type u_1) →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : Semiring A] →
            [inst_4 : StarRing A] →
              [IsSemitopologicalSemiring A] →
                [ContinuousStar A] → [inst_7 : Algebra R A] → [inst_8 : StarModule R A] → A → StarSubalgebra R A
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
essentiallySmall_of_le : ∀ {Q : CategoryTheory.MorphismProperty CommRingCat},
  (Q ≤ RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => RingHom.FiniteType) →
    ∀ (R : CommRingCat), CategoryTheory.EssentiallySmall.{u, u, u + 1} (Q.Under ⊤ R)
-- Mathlib.Data.Matrix.Block
Matrix.toBlocks₂₁_diagonal : ∀ {l : Type u_1} {m : Type u_2} {α : Type u_12} [inst : DecidableEq l] [inst_1 : DecidableEq m] [inst_2 : Zero α]
  (v : l ⊕ m → α), (Matrix.diagonal v).toBlocks₂₁ = 0
-- Mathlib.Data.DFinsupp.BigOperators
/-- **Alias** of `DFinsupp.sum_finsetSum_index`. -/
DFinsupp.sum_finset_sum_index : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {γ : Type w} {α : Type x}
  [inst_1 : (i : ι) → AddCommMonoid (β i)] [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ]
  {s : Finset α} {g : α → Π₀ (i : ι), β i} {h : (i : ι) → β i → γ},
  (∀ (i : ι), h i 0 = 0) →
    (∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂) → ∑ i ∈ s, (g i).sum h = (∑ i ∈ s, g i).sum h
-- Mathlib.SetTheory.Cardinal.Ordinal
/-- **Alias** of `Ordinal.isPrincipal_add_ord`. -/
Ordinal.principal_add_ord : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) c.ord
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.mul_add : ∀ {R : Type u_1} [inst : CommSemiring R] {a b₁ b₂ c₁ c₂ d : R},
  a * b₁ = c₁ → a * b₂ = c₂ → c₁ + 0 + c₂ = d → a * (b₁ + b₂) = d
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_inf : ∀ {M : Type u_2} [inst : MulOneClass M] (S₁ S₂ : Submonoid M), (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
-- Mathlib.Algebra.Category.Grp.Basic
CategoryTheory.Iso.addGroupIsoToAddEquiv.eq_1 : ∀ {X Y : AddGrpCat} (i : X ≅ Y),
  i.addGroupIsoToAddEquiv = (AddGrpCat.Hom.hom i.hom).toAddEquiv (AddGrpCat.Hom.hom i.inv) ⋯ ⋯
-- Mathlib.GroupTheory.Index
AddMonoidHom.surjective_of_card_ker_le_div : ∀ {G : Type u_1} {M : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup M] [Finite G] [Finite M] (f : G →+ M),
  Nat.card ↥f.ker ≤ Nat.card G / Nat.card M → Function.Surjective ⇑f
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
zmodAddEquivOfGenerator_apply_intCast : ∀ {G : Type u_2} [inst : AddGroup G] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {n : ℕ}
  (hn : Nat.card G = n) (i : ℤ), (zmodAddEquivOfGenerator hg hn) ↑i = i • g
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.nonempty_support : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [HereditarilyLindelofSpace X], μ ≠ 0 → μ.support.Nonempty
-- Mathlib.Algebra.BigOperators.Finprod
/-- If `R` has no zero divisors, then multiplication commutes with `finsum_mem`. See `finsum_mem_mul'`
for a statement assuming finiteness of support.
 -/
finsum_mem_mul : ∀ {α : Type u_1} {R : Type u_7} [inst : NonUnitalNonAssocSemiring R] [NoZeroDivisors R] {s : Set α} (f : α → R) (r : R),
  (∑ᶠ (a : α) (_ : a ∈ s), f a) * r = ∑ᶠ (a : α) (_ : a ∈ s), f a * r