mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit_comp_ι_map_whiskerRight_app : ∀ (C : Type u₁) {inst : CategoryTheory.Category.{v₁, u₁} C} (V : Type u₂) {inst_1 : CategoryTheory.Category.{v₂, u₂} V}
  {inst_2 : CategoryTheory.MonoidalCategory C} {inst_3 : CategoryTheory.MonoidalCategory V} {D : Type u₃}
  {inst_4 : CategoryTheory.Category.{v₃, u₃} D} {inst_5 : CategoryTheory.MonoidalCategoryStruct D}
  [self : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] {d₁ d₁' : D} (f₁ : d₁ ⟶ d₁')
  (d₂ : D) (x y : C),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit C V d₁
            d₂).app
        (x, y))
      (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₁ d₂)).app
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map f₁).app x)
        (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d₂).obj y))
      ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit C V d₁'
            d₂).app
        (x, y))
-- Init.Data.Vector.Lemmas
Vector.replace_push : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {n : ℕ} {xs : Vector α n} {a b c : α},
  (xs.push a).replace b c = if b ∈ xs then (xs.replace b c).push a else xs.push (if (b == a) = true then c else a)
-- Mathlib.RingTheory.Polynomial.ShiftedLegendre
/-- The degree of `shiftedLegendre n` is `n`.  -/
Polynomial.degree_shiftedLegendre : ∀ (n : ℕ), (Polynomial.shiftedLegendre n).degree = ↑n
-- Mathlib.RingTheory.HopfAlgebra.Convolution
AlgHom.antipode_id_cancel : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : HopfAlgebra R A],
  WithConv.toConv (HopfAlgebra.antipodeAlgHom R A) * WithConv.toConv (AlgHom.id R A) = 1
-- Mathlib.Algebra.Order.Archimedean.Class
/-- A closed ball defined by `FiniteArchimedeanClass.addSubgroup` of `UpperSet.Ici c`.  -/
FiniteArchimedeanClass.closedBallAddSubgroup : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] → [inst_2 : IsOrderedAddMonoid M] → FiniteArchimedeanClass M → AddSubgroup M
-- Mathlib.Algebra.Exact.Basic
LinearMap.exact_zero_iff_surjective : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_8} {N : Type u_9} (P : Type u_10) [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommMonoid P] [inst_4 : Module R N] [inst_5 : Module R M] [inst_6 : Module R P]
  (f : M →ₗ[R] N), Function.Exact ⇑f ⇑0 ↔ Function.Surjective ⇑f
-- Mathlib.Combinatorics.Graph.Basic
Graph.Compatible.symm : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, G.Compatible H → H.Compatible G
-- Mathlib.Order.Filter.Extr
IsMinOn.bicomp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α}
  {a : α} [inst_2 : Preorder δ] {op : β → γ → δ},
  Relator.LiftFun (fun x1 x2 => x1 ≤ x2) (Relator.LiftFun (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2) op op →
    IsMinOn f s a → ∀ {g : α → γ}, IsMinOn g s a → IsMinOn (fun x => op (f x) (g x)) s a
-- Lean.Meta.Closure
Lean.Meta.Closure.mkValueTypeClosure : Lean.Expr → Lean.Expr → Bool → Lean.MetaM Lean.Meta.Closure.MkValueTypeClosureResult
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- Euler's limit formula for the complex Gamma function.  -/
Complex.GammaSeq_tendsto_Gamma : ∀ (s : ℂ), Filter.Tendsto s.GammaSeq Filter.atTop (nhds (Complex.Gamma s))
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivativeFinsupp_derivative : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R),
  Polynomial.derivativeFinsupp (Polynomial.derivative p) =
    Finsupp.comapDomain Nat.succ (Polynomial.derivativeFinsupp p) ⋯
-- Init.Data.Int.DivMod.Lemmas
/-- If `a % b = c` then `b` divides `a - c`.  -/
Int.dvd_self_sub_of_emod_eq : ∀ {a b c : ℤ}, a % b = c → b ∣ a - c
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.has_both : ∀ (b : Bool),
  Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b Std.Tactic.BVDecide.LRAT.Internal.Assignment.both = true
