awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g_1 f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ norm.{u_3} (E := V₂) ((g : (a : V₁) → V₂) v : V₂) ≤ ‖g‖ * ‖v‖

Tactic:
apply le_opNorm

Premises used: NormedAddGroupHom.le_opNorm
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g_1 f g : NormedAddGroupHom V₁ V₂
v : V₁
rw rw₁ : ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖ = ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖
⊢ ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖ = (‖f‖ + ‖g‖) * ‖v‖

Tactic:
rw [add_mul]

Premises used: add_mul
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f g : NormedAddGroupHom V₁ V₂
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
mkNormedAddGroupHom_norm_le _ (add_nonneg (opNorm_nonneg _) (opNorm_nonneg _)) _

Premises used: NormedAddGroupHom.mkNormedAddGroupHom_norm_le, add_nonneg, NormedAddGroupHom.opNorm_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f g : NormedAddGroupHom V₁ V₂
⊢ (⇑(f + g) : (a : V₁) → V₂) = HAdd.hAdd (α := (a : V₁) → V₂) (⇑f : (a : V₁) → V₂) (⇑g : (a : V₁) → V₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ (f + g : (a : V₁) → V₂) v = HAdd.hAdd (α := V₂) (β := V₂) ((f : (a : V₁) → V₂) v : V₂) ((g : (a : V₁) → V₂) v : V₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
⊢ ∀ (v : V₁), norm.{u_3} (E := V₂) ((0 : (a : V₁) → V₂) v : V₂) ≤ 0 * ‖v‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
x : V₁
rw : norm.{u_3} (E := V₂) ((0 : (a : V₁) → V₂) x : V₂) = 0
⊢ norm.{u_3} (E := V₂) ((0 : (a : V₁) → V₂) x : V₂) = 0 * ‖x‖

Tactic:
rw [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
x : V₁
⊢ norm.{u_3} (E := V₂) ((0 : (a : V₁) → V₂) x : V₂) = 0

Tactic:
norm_zero

Premises used: norm_zero
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
x : V₁
⊢ norm.{u_3} (E := V₂) ((0 : (a : V₁) → V₂) x : V₂) = 0

Tactic:
exact norm_zero

Premises used: norm_zero
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_5
V₂ : Type u_6
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
hn : ‖f‖ = 0
x : V₁
rw : 0 * ‖x‖ = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ ‖f‖ * ‖x‖ = 0

Tactic:
rw [hn, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_5
V₂ : Type u_6
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
hf : f = 0
rw : norm (E := NormedAddGroupHom V₁ V₂) 0 = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ ‖f‖ = 0

Tactic:
rw [hf, opNorm_zero]

Premises used: NormedAddGroupHom.opNorm_zero
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
⊢ Eq (α := (a : V₁) → V₂) (⇑0 : (a : V₁) → V₂) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
v : V₁
⊢ Eq.{u_3 + 1} (α := V₂) ((0 : (a : V₁) → V₂) v : V₂) (0 : V₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
⊢ ∀ (v : V), norm (E := V) ((AddMonoidHom.id V : (a : V) → V) v : V) ≤ 1 * ‖v‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
x : V
⊢ norm (E := V) ((id V : (a : V) → V) x : V) ≤ 1 * ‖x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NontrivialTopology V
let : ∀ (x : V) (hx : ‖x‖ ≠ 0), 1 ≤ norm (E := NormedAddGroupHom V V) (id V)
⊢ 1 ≤ norm (E := NormedAddGroupHom V V) (id V)

Tactic:
let ⟨x, hx⟩ := exists_norm_ne_zero V
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NontrivialTopology V
x : V
hx : ‖x‖ ≠ 0
⊢ norm (E := V) ((id V : (a : V) → V) x : V) / ‖x‖ ≤ norm (E := NormedAddGroupHom V V) (id V)

Tactic:
have := (id V).ratio_le_opNorm x
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NontrivialTopology V
x : V
hx : ‖x‖ ≠ 0
this : norm (E := V) ((id V : (a : V) → V) x : V) / ‖x‖ ≤ norm (E := NormedAddGroupHom V V) (id V)
rwa : ∀ (this : ‖x‖ / ‖x‖ ≤ norm (E := NormedAddGroupHom V V) (id V)), 1 ≤ norm (E := NormedAddGroupHom V V) (id V)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : 1 ≤ norm (E := NormedAddGroupHom V V) (id V)), 1 ≤ norm (E := NormedAddGroupHom V V) (id V)
⊢ 1 ≤ norm (E := NormedAddGroupHom V V) (id V)

Tactic:
rwa [id_apply, div_self hx] at this

Premises used: NormedAddGroupHom.id_apply, div_self
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
⊢ Eq (α := (a : V) → V) (⇑(id V) : (a : V) → V) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ norm.{u_3} (E := V₂) ((-f.toAddMonoidHom : (a : V₁) → V₂) v : V₂) ≤ ‖f‖ * ‖v‖

Tactic:
simp [le_opNorm f v]

Premises used: NormedAddGroupHom.le_opNorm
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
⊢ Eq (α := (a : V₁) → V₂) (⇑(-f) : (a : V₁) → V₂) (-(⇑f : (a : V₁) → V₂))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ Eq.{u_3 + 1} (α := V₂) ((-f : (a : V₁) → V₂) v : V₂) (-(f : (a : V₁) → V₂) v : V₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
⊢ ‖-f‖ = ‖f‖

Tactic:
simp only [norm_def, coe_neg, norm_neg, Pi.neg_apply]

Premises used: NormedAddGroupHom.coe_neg, norm_neg, NormedAddGroupHom.norm_def, Pi.neg_apply
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g_1 f g : NormedAddGroupHom V₁ V₂
simp :
  ∃ (C : ℝ), ∀ (v : V₁), norm.{u_3} (E := V₂) ((f.toAddMonoidHom + -g.toAddMonoidHom : (a : V₁) → V₂) v : V₂) ≤ C * ‖v‖
⊢ ∃ (C : ℝ), ∀ (v : V₁), ‖(↑(f.toAddMonoidHom - g.toAddMonoidHom) : ZeroHom V₁ V₂).toFun v‖ ≤ C * ‖v‖

Tactic:
simp only [AddMonoidHom.toFun_eq_coe, sub_eq_add_neg]

Premises used: AddMonoidHom.toFun_eq_coe, sub_eq_add_neg
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g_1 f g : NormedAddGroupHom V₁ V₂
⊢ ∃ (C : ℝ), ∀ (v : V₁), norm.{u_3} (E := V₂) ((f.toAddMonoidHom + -g.toAddMonoidHom : (a : V₁) → V₂) v : V₂) ≤ C * ‖v‖

Tactic:
(f + -g).bound'

Premises used: NormedAddGroupHom.bound', HAdd.hAdd, Neg.neg
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g_1 f g : NormedAddGroupHom V₁ V₂
⊢ ∃ (C : ℝ), ∀ (v : V₁), norm.{u_3} (E := V₂) ((f.toAddMonoidHom + -g.toAddMonoidHom : (a : V₁) → V₂) v : V₂) ≤ C * ‖v‖

Tactic:
exact (f + -g).bound'

Premises used: NormedAddGroupHom.bound', HAdd.hAdd, Neg.neg
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f g : NormedAddGroupHom V₁ V₂
⊢ (⇑(f - g) : (a : V₁) → V₂) = HSub.hSub (α := (a : V₁) → V₂) (⇑f : (a : V₁) → V₂) (⇑g : (a : V₁) → V₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ (f - g : (a : V₁) → V₂) v = HSub.hSub (α := V₂) (β := V₂) ((f : (a : V₁) → V₂) v : V₂) ((g : (a : V₁) → V₂) v : V₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst_4 : MonoidWithZero R
inst_5 : DistribMulAction R V₂
inst_6 : PseudoMetricSpace R
inst_7 : IsBoundedSMul R V₂
inst_8 : MonoidWithZero R'
inst_9 : DistribMulAction R' V₂
inst_10 : PseudoMetricSpace R'
inst_11 : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
⊢ dist (HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) x : V₂)) (HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) 0 : V₂)) ≤
    dist r 0 * dist.{u_3} (α := V₂) ((f : (a : V₁) → V₂) x : V₂) ((f : (a : V₁) → V₂) 0 : V₂)

Tactic:
have := dist_smul_pair r (f x) (f 0)
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst_4 : MonoidWithZero R
inst_5 : DistribMulAction R V₂
inst_6 : PseudoMetricSpace R
inst_7 : IsBoundedSMul R V₂
inst_8 : MonoidWithZero R'
inst_9 : DistribMulAction R' V₂
inst_10 : PseudoMetricSpace R'
inst_11 : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this :
  dist (HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) x : V₂)) (HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) 0 : V₂)) ≤
    dist r 0 * dist.{u_3} (α := V₂) ((f : (a : V₁) → V₂) x : V₂) ((f : (a : V₁) → V₂) 0 : V₂)
