awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
h : ‖f‖ ≤ 1
v : V
⊢ norm.{u_2} (E := W) ((f : (a : V) → W) v : W) ≤ ‖v‖

Tactic:
simpa using le_of_opNorm_le f h v

Premises used: NormedAddGroupHom.le_of_opNorm_le
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
v : V₁
⊢ norm.{u_4} (E := V₂) ((0 : (a : V₁) → V₂) v : V₂) ≤ ‖v‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
⊢ NormNoninc (NormedAddGroupHom.id V)

Tactic:
fun _v => le_rfl

Premises used: le_rfl, NormedAddGroupHom.NormNoninc
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
hg : g.NormNoninc
hf : f.NormNoninc
⊢ (g.comp f).NormNoninc

Tactic:
fun v => (hg (f v)).trans (hf v)

Premises used: LE.le.trans, DFunLike.coe, NormedAddGroupHom.NormNoninc
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
h : (-f).NormNoninc
x : V₁
⊢ norm.{u_4} (E := V₂) ((f : (a : V₁) → V₂) x : V₂) ≤ ‖x‖

Tactic:
simpa using h x
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
hf : Isometry.{u_1, u_2} (α := V) (β := W) (⇑f : (a : V) → W)
v : V
⊢ norm.{u_2} (E := W) ((f : (a : V) → W) v : W) = ‖v‖

Tactic:
(AddMonoidHomClass.isometry_iff_norm f).mp hf v

Premises used: AddMonoidHomClass.isometry_iff_norm, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
⊢ Isometry (α := V) (β := V) (⇑(id V) : (a : V) → V)

Tactic:
_root_.isometry_id

Premises used: isometry_id
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
hg : Isometry.{u_4, u_5} (α := V₂) (β := V₃) (⇑g : (a : V₂) → V₃)
hf : Isometry.{u_3, u_4} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)
⊢ Isometry.{u_3, u_5} (α := V₁) (β := V₃) (⇑(g.comp f) : (a : V₁) → V₃)

Tactic:
hg.comp hf

Premises used: Isometry.comp
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
hf : Isometry.{u_1, u_2} (α := V) (β := W) (⇑f : (a : V) → W)
⊢ f.NormNoninc

Tactic:
fun v =>
  le_of_eq <| norm_eq_of_isometry hf v

Premises used: NormedAddGroupHom.norm_eq_of_isometry, le_of_eq, NormedAddGroupHom.NormNoninc
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
H :
  ∀ (x : ↥(f.equalizer g)),
    Eq.{u_2 + 1} (α := W) ((f.comp (ι f g) : (a : ↥(f.equalizer g)) → W) x : W)
      ((g.comp (ι f g) : (a : ↥(f.equalizer g)) → W) x : W)
⊢ f.comp (ι f g) = g.comp (ι f g)

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
x : ↥(f.equalizer g)
H : Eq.{u_2 + 1} (α := W) ((f - g : (a : V) → W) ((ι f g : (a : ↥(f.equalizer g)) → V) x : V) : W) (0 : W)
⊢ Eq.{u_2 + 1} (α := W) ((f.comp (ι f g) : (a : ↥(f.equalizer g)) → W) x : W)
    ((g.comp (ι f g) : (a : ↥(f.equalizer g)) → W) x : W)

Tactic:
rw [comp_apply, comp_apply, ← sub_eq_zero, ← NormedAddGroupHom.sub_apply]

Premises used: sub_eq_zero, NormedAddGroupHom.sub_apply, NormedAddGroupHom.comp_apply
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
x : ↥(f.equalizer g)
⊢ Eq.{u_2 + 1} (α := W) ((f - g : (a : V) → W) ((ι f g : (a : ↥(f.equalizer g)) → V) x : V) : W) (0 : W)

Tactic:
x.2

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Subtype.property
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
x : ↥(f.equalizer g)
⊢ Eq.{u_2 + 1} (α := W) ((f - g : (a : V) → W) ((ι f g : (a : ↥(f.equalizer g)) → V) x : V) : W) (0 : W)