-- Init.BinderPredicates
/-- Declare `∀ x ⊇ y, ...` as syntax for `∀ x, x ⊇ y → ...` and `∃ x ⊇ y, ...` as syntax for
`∃ x, x ⊇ y ∧ ...`  -/
Lean.«binderPred⊇_» : Lean.ParserDescr
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.apply_symm_apply : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β) (x : β), h (h.symm x) = x
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pushforward_arrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (S : CategoryTheory.Sieve X),
  (CategoryTheory.Sieve.pushforward f S).arrows = CategoryTheory.Presieve.pushforward f S.arrows
-- Mathlib.Analysis.RCLike.Extend
/-- **Alias** of `Module.Dual.norm_extendRCLike_apply_sq`. -/
LinearMap.norm_extendTo𝕜'_apply_sq : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : AddCommGroup F] [inst_2 : Module ℝ F] [inst_3 : Module 𝕜 F]
  [inst_4 : IsScalarTower ℝ 𝕜 F] (fr : Module.Dual ℝ F) (x : F),
  ‖fr.extendRCLike x‖ ^ 2 = fr ((starRingEnd 𝕜) (fr.extendRCLike x) • x)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.id_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (z₂ : CochainComplex.HomComplex.Cochain F G n),
  (CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id F)).comp z₂ ⋯ = z₂
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.step_intermediateZip.match_3.eq_2 : ∀ {α₁ β₁ : Type u_1} [inst : Std.Iterator α₁ Id β₁]
  (motive : Option { out // ∃ it, it.toIterM.IsPlausibleOutput out } → Sort u_2)
  (out₁ : { out // ∃ it, it.toIterM.IsPlausibleOutput out }) (h_1 : Unit → motive none)
  (h_2 : (out₁ : { out // ∃ it, it.toIterM.IsPlausibleOutput out }) → motive (some out₁)),
  (match some out₁ with
    | none => h_1 ()
    | some out₁ => h_2 out₁) =
    h_2 out₁
-- Mathlib.Algebra.Homology.CochainComplexPlus
CategoryTheory.Functor.mapCochainComplexPlusCompι_hom_app_f : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  [inst_4 : F.PreservesZeroMorphisms] (X : CochainComplex.Plus C) (x : ℤ),
  (F.mapCochainComplexPlusCompι.hom.app X).f x = CategoryTheory.CategoryStruct.id (F.obj (X.obj.X x))
-- Mathlib.InformationTheory.KullbackLeibler.Basic
/-- **Converse Gibbs' inequality**: the Kullback-Leibler divergence between two finite measures is
zero if and only if the two measures are equal.  -/
InformationTheory.klDiv_eq_zero_iff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν], InformationTheory.klDiv μ ν = 0 ↔ μ = ν
-- Mathlib.NumberTheory.Divisors
Nat.divisors_one : Nat.divisors 1 = {1}
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.coherentExtensiveEquivalence_functor_obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.Preregular C]
  [inst_3 : CategoryTheory.FinitaryExtensive C] [inst_4 : ∀ (X : C), CategoryTheory.Projective X]
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A),
  (CategoryTheory.Presheaf.coherentExtensiveEquivalence.functor.obj X).obj = X.obj
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstr.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr → Sort u}
  {motive_2 : Lean.Meta.Grind.Arith.Linear.EqCnstrProof → Sort u}
  {motive_3 : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Sort u}
  {motive_4 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Sort u}
  {motive_5 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Sort u}
  {motive_6 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof → Sort u}
  {motive_7 : Lean.Meta.Grind.Arith.Linear.UnsatProof → Sort u} (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstr)
  (F_1 : (t : Lean.Meta.Grind.Arith.Linear.EqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.Arith.Linear.EqCnstrProof) → t.below → motive_2 t)
  (F_3 : (t : Lean.Meta.Grind.Arith.Linear.IneqCnstr) → t.below → motive_3 t)
  (F_4 : (t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) → t.below → motive_4 t)
  (F_5 : (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) → t.below → motive_5 t)
  (F_6 : (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) → t.below → motive_6 t)
  (F_7 : (t : Lean.Meta.Grind.Arith.Linear.UnsatProof) → t.below → motive_7 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_5 t (Lean.Meta.Grind.Arith.Linear.DiseqCnstr.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.RingTheory.Polynomial.Pochhammer
_private.Mathlib.RingTheory.Polynomial.Pochhammer.0.ascPochhammer.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Turn minimal axioms for `CompleteDistribLattice` into minimal axioms for `Order.Frame`.  -/
CompleteDistribLattice.MinimalAxioms.toFrame : ∀ {α : Type u} [inst : CompleteLattice α], CompleteDistribLattice.MinimalAxioms α → Order.Frame.MinimalAxioms α
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.mk.inj : ∀ {toBddDistLat : BddDistLat} {isFintype : Fintype ↑toBddDistLat.toDistLat} {toBddDistLat_1 : BddDistLat}
  {isFintype_1 : Fintype ↑toBddDistLat_1.toDistLat},
  { toBddDistLat := toBddDistLat, isFintype := isFintype } =
      { toBddDistLat := toBddDistLat_1, isFintype := isFintype_1 } →
    toBddDistLat = toBddDistLat_1 ∧ isFintype ≍ isFintype_1
-- Batteries.Lean.Meta.Inaccessible
/-- Obtain the inaccessible fvars from the given local context. An fvar is
inaccessible if (a) its user name is inaccessible or (b) it is shadowed by a
later fvar with the same user name.
 -/
Lean.LocalContext.inaccessibleFVars : Lean.LocalContext → Array Lean.LocalDecl
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicClosure_empty : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P], intrinsicClosure 𝕜 ∅ = ∅
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_map_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (obj : Fin (n + 1) → C)
  (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ) (i : ℕ)
  (hi : autoParam (i < n) CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_map_succ._auto_1),
  (CategoryTheory.ComposableArrows.mkOfObjOfMapSucc obj mapSucc).map' i (i + 1) ⋯ hi = mapSucc ⟨i, hi⟩
-- Mathlib.MeasureTheory.Group.FoelnerFilter
/-- The limit along an ultrafilter of the density of a set with respect to a sequence in `X`.  -/
IsFoelner.mean : {X : Type u_2} →
  [inst : MeasurableSpace X] → MeasureTheory.Measure X → {ι : Type u_3} → Ultrafilter ι → (ι → Set X) → Set X → ENNReal
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.generate_map_eq_functorPushforward : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} {s : CategoryTheory.Presieve X},
  CategoryTheory.Sieve.generate (CategoryTheory.Presieve.map F s) =
    CategoryTheory.Sieve.functorPushforward F (CategoryTheory.Sieve.generate s)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_add_natCast' : ∀ {x y : ℝ} {n : ℕ}, 0 ≤ x → y + ↑n ≠ 0 → x ^ (y + ↑n) = x ^ y * x ^ n
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.instPreservesLimitWalkingParallelPairParallelPairOfIsCosplitPairOfPreservesLimitOfIsCosplitPair : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g]
  [CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair F],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) F
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.ext_iff : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {φ₁ φ₂ : A →ₐc[R] B}, φ₁ = φ₂ ↔ ∀ (x : A), φ₁ x = φ₂ x
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Limits.sigmaConst.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C],
  CategoryTheory.Limits.sigmaConst = CategoryTheory.Limits.sigmaConst
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.karoubi.F'_map_f : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] {X Y : A} (f : X ⟶ Y),
  ((CategoryTheory.Abelian.LeftResolution.karoubi.F' Λ).map f).f = Λ.F.map f - Λ.F.map 0
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.instBEqEvalConfigItemHandlerKind.beq : Lean.Elab.ConfigEval.EvalConfigItemHandlerKind → Lean.Elab.ConfigEval.EvalConfigItemHandlerKind → Bool
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.sheafPushforwardContinuousComp'_hom_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D E} {FG : CategoryTheory.Functor C E} (eFG : F.comp G ≅ FG) (A : Type u)
  [inst_3 : CategoryTheory.Category.{t, u} A] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (L : CategoryTheory.GrothendieckTopology E) [inst_4 : F.IsContinuous J K]
  [inst_5 : G.IsContinuous K L] [inst_6 : FG.IsContinuous J L] (X : CategoryTheory.Sheaf L A) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Functor.sheafPushforwardContinuousComp' eFG A J K L).hom.app X).hom.app X_1 =
    X.obj.map (eFG.inv.app (Opposite.unop X_1)).op
-- Mathlib.Topology.MetricSpace.IsometricSMul
dist_mul_left : ∀ {M : Type u} [inst : PseudoMetricSpace M] [inst_1 : Mul M] [IsIsometricSMul M M] (a b c : M),
  dist (a * b) (a * c) = dist b c
-- Init.Data.Array.MapIdx
Array.mapFinIdxM.map.eq_1 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α) (f : (i : ℕ) → α → i < as.size → m β)
  (j : ℕ) (bs : Array β) (x : 0 + j = as.size), Array.mapFinIdxM.map as f 0 j x bs = pure bs
-- Mathlib.Topology.Algebra.Group.Matrix
Matrix.SpecialLinearGroup.continuous_apply : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] {α : Type u_4} [inst_4 : TopologicalSpace α] (f : α → Matrix.SpecialLinearGroup n R),
  Continuous f → ∀ (i : n), Continuous fun x => ↑(f x) i