⊢ ‖HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) x : V₂)‖ ≤ dist r 0 * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂)

Tactic:
rw [map_zero, smul_zero, dist_zero_right, dist_zero_right] at this

Premises used: smul_zero, map_zero, dist_zero_right
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst_4 : MonoidWithZero R
inst_5 : DistribMulAction R V₂
inst_6 : PseudoMetricSpace R
inst_7 : IsBoundedSMul R V₂
inst_8 : MonoidWithZero R'
inst_9 : DistribMulAction R' V₂
inst_10 : PseudoMetricSpace R'
inst_11 : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this :
  ‖HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) x : V₂)‖ ≤ dist r 0 * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂)
rw : ‖HSMul.hSMul (β := (a : V₁) → V₂) r (⇑f : (a : V₁) → V₂) x‖ ≤ dist r 0 * (b * ‖x‖)
⊢ ‖HSMul.hSMul (β := (a : V₁) → V₂) r (⇑f : (a : V₁) → V₂) x‖ ≤ dist r 0 * b * ‖x‖

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst_4 : MonoidWithZero R
inst_5 : DistribMulAction R V₂
inst_6 : PseudoMetricSpace R
inst_7 : IsBoundedSMul R V₂
inst_8 : MonoidWithZero R'
inst_9 : DistribMulAction R' V₂
inst_10 : PseudoMetricSpace R'
inst_11 : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this :
  ‖HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) x : V₂)‖ ≤ dist r 0 * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂)
