awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
toFun : V₁ → V₂
map_add' : ∀ (v₁ v₂ : V₁), toFun (v₁ + v₂) = toFun v₁ + toFun v₂
bound' : ∃ (C : ℝ), ∀ (v : V₁), ‖toFun v‖ ≤ C * ‖v‖
toFun_1 : V₁ → V₂
map_add'_1 : ∀ (v₁ v₂ : V₁), toFun_1 (v₁ + v₂) = toFun_1 v₁ + toFun_1 v₂
bound'_1 : ∃ (C : ℝ), ∀ (v : V₁), ‖toFun_1 v‖ ≤ C * ‖v‖
H :
  Eq (α := (a : V₁) → V₂)
    (⇑{ toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } : (a : V₁) → V₂)
    (⇑{ toFun := toFun_1, map_add' := map_add'_1, bound' := bound'_1 : NormedAddGroupHom V₁ V₂ } : (a : V₁) → V₂)
⊢ { toFun := toFun, map_add' := map_add', bound' := bound' : NormedAddGroupHom V₁ V₂ } =
    { toFun := toFun_1, map_add' := map_add'_1, bound' := bound'_1 }

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
⊢ Function.Injective (α := NormedAddGroupHom V₁ V₂) toFun

Tactic:
apply coe_inj

Premises used: NormedAddGroupHom.coe_inj
-- 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 ↔ Eq (α := (a : V₁) → V₂) (⇑f : (a : V₁) → V₂) (⇑g : (a : V₁) → V₂)

Tactic:
⟨congr_arg _, coe_inj⟩

Premises used: NormedAddGroupHom.coe_inj, congr_arg, Iff.intro
-- 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₂
H : ∀ (x : V₁), Eq.{u_3 + 1} (α := V₂) ((f : (a : V₁) → V₂) x : V₂) ((g : (a : V₁) → V₂) x : V₂)
⊢ f = g

Tactic:
coe_inj <| funext H

