case H
M : Type u_2
N✝ : Type ?u.463092
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_1
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
x : M ⧸ S
⊢ ↑g x = ↑(lift S f hf) x
M : Type u_2
N✝ : Type ?u.463092
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_1
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
⊢ g = lift S f hf
ext x
case H.intro
M : Type u_2
N✝ : Type ?u.463092
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_1
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
x : M
⊢ ↑g (↑(AddSubgroup.normedMk S) x) = ↑(lift S f hf) (↑(AddSubgroup.normedMk S) x)
case H
M : Type u_2
N✝ : Type ?u.463092
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_1
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
x : M ⧸ S
⊢ ↑g x = ↑(lift S f hf) x
rcases AddSubgroup.surjective_normedMk _ x with ⟨x, rfl⟩
case H.intro
M : Type u_2
N✝ : Type ?u.463092
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_1
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
x : M
⊢ ↑(NormedAddGroupHom.comp g (AddSubgroup.normedMk S)) x = ↑(lift S f hf) (↑(AddSubgroup.normedMk S) x)
case H.intro
M : Type u_2
N✝ : Type ?u.463092
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_1
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
x : M
⊢ ↑g (↑(AddSubgroup.normedMk S) x) = ↑(lift S f hf) (↑(AddSubgroup.normedMk S) x)
change g.comp S.normedMk x = _
case H.intro
M : Type u_2
N✝ : Type ?u.463092
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_1
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
x : M
⊢ ↑f x = ↑(lift S f hf) (↑(AddSubgroup.normedMk S) x)
case H.intro
M : Type u_2
N✝ : Type ?u.463092
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_1
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
x : M
⊢ ↑(NormedAddGroupHom.comp g (AddSubgroup.normedMk S)) x = ↑(lift S f hf) (↑(AddSubgroup.normedMk S) x)
simp only [h]
no goals
case H.intro
M : Type u_2
N✝ : Type ?u.463092
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_1
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
x : M
⊢ ↑f x = ↑(lift S f hf) (↑(AddSubgroup.normedMk S) x)
rfl