⊢ ‖HSMul.hSMul (β := (a : V₁) → V₂) r (⇑f : (a : V₁) → V₂) x‖ ≤ dist r 0 * (b * ‖x‖)

Tactic:
this.trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst_4 : MonoidWithZero R
inst_5 : DistribMulAction R V₂
inst_6 : PseudoMetricSpace R
inst_7 : IsBoundedSMul R V₂
inst_8 : MonoidWithZero R'
inst_9 : DistribMulAction R' V₂
inst_10 : PseudoMetricSpace R'
inst_11 : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this :
  ‖HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) x : V₂)‖ ≤ dist r 0 * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂)
refine : dist r 0 * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ dist r 0 * (b * ‖x‖)
⊢ ‖HSMul.hSMul (β := (a : V₁) → V₂) r (⇑f : (a : V₁) → V₂) x‖ ≤ dist r 0 * (b * ‖x‖)

Tactic:
refine this.trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst_4 : MonoidWithZero R
inst_5 : DistribMulAction R V₂
inst_6 : PseudoMetricSpace R
inst_7 : IsBoundedSMul R V₂
inst_8 : MonoidWithZero R'
inst_9 : DistribMulAction R' V₂
inst_10 : PseudoMetricSpace R'
inst_11 : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this :
  ‖HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) x : V₂)‖ ≤ dist r 0 * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂)
hbc : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ b * ‖x‖
⊢ dist r 0 * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ dist r 0 * (b * ‖x‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst_4 : MonoidWithZero R
inst_5 : DistribMulAction R V₂
inst_6 : PseudoMetricSpace R
inst_7 : IsBoundedSMul R V₂
inst_8 : MonoidWithZero R'
inst_9 : DistribMulAction R' V₂
inst_10 : PseudoMetricSpace R'
inst_11 : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this :
  ‖HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) x : V₂)‖ ≤ dist r 0 * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂)
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ b * ‖x‖

Tactic:
hb x
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst_4 : MonoidWithZero R
inst_5 : DistribMulAction R V₂
inst_6 : PseudoMetricSpace R
inst_7 : IsBoundedSMul R V₂
inst_8 : MonoidWithZero R'
inst_9 : DistribMulAction R' V₂
inst_10 : PseudoMetricSpace R'
inst_11 : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this :
  ‖HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) x : V₂)‖ ≤ dist r 0 * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂)
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ b * ‖x‖