Premises used: NormedAddGroupHom.coe_inj, funext
-- 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.toFun = (⇑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 : V₁ → V₂
h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂
h₂ : ℝ
h₃ : ∀ (v : V₁), ‖f v‖ ≤ h₂ * ‖v‖
⊢ (⇑{ toFun := f, map_add' := h₁, bound' := ⋯ : NormedAddGroupHom V₁ V₂ } : (a : V₁) → V₂) = f

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 : V₁ →+ V₂
C : ℝ
hC : ∀ (v : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ C * ‖v‖
⊢ Eq (α := (a : V₁) → V₂) (⇑(f.mkNormedAddGroupHom C hC) : (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 : V₁ →+ V₂
C : ℝ≥0
hC : ∀ (x : V₁), nnnorm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖₊
⊢ Eq (α := (a : V₁) → V₂) (⇑(f.mkNormedAddGroupHom' C hC) : (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₂
⊢ Eq (α := (a : V₁) → V₂) (⇑f.toAddMonoidHom : (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 g : NormedAddGroupHom V₁ V₂
h : f.toAddMonoidHom = g.toAddMonoidHom
rw : Eq (α := (a : V₁) → V₂) (⇑f.toAddMonoidHom : (a : V₁) → V₂) (⇑g : (a : V₁) → V₂)
rw₁ : Eq (α := (a : V₁) → V₂) (⇑f.toAddMonoidHom : (a : V₁) → V₂) (⇑g.toAddMonoidHom : (a : V₁) → V₂)
rw₂ rw₃ : Eq (α := (a : V₁) → V₂) (⇑g.toAddMonoidHom : (a : V₁) → V₂) (⇑g.toAddMonoidHom : (a : V₁) → V₂)
⊢ Eq (α := (a : V₁) → V₂) (⇑f : (a : V₁) → V₂) (⇑g : (a : V₁) → V₂)

Tactic:
rw [← coe_toAddMonoidHom f, ← coe_toAddMonoidHom g, h]

Premises used: NormedAddGroupHom.coe_toAddMonoidHom
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : V₁ → V₂
h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂
h₂ : ∃ (C : ℝ), ∀ (v : V₁), ‖f v‖ ≤ C * ‖v‖
⊢ { toFun := f, map_add' := h₁, bound' := h₂ : NormedAddGroupHom V₁ V₂ }.toAddMonoidHom = AddMonoidHom.mk' f h₁

Tactic:
rfl

Premises used: NormedAddGroupHom.toAddMonoidHom, 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₂
⊢ ∃ (C : ℝ), 0 < C ∧ ∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖

Tactic:
let ⟨_C, hC⟩ := f.bound'
  exists_pos_bound_of_bound _ hC

Premises used: _private.0.NormedAddGroupHom.bound.match_1, exists_pos_bound_of_bound, Exists, NormedAddGroupHom.bound', And, LT.lt, OfNat.ofNat
-- 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₂
K : ℝ≥0
h : ∀ (x : V₁), ‖x‖ ≤ (↑K : ℝ) * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂)
x y : V₁
⊢ dist x y ≤ (↑K : ℝ) * dist.{u_3} (α := V₂) ((f : (a : V₁) → V₂) x : V₂) ((f : (a : V₁) → V₂) y : V₂)

Tactic:
simpa only [dist_eq_norm, map_sub] using h (x - y)

Premises used: dist_eq_norm, map_sub, HSub.hSub
-- 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₂
K : AddSubgroup V₂
C C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
k : V₂
k_in : k ∈ K
rcases :
  ∀ (g : V₁) (k_in : Membership.mem (α := V₂) K ((f : (a : V₁) → V₂) g : V₂))
    (hg : ‖g‖ ≤ C * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)),
    ∃ (g_1 : V₁),
      Eq.{u_3 + 1} (α := V₂) ((f : (a : V₁) → V₂) g_1 : V₂) ((f : (a : V₁) → V₂) g : V₂) ∧
        ‖g_1‖ ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
⊢ ∃ (g : V₁), (f : (a : V₁) → V₂) g = k ∧ ‖g‖ ≤ C' * ‖k‖

Tactic:
rcases h k k_in with ⟨g, rfl, hg⟩

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₂
K : AddSubgroup V₂
C C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
g : V₁
k_in : Membership.mem (α := V₂) K ((f : (a : V₁) → V₂) g : V₂)
hg : ‖g‖ ≤ C * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
right : ‖g‖ ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
⊢ ∃ (g_1 : V₁),
    Eq.{u_3 + 1} (α := V₂) ((f : (a : V₁) → V₂) g_1 : V₂) ((f : (a : V₁) → V₂) g : V₂) ∧
      ‖g_1‖ ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)

Tactic:
use g, 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₂
K : AddSubgroup V₂
C C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
g : V₁
k_in : Membership.mem (α := V₂) K ((f : (a : V₁) → V₂) g : V₂)
hg : ‖g‖ ≤ C * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
pos :
  ∀ (Hg : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂) = 0),
    ‖g‖ ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
neg :
  ∀ (Hg : ¬norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂) = 0),
    ‖g‖ ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
⊢ ‖g‖ ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)

Tactic:
by_cases Hg : ‖f g‖ = 0

Premises used: DFunLike.coe
-- 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₂
K : AddSubgroup V₂
C C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
g : V₁
k_in : Membership.mem (α := V₂) K ((f : (a : V₁) → V₂) g : V₂)
hg : ‖g‖ ≤ C * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
Hg : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂) = 0
⊢ ‖g‖ ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)

Tactic:
simpa [Hg] using hg
-- 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₂
K : AddSubgroup V₂
C C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
g : V₁
k_in : Membership.mem (α := V₂) K ((f : (a : V₁) → V₂) g : V₂)
hg : ‖g‖ ≤ C * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
Hg : ¬norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂) = 0
ha : 0 ≤ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
⊢ C * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂) ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)

