case h
V : Type ?u.489284
W : Type ?u.489287
V₁ : Type u_1
V₂ : Type ?u.489293
V₃ : Type ?u.489296
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
s : AddSubgroup V₁
x : V₁
⊢ x ∈ range (incl s) ↔ x ∈ s
V : Type ?u.489284
W : Type ?u.489287
V₁ : Type u_1
V₂ : Type ?u.489293
V₃ : Type ?u.489296
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
s : AddSubgroup V₁
⊢ range (incl s) = s
ext x
no goals
case h
V : Type ?u.489284
W : Type ?u.489287
V₁ : Type u_1
V₂ : Type ?u.489293
V₃ : Type ?u.489296
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
s : AddSubgroup V₁
x : V₁
⊢ x ∈ range (incl s) ↔ x ∈ s
exact ⟨fun ⟨y, hy⟩ => by rw [← hy]; simp, fun hx => ⟨⟨x, hx⟩, by simp⟩⟩
V : Type ?u.489284
W : Type ?u.489287
V₁ : Type u_1
V₂ : Type ?u.489293
V₃ : Type ?u.489296
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
s : AddSubgroup V₁
x : V₁
x✝ : x ∈ range (incl s)
y : { x // x ∈ s }
hy : ↑(toAddMonoidHom (incl s)) y = x
⊢ ↑(toAddMonoidHom (incl s)) y ∈ s
V : Type ?u.489284
W : Type ?u.489287
V₁ : Type u_1
V₂ : Type ?u.489293
V₃ : Type ?u.489296
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
s : AddSubgroup V₁
x : V₁
x✝ : x ∈ range (incl s)
y : { x // x ∈ s }
hy : ↑(toAddMonoidHom (incl s)) y = x
⊢ x ∈ s
rw [← hy]
no goals
V : Type ?u.489284
W : Type ?u.489287
V₁ : Type u_1
V₂ : Type ?u.489293
V₃ : Type ?u.489296
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
s : AddSubgroup V₁
x : V₁
x✝ : x ∈ range (incl s)
y : { x // x ∈ s }
hy : ↑(toAddMonoidHom (incl s)) y = x
⊢ ↑(toAddMonoidHom (incl s)) y ∈ s
simp
no goals
V : Type ?u.489284
W : Type ?u.489287
V₁ : Type u_1
V₂ : Type ?u.489293
V₃ : Type ?u.489296
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
s : AddSubgroup V₁
x : V₁
hx : x ∈ s
⊢ ↑(toAddMonoidHom (incl s)) { val := x, property := hx } = x
simp