mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.neg_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.neg P = -P 1 • ![0, 1, 0]
-- Mathlib.Algebra.Group.Pi.Basic
Pi.cancelCommMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → CancelCommMonoid (f i)] → CancelCommMonoid ((i : I) → f i)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientBot_symm_apply : ∀ {G : Type u} [inst : Group G] (a : G), QuotientGroup.quotientBot.symm a = ↑a
-- Init.Internal.Order.Basic
Lean.Order.sup_le : ∀ {α : Sort u} [inst : Lean.Order.CompleteLattice α] {x : α} (c : α → Prop),
  (∀ (y : α), c y → Lean.Order.PartialOrder.rel y x) → Lean.Order.PartialOrder.rel (Lean.Order.CompleteLattice.sup c) x
-- Init.Data.SInt.Bitwise
ISize.toInt16_or : ∀ (a b : ISize), (a ||| b).toInt16 = a.toInt16 ||| b.toInt16
-- Mathlib.Data.QPF.Multivariate.Constructions.Quot
/-- `map` of the `Quot1` functor  -/
MvQPF.Quot1.map : {n : ℕ} →
  {F : TypeVec.{u} n → Type u} →
    (R : ⦃α : TypeVec.{u} n⦄ → F α → F α → Prop) →
      [inst : MvFunctor F] →
        (∀ ⦃α β : TypeVec.{u} n⦄ (a b : F α) (f : α.Arrow β), R a b → R (MvFunctor.map f a) (MvFunctor.map f b)) →
          ⦃α β : TypeVec.{u} n⦄ → α.Arrow β → MvQPF.Quot1 R α → MvQPF.Quot1 R β
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_right : ∀ {R : Type u} [inst : CommRing R] {M N P : Type u} [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P] [inst_7 : Coalgebra R M]
  [inst_8 : Coalgebra R N] [inst_9 : Coalgebra R P], CoalgebraStruct.counit = CoalgebraStruct.counit
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_eq_getKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α} {h' : a ∈ t}, t.getKey a h' = t.getKeyD a fallback
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_eq_sum_iff_single : ∀ {ι : Type u_1} {M : Type u_3} {s : Finset ι} [inst : AddCommMonoid M] [IsRightCancelAdd M] {f g : ι → M} {i : ι},
  i ∈ s → (∀ j ∈ s, j ≠ i → f j = g j) → (∑ j ∈ s, f j = ∑ j ∈ s, g j ↔ f i = g i)
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- The canonical map from the kernel of `g` to the kernel of `g` localized at a submonoid.

This is a localization map by `LinearMap.toKerLocalized_isLocalizedModule`.
 -/
LinearMap.toKerIsLocalized : {R : Type u_1} →
  {M : Type u_3} →
    {N : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] →
                (p : Submonoid R) →
                  (f : M →ₗ[R] N) →
                    [inst_5 : IsLocalizedModule p f] →
                      {P : Type u_5} →
                        [inst_6 : AddCommMonoid P] →
                          [inst_7 : Module R P] →
                            {Q : Type u_6} →
                              [inst_8 : AddCommMonoid Q] →
                                [inst_9 : Module R Q] →
                                  (f' : P →ₗ[R] Q) →
                                    [inst_10 : IsLocalizedModule p f'] →
                                      (g : M →ₗ[R] P) → ↥g.ker →ₗ[R] ↥((IsLocalizedModule.map p f f') g).ker
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
fourier_gaussian_innerProductSpace : ∀ {b : ℂ} {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V],
  0 < b.re →
    ∀ (w : V),
      FourierTransform.fourier (fun v => Complex.exp (-b * ↑‖v‖ ^ 2)) w =
        (↑Real.pi / b) ^ (↑(Module.finrank ℝ V) / 2) * Complex.exp (-↑Real.pi ^ 2 * ↑‖w‖ ^ 2 / b)
-- Mathlib.Dynamics.Minimal
isMinimal_iff_isClosed_vadd_invariant : ∀ (M : Type u_1) {α : Type u_3} [inst : AddMonoid M] [inst_1 : TopologicalSpace α] [inst_2 : AddAction M α]
  [ContinuousConstVAdd M α],
  AddAction.IsMinimal M α ↔ ∀ (s : Set α), IsClosed s → (∀ (c : M), c +ᵥ s ⊆ s) → s = ∅ ∨ s = Set.univ
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfoldRev.match_1.eq_2 : ∀
  (motive :
    (n : ℕ) →
      {α : (i : ℕ) → autoParam (i ≤ n) Nat.dfoldRev._auto_1 → Type u_1} →
        ((i : ℕ) → (h : i < n) → α (i + 1) ⋯ → α i ⋯) → α n ⋯ → Sort u_2)
  (n : ℕ) (α : (i : ℕ) → autoParam (i ≤ n + 1) Nat.dfoldRev._auto_1 → Type u_1)
  (f : (i : ℕ) → (h : i < n + 1) → α (i + 1) ⋯ → α i ⋯) (init : α (n + 1) ⋯)
  (h_1 :
    (α : (i : ℕ) → autoParam (i ≤ 0) Nat.dfoldRev._auto_1 → Type u_1) →
      (f : (i : ℕ) → (h : i < 0) → α (i + 1) ⋯ → α i ⋯) → (init : α 0 ⋯) → motive 0 f init)
  (h_2 :
    (n : ℕ) →
      (α : (i : ℕ) → autoParam (i ≤ n + 1) Nat.dfoldRev._auto_1 → Type u_1) →
        (f : (i : ℕ) → (h : i < n + 1) → α (i + 1) ⋯ → α i ⋯) → (init : α (n + 1) ⋯) → motive n.succ f init),
  (match n.succ, α, f, init with
    | 0, α, f, init => h_1 α f init
    | n.succ, α, f, init => h_2 n α f init) =
    h_2 n α f init
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)} {fallback : α},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.isEmpty = false →
    ((Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.maxKeyD fallback = k ↔
      (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (compare k' k).isLE = true)
-- Mathlib.GroupTheory.Congruence.Defs
Con.group.eq_1 : ∀ {M : Type u_1} [inst : Group M] (c : Con M),
  c.group =
    { toMonoid := c.monoid, toInv := c.hasInv, toDiv := c.hasDiv, toZPow := ZPow.ofPow, div_eq_mul_inv := ⋯,
      zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.QuasiCompactCover.instOfIsEmptyCarrierCarrierCommRingCat : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : CategoryTheory.PreZeroHypercover S} [IsEmpty ↥S],
  AlgebraicGeometry.QuasiCompactCover 𝒰
-- Mathlib.Algebra.Module.PUnit
PUnit.mulSemiringAction : {R : Type u_1} → [inst : Semiring R] → MulSemiringAction R PUnit.{u_3 + 1}
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k} [inst_1 : Inhabited (β k')],
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l → ⟨k, v⟩ ∈ l → (m.insertMany l).get! k' = cast ⋯ v
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.lift_mk'_spec : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (x : M) (v : P)
  (y : ↥S), (f.lift hg) (f.mk' x y) = v ↔ g x = g ↑y * v
-- Init.Data.SInt.Lemmas
Int8.toInt16_neg_of_ne : ∀ {x : Int8}, x ≠ -128 → (-x).toInt16 = -x.toInt16
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_bot : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α], ⨆ x, ⊥ = ⊥
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.apply_skipPrefixWhile_prop : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {h : s.skipPrefixWhile P ≠ s.endPos},
  ¬P ((s.skipPrefixWhile P).get h)
-- Mathlib.Topology.Homeomorph.Defs
Equiv.toHomeomorph_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ Y)
  (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) (x : X), (e.toHomeomorph he) x = e x
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
/-- A helper structure that bundles the necessary data to
construct a `StrictPseudofunctor` without specifying the redundant
fields `mapId` and `mapComp`.  -/
CategoryTheory.StrictPseudofunctorCore : (B : Type u₁) →
  [CategoryTheory.Bicategory B] →
    (C : Type u₂) → [CategoryTheory.Bicategory C] → Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.cyclotomic_two : ∀ (R : Type u_1) [inst : Ring R], Polynomial.cyclotomic 2 R = Polynomial.X + 1
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.explicit.sizeOf_spec : ∀ (ref : Lean.Syntax) (a : Lean.Elab.Tactic.RCases.RCasesPatt),
  sizeOf (Lean.Elab.Tactic.RCases.RCasesPatt.explicit ref a) = 1 + sizeOf ref + sizeOf a
-- Mathlib.Data.Nat.Count
Nat.count_monotone : ∀ (p : ℕ → Prop) [inst : DecidablePred p], Monotone (Nat.count p)
-- Mathlib.Algebra.GroupWithZero.Invertible
/-- `b / a` is the inverse of `a / b`  -/
invertibleDiv : {α : Type u} → [inst : GroupWithZero α] → (a b : α) → [Invertible a] → [Invertible b] → Invertible (a / b)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Consumer.normal : {α : Type} → IO.Promise (Option α) → Std.CloseableChannel.Consumer✝ α
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.mk.injEq : ∀ {X : Type u_4} [inst : TopologicalSpace X] (toFun : ℕ → Set X) (isCompact' : ∀ (n : ℕ), IsCompact (toFun n))
  (subset_interior_succ' : ∀ (n : ℕ), toFun n ⊆ interior (toFun (n + 1))) (iUnion_eq' : ⋃ n, toFun n = Set.univ)
  (toFun_1 : ℕ → Set X) (isCompact'_1 : ∀ (n : ℕ), IsCompact (toFun_1 n))
  (subset_interior_succ'_1 : ∀ (n : ℕ), toFun_1 n ⊆ interior (toFun_1 (n + 1)))
  (iUnion_eq'_1 : ⋃ n, toFun_1 n = Set.univ),
  ({ toFun := toFun, isCompact' := isCompact', subset_interior_succ' := subset_interior_succ',
        iUnion_eq' := iUnion_eq' } =
      { toFun := toFun_1, isCompact' := isCompact'_1, subset_interior_succ' := subset_interior_succ'_1,
        iUnion_eq' := iUnion_eq'_1 }) =
    (toFun = toFun_1)
-- Mathlib.Algebra.Order.Ring.Canonical
/-- The `tsub` version of `sq_sub_sq`. Notably, this holds for `Nat` and `NNReal`.  -/
sq_tsub_sq : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] [inst_3 : Sub R]
  [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [AddLeftReflectLE R] (a b : R), a ^ 2 - b ^ 2 = (a + b) * (a - b)
-- Lean.Meta.InferType
/-- The expression is definitely *not* of the form `A_1 -> ... -> A_n -> B`
where `B` is a proposition.
 -/
_private.Lean.Meta.InferType.0.Lean.Meta.ArrowPropResult.false : Lean.Meta.ArrowPropResult✝
-- Mathlib.Data.ENNReal.Inv
ENNReal.orderIsoUnitIntervalBirational_apply_coe : ∀ (x : ENNReal), ↑(ENNReal.orderIsoUnitIntervalBirational x) = (x⁻¹ + 1)⁻¹.toReal
-- Mathlib.CategoryTheory.Comma.CardinalArrow
CategoryTheory.Arrow.finite : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [CategoryTheory.FinCategory C], Finite (CategoryTheory.Arrow C)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct.eq_1 : ∀ {α : Type u},
  Stream'.WSeq.destruct =
    Computation.corec fun s =>
      match Stream'.Seq.destruct s with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s'))
-- Mathlib.Order.Filter.Pi
Filter.pi_inj : ∀ {ι : Type u_1} {α : ι → Type u_2} {f₁ f₂ : (i : ι) → Filter (α i)} [∀ (i : ι), (f₁ i).NeBot],
  Filter.pi f₁ = Filter.pi f₂ ↔ f₁ = f₂
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_map_iff : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α ↪ β} {t : Set β},
  (SimpleGraph.map (⇑f) G).IsClique t ↔ t.Subsingleton ∨ ∃ s, G.IsClique s ∧ ⇑f '' s = t
-- Init.Data.Array.Lemmas
Array.getElem_reverse : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (hi : i < xs.reverse.size), xs.reverse[i] = xs[xs.size - 1 - i]
-- Mathlib.Data.Nat.Factorization.Defs
/-- Any Finsupp `f : ℕ →₀ ℕ` whose support is in the primes is equal to the factorization of
the product `∏ (a : ℕ) ∈ f.support, a ^ f a`.  -/
Nat.prod_pow_factorization_eq_self : ∀ {f : ℕ →₀ ℕ}, (∀ p ∈ f.support, Nat.Prime p) → (f.prod fun x1 x2 => x1 ^ x2).factorization = f
-- Mathlib.Algebra.Group.Units.Hom
IsAddUnit.coe_liftRight : ∀ {M : Type u_3} {N : Type u_4} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M →+ N)
  (hf : ∀ (x : M), IsAddUnit (f x)) (x : M), ↑((IsAddUnit.liftRight f hf) x) = f x
-- Mathlib.Algebra.Group.Submonoid.Defs
SubmonoidClass.instIsDedekindFiniteMonoidSubtypeMem : ∀ {M : Type u_1} {A : Type u_3} [inst : MulOneClass M] [inst_1 : SetLike A M] [hA : SubmonoidClass A M] (S : A)
  [IsDedekindFiniteMonoid M], IsDedekindFiniteMonoid ↥S
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.isValue.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Measure.Restrict
map_restrict_ae_le_map_indicator_ae : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β}
  [inst_1 : Zero β],
  MeasurableSet s → Filter.map f (MeasureTheory.ae (μ.restrict s)) ≤ Filter.map (s.indicator f) (MeasureTheory.ae μ)
-- Lean.Elab.AssertExists
Lean.Elab.Command.AssertExists.mk.injEq : ∀ (isDecl : Bool) (givenName modName : Lean.Name) (isDecl_1 : Bool) (givenName_1 modName_1 : Lean.Name),
  ({ isDecl := isDecl, givenName := givenName, modName := modName } =
      { isDecl := isDecl_1, givenName := givenName_1, modName := modName_1 }) =
    (isDecl = isDecl_1 ∧ givenName = givenName_1 ∧ modName = modName_1)
-- Lean.Meta.Tactic.Grind.Types
/-- Delayed instantiations is a mapping from guards to theorems that are waiting them
to become `True`.
 -/
Lean.Meta.Grind.EMatch.State.delayedThmInsts : Lean.Meta.Grind.EMatch.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr (List Lean.Meta.Grind.DelayedTheoremInstance)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.mkIte : Lean.Syntax →
  Lean.Syntax →
    Lean.Syntax →
      Lean.Elab.Term.Do.CodeBlock → Lean.Elab.Term.Do.CodeBlock → Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_ric_eq_push : ∀ {n : ℕ}, 0 < n → (*...=n).toArray = (*...=n - 1).toArray.push n
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.prod.fst.match_1.eq_1 : ∀ (motive : (x : ℕ) → TypeVec.{u_1} x → TypeVec.{u_1} x → Fin2 x → Sort u_2) (n : ℕ) (α β : TypeVec.{u_1} n.succ)
  (i : Fin2 n) (h_1 : (n : ℕ) → (α β : TypeVec.{u_1} n.succ) → (i : Fin2 n) → motive n.succ α β i.fs)
  (h_2 : (n : ℕ) → (x x_1 : TypeVec.{u_1} n.succ) → motive n.succ x x_1 Fin2.fz),
  (match n.succ, α, β, i.fs with
    | n.succ, α, β, i.fs => h_1 n α β i
    | n.succ, x, x_1, Fin2.fz => h_2 n x x_1) =
    h_1 n α β i
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.kernelUnopUnop_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {A B : Cᵒᵖ}
  (g : A ⟶ B),
  (CategoryTheory.kernelUnopUnop g).inv =
    CategoryTheory.Limits.kernel.lift g.unop (CategoryTheory.Limits.cokernel.π g).unop ⋯
-- Lean.Level
Lean.Level.any : Lean.Level → (Lean.Level → Bool) → Bool
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkCoinductiveAux₁.congr_simp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero zero_1 : P.X 1 ⟶ Q.X 0) (e_zero : zero = zero_1)
  (one one_1 : P.X 2 ⟶ Q.X 1) (e_one : one = one_1)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one)
  (succ succ_1 :
    (n : ℕ) →
      (p :
          (f : P.X (n + 1) ⟶ Q.X n) ×'
            (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) +
                  CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') →
        (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) +
              CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f''),
  succ = succ_1 →
    ∀ (n : ℕ),
      Homotopy.mkCoinductiveAux₁ e zero one comm_one succ n = Homotopy.mkCoinductiveAux₁ e zero_1 one_1 ⋯ succ_1 n
-- Mathlib.MeasureTheory.Order.Lattice
/-- We say that a type has `MeasurableInf` if `(c ⊓ ·)` and `(· ⊓ c)` are measurable functions.
For a typeclass assuming measurability of `uncurry (· ⊓ ·)` see `MeasurableInf₂`.  -/
MeasurableInf : (M : Type u_1) → [MeasurableSpace M] → [Min M] → Prop
-- Mathlib.Algebra.Group.Action.Defs
/-- **Alias** of `smul_mul_smul_comm`.

---

Note that the `IsScalarTower α β β` and `SMulCommClass α β β` typeclass arguments are usually
satisfied by `Algebra α β`.  -/
smul_mul_smul : ∀ {α : Type u_5} {β : Type u_6} [inst : Mul α] [inst_1 : Mul β] [inst_2 : SMul α β] [IsScalarTower α β β]
  [IsScalarTower α α β] [SMulCommClass α β β] (a : α) (b : β) (c : α) (d : β), a • b * c • d = (a * c) • (b * d)
-- Mathlib.Algebra.Order.Interval.Basic
Interval.inv_bot : ∀ {α : Type u_2} [inst : CommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedMonoid α], ⊥⁻¹ = ⊥
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.nameNotRoundtrippable : Lean.Name → Bool
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.hom_ext_iff : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F] {X : C}
  {f f' : CategoryTheory.Limits.colimit F ⟶ X},
  f = f' ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) f'
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.ext_iff : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  {f₁ f₂ : 𝒜 →ₐᵍ[R] ℬ}, f₁ = f₂ ↔ ∀ (x : A), f₁ x = f₂ x
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.instProductive : ∀ {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α₁ m β]
  [inst_2 : Std.Iterator α₂ m β] [Std.Iterators.Productive α₁ m] [Std.Iterators.Productive α₂ m],
  Std.Iterators.Productive (Std.Iterators.Types.Append α₁ α₂ m β) m
-- Mathlib.Analysis.Convex.Function
/-- The pointwise maximum of convex functions is convex.  -/
ConvexOn.sup : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulStrictMono 𝕜 β] {s : Set E} {f g : E → β}, ConvexOn 𝕜 s f → ConvexOn 𝕜 s g → ConvexOn 𝕜 s (f ⊔ g)
-- Mathlib.Order.Interval.Set.Pi
Set.pi_univ_Ioi_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] (x : (i : ι) → α i) [Nonempty ι],
  (Set.univ.pi fun i => Set.Ioi (x i)) ⊆ Set.Ioi x
-- Mathlib.Control.LawfulFix
Part.lawfulFix : {α : Type u_1} → LawfulFix (Part α)
-- Mathlib.Algebra.Category.AlgCat.Basic
_private.Mathlib.Algebra.Category.AlgCat.Basic.0.AlgCat.Hom.mk.injEq : ∀ {R : Type u} [inst : CommRing R] {A B : AlgCat R} (hom' hom'_1 : ↑A →ₐ[R] ↑B),
  ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.GroupTheory.Complement
/-- The equivalence `G ≃ S × T`, such that the inverse is  `(*) : S × T → G`  -/
Subgroup.IsComplement.equiv : {G : Type u_1} → [inst : Group G] → {S T : Set G} → Subgroup.IsComplement S T → G ≃ ↑S × ↑T
-- Mathlib.Topology.Order.LeftRightLim
leftLim_eq_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [hα : TopologicalSpace α]
  [h'α : OrderTopology α] [T2Space β] {f : α → β} {a : α} {y : β} [h : (nhdsWithin a (Set.Iio a)).NeBot],
  Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds y) → Function.leftLim f a = y
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.arrowCongr'_trans : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} {A₁' : Type u_5} {A₂' : Type u_6} {A₃' : Type u_7}
  [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A₁] [inst_2 : DistribMulAction R A₁] [inst_3 : Star A₁]
  [inst_4 : NonUnitalNonAssocSemiring A₂] [inst_5 : DistribMulAction R A₂] [inst_6 : Star A₂]
  [inst_7 : NonUnitalNonAssocSemiring A₃] [inst_8 : DistribMulAction R A₃] [inst_9 : Star A₃]
  [inst_10 : NonUnitalNonAssocSemiring A₁'] [inst_11 : DistribMulAction R A₁'] [inst_12 : Star A₁']
  [inst_13 : NonUnitalNonAssocSemiring A₂'] [inst_14 : DistribMulAction R A₂'] [inst_15 : Star A₂']
  [inst_16 : NonUnitalNonAssocSemiring A₃'] [inst_17 : DistribMulAction R A₃'] [inst_18 : Star A₃'] (e₁ : A₁ ≃⋆ₐ[R] A₂)
  (e₁' : A₁' ≃⋆ₐ[R] A₂') (e₂ : A₂ ≃⋆ₐ[R] A₃) (e₂' : A₂' ≃⋆ₐ[R] A₃'),
  (e₁.trans e₂).arrowCongr' (e₁'.trans e₂') = (e₁.arrowCongr' e₁').trans (e₂.arrowCongr' e₂')
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C}
  [self : W.IsMultiplicative], W.IsStableUnderComposition
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.inr_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β]
  (y : β), (OrderMonoidHom.inr α β) y = (1, y)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.coe_injective : Function.Injective UpperHalfPlane.coe
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_of_contains_insertManyIfNewUnit_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] (h : t.WF) {l : List α} {k : α},
  l.contains k = false →
    Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯) = true →
      Std.DTreeMap.Internal.Impl.contains k t = true
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_sup_eq : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {f g : ι → α},
  BddAbove (Set.range f) → BddAbove (Set.range g) → ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x
-- Init.Data.UInt.Lemmas
UInt32.eq_iff_toBitVec_eq : ∀ {a b : UInt32}, a = b ↔ a.toBitVec = b.toBitVec
-- Init.Data.Vector.Lemmas
Vector.foldl_flatten : ∀ {β : Type u_1} {α : Type u_2} {m n : ℕ} {f : β → α → β} {b : β} {xss : Vector (Vector α m) n},
  Vector.foldl f b xss.flatten = Vector.foldl (fun b xs => Vector.foldl f b xs) b xss
-- Mathlib.Data.Int.Bitwise
/-- `Int.bitwise` applies the function `f` to pairs of bits in the same position in
the binary representations of its inputs.  -/
Int.bitwise : (Bool → Bool → Bool) → ℤ → ℤ → ℤ
-- Mathlib.CategoryTheory.Bicategory.EqToHom
CategoryTheory.Bicategory.eqToHomTransIso_refl_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {x y : B} (e₁ : x = y),
  CategoryTheory.Bicategory.eqToHomTransIso e₁ ⋯ =
    (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.eqToHom e₁)).symm
-- Mathlib.Data.Matrix.Diagonal
Matrix.diag_neg : ∀ {n : Type u_3} {α : Type v} [inst : Neg α] (A : Matrix n n α), (-A).diag = -A.diag
-- Init.Grind.Lemmas
Lean.Grind.Bool.ne_of_eq_false_of_eq_true : ∀ {a b : Bool}, a = false → b = true → (a = b) = False
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.shiftFunctorAdd_hom_app_f : ∀ {S : Type u_1} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (m n : S)
  (X : CategoryTheory.DifferentialObject S C),
  ((CategoryTheory.DifferentialObject.shiftFunctorAdd C m n).hom.app X).f =
    (CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- `G.edgeSet` is the edge set for `G`.
This is an abbreviation for `edgeSetEmbedding G` that permits dot notation.  -/
SimpleGraph.edgeSet : {V : Type u} → SimpleGraph V → Set (Sym2 V)