Tactic:
gcongr
-- 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₂
K : AddSubgroup V₂
C C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
g : V₁
k_in : Membership.mem (α := V₂) K ((f : (a : V₁) → V₂) g : V₂)
hg : ‖g‖ ≤ C * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)
Hg : ¬norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂) = 0
⊢ ‖g‖ ≤ C' * norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) g : V₂)

Tactic:
exact hg.trans (by gcongr)

Premises used: 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₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ ∃ C' > 0, f.SurjectiveOnWith K C'

Tactic:
⟨|C| + 1, ?_, ?_⟩

Premises used: abs, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- 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₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
refine_1 : |C| + 1 > 0
refine_2 : f.SurjectiveOnWith K (|C| + 1)
⊢ ∃ C' > 0, f.SurjectiveOnWith K C'

Tactic:
refine ⟨|C| + 1, ?_, ?_⟩
-- 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₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
linarith : |C| + 1 ≤ 0 → -1 + (|C| + 1 - 0) + (0 - |C|) = 0
⊢ |C| + 1 > 0

Tactic:
linarith [abs_nonneg C]

Premises used: abs_nonneg
-- 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₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
refine_2 : C ≤ |C| + 1
⊢ f.SurjectiveOnWith K (|C| + 1)

Tactic:
apply h.mono

Premises used: NormedAddGroupHom.SurjectiveOnWith.mono
-- 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₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
linarith : |C| + 1 < C → -1 + (|C| + 1 - C) + (C - |C|) = 0
⊢ C ≤ |C| + 1

Tactic:
linarith [le_abs_self C]

Premises used: le_abs_self
-- 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₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ Set.SurjOn.{u_2, u_3} (α := V₁) (⇑f : (a : V₁) → V₂) Set.univ (↑K : Set V₂)

Tactic:
fun x hx =>
  (h x hx).imp fun _a ⟨ha, _⟩ => ⟨Set.mem_univ _, ha⟩

Premises used: Set.Mem, setOf, Set.SurjOn, Exists.imp, Set.Subset, Set.image
-- 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‖ = sInf {c : ℝ | 0 ≤ c ∧ ∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ c * ‖x‖}

Tactic:
rfl

Premises used: NormedAddGroupHom.opNorm, 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₂
⊢ ∃ (c : ℝ),
    Membership.mem (γ := Set ℝ)
      {c : ℝ | 0 ≤ c ∧ ∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ c * ‖x‖} c

Tactic:
let ⟨M, hMp, hMb⟩ := f.bound
  ⟨M, le_of_lt hMp, hMb⟩

Premises used: setOf, le_of_lt, Membership.mem, Exists, _private.0.NormedAddGroupHom.bounds_nonempty.match_1, LE.le, NormedAddGroupHom.bound, And, And.intro, Exists.intro, OfNat.ofNat
-- 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₂
⊢ BddBelow (α := ℝ) {c : ℝ | 0 ≤ c ∧ ∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ c * ‖x‖}

Tactic:
⟨0, fun _ ⟨hn, _⟩ => hn⟩

Premises used: _private.0.NormedAddGroupHom.bounds_bddBelow.match_1, LE.le, Set.Nonempty, BddBelow, Exists.intro, OfNat.ofNat
-- 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₂
⊢ 0 ≤ ‖f‖

Tactic:
le_csInf bounds_nonempty fun _ ⟨hx, _⟩ => hx

Premises used: le_csInf, _private.0.NormedAddGroupHom.bounds_bddBelow.match_1, NormedAddGroupHom.opNorm, LE.le, NormedAddGroupHom.bounds_nonempty, OfNat.ofNat
-- 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₂
x : V₁
obtain :
  ∀ (C : ℝ) (_Cpos : 0 < C) (hC : ∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖),
    norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖

Tactic:
obtain ⟨C, _Cpos, hC⟩ := f.bound

Premises used: NormedAddGroupHom.bound
-- 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₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖

Tactic:
replace hC := hC x
-- 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₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
pos : ∀ (h : ‖x‖ = 0), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖
neg : ∀ (h : ¬‖x‖ = 0), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖

Tactic:
by_cases h : ‖x‖ = 0
-- 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₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
h : ‖x‖ = 0
pos :
  ∀ (hC : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * 0) (h : ‖x‖ = 0),
    norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * 0
pos₁ pos₂ pos₃ pos₄ :
  ∀ (hC : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ 0) (h : ‖x‖ = 0),
    norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ 0
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖

Tactic:
rwa [h, mul_zero] at hC ⊢

Premises used: MulZeroClass.mul_zero
-- 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₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
h : ¬‖x‖ = 0
⊢ 0 < ‖x‖

Tactic:
have hlt : 0 < ‖x‖ := lt_of_le_of_ne (norm_nonneg x) (Ne.symm h)
-- 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₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
h : ¬‖x‖ = 0
hlt : 0 < ‖x‖
c : ℝ
h_1 :
  Membership.mem (γ := Set ℝ) {c : ℝ | 0 ≤ c ∧ ∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ c * ‖x‖}
    c
left : 0 ≤ c
hc : ∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ c * ‖x‖
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ c * ‖x‖

Tactic:
apply hc
-- 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₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
h : ¬‖x‖ = 0
hlt : 0 < ‖x‖
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖f‖ * ‖x‖

Tactic:
exact
    (div_le_iff₀ hlt).mp
      (le_csInf bounds_nonempty fun c ⟨_, hc⟩ => (div_le_iff₀ hlt).mpr <| by apply hc)

Premises used: div_le_iff₀, le_csInf, NormedAddGroupHom.bounds_nonempty, Iff.mp
-- 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₂
c : ℝ
x : V₁
h : ‖x‖ ≤ c
ha : 0 ≤ ‖f‖
⊢ ‖f‖ * ‖x‖ ≤ ‖f‖ * c

Tactic:
gcongr
-- 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₂
c : ℝ
x : V₁
h : ‖x‖ ≤ c
⊢ 0 ≤ ‖f‖

Tactic:
f.opNorm_nonneg

Premises used: 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 : NormedAddGroupHom V₁ V₂
c : ℝ
x : V₁
h : ‖x‖ ≤ c
⊢ 0 ≤ ‖f‖

Tactic:
exact f.opNorm_nonneg

Premises used: 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 : NormedAddGroupHom V₁ V₂
c : ℝ
h : ‖f‖ ≤ c
x : V₁
ha : 0 ≤ ‖x‖
⊢ ‖f‖ * ‖x‖ ≤ c * ‖x‖

Tactic:
gcongr
-- 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₂
x y : V₁
rw :
  norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) (x - y) : V₂) ≤
    (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ‖f‖ ⋯) : ℝ) * ‖x - y‖
⊢ dist.{u_3} (α := V₂) ((f : (a : V₁) → V₂) x : V₂) ((f : (a : V₁) → V₂) y : V₂) ≤
    (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ‖f‖ ⋯) : ℝ) * dist x y

Tactic:
rw [dist_eq_norm, dist_eq_norm, ← map_sub]

Premises used: dist_eq_norm, map_sub
-- 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₂
x y : V₁
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) (x - y) : V₂) ≤
    (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ‖f‖ ⋯) : ℝ) * ‖x - y‖

Tactic:
apply le_opNorm

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₂
⊢ UniformContinuous.{u_2, u_3} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)

Tactic:
f.lipschitz.uniformContinuous

Premises used: LipschitzWith.uniformContinuous, NormedAddGroupHom.lipschitz
-- 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₂
⊢ Continuous.{u_2, u_3} (X := V₁) (Y := V₂) (⇑f : (a : V₁) → V₂)

Tactic:
f.uniformContinuous.continuous

Premises used: NormedAddGroupHom.uniformContinuous, UniformContinuous.continuous
-- 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₂
x : V₁
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) / ‖x‖ ≤ ‖f‖

