case h
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.9010
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.9526
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.10489
inst✝² : Semiring S
M : Type ?u.10495
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
⊢ x ∈ ker (id - comp (Submodule.subtype p) f) ↔ x ∈ p
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.9010
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.9526
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.10489
inst✝² : Semiring S
M : Type ?u.10495
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
⊢ ker (id - comp (Submodule.subtype p) f) = p
ext x
case h
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.9010
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.9526
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.10489
inst✝² : Semiring S
M : Type ?u.10495
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
⊢ x = ↑(↑f x) ↔ x ∈ p
case h
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.9010
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.9526
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.10489
inst✝² : Semiring S
M : Type ?u.10495
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
⊢ x ∈ ker (id - comp (Submodule.subtype p) f) ↔ x ∈ p
simp only [comp_apply, mem_ker, subtype_apply, sub_apply, id_apply, sub_eq_zero]
no goals
case h
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.9010
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.9526
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.10489
inst✝² : Semiring S
M : Type ?u.10495
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
⊢ x = ↑(↑f x) ↔ x ∈ p
exact ⟨fun h => h.symm ▸ Submodule.coe_mem _, fun hx => by erw [hf ⟨x, hx⟩, Subtype.coe_mk]⟩
no goals
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.9010
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.9526
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type ?u.10489
inst✝² : Semiring S
M : Type ?u.10495
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] { x // x ∈ p }
hf : ∀ (x : { x // x ∈ p }), ↑f ↑x = x
x : E
hx : x ∈ p
⊢ x = ↑(↑f x)
erw [hf ⟨x, hx⟩, Subtype.coe_mk]