mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_erase_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  (m.erase k).size ≤ m.size
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.smul_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [inst : SMul β α] (r : β) (A : Matrix m n α) (i : m) (j : n),
  (r • A) i j = r • A i j
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instNonUnitalCommRing : {R : Type u_1} → [NonUnitalCommRing R] → NonUnitalCommRing Rᵐᵒᵖ
-- Mathlib.Analysis.InnerProductSpace.Dual
InnerProductSpace.toContinuousLinearMap_toDualMap : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  (InnerProductSpace.toDualMap 𝕜 E).toContinuousLinearMap = innerSL 𝕜
-- Lean.Elab.ConfigEval.Types
/-- Given a configuration, produces an array of configuration items representing it.
 -/
_private.Lean.Elab.ConfigEval.Types.0.Lean.Elab.ConfigEval.ReflectConfigItems.reflect : {α : Type} →
  Lean.Elab.ConfigEval.ReflectConfigItems✝ α → α → Lean.Elab.TermElabM (Lean.TSyntaxArray `Lean.Parser.Term.configItem)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.ext_getElem? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {m₁ m₂ : Std.ExtHashMap α β},
  (∀ (k : α), m₁[k]? = m₂[k]?) → m₁ = m₂
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.inf_imp_left : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ ψ : L.BoundedFormula α n), T.Imp (φ ⊓ ψ) φ
-- Lean.Meta.AppBuilder
Lean.Meta.mkExpectedTypeHintCore : Lean.Expr → Lean.Expr → Lean.Level → Lean.Expr
-- Lean.Parser.Basic
Lean.Parser.mkTokenAndFixPos : String.Pos.Raw → Option Lean.Parser.Token → Lean.Parser.ParserFn
-- Std.Http.Data.Request
Std.Http.Request.instEncodeV11Head : Std.Http.Internal.Encode Std.Http.Version.v11 Std.Http.Request.Head
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons counted by weight, non-strict inequality
version: if the total weight of a finite set of pigeons is less than or equal to `n • b`, and they
are sorted into `n > 0` pigeonholes, then for some pigeonhole, the total weight of the pigeons in
this pigeonhole is less than or equal to `b`.  -/
Finset.exists_sum_fiber_le_of_maps_to_of_sum_le_nsmul : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M}
  {b : M} [inst_1 : AddCommMonoid M] [inst_2 : LinearOrder M] [IsOrderedCancelAddMonoid M],
  (∀ a ∈ s, f a ∈ t) → t.Nonempty → ∑ x ∈ s, w x ≤ t.card • b → ∃ y ∈ t, ∑ x ∈ s with f x = y, w x ≤ b
-- Mathlib.Algebra.Torsor.Basic
/-- `x` is the only fixed point of `pointReflection x`. This lemma requires
`x + x = y + y ↔ x = y`. There is no typeclass to use here, so we add it as an explicit argument.  -/
Equiv.pointReflection_fixed_iff_of_injective_two_nsmul : ∀ {G : Type u_3} {P : Type u_4} [inst : AddGroup G] [T : AddTorsor G P] {x y : P},
  (Function.Injective fun x => 2 • x) → ((Equiv.pointReflection x) y = y ↔ y = x)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.entries : {α : Type u} →
  {β : Type v} →
    Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Lean.PersistentHashMap.Node α β
-- Lean.PrettyPrinter.Formatter
/-- Execute `x`, pass array of generated Format objects to `fn`, and push result.  -/
Lean.PrettyPrinter.Formatter.fold : (Array Std.Format → Std.Format) → Lean.PrettyPrinter.FormatterM Unit → Lean.PrettyPrinter.FormatterM Unit
-- Mathlib.Data.Seq.Computation
/-- `c₁ ~ c₂` asserts that `c₁` and `c₂` either both terminate with the same result,
or both loop forever.  -/
Computation.Equiv : {α : Type u} → Computation α → Computation α → Prop
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A sequentially compact space is countably compact.  -/
instSeqCompactSpaceCountablyCompactSpace : ∀ {X : Type u_4} [inst : TopologicalSpace X] [SeqCompactSpace X], CountablyCompactSpace X
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.not_nil_of_ne : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w}, v ≠ w → ¬p.Nil
-- Mathlib.CategoryTheory.Monad.Types
CategoryTheory.ofTypeMonad.congr_simp : ∀ (m : Type u → Type u) [inst : Monad m] [inst_1 : LawfulMonad m],
  CategoryTheory.ofTypeMonad m = CategoryTheory.ofTypeMonad m
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.empty_of_word_prod_eq_one : ∀ {ι : Type u_1} {G : Type u_4} [inst : Group G] {H : ι → Type u_5} [inst_1 : (i : ι) → Group (H i)]
  (f : (i : ι) → H i →* G),
  (3 ≤ Cardinal.mk ι ∨ ∃ i, 3 ≤ Cardinal.mk (H i)) →
    ∀ {α : Type u_6} [inst_2 : MulAction G α] (X : ι → Set α),
      (∀ (i : ι), (X i).Nonempty) →
        Pairwise (Function.onFun Disjoint X) →
          (Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i) →
            ∀ [Nontrivial ι] {w : Monoid.CoprodI.Word H},
              (Monoid.CoprodI.lift f) w.prod = 1 → w = Monoid.CoprodI.Word.empty
-- Mathlib.MeasureTheory.Function.ContinuousMapDense
/-- A variant of Urysohn's lemma, `ℒ^p` version, for an outer regular measure `μ`:
consider two sets `s ⊆ u` which are respectively closed and open with `μ s < ∞`, and a vector `c`.
Then one may find a continuous function `f` equal to `c` on `s` and to `0` outside of `u`,
bounded by `‖c‖` everywhere, and such that the `ℒ^p` norm of `f - s.indicator (fun y ↦ c)` is
arbitrarily small. Additionally, this function `f` belongs to `ℒ^p`.  -/
MeasureTheory.exists_continuous_eLpNorm_sub_le_of_closed : ∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [BorelSpace α] {E : Type u_2}
  [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace ℝ E] [μ.OuterRegular],
  p ≠ ⊤ →
    ∀ {s u : Set α},
      IsClosed s →
        IsOpen u →
          s ⊆ u →
            μ s ≠ ⊤ →
              ∀ (c : E) {ε : ENNReal},
                ε ≠ 0 →
                  ∃ f,
                    Continuous f ∧
                      MeasureTheory.eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧
                        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MeasureTheory.MemLp f p μ
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instLawfulOrderLT : ∀ {n : ℕ}, Std.LawfulOrderLT (BitVec n)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_norm_eq_card : ∀ {α : Type u_2} {β : Type u_3} [inst : Norm α] [inst_1 : Norm β] (f : WithLp 0 (α × β)),
  ‖f‖ = (if ‖f.fst‖ = 0 then 0 else 1) + if ‖f.snd‖ = 0 then 0 else 1
-- Lean.Environment
Lean.Kernel.Exception.thmTypeIsNotProp.sizeOf_spec : ∀ (env : Lean.Kernel.Environment) (name : Lean.Name) (type : Lean.Expr),
  sizeOf (Lean.Kernel.Exception.thmTypeIsNotProp env name type) = 1 + sizeOf env + sizeOf name + sizeOf type
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.CostructuredArrow.Hom.ext_iff : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} D] {P : CategoryTheory.MorphismProperty D}
  {Q : CategoryTheory.MorphismProperty C} [inst_2 : Q.IsMultiplicative] {F : CategoryTheory.Functor C D} {X : D}
  {A B : P.CostructuredArrow Q F X} {f g : A ⟶ B}, f = g ↔ f.left = g.left
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.finiteAtFilter_of_finite : ∀ {α : Type u_1} {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ]
  (f : Filter α), μ.FiniteAtFilter f
-- Mathlib.RingTheory.Localization.BaseChange
Localization.tensorRightAlgEquiv_apply_tmul_one : ∀ {R : Type u_10} [inst : CommRing R] (M : Submonoid R) (S : Type u_12) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (x : Localization M),
  (Localization.tensorRightAlgEquiv M S) (x ⊗ₜ[R] 1) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M))) x
-- Mathlib.Geometry.Euclidean.Projection
/-- The linear map corresponding to `orthogonalProjection`.  -/
EuclideanGeometry.orthogonalProjection_linear : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection],
  (↑(EuclideanGeometry.orthogonalProjection s)).linear = ↑s.direction.orthogonalProjectionOnto
-- Lean.Message
Lean.Message.toJson : Lean.Message → BaseIO Lean.Json
-- Mathlib.Topology.MetricSpace.Algebra
/-- Eta-expanded form of `TendstoLocallyUniformlyOn.smul₀` -/
TendstoLocallyUniformlyOn.fun_smul₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β] [IsBoundedSMul α β] {X : Type u_3} {ι : Type u_4} [inst_6 : TopologicalSpace X]
  {s : Set X} {F : ι → X → α} {G : ι → X → β} {f : X → α} {g : X → β} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    TendstoLocallyUniformlyOn G g l s →
      ContinuousOn f s →
        ContinuousOn g s → TendstoLocallyUniformlyOn (fun i i_1 => F i i_1 • G i i_1) (fun i => f i • g i) l s
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_maxKey?_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α}
  {f : β → β}, t.WF → (t.modify k f).maxKey?.isSome = !t.isEmpty
-- Mathlib.GroupTheory.OrderOfElement
Nat.Coprime.pow_left_bijective : ∀ {n : ℕ} {G : Type u_6} [inst : Group G], (Nat.card G).Coprime n → Function.Bijective fun x => x ^ n
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.genSpecs : Lean.Name → Lean.MetaM Unit
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instMul : {σ : Type u_1} → {R : Type u_2} → [Semiring R] → Mul (MvPowerSeries σ R)
-- Mathlib.Algebra.Order.Hom.Basic
/-- `GroupNormClass F α` states that `F` is a type of `β`-valued norms on the group `α`.

You should extend this class when you extend `GroupNorm`.  -/
GroupNormClass : (F : Type u_7) →
  (α : outParam (Type u_8)) →
    (β : outParam (Type u_9)) → [Group α] → [AddCommMonoid β] → [PartialOrder β] → [FunLike F α β] → Prop
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracket_const_smul_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} {V W : (x : M) → TangentSpace I x} {c : 𝕜}
  [inst_6 : IsManifold I 2 M] [CompleteSpace E],
  MDiffAt (T% V) x → VectorField.mlieBracket I (c • V) W x = c • VectorField.mlieBracket I V W x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.equation_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P : Fin 3 → R},
  P 2 = 0 → (W'.Equation P ↔ P 0 ^ 3 = 0)
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- The bilinear map `kahler` is invariant under pullback by a positively-oriented isometric
automorphism.  -/
Orientation.kahler_comp_linearIsometryEquiv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (φ : E ≃ₗᵢ[ℝ] E),
  0 < LinearMap.det ↑φ.toLinearEquiv → ∀ (x y : E), (o.kahler (φ x)) (φ y) = (o.kahler x) y
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.shape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j : ι), ¬c.Rel i j → HomologicalComplex.homotopyCofiber.d φ i j = 0
-- Mathlib.RingTheory.PowerSeries.GaussNorm
/-- **Alias** of `PowerSeries.HasGaussNorm.hasMvGaussNorm`. -/
PowerSeries.HasGaussNorm.HasMvGaussNorm : ∀ {R : Type u_1} [inst : Semiring R] (v : R → ℝ) (c : ℝ) (f : PowerSeries R),
  PowerSeries.HasGaussNorm v c f → MvPowerSeries.HasGaussNorm v (fun x => c) f
-- Mathlib.Algebra.Order.Nonneg.Ring
Nonneg.isStrictOrderedRing : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : IsStrictOrderedRing α],
  IsStrictOrderedRing { x // 0 ≤ x }
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ShowDocumentClientCapabilities.mk.inj : ∀ {support support_1 : Bool}, { support := support } = { support := support_1 } → support = support_1
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The product of weighted homogeneous polynomials of weighted degrees `m` and `n` is weighted
homogeneous of weighted degree `m + n`.  -/
MvPolynomial.IsWeightedHomogeneous.mul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
  {φ ψ : MvPolynomial σ R} {m n : M} {w : σ → M},
  MvPolynomial.IsWeightedHomogeneous w φ m →
    MvPolynomial.IsWeightedHomogeneous w ψ n → MvPolynomial.IsWeightedHomogeneous w (φ * ψ) (m + n)
-- Mathlib.Topology.Gluing
TopCat.GlueData.ι_mono : ∀ (D : TopCat.GlueData) (i : D.J), CategoryTheory.Mono (D.ι i)
-- Lean.Meta.CongrTheorems
Lean.Meta.CongrArgKind.eq.sizeOf_spec : sizeOf Lean.Meta.CongrArgKind.eq = 1
-- Mathlib.Algebra.Group.Prod
AddHom.coe_prod : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : M →ₙ+ N)
  (g : M →ₙ+ P), ⇑(f.prod g) = Function.prod ⇑f ⇑g
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.sum_Icc_mu'_left : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : PartialOrder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] (a b : α),
  ∑ x ∈ Finset.Icc a b, (IncidenceAlgebra.mu'✝ 𝕜) x b = if a = b then 1 else 0
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.isoOfLE_hom_ι_assoc : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (hUV : U ≤ V) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Opens.isoOfLE hUV).hom
      (CategoryTheory.CategoryStruct.comp U.ι h) =
    CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map V.ι.base).obj U).ι
      (CategoryTheory.CategoryStruct.comp V.ι h)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_f_map_epi : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  Function.Injective ⇑f → ∀ [CategoryTheory.Epi φ] (i : ℕ), CategoryTheory.Epi ((groupCohomology.cochainsMap f φ).f i)
-- Mathlib.NumberTheory.LucasLehmer
/-- **Alias** of `LucasLehmer.norm_num_ext.sModNatAux_eq`. -/
LucasLehmer.norm_num_ext.sModNat_aux_eq : ∀ (q k : ℕ), LucasLehmer.norm_num_ext.sModNatAux (4 % q) q k = LucasLehmer.norm_num_ext.sModNat q k
-- Mathlib.Topology.MetricSpace.Algebra
/-- The Lipschitz constant of a monoid `β` satisfying `LipschitzMul`  -/
LipschitzMul.C : (β : Type u_2) → [inst : PseudoMetricSpace β] → [inst_1 : Monoid β] → [_i : LipschitzMul β] → NNReal
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.mk.sizeOf_spec : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] [inst_1 : SizeOf B] (obj : B),
  sizeOf { obj := obj } = 1 + sizeOf obj
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Multiset.toFinset_prod_dvd_prod : ∀ {M : Type u_3} [inst : DecidableEq M] [inst_1 : CommMonoid M] (S : Multiset M), S.toFinset.prod id ∣ S.prod
-- Mathlib.AlgebraicTopology.ModelCategory.Opposite
HomotopicalAlgebra.instIsStableUnderRetractsOppositeFibrationsOfCofibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  [(HomotopicalAlgebra.cofibrations C).IsStableUnderRetracts], (HomotopicalAlgebra.fibrations Cᵒᵖ).IsStableUnderRetracts
-- Mathlib.Tactic.Widget.StringDiagram
/-- The kind of the context.  -/
Mathlib.Tactic.Widget.StringDiagram.Kind : Type
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
/-- The complement projection `Q q` to `P q` is homotopic to zero.  -/
AlgebraicTopology.DoldKan.homotopyQToZero : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (X : CategoryTheory.SimplicialObject C) → (q : ℕ) → Homotopy (AlgebraicTopology.DoldKan.Q q) 0
-- Lean.Exception
Lean.Exception.internal.sizeOf_spec : ∀ (id : Lean.InternalExceptionId) (extra : optParam Lean.KVMap { }),
  sizeOf (Lean.Exception.internal id extra) = 1 + sizeOf id + sizeOf extra
-- Std.Time.Time.Unit.Nanosecond
/-- `Span` represents a bounded value for nanoseconds, ranging between -999999999 and 999999999.
This can be used for operations that involve differences or adjustments within this range.
 -/
Std.Time.Nanosecond.Span : Type
-- Init.Data.Fin.Basic
Fin.val_inj : ∀ {n : ℕ} {a b : Fin n}, ↑a = ↑b ↔ a = b
-- Mathlib.GroupTheory.NoncommCoprod
MonoidHom.noncommCoprod_injective : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Group M] [inst_1 : Group N] [inst_2 : Group P] (f : M →* P)
  (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)),
  Function.Injective ⇑(f.noncommCoprod g comm) ↔
    Function.Injective ⇑f ∧ Function.Injective ⇑g ∧ Disjoint f.range g.range
-- Mathlib.Topology.Sets.Compacts
/-- The product of two `TopologicalSpace.Compacts`, as a `TopologicalSpace.Compacts` in the product
space.  -/
TopologicalSpace.Compacts.instSProdProd : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        SProd (TopologicalSpace.Compacts α) (TopologicalSpace.Compacts β) (TopologicalSpace.Compacts (α × β))
-- Std.Time.DateTime.PlainDateTime
/-- Determines the quarter of the year for the given `PlainDateTime`.
 -/
Std.Time.PlainDateTime.quarter : Std.Time.PlainDateTime → Std.Time.Internal.Bounded.LE 1 4
-- Std.Time.Date.Unit.Month
Std.Time.Month.instInhabitedQuarter : Inhabited Std.Time.Month.Quarter
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- If `i + 1 > j`, `mkOfSucc i ≫ δ j` is the morphism `⦋1⦌ ⟶ ⦋n⦌` that
sends `0` and `1` to `i + 1` and `i + 2`, respectively.  -/
SimplexCategory.mkOfSucc_δ_gt : ∀ {n : ℕ} {i : Fin n} {j : Fin (n + 2)},
  j < i.succ.castSucc →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.mkOfSucc i) (SimplexCategory.δ j) =
      SimplexCategory.mkOfSucc i.succ
-- Std.Sync.CancellationToken
Std.CancellationToken.Consumer : Type
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
AddSubgroup.range_zmultiplesHom : ∀ {A : Type u_2} [inst : AddGroup A] (a : A), ((zmultiplesHom A) a).range = AddSubgroup.zmultiples a
-- Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom
CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {K L : CochainComplex C ℤ}
  {n : ℤ}
  [inst_2 :
    CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L]
  [inst_3 : HasDerivedCategory C] (x : CochainComplex.HomComplex.Cocycle K L n),
  (CategoryTheory.Localization.SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
        DerivedCategory.Q)
      (CochainComplex.HomComplex.CohomologyClass.mk x).toSmallShiftedHom =
    CategoryTheory.ShiftedHom.map (CochainComplex.HomComplex.Cocycle.equivHomShift.symm x) DerivedCategory.Q
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RciSlice : (α : Type u_1) → [Ord α] → Type u_1
-- Mathlib.Topology.Algebra.Valued.NormedValued
/-- The nontrivially normed field structure determined by a rank one valuation.
 -/
Valued.toNontriviallyNormedField : (L : Type u_1) →
  [inst : Field L] →
    (Γ₀ : Type u_2) →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
        [val : Valued L Γ₀] → [hv : Valued.v.RankOne] → NontriviallyNormedField L
-- Init.Data.Option.Attach
Option.filter_attach : ∀ {α : Type u_1} {o : Option α} {p : { x // o = some x } → Bool},
  Option.filter p o.attach = o.pbind fun a h => if p ⟨a, h⟩ = true then some ⟨a, h⟩ else none
-- Mathlib.Algebra.Star.Unitary
/-- Unitary conjugation preserves the spectrum, star on left.  -/
Unitary.spectrum_star_left_conjugate : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] [inst_3 : StarMul A]
  {a : A} {U : ↥(unitary A)}, spectrum R (star ↑U * a * ↑U) = spectrum R a
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_bijective : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀),
  Function.Bijective (WithVal.toVal v)
-- Mathlib.Combinatorics.SimpleGraph.Cayley
/-- See `addCayley_adj` for the more convenient form in an `AddGroup`.  -/
SimpleGraph.addCayley_adj' : ∀ {M : Type u_1} (s : Set M) [inst : Add M] (u v : M),
  (SimpleGraph.addCayley s).Adj u v ↔ u ≠ v ∧ ∃ g ∈ s, u + g = v ∨ u = v + g
-- Mathlib.GroupTheory.Generators
Group.Generators.map_val : ∀ {G : Type u_1} {H : Type u_2} {ι : Type u_3} [inst : Group G] [inst_1 : Group H] (P : Group.Generators G ι)
  (f : G →* H) (hf : Function.Surjective ⇑f), (P.map f hf).val = ⇑f ∘ P.val
-- Mathlib.CategoryTheory.Monoidal.Rigid.Braided
/-- If `X` has a left dual in a braided category, then it has a right dual.  -/
CategoryTheory.BraidedCategory.hasRightDualOfHasLeftDual : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → {X : C} → [CategoryTheory.HasLeftDual X] → CategoryTheory.HasRightDual X
-- Mathlib.MeasureTheory.OuterMeasure.Defs
MeasureTheory.OuterMeasureClass.mk : ∀ {F : Type u_2} {α : outParam (Type u_3)} [inst : FunLike F (Set α) ENNReal],
  (∀ (f : F), f ∅ = 0) →
    (∀ (f : F) {s t : Set α}, s ⊆ t → f s ≤ f t) →
      (∀ (f : F) (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → f (⋃ i, s i) ≤ ∑' (i : ℕ), f (s i)) →
        MeasureTheory.OuterMeasureClass F α
-- Init.Data.List.Nat.Modify
List.eraseIdx_modify_of_lt : ∀ {α : Type u_1} (f : α → α) (i j : ℕ) (l : List α), j < i → (l.modify i f).eraseIdx j = (l.eraseIdx j).modify (i - 1) f
-- Mathlib.Algebra.Order.Module.Defs
lt_smul_of_one_lt_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Monoid α] [inst_1 : Zero β] [inst_2 : MulAction α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosStrictMono α β], 0 < b → 1 < a → b < a • b
-- Aesop.Forward.SlotIndex
Aesop.SlotIndex.toNat : Aesop.SlotIndex → ℕ
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.mem_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  {s : TopologicalSpace.Clopens α} {t : TopologicalSpace.Clopens β} {x : α × β}, x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t
-- Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous
properlyDiscontinuousSL2ZRange : ProperlyDiscontinuousSMul (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range) UpperHalfPlane
-- Std.Internal.Do.Order.Instances
Std.Internal.Do.CompleteLattice.instReflRel_std : ∀ {l : Sort u_1} [inst : Lean.Order.CompleteLattice l], Std.Refl fun x1 x2 => Lean.Order.PartialOrder.rel x1 x2
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.Hom.comm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} (self : D₁.Hom D₂) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄
  (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
  (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q) {Z : ↑(F.obj { as := Opposite.op Y })}
  (h : (F.map f₂.op.toLoc).toFunctor.obj (D₂.obj i₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (self.hom i₁))
      (CategoryTheory.CategoryStruct.comp (D₂.hom q f₁ f₂ ⋯ ⋯) h) =
    CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯)
      (CategoryTheory.CategoryStruct.comp ((F.map f₂.op.toLoc).toFunctor.map (self.hom i₂)) h)