case h
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x : E × F
⊢ x ∈ LinearPMap.graph (toLinearPMap g hg) ↔ x ∈ g
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
⊢ LinearPMap.graph (toLinearPMap g hg) = g
ext x
case h.mp
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x : E × F
hx : x ∈ LinearPMap.graph (toLinearPMap g hg)
⊢ x ∈ g

case h.mpr
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x : E × F
hx : x ∈ g
⊢ x ∈ LinearPMap.graph (toLinearPMap g hg)
case h
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x : E × F
⊢ x ∈ LinearPMap.graph (toLinearPMap g hg) ↔ x ∈ g
constructor <;> intro hx
case h.mpr
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x : E × F
hx : x ∈ g
⊢ ∃ y, ↑y = x.fst ∧ ↑(toLinearPMap g hg) y = x.snd
case h.mpr
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x : E × F
hx : x ∈ g
⊢ x ∈ LinearPMap.graph (toLinearPMap g hg)
rw [LinearPMap.mem_graph_iff]
case h.mpr.mk
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
⊢ ∃ y, ↑y = (x_fst, x_snd).fst ∧ ↑(toLinearPMap g hg) y = (x_fst, x_snd).snd
case h.mpr
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x : E × F
hx : x ∈ g
⊢ ∃ y, ↑y = x.fst ∧ ↑(toLinearPMap g hg) y = x.snd
cases' x with x_fst x_snd
case h.mpr.mk
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
⊢ ∃ y, ↑y = (x_fst, x_snd).fst ∧ ↑(toLinearPMap g hg) y = (x_fst, x_snd).snd
case h.mpr.mk
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
⊢ ∃ y, ↑y = (x_fst, x_snd).fst ∧ ↑(toLinearPMap g hg) y = (x_fst, x_snd).snd
have hx_fst : x_fst ∈ g.map (LinearMap.fst R E F) := by
  simp only [mem_map, LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]
  exact ⟨x_snd, hx⟩
case h.mpr.mk
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
⊢ ↑(toLinearPMap g hg) { val := x_fst, property := hx_fst } = (x_fst, x_snd).snd
case h.mpr.mk
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
⊢ ∃ y, ↑y = (x_fst, x_snd).fst ∧ ↑(toLinearPMap g hg) y = (x_fst, x_snd).snd
refine' ⟨⟨x_fst, hx_fst⟩, Subtype.coe_mk x_fst hx_fst, _⟩
no goals
case h.mpr.mk
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
⊢ ↑(toLinearPMap g hg) { val := x_fst, property := hx_fst } = (x_fst, x_snd).snd
exact (existsUnique_from_graph @hg hx_fst).unique (valFromGraph_mem hg hx_fst) hx
case h.mp
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x : E × F
hx : ∃ y, ↑y = x.fst ∧ ↑(toLinearPMap g hg) y = x.snd
⊢ x ∈ g
case h.mp
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x : E × F
hx : x ∈ LinearPMap.graph (toLinearPMap g hg)
⊢ x ∈ g
rw [LinearPMap.mem_graph_iff] at hx
case h.mp.intro.intro
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x : E × F
y : { x // x ∈ (toLinearPMap g hg).domain }
hx1 : ↑y = x.fst
hx2 : ↑(toLinearPMap g hg) y = x.snd
⊢ x ∈ g
case h.mp
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x : E × F
hx : ∃ y, ↑y = x.fst ∧ ↑(toLinearPMap g hg) y = x.snd
⊢ x ∈ g
rcases hx with ⟨y, hx1, hx2⟩
case h.e'_4
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x : E × F
y : { x // x ∈ (toLinearPMap g hg).domain }
hx1 : ↑y = x.fst
hx2 : ↑(toLinearPMap g hg) y = x.snd
⊢ x = (↑y, ↑(toLinearPMap g hg) y)
case h.mp.intro.intro
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x : E × F
y : { x // x ∈ (toLinearPMap g hg).domain }
hx1 : ↑y = x.fst
hx2 : ↑(toLinearPMap g hg) y = x.snd
⊢ x ∈ g
convert g.mem_graph_toLinearPMap hg y using 1
no goals
case h.e'_4
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x : E × F
y : { x // x ∈ (toLinearPMap g hg).domain }
hx1 : ↑y = x.fst
hx2 : ↑(toLinearPMap g hg) y = x.snd
⊢ x = (↑y, ↑(toLinearPMap g hg) y)
exact Prod.ext hx1.symm hx2.symm
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
⊢ ∃ x, (x_fst, x) ∈ g
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
⊢ x_fst ∈ map (LinearMap.fst R E F) g
simp only [mem_map, LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]
no goals
R : Type u_1
inst✝⁶ : Ring R
E : Type u_3
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.666279
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ (x : E × F), x ∈ g → x.fst = 0 → x.snd = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
⊢ ∃ x, (x_fst, x) ∈ g
exact ⟨x_snd, hx⟩