[GOAL]
V : SemiNormedGroupCat
v : ↑V
⊢ ‖(fun v => ↑↑V v) v‖ ≤ 1 * ‖v‖
[PROOFSTEP]
simp
[GOAL]
V : SemiNormedGroupCat
W : SemiNormedGroupCat
⊢ ∀ (P Q R : SemiNormedGroupCat) (f f' : P ⟶ Q) (g : Q ⟶ R), (f + f') ≫ g = f ≫ g + f' ≫ g
[PROOFSTEP]
intros _ Q _ f f' g
[GOAL]
V : SemiNormedGroupCat
W : SemiNormedGroupCat
P✝ Q R✝ : SemiNormedGroupCat
f f' : P✝ ⟶ Q
g : Q ⟶ R✝
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g
[PROOFSTEP]
ext x
[GOAL]
case h
V : SemiNormedGroupCat
W : SemiNormedGroupCat
P✝ Q R✝ : SemiNormedGroupCat
f f' : P✝ ⟶ Q
g : Q ⟶ R✝
x : ↑P✝
⊢ ↑((f + f') ≫ g) x = ↑(f ≫ g + f' ≫ g) x
[PROOFSTEP]
rw [NormedAddGroupHom.add_apply, CategoryTheory.comp_apply, CategoryTheory.comp_apply, CategoryTheory.comp_apply,
  @NormedAddGroupHom.add_apply _ _ (_) (_)]
[GOAL]
case h
V : SemiNormedGroupCat
W : SemiNormedGroupCat
P✝ Q R✝ : SemiNormedGroupCat
f f' : P✝ ⟶ Q
g : Q ⟶ R✝
x : ↑P✝
⊢ ↑g (↑f x + ↑f' x) = ↑g (↑f x) + ↑g (↑f' x)
[PROOFSTEP]
convert map_add g (f x) (f' x)
[GOAL]
V : SemiNormedGroupCat
W : SemiNormedGroupCat
⊢ ∀ (P Q R : SemiNormedGroupCat) (f : P ⟶ Q) (g g' : Q ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g'
[PROOFSTEP]
intros
[GOAL]
V : SemiNormedGroupCat
W : SemiNormedGroupCat
P✝ Q✝ R✝ : SemiNormedGroupCat
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ f✝ ≫ (g✝ + g'✝) = f✝ ≫ g✝ + f✝ ≫ g'✝
[PROOFSTEP]
ext
  -- Porting note: failing simps probably due to instance synthesis issues with concrete
      -- cats; see the gymnastics below for what used to be
      -- simp only [add_apply, comp_apply. map_add]
[GOAL]
case h
V : SemiNormedGroupCat
W : SemiNormedGroupCat
P✝ Q✝ R✝ : SemiNormedGroupCat
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
x✝ : ↑P✝
⊢ ↑(f✝ ≫ (g✝ + g'✝)) x✝ = ↑(f✝ ≫ g✝ + f✝ ≫ g'✝) x✝
[PROOFSTEP]
rw [NormedAddGroupHom.add_apply, CategoryTheory.comp_apply, CategoryTheory.comp_apply, CategoryTheory.comp_apply,
  @NormedAddGroupHom.add_apply _ _ (_) (_)]