-- Mathlib.Order.Filter.IsBounded
Filter.Tendsto.isBoundedUnder_comp : ∀ {ι : Type u_5} {κ : Type u_6} {X : Type u_7} {r : X → X → Prop} {f : ι → X} {φ : κ → ι} {𝓕 : Filter ι} {𝓖 : Filter κ},
  Filter.Tendsto φ 𝓖 𝓕 → Filter.IsBoundedUnder r 𝓕 f → Filter.IsBoundedUnder r 𝓖 (f ∘ φ)
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.addUnit_of_mem_ofAddUnits_spec_eq_of_val_mem : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : AddUnits M} (h : ↑x ∈ S.ofAddUnits),
  S.addUnit_of_mem_ofAddUnits h = x
-- Mathlib.Analysis.Normed.Group.Basic
nsmul_mem_closedBall : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {a b : E} {r : ℝ} {n : ℕ},
  a ∈ Metric.closedBall b r → n • a ∈ Metric.closedBall (n • b) (n • r)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.liftNC_smul : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : MulOneClass G] {R : Type u_3} [inst_2 : Semiring R]
  (f : k →+* R) (g : G →* R) (c : k) (φ : SkewMonoidAlgebra k G),
  (SkewMonoidAlgebra.liftNC ↑f ⇑g) (c • φ) = f c * (SkewMonoidAlgebra.liftNC ↑f ⇑g) φ
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.instIsMulCommutative_iSup : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {ι : Type u_2} [Nonempty ι] [inst_2 : Preorder ι]
  [IsDirectedOrder ι] {S : ι →o NonUnitalSubsemiring R} [hS : ∀ (i : ι), IsMulCommutative ↥(S i)],
  IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.Data.Stream.Init
