R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.203526
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
h : ∀ (x : { x // x ∈ f.domain }) (y : { x // x ∈ g.domain }), ↑x = ↑y → ↑f x = ↑g y
z₁ : { x // x ∈ g.domain }
z₂ : { x // x ∈ (LinearPMap.sup f g h).domain }
hz : ↑z₁ = ↑z₂
⊢ ↑g z₁ = ↑(LinearPMap.sup f g h) z₂
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.203526
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
h : ∀ (x : { x // x ∈ f.domain }) (y : { x // x ∈ g.domain }), ↑x = ↑y → ↑f x = ↑g y
⊢ g ≤ LinearPMap.sup f g h
refine' ⟨le_sup_right, fun z₁ z₂ hz => _⟩
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.203526
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
h : ∀ (x : { x // x ∈ f.domain }) (y : { x // x ∈ g.domain }), ↑x = ↑y → ↑f x = ↑g y
z₁ : { x // x ∈ g.domain }
z₂ : { x // x ∈ (LinearPMap.sup f g h).domain }
hz : ↑z₁ = ↑z₂
⊢ ↑f 0 + ↑g z₁ = ↑(LinearPMap.sup f g h) z₂
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.203526
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
h : ∀ (x : { x // x ∈ f.domain }) (y : { x // x ∈ g.domain }), ↑x = ↑y → ↑f x = ↑g y
z₁ : { x // x ∈ g.domain }
z₂ : { x // x ∈ (LinearPMap.sup f g h).domain }
hz : ↑z₁ = ↑z₂
⊢ ↑g z₁ = ↑(LinearPMap.sup f g h) z₂
rw [← zero_add (g _), ← f.map_zero]
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.203526
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
h : ∀ (x : { x // x ∈ f.domain }) (y : { x // x ∈ g.domain }), ↑x = ↑y → ↑f x = ↑g y
z₁ : { x // x ∈ g.domain }
z₂ : { x // x ∈ (LinearPMap.sup f g h).domain }
hz : ↑z₁ = ↑z₂
⊢ ↑0 + ↑z₁ = ↑z₂
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.203526
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
h : ∀ (x : { x // x ∈ f.domain }) (y : { x // x ∈ g.domain }), ↑x = ↑y → ↑f x = ↑g y
z₁ : { x // x ∈ g.domain }
z₂ : { x // x ∈ (LinearPMap.sup f g h).domain }
hz : ↑z₁ = ↑z₂
⊢ ↑f 0 + ↑g z₁ = ↑(LinearPMap.sup f g h) z₂
refine' (sup_apply h _ _ _ _).symm
no goals
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.203526
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
h : ∀ (x : { x // x ∈ f.domain }) (y : { x // x ∈ g.domain }), ↑x = ↑y → ↑f x = ↑g y
z₁ : { x // x ∈ g.domain }
z₂ : { x // x ∈ (LinearPMap.sup f g h).domain }
hz : ↑z₁ = ↑z₂
⊢ ↑0 + ↑z₁ = ↑z₂
simpa