Tactic:
div_le_of_le_mul₀ (norm_nonneg _) f.opNorm_nonneg (le_opNorm _ _)

Premises used: div_le_of_le_mul₀, NormedAddGroupHom.le_opNorm, NormedAddGroupHom.opNorm_nonneg, norm_nonneg
-- 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₂
M : ℝ
hMp : 0 ≤ M
hM : ∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ M * ‖x‖
⊢ ‖f‖ ≤ M

Tactic:
csInf_le bounds_bddBelow ⟨hMp, hM⟩

Premises used: NormedAddGroupHom.opNorm, NormedAddGroupHom.bounds_bddBelow, And.intro, csInf_le
-- 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₂
M : ℝ
M_nonneg : 0 ≤ M
h_above : ∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ M * ‖x‖
h_below : ∀ N ≥ 0, (∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ N * ‖x‖) → M ≤ N
⊢ ‖f‖ = M

Tactic:
le_antisymm (f.opNorm_le_bound M_nonneg h_above)
    ((le_csInf_iff NormedAddGroupHom.bounds_bddBelow ⟨M, M_nonneg, h_above⟩).mpr
      fun N ⟨N_nonneg, hN⟩ => h_below N N_nonneg hN)

Premises used: Iff.mpr, le_csInf_iff, _private.0.NormedAddGroupHom.bounds_bddBelow.match_1, LE.le, NormedAddGroupHom.opNorm_le_bound, le_antisymm, NormedAddGroupHom.bounds_bddBelow, And.intro, Exists.intro
-- 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₂
K : ℝ≥0
hf : LipschitzWith.{u_2, u_3} (α := V₁) (β := V₂) K (⇑f : (a : V₁) → V₂)
x : V₁
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ (↑K : ℝ) * ‖x‖

Tactic:
simpa only [dist_zero_right, map_zero] using hf.dist_le_mul x 0

Premises used: LipschitzWith.dist_le_mul, map_zero, OfNat.ofNat, dist_zero_right
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : V₁ →+ V₂
C : ℝ
hC : 0 ≤ C
h : ∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
⊢ ‖f.mkNormedAddGroupHom C h‖ ≤ C

Tactic:
opNorm_le_bound _ hC h

Premises used: NormedAddGroupHom.opNorm_le_bound
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : V₁ →+ V₂
K : ℝ≥0
h : LipschitzWith.{u_2, u_3} (α := V₁) (β := V₂) K (⇑f : (a : V₁) → V₂)
⊢ ‖ofLipschitz f h‖ ≤ (↑K : ℝ)

Tactic:
mkNormedAddGroupHom_norm_le f K.coe_nonneg _

Premises used: NormedAddGroupHom.mkNormedAddGroupHom_norm_le, NormedAddGroupHom.ofLipschitz, NNReal.coe_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : V₁ →+ V₂
C : ℝ
h : ∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
x : V₁
hbc : C ≤ max C 0
⊢ C * ‖x‖ ≤ max C 0 * ‖x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_2
V₂ : Type u_3
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : V₁ →+ V₂
C : ℝ
h : ∀ (x : V₁), norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ C * ‖x‖
x : V₁
⊢ C ≤ max C 0

Tactic:
apply le_max_left

Premises used: le_max_left
-- 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₁
h₁ : norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ ‖f‖ * ‖v‖
h₂ : norm.{u_3} (E := V₂) ((g : (a : V₁) → V₂) v : V₂) ≤ ‖g‖ * ‖v‖
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) + norm.{u_3} (E := V₂) ((g : (a : V₁) → V₂) v : V₂) ≤
    ‖f‖ * ‖v‖ + ‖g‖ * ‖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_1 f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ norm.{u_3} (E := V₂) ((f : (a : V₁) → V₂) v : V₂) ≤ ‖f‖ * ‖v‖

Tactic:
apply le_opNorm

Premises used: NormedAddGroupHom.le_opNorm