Tactic:
exact hb x
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
R : Type u_5
inst_2 : MonoidWithZero R
inst_3 : DistribMulAction R V₂
inst_4 : PseudoMetricSpace R
inst_5 : IsBoundedSMul R V₂
r : R
f : NormedAddGroupHom V₁ V₂
⊢ (⇑(r • f) : (a : V₁) → V₂) = HSMul.hSMul (β := (a : V₁) → V₂) r (⇑f : (a : V₁) → V₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
R : Type u_5
inst_2 : MonoidWithZero R
inst_3 : DistribMulAction R V₂
inst_4 : PseudoMetricSpace R
inst_5 : IsBoundedSMul R V₂
r : R
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ (r • f : (a : V₁) → V₂) v = HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) v : V₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
n : ℕ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
rw : ‖HSMul.hSMul (β := V₂) n ((f : (a : V₁) → V₂) v : V₂)‖ ≤ (↑n : ℝ) * (b * ‖v‖)
⊢ ‖HSMul.hSMul (β := (a : V₁) → V₂) n (⇑f : (a : V₁) → V₂) v‖ ≤ n • b * ‖v‖

Tactic:
rw [Pi.smul_apply, nsmul_eq_mul, mul_assoc]

Premises used: mul_assoc, nsmul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
n : ℕ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
hbc : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ b * ‖v‖
⊢ (↑n : ℝ) * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ (↑n : ℝ) * (b * ‖v‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
n : ℕ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ b * ‖v‖

Tactic:
apply hb
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
n : ℕ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖HSMul.hSMul (β := V₂) n ((f : (a : V₁) → V₂) v : V₂)‖ ≤ (↑n : ℝ) * (b * ‖v‖)

Tactic:
exact norm_nsmul_le.trans (by gcongr; apply hb)

Premises used: norm_nsmul_le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
r : ℕ
f : NormedAddGroupHom V₁ V₂
⊢ (⇑(r • f) : (a : V₁) → V₂) = HSMul.hSMul (β := (a : V₁) → V₂) r (⇑f : (a : V₁) → V₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
r : ℕ
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ (r • f : (a : V₁) → V₂) v = HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) v : V₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
rw : ‖HSMul.hSMul (β := V₂) z ((f : (a : V₁) → V₂) v : V₂)‖ ≤ ‖z‖ * (b * ‖v‖)
⊢ ‖HSMul.hSMul (β := (a : V₁) → V₂) z (⇑f : (a : V₁) → V₂) v‖ ≤ ‖z‖ • b * ‖v‖

Tactic:
rw [Pi.smul_apply, smul_eq_mul, mul_assoc]

Premises used: mul_assoc, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
hbc : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ b * ‖v‖
⊢ ‖z‖ * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ ‖z‖ * (b * ‖v‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ b * ‖v‖

Tactic:
apply hb
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup V₁
inst_2 : SeminormedAddCommGroup V₂
inst_3 : SeminormedAddCommGroup V₃
f_1 g : NormedAddGroupHom V₁ V₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖HSMul.hSMul (β := V₂) z ((f : (a : V₁) → V₂) v : V₂)‖ ≤ ‖z‖ * (b * ‖v‖)

Tactic:
exact (norm_zsmul_le _ _).trans (by gcongr; apply hb)

Premises used: norm_zsmul_le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
r : ℤ
f : NormedAddGroupHom V₁ V₂
⊢ (⇑(r • f) : (a : V₁) → V₂) = HSMul.hSMul (β := (a : V₁) → V₂) r (⇑f : (a : V₁) → V₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
r : ℤ
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ (r • f : (a : V₁) → V₂) v = HSMul.hSMul (β := V₂) r ((f : (a : V₁) → V₂) v : V₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
ι : Type u_5
s : Finset ι
f : ι → NormedAddGroupHom V₁ V₂
⊢ Eq (α := (a : V₁) → V₂) (⇑(∑ i ∈ s, f i) : (a : V₁) → V₂) (∑ i ∈ s, (⇑(f i) : (a : V₁) → V₂))

Tactic:
map_sum coeAddHom f s

Premises used: map_sum, NormedAddGroupHom.coeAddHom
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
ι : Type u_5
s : Finset ι
f : ι → NormedAddGroupHom V₁ V₂
v : V₁
⊢ Eq.{u_3 + 1} (α := V₂) ((∑ i ∈ s, f i : (a : V₁) → V₂) v : V₂) (∑ i ∈ s, (f i : (a : V₁) → V₂) v : V₂)

Tactic:
simp only [coe_sum, Finset.sum_apply]

Premises used: Finset.sum_apply, NormedAddGroupHom.coe_sum