Tactic:
exact x.2

Premises used: Subtype.property
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v : V₁
rw :
  HSub.hSub (α := W) (β := W) ((f : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
      ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W) =
    0
rw₁ :
  Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
    ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
rw₂ : Eq.{u_2 + 1} (α := W) ((f.comp φ : (a : V₁) → W) v : W) ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
rw₃ : Eq.{u_2 + 1} (α := W) ((g.comp φ : (a : V₁) → W) v : W) ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
rw₄ rw₅ :
  Eq.{u_2 + 1} (α := W) ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
    ((g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W)
⊢ Eq.{u_2 + 1} (α := W) ((f - g : (a : V) → W) ((φ : (a : V₁) → V) v : V) : W) (0 : W)

Tactic:
rw [NormedAddGroupHom.sub_apply, sub_eq_zero, ← comp_apply, h, comp_apply]

Premises used: sub_eq_zero, NormedAddGroupHom.sub_apply, NormedAddGroupHom.comp_apply
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v₁ v₂ : V₁
a :
  (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) (v₁ + v₂)) ⋯) : V) =
    (↑(HAdd.hAdd (α := ↥(f.equalizer g)) (β := ↥(f.equalizer g))
          (Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) v₁) ⋯ : ↥(f.equalizer g))
          (Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) v₂) ⋯ : ↥(f.equalizer g))) :
      V)
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) (v₁ + v₂)) ⋯ =
    HAdd.hAdd (α := ↥(f.equalizer g)) (β := ↥(f.equalizer g))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) v₁) ⋯ : ↥(f.equalizer g))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) v₂) ⋯ : ↥(f.equalizer g))

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v₁ v₂ : V₁
⊢ (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) (v₁ + v₂)) ⋯) : V) =
    (↑(HAdd.hAdd (α := ↥(f.equalizer g)) (β := ↥(f.equalizer g))
          (Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) v₁) ⋯ : ↥(f.equalizer g))
          (Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) v₂) ⋯ : ↥(f.equalizer g))) :
      V)

Tactic:
simp only [map_add, AddSubgroup.coe_add]

Premises used: map_add, AddSubgroup.coe_add
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
obtain :
  ∀ (C : ℝ) (_C_pos : 0 < C) (hC : ∀ (x : V₁), norm.{u_1} (E := V) ((φ : (a : V₁) → V) x : V) ≤ C * ‖x‖),
    ∃ (C : ℝ),
      ∀ (v : V₁),
        norm.{u_1} (E := ↥(f.equalizer g))
            (Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) v) ⋯ : ↥(f.equalizer g)) ≤
          C * ‖v‖
⊢ ∃ (C : ℝ),
    ∀ (v : V₁),
      norm.{u_1} (E := ↥(f.equalizer g))
          (Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) v) ⋯ : ↥(f.equalizer g)) ≤
        C * ‖v‖

Tactic:
obtain ⟨C, _C_pos, hC⟩ := φ.bound

Premises used: NormedAddGroupHom.bound
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
C : ℝ
_C_pos : 0 < C
hC : ∀ (x : V₁), norm.{u_1} (E := V) ((φ : (a : V₁) → V) x : V) ≤ C * ‖x‖
⊢ ∃ (C : ℝ),
    ∀ (v : V₁),
      norm.{u_1} (E := ↥(f.equalizer g))
          (Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) v) ⋯ : ↥(f.equalizer g)) ≤
        C * ‖v‖

Tactic:
⟨C, hC⟩

Premises used: Exists.intro
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
C : ℝ
_C_pos : 0 < C
hC : ∀ (x : V₁), norm.{u_1} (E := V) ((φ : (a : V₁) → V) x : V) ≤ C * ‖x‖
⊢ ∃ (C : ℝ),
    ∀ (v : V₁),
      norm.{u_1} (E := ↥(f.equalizer g))
          (Subtype.mk (p := fun (x : V) ↦ x ∈ f.equalizer g) ((φ : (a : V₁) → V) v) ⋯ : ↥(f.equalizer g)) ≤
        C * ‖v‖

