[GOAL]
⊢ ConcreteCategory SemiNormedGroupCat
[PROOFSTEP]
dsimp [SemiNormedGroupCat]
[GOAL]
⊢ ConcreteCategory (Bundled SeminormedAddCommGroup)
[PROOFSTEP]
infer_instance
[GOAL]
V W : SemiNormedGroupCat
f g : V ⟶ W
h : (forget SemiNormedGroupCat).map f = (forget SemiNormedGroupCat).map g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
V W : SemiNormedGroupCat
g : V ⟶ W
toFun✝ : ↑V → ↑W
map_add'✝ : ∀ (v₁ v₂ : ↑V), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : ↑V), ‖toFun✝ v‖ ≤ C * ‖v‖
h :
  (forget SemiNormedGroupCat).map { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } =
    (forget SemiNormedGroupCat).map g
⊢ { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
V W : SemiNormedGroupCat
toFun✝¹ : ↑V → ↑W
map_add'✝¹ : ∀ (v₁ v₂ : ↑V), toFun✝¹ (v₁ + v₂) = toFun✝¹ v₁ + toFun✝¹ v₂
bound'✝¹ : ∃ C, ∀ (v : ↑V), ‖toFun✝¹ v‖ ≤ C * ‖v‖
toFun✝ : ↑V → ↑W
map_add'✝ : ∀ (v₁ v₂ : ↑V), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : ↑V), ‖toFun✝ v‖ ≤ C * ‖v‖
h :
  (forget SemiNormedGroupCat).map { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    (forget SemiNormedGroupCat).map { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }
⊢ { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }
[PROOFSTEP]
congr
[GOAL]
V : SemiNormedGroupCat
inst✝ : Subsingleton ↑V
⊢ Limits.IsZero V
[PROOFSTEP]
refine' ⟨fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩⟩
[GOAL]
case refine'_1
V : SemiNormedGroupCat
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat
f : V ⟶ X
⊢ f = default
[PROOFSTEP]
ext x
[GOAL]
case refine'_1.h
V : SemiNormedGroupCat
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat
f : V ⟶ X
x : ↑V
⊢ ↑f x = ↑default x
[PROOFSTEP]
have : x = 0 := Subsingleton.elim _ _
[GOAL]
case refine'_1.h
V : SemiNormedGroupCat
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat
f : V ⟶ X
x : ↑V
this : x = 0
⊢ ↑f x = ↑default x
[PROOFSTEP]
simp only [this, map_zero]
[GOAL]
case refine'_2
V : SemiNormedGroupCat
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat
f : X ⟶ V
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case refine'_2.h
V : SemiNormedGroupCat
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat
f : X ⟶ V
x✝ : ↑X
⊢ ↑f x✝ = ↑default x✝
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
V W : SemiNormedGroupCat
i : V ≅ W
h1 : NormedAddGroupHom.NormNoninc i.hom
h2 : NormedAddGroupHom.NormNoninc i.inv
⊢ Isometry ↑i.hom
[PROOFSTEP]
apply AddMonoidHomClass.isometry_of_norm
[GOAL]
case a
V W : SemiNormedGroupCat
i : V ≅ W
h1 : NormedAddGroupHom.NormNoninc i.hom
h2 : NormedAddGroupHom.NormNoninc i.inv
⊢ ∀ (x : ↑V), ‖↑i.hom x‖ = ‖x‖
[PROOFSTEP]
intro v
[GOAL]
case a
V W : SemiNormedGroupCat
i : V ≅ W
h1 : NormedAddGroupHom.NormNoninc i.hom
h2 : NormedAddGroupHom.NormNoninc i.inv
v : ↑V
⊢ ‖↑i.hom v‖ = ‖v‖
[PROOFSTEP]
apply le_antisymm (h1 v)
[GOAL]
case a
V W : SemiNormedGroupCat
i : V ≅ W
h1 : NormedAddGroupHom.NormNoninc i.hom
h2 : NormedAddGroupHom.NormNoninc i.inv
v : ↑V
⊢ ‖v‖ ≤ ‖↑i.hom v‖
[PROOFSTEP]
calc
  ‖v‖ = ‖i.inv (i.hom v)‖ := by rw [Iso.hom_inv_id_apply]
  _ ≤ ‖i.hom v‖ := h2 _
[GOAL]
V W : SemiNormedGroupCat
i : V ≅ W
h1 : NormedAddGroupHom.NormNoninc i.hom
h2 : NormedAddGroupHom.NormNoninc i.inv
v : ↑V
⊢ ‖v‖ = ‖↑i.inv (↑i.hom v)‖
[PROOFSTEP]
rw [Iso.hom_inv_id_apply]
[GOAL]
M N : SemiNormedGroupCat
f : M ≅ N
i : NormedAddGroupHom.NormNoninc f.hom
i' : NormedAddGroupHom.NormNoninc f.inv
⊢ mkHom f.hom i ≫ mkHom f.inv i' = 𝟙 (of ↑M)
[PROOFSTEP]
apply Subtype.eq
[GOAL]
case a
M N : SemiNormedGroupCat
f : M ≅ N
i : NormedAddGroupHom.NormNoninc f.hom
i' : NormedAddGroupHom.NormNoninc f.inv
⊢ ↑(mkHom f.hom i ≫ mkHom f.inv i') = ↑(𝟙 (of ↑M))
[PROOFSTEP]
exact f.hom_inv_id
[GOAL]
M N : SemiNormedGroupCat
f : M ≅ N
i : NormedAddGroupHom.NormNoninc f.hom
i' : NormedAddGroupHom.NormNoninc f.inv
⊢ mkHom f.inv i' ≫ mkHom f.hom i = 𝟙 (of ↑N)
[PROOFSTEP]
apply Subtype.eq
[GOAL]
case a
M N : SemiNormedGroupCat
f : M ≅ N
i : NormedAddGroupHom.NormNoninc f.hom
i' : NormedAddGroupHom.NormNoninc f.inv
⊢ ↑(mkHom f.inv i' ≫ mkHom f.hom i) = ↑(𝟙 (of ↑N))
[PROOFSTEP]
exact f.inv_hom_id
[GOAL]
V : SemiNormedGroupCat₁
inst✝ : Subsingleton ↑V
⊢ Limits.IsZero V
[PROOFSTEP]
refine' ⟨fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩⟩
[GOAL]
case refine'_1
V : SemiNormedGroupCat₁
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat₁
f : V ⟶ X
⊢ f = default
[PROOFSTEP]
ext x
[GOAL]
case refine'_1.w.h
V : SemiNormedGroupCat₁
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat₁
f : V ⟶ X
x : ↑V
⊢ ↑f x = ↑default x
[PROOFSTEP]
have : x = 0 := Subsingleton.elim _ _
[GOAL]
case refine'_1.w.h
V : SemiNormedGroupCat₁
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat₁
f : V ⟶ X
x : ↑V
this : x = 0
⊢ ↑f x = ↑default x
[PROOFSTEP]
simp only [this, map_zero]
[GOAL]
case refine'_2
V : SemiNormedGroupCat₁
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat₁
f : X ⟶ V
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case refine'_2.w.h
V : SemiNormedGroupCat₁
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat₁
f : X ⟶ V
x✝ : ↑X
⊢ ↑f x✝ = ↑default x✝
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
V W : SemiNormedGroupCat₁
i : V ≅ W
⊢ Isometry ↑i.hom
[PROOFSTEP]
change Isometry (⟨⟨i.hom, map_zero _⟩, fun _ _ => map_add _ _ _⟩ : V →+ W)
[GOAL]
V W : SemiNormedGroupCat₁
i : V ≅ W
⊢ Isometry
    ↑{ toZeroHom := { toFun := ↑i.hom, map_zero' := (_ : ↑i.hom 0 = 0) },
        map_add' := (_ : ∀ (x x_1 : ↑V), ↑i.hom (x + x_1) = ↑i.hom x + ↑i.hom x_1) }
[PROOFSTEP]
refine' AddMonoidHomClass.isometry_of_norm _ _
[GOAL]
V W : SemiNormedGroupCat₁
i : V ≅ W
⊢ ∀ (x : ↑V),
    ‖↑{ toZeroHom := { toFun := ↑i.hom, map_zero' := (_ : ↑i.hom 0 = 0) },
              map_add' := (_ : ∀ (x x_1 : ↑V), ↑i.hom (x + x_1) = ↑i.hom x + ↑i.hom x_1) }
          x‖ =
      ‖x‖
[PROOFSTEP]
intro v
[GOAL]
V W : SemiNormedGroupCat₁
i : V ≅ W
v : ↑V
⊢ ‖↑{ toZeroHom := { toFun := ↑i.hom, map_zero' := (_ : ↑i.hom 0 = 0) },
            map_add' := (_ : ∀ (x x_1 : ↑V), ↑i.hom (x + x_1) = ↑i.hom x + ↑i.hom x_1) }
        v‖ =
    ‖v‖
[PROOFSTEP]
apply le_antisymm (i.hom.2 v)
[GOAL]
V W : SemiNormedGroupCat₁
i : V ≅ W
v : ↑V
⊢ ‖v‖ ≤ ‖↑↑i.hom v‖
[PROOFSTEP]
calc
  ‖v‖ = ‖i.inv (i.hom v)‖ := by rw [Iso.hom_inv_id_apply]
  _ ≤ ‖i.hom v‖ := i.inv.2 _
[GOAL]
V W : SemiNormedGroupCat₁
i : V ≅ W
v : ↑V
⊢ ‖v‖ = ‖↑i.inv (↑i.hom v)‖
[PROOFSTEP]
rw [Iso.hom_inv_id_apply]
