case mp
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
⊢ (∃ p, IsProj p f) → comp f f = f

case mpr
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
⊢ comp f f = f → ∃ p, IsProj p f
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
⊢ (∃ p, IsProj p f) ↔ comp f f = f
constructor
case mp
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : ∃ p, IsProj p f
⊢ comp f f = f
case mp
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
⊢ (∃ p, IsProj p f) → comp f f = f
intro h
case mp.intro
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p✝ q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
p : Submodule S M
hp : IsProj p f
⊢ comp f f = f
case mp
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : ∃ p, IsProj p f
⊢ comp f f = f
obtain ⟨p, hp⟩ := h
case mp.intro.h
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p✝ q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
p : Submodule S M
hp : IsProj p f
x : M
⊢ ↑(comp f f) x = ↑f x
case mp.intro
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p✝ q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
p : Submodule S M
hp : IsProj p f
⊢ comp f f = f
ext x
case mp.intro.h
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p✝ q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
p : Submodule S M
hp : IsProj p f
x : M
⊢ ↑f (↑f x) = ↑f x
case mp.intro.h
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p✝ q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
p : Submodule S M
hp : IsProj p f
x : M
⊢ ↑(comp f f) x = ↑f x
rw [comp_apply]
no goals
case mp.intro.h
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p✝ q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
p : Submodule S M
hp : IsProj p f
x : M
⊢ ↑f (↑f x) = ↑f x
exact hp.map_id (f x) (hp.map_mem x)
case mpr
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
⊢ ∃ p, IsProj p f
case mpr
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
⊢ comp f f = f → ∃ p, IsProj p f
intro h
case mpr
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
⊢ IsProj (range f) f
case mpr
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
⊢ ∃ p, IsProj p f
use range f
case mpr.map_mem
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
⊢ ∀ (x : M), ↑f x ∈ range f

case mpr.map_id
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
⊢ ∀ (x : M), x ∈ range f → ↑f x = x
case mpr
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
⊢ IsProj (range f) f
constructor
case mpr.map_mem
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
x : M
⊢ ↑f x ∈ range f
case mpr.map_mem
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
⊢ ∀ (x : M), ↑f x ∈ range f
intro x
no goals
case mpr.map_mem
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
x : M
⊢ ↑f x ∈ range f
exact mem_range_self f x
case mpr.map_id
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
x : M
hx : x ∈ range f
⊢ ↑f x = x
case mpr.map_id
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
⊢ ∀ (x : M), x ∈ range f → ↑f x = x
intro x hx
case mpr.map_id.intro
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
x : M
hx : x ∈ range f
y : M
hy : ↑f y = x
⊢ ↑f x = x
case mpr.map_id
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
x : M
hx : x ∈ range f
⊢ ↑f x = x
obtain ⟨y, hy⟩ := mem_range.1 hx
no goals
case mpr.map_id.intro
R : Type ?u.424574
inst✝⁹ : Ring R
E : Type ?u.424580
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type ?u.425139
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type ?u.425655
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_1
inst✝² : Semiring S
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
h : comp f f = f
x : M
hx : x ∈ range f
y : M
hy : ↑f y = x
⊢ ↑f x = x
rw [← hy, ← comp_apply, h]