Tactic:
exact ⟨C, hC⟩
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
f g : NormedAddGroupHom V W
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
H : ∀ (x : V₁), Eq.{u_1 + 1} (α := V) (((ι f g).comp (lift φ h) : (a : V₁) → V) x : V) ((φ : (a : V₁) → V) x : V)
⊢ (ι f g).comp (lift φ h) = φ

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
f g : NormedAddGroupHom V W
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
x : V₁
⊢ Eq.{u_1 + 1} (α := V) (((ι f g).comp (lift φ h) : (a : V₁) → V) x : V) ((φ : (a : V₁) → V) x : V)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
ψ : NormedAddGroupHom.{u_3, u_1} V₁ ↥(f.equalizer g)
rw : (f.comp (ι f g)).comp ψ = g.comp ((ι f g).comp ψ)
rw₁ : (f.comp (ι f g)).comp ψ = (g.comp (ι f g)).comp ψ
rw₂ rw₃ : (g.comp (ι f g)).comp ψ = (g.comp (ι f g)).comp ψ
⊢ f.comp ((ι f g).comp ψ) = g.comp ((ι f g).comp ψ)

Tactic:
rw [← comp_assoc, ← comp_assoc, comp_ι_eq]

Premises used: NormedAddGroupHom.comp_assoc, NormedAddGroupHom.Equalizer.comp_ι_eq
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : { φ : NormedAddGroupHom V₁ V // f.comp φ = g.comp φ }
⊢ (fun (ψ : NormedAddGroupHom.{u_3, u_1} V₁ ↥(f.equalizer g)) ↦
        (Subtype.mk (p := fun (φ : NormedAddGroupHom V₁ V) ↦ f.comp φ = g.comp φ) ((ι f g).comp ψ) ⋯ :
          { φ : NormedAddGroupHom V₁ V // f.comp φ = g.comp φ }))
      ((fun (φ : { φ : NormedAddGroupHom V₁ V // f.comp φ = g.comp φ }) ↦ lift (↑φ : NormedAddGroupHom V₁ V) ⋯) φ) =
    φ

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
simp : (ψ.comp f₁).comp (ι f₁ g₁) = (ψ.comp g₁).comp (ι f₁ g₁)
⊢ f₂.comp (φ.comp (ι f₁ g₁)) = g₂.comp (φ.comp (ι f₁ g₁))

Tactic:
simp only [← comp_assoc, ← hf, ← hg]

Premises used: NormedAddGroupHom.comp_assoc
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
inst_3 : SeminormedAddCommGroup V₂
inst_4 : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_5 : SeminormedAddCommGroup W₁
inst_6 : SeminormedAddCommGroup W₂
inst_7 : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
⊢ (ψ.comp f₁).comp (ι f₁ g₁) = (ψ.comp g₁).comp (ι f₁ g₁)

Tactic:
simp only [comp_assoc, comp_ι_eq f₁ g₁]

Premises used: NormedAddGroupHom.comp_assoc, NormedAddGroupHom.Equalizer.comp_ι_eq
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
W₁ : Type u_6
W₂ : Type u_7
inst_2 : SeminormedAddCommGroup W₁
inst_3 : SeminormedAddCommGroup W₂
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
⊢ (ι f₂ g₂).comp (map φ ψ hf hg) = φ.comp (ι f₁ g₁)

Tactic:
ι_comp_lift _ _

Premises used: NormedAddGroupHom.Equalizer.map, NormedAddGroupHom.Equalizer.ι_comp_lift
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
inst : SeminormedAddCommGroup V₁
W₁ : Type u_6
inst_1 : SeminormedAddCommGroup W₁
f₁ g₁ : NormedAddGroupHom V₁ W₁
H :
  ∀ (x : ↥(f₁.equalizer g₁)),
    Eq.{u_3 + 1} (α := V₁) (↑((map (id V₁) (id W₁) ⋯ ⋯ : (a : ↥(f₁.equalizer g₁)) → ↥(f₁.equalizer g₁)) x) : V₁)
      (↑((id ↥(f₁.equalizer g₁) : (a : ↥(f₁.equalizer g₁)) → ↥(f₁.equalizer g₁)) x) : V₁)
⊢ Eq (α := NormedAddGroupHom ↥(f₁.equalizer g₁) ↥(f₁.equalizer g₁)) (map (id V₁) (id W₁) ⋯ ⋯) (id ↥(f₁.equalizer g₁))

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
inst : SeminormedAddCommGroup V₁
W₁ : Type u_6
inst_1 : SeminormedAddCommGroup W₁
f₁ g₁ : NormedAddGroupHom V₁ W₁
x : ↥(f₁.equalizer g₁)
⊢ Eq.{u_3 + 1} (α := V₁) (↑((map (id V₁) (id W₁) ⋯ ⋯ : (a : ↥(f₁.equalizer g₁)) → ↥(f₁.equalizer g₁)) x) : V₁)
    (↑((id ↥(f₁.equalizer g₁) : (a : ↥(f₁.equalizer g₁)) → ↥(f₁.equalizer g₁)) x) : V₁)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_3 : SeminormedAddCommGroup W₁
inst_4 : SeminormedAddCommGroup W₂
inst_5 : SeminormedAddCommGroup W₃
f₁ : NormedAddGroupHom V₁ W₁
f₂ : NormedAddGroupHom V₂ W₂
f₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
rw : ψ'.comp (ψ.comp f₁) = f₃.comp (φ'.comp φ)
rw₁ : ψ'.comp (f₂.comp φ) = f₃.comp (φ'.comp φ)
rw₂ : (ψ'.comp f₂).comp φ = f₃.comp (φ'.comp φ)
rw₃ : (f₃.comp φ').comp φ = f₃.comp (φ'.comp φ)
rw₄ rw₅ : f₃.comp (φ'.comp φ) = f₃.comp (φ'.comp φ)
⊢ (ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)

Tactic:
rw [comp_assoc, hf, ← comp_assoc, hf', comp_assoc]

Premises used: NormedAddGroupHom.comp_assoc
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_3 : SeminormedAddCommGroup W₁
inst_4 : SeminormedAddCommGroup W₂
inst_5 : SeminormedAddCommGroup W₃
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
hg' : ψ'.comp g₂ = g₃.comp φ'
H :
  ∀ (x : ↥(f₁.equalizer g₁)),
    Eq.{u_5 + 1} (α := V₃)
      (↑(((map φ' ψ' hf' hg').comp (map φ ψ hf hg) : (a : ↥(f₁.equalizer g₁)) → ↥(f₃.equalizer g₃)) x) : V₃)
      (↑((map (φ'.comp φ) (ψ'.comp ψ) ⋯ ⋯ : (a : ↥(f₁.equalizer g₁)) → ↥(f₃.equalizer g₃)) x) : V₃)
⊢ (map φ' ψ' hf' hg').comp (map φ ψ hf hg) = map (φ'.comp φ) (ψ'.comp ψ) ⋯ ⋯

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
inst_2 : SeminormedAddCommGroup V₃
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst_3 : SeminormedAddCommGroup W₁
inst_4 : SeminormedAddCommGroup W₂
inst_5 : SeminormedAddCommGroup W₃
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
hg' : ψ'.comp g₂ = g₃.comp φ'
x : ↥(f₁.equalizer g₁)
⊢ Eq.{u_5 + 1} (α := V₃)
    (↑(((map φ' ψ' hf' hg').comp (map φ ψ hf hg) : (a : ↥(f₁.equalizer g₁)) → ↥(f₃.equalizer g₃)) x) : V₃)
    (↑((map (φ'.comp φ) (ψ'.comp ψ) ⋯ ⋯ : (a : ↥(f₁.equalizer g₁)) → ↥(f₃.equalizer g₃)) x) : V₃)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
⊢ (ι f g).NormNoninc

Tactic:
fun _v => le_rfl

Premises used: le_rfl, NormedAddGroupHom.NormNoninc
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
f g : NormedAddGroupHom V W
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
hφ : φ.NormNoninc
⊢ (lift φ h).NormNoninc

Tactic:
hφ

Premises used: NormedAddGroupHom.NormNoninc, NormedAddGroupHom.Equalizer.lift
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V : Type u_1
W : Type u_2
V₁ : Type u_3
inst : SeminormedAddCommGroup V
inst_1 : SeminormedAddCommGroup W
inst_2 : SeminormedAddCommGroup V₁
f g : NormedAddGroupHom V W
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
C : ℝ
hφ : ‖φ‖ ≤ C
⊢ ‖lift φ h‖ ≤ C

Tactic:
hφ

Premises used: setOf, NormedAddGroupHom.opNorm, NormedAddGroupHom.Equalizer.lift
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
W₁ : Type u_6
W₂ : Type u_7
inst_2 : SeminormedAddCommGroup W₁
inst_3 : SeminormedAddCommGroup W₂
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
hφ : φ.NormNoninc
⊢ (map φ ψ hf hg).NormNoninc

Tactic:
lift_normNoninc _ _ <| hφ.comp ι_normNoninc

Premises used: NormedAddGroupHom.Equalizer.ι_normNoninc, NormedAddGroupHom.Equalizer.map, NormedAddGroupHom.Equalizer.lift_normNoninc, NormedAddGroupHom.NormNoninc.comp
-- Module: Mathlib.Analysis.Normed.Group.Hom
Goal:
V₁ : Type u_3
V₂ : Type u_4
inst : SeminormedAddCommGroup V₁
inst_1 : SeminormedAddCommGroup V₂
W₁ : Type u_6
W₂ : Type u_7
inst_2 : SeminormedAddCommGroup W₁
inst_3 : SeminormedAddCommGroup W₂
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
C : ℝ
hφ : ‖φ.comp (ι f₁ g₁)‖ ≤ C
⊢ ‖map φ ψ hf hg‖ ≤ C

Tactic:
norm_lift_le _ _ _ hφ

Premises used: NormedAddGroupHom.Equalizer.map, NormedAddGroupHom.Equalizer.norm_lift_le
-- Module: Mathlib.Analysis.Normed.Group.Rat
Goal:
r₁ r₂ : ℚ
simp : |HSub.hSub (α := ℝ) (↑r₁ : ℝ) (↑r₂ : ℝ)| = |HAdd.hAdd (α := ℝ) (-(↑r₁ : ℝ)) (↑r₂ : ℝ)|
⊢ dist r₁ r₂ = norm (E := ℝ) (↑(-r₁ + r₂) : ℝ)

Tactic:
simp only [dist_eq, norm, cast_add, cast_neg]

Premises used: Norm.norm, Rat.dist_eq, Rat.cast_add, Rat.cast_neg
-- Module: Mathlib.Analysis.Normed.Group.Rat
Goal:
r₁ r₂ : ℚ
rw : |HSub.hSub (α := ℝ) (↑r₂ : ℝ) (↑r₁ : ℝ)| = |HAdd.hAdd (α := ℝ) (-(↑r₁ : ℝ)) (↑r₂ : ℝ)|
⊢ |HSub.hSub (α := ℝ) (↑r₁ : ℝ) (↑r₂ : ℝ)| = |HAdd.hAdd (α := ℝ) (-(↑r₁ : ℝ)) (↑r₂ : ℝ)|

Tactic:
rw [← abs_neg, neg_sub]

Premises used: abs_neg, neg_sub
-- Module: Mathlib.Analysis.Normed.Group.Rat
Goal:
r₁ r₂ : ℚ
⊢ |HSub.hSub (α := ℝ) (↑r₂ : ℝ) (↑r₁ : ℝ)| = |HAdd.hAdd (α := ℝ) (-(↑r₁ : ℝ)) (↑r₂ : ℝ)|

Tactic:
abel_nf
-- Module: Mathlib.Analysis.Normed.Group.Rat
Goal:
r : ℚ
⊢ norm (E := ℝ) (↑r : ℝ) = ‖r‖

Tactic:
rfl

Premises used: rfl