case refine'_1
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.618707
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.fst = 0 → x.snd = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ ∃ x, (a, x) ∈ g

case refine'_2
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.618707
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.fst = 0 → x.snd = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ ∀ (y₁ y₂ : F), (a, y₁) ∈ g → (a, y₂) ∈ g → y₁ = y₂
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.618707
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.fst = 0 → x.snd = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ ∃! b, (a, b) ∈ g
refine' exists_unique_of_exists_of_unique _ _
case refine'_2
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.618707
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.fst = 0 → x.snd = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
⊢ y₁ = y₂
case refine'_2
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.618707
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.fst = 0 → x.snd = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ ∀ (y₁ y₂ : F), (a, y₁) ∈ g → (a, y₂) ∈ g → y₁ = y₂
intro y₁ y₂ hy₁ hy₂
case refine'_2
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.618707
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.fst = 0 → x.snd = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
hy : (0, y₁ - y₂) ∈ g
⊢ y₁ = y₂
case refine'_2
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.618707
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.fst = 0 → x.snd = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
⊢ y₁ = y₂
have hy : ((0 : E), y₁ - y₂) ∈ g := by
  convert g.sub_mem hy₁ hy₂
  exact (sub_self _).symm
no goals
case refine'_2
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.618707
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.fst = 0 → x.snd = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
hy : (0, y₁ - y₂) ∈ g
⊢ y₁ = y₂
exact sub_eq_zero.mp (hg hy (by simp))
case a
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.618707
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.fst = 0 → x.snd = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ (∃ x, (a, x) ∈ g) ↔ a ∈ map (LinearMap.fst R E F) g
case refine'_1
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.618707
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.fst = 0 → x.snd = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ ∃ x, (a, x) ∈ g
convert ha
no goals
case a
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.618707
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.fst = 0 → x.snd = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
⊢ (∃ x, (a, x) ∈ g) ↔ a ∈ map (LinearMap.fst R E F) g
simp
case h.e'_4.h.e'_3
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.618707
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.fst = 0 → x.snd = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
⊢ 0 = ((a, y₁) - (a, y₂)).fst
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.618707
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.fst = 0 → x.snd = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
⊢ (0, y₁ - y₂) ∈ g
convert g.sub_mem hy₁ hy₂
no goals
case h.e'_4.h.e'_3
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.618707
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.fst = 0 → x.snd = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
⊢ 0 = ((a, y₁) - (a, y₂)).fst
exact (sub_self _).symm
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.618707
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : Submodule R (E × F)
hg : ∀ {x : E × F}, x ∈ g → x.fst = 0 → x.snd = 0
a : E
ha : a ∈ map (LinearMap.fst R E F) g
y₁ y₂ : F
hy₁ : (a, y₁) ∈ g
hy₂ : (a, y₂) ∈ g
hy : (0, y₁ - y₂) ∈ g
⊢ (0, y₁ - y₂).fst = 0
simp