Stream'.map_take : ∀ {α : Type u} {β : Type v} (n : ℕ) (a : Stream' α) (f : α → β),
  List.map f (Stream'.take n a) = Stream'.take n (Stream'.map f a)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPushout f g] {Z_1 : C} (h : CategoryTheory.Limits.pushout f g ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) h) =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) h)
-- Mathlib.Order.Hom.Bounded
/-- The underlying function. The preferred spelling is `DFunLike.coe`.  -/
BotHom.toFun : {α : Type u_6} → {β : Type u_7} → [inst : Bot α] → [inst_1 : Bot β] → BotHom α β → α → β
-- Lean.DocString.Types
Lean.Doc.Block.brecOn_5.go : {i : Type u} →
  {b : Type v} →
    {motive_1 : Lean.Doc.Block i b → Sort u_1} →
      {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
        {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
          {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1} →
            {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
              {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
                {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} →
                  {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1} →
                    {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1} →
                      (t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                        ((t : Lean.Doc.Block i b) → t.below → motive_1 t) →
                          ((t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                              Lean.Doc.Block.below_1 t → motive_2 t) →
                            ((t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                Lean.Doc.Block.below_2 t → motive_3 t) →
                              ((t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t) →
                                ((t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                                    Lean.Doc.Block.below_4 t → motive_5 t) →
                                  ((t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                      Lean.Doc.Block.below_5 t → motive_6 t) →
                                    ((t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t) →
                                      ((t : Lean.Doc.ListItem (Lean.Doc.Block i b)) →
                                          Lean.Doc.Block.below_7 t → motive_8 t) →
                                        ((t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) →
                                            Lean.Doc.Block.below_8 t → motive_9 t) →
                                          motive_6 t ×' Lean.Doc.Block.below_5 t
-- Mathlib.Algebra.Star.StarAlgHom
/-- If `A₁` is equivalent to `A₁'` and `A₂` is equivalent to `A₂'` as star algebras, then the type
of maps `A₁ →⋆ₐ[R] A₂` is equivalent to the type of maps `A₁' →⋆ₐ[R] A₂'`.

For non-unital star algebra homomorphisms, see `StarAlgEquiv.arrowCongr'`.  -/
StarAlgEquiv.arrowCongr : {R : Type u_1} →
  {A₁ : Type u_2} →
    {A₂ : Type u_3} →
      {A₁' : Type u_5} →
        {A₂' : Type u_6} →
          [inst : CommSemiring R] →
            [inst_1 : Semiring A₁] →
              [inst_2 : Semiring A₂] →
                [inst_3 : Semiring A₁'] →
                  [inst_4 : Semiring A₂'] →
                    [inst_5 : Algebra R A₁] →
                      [inst_6 : Algebra R A₂] →
                        [inst_7 : Algebra R A₁'] →
                          [inst_8 : Algebra R A₂'] →
                            [inst_9 : Star A₁] →
                              [inst_10 : Star A₂] →
                                [inst_11 : Star A₁'] →
                                  [inst_12 : Star A₂'] →
                                    (A₁ ≃⋆ₐ[R] A₁') → (A₂ ≃⋆ₐ[R] A₂') → (A₁ →⋆ₐ[R] A₂) ≃ (A₁' →⋆ₐ[R] A₂')
-- Init.Data.Fin.Lemmas
Fin.pred_one : ∀ {n : ℕ}, Fin.pred 1 ⋯ = 0
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.range_prodMap : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {R' : Type u_1} {S' : Type u_2}
  [inst_2 : Ring R'] [inst_3 : Ring S'] (f : R →+* S) (g : R' →+* S'), (f.prodMap g).range = f.range.prod g.range
-- Mathlib.Order.Hom.Lattice
InfHom.instOrderBot.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β] [inst_2 : OrderBot β],
  InfHom.instOrderBot = OrderBot.lift DFunLike.coe ⋯ ⋯
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor for additive groups preserves limits of arbitrary size.  -/
AddGrpCat.uliftFunctor_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} AddGrpCat.uliftFunctor
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.mem_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset α} {t : Finset β} {x : β},
  x ∈ s • t ↔ ∃ y ∈ s, ∃ z ∈ t, y • z = x
-- Mathlib.Analysis.Normed.Field.Basic
nnnorm_commutator_sub_one_le : ∀ {α : Type u_2} [inst : NormedDivisionRing α] {a b : α},
  a ≠ 0 → b ≠ 0 → ‖a * b * a⁻¹ * b⁻¹ - 1‖₊ ≤ 2 * ‖a‖₊⁻¹ * ‖b‖₊⁻¹ * ‖a - 1‖₊ * ‖b - 1‖₊
-- Init.Data.Int.Lemmas
Int.mul_def : ∀ {a b : ℤ}, a.mul b = a * b
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ContInfo.mk.injEq : ∀ (returnCont : Lean.Elab.Do.ReturnCont) (breakCont continueCont : Option (Lean.Elab.Do.DoElabM Lean.Expr))
  (returnCont_1 : Lean.Elab.Do.ReturnCont) (breakCont_1 continueCont_1 : Option (Lean.Elab.Do.DoElabM Lean.Expr)),
  ({ returnCont := returnCont, breakCont := breakCont, continueCont := continueCont } =
      { returnCont := returnCont_1, breakCont := breakCont_1, continueCont := continueCont_1 }) =
    (returnCont = returnCont_1 ∧ breakCont = breakCont_1 ∧ continueCont = continueCont_1)