-- Mathlib/LinearAlgebra/Projection.lean
theorem isProj_iff_isIdempotentElem (f : M →ₗ[S] M) :
    (∃ p : Submodule S M, IsProj p f) ↔ IsIdempotentElem f

Proof state:
case h.map_id
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
h : IsIdempotentElem f
x : M
hx : x ∈ range f
⊢ f x = x

Tactic:
obtain ⟨y, hy⟩ := mem_range.1 hx

Result:
case h.map_id.intro
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
h : IsIdempotentElem f
x : M
hx : x ∈ range f
y : M
hy : f y = x
⊢ f x = x

Proof state:
case mp
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
p : Submodule S M
hp : IsProj p f
⊢ IsIdempotentElem f

Tactic:
ext x

Result:
case mp.h
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
p : Submodule S M
hp : IsProj p f
x : M
⊢ (f * f) x = f x

Proof state:
case h.map_mem
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
h : IsIdempotentElem f
x : M
⊢ f x ∈ range f

Tactic:
exact mem_range_self f x

Result:
no goals

Proof state:
case h
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
h : IsIdempotentElem f
⊢ IsProj (range f) f

Tactic:
constructor

Result:
case h.map_mem
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
h : IsIdempotentElem f
⊢ ∀ (x : M), f x ∈ range f

case h.map_id
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
h : IsIdempotentElem f
⊢ ∀ x ∈ range f, f x = x

Proof state:
case h.map_id
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
h : IsIdempotentElem f
⊢ ∀ x ∈ range f, f x = x

Tactic:
intro x hx

Result:
case h.map_id
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
h : IsIdempotentElem f
x : M
hx : x ∈ range f
⊢ f x = x

Proof state:
case h.map_mem
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
h : IsIdempotentElem f
⊢ ∀ (x : M), f x ∈ range f

Tactic:
intro x

Result:
case h.map_mem
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
h : IsIdempotentElem f
x : M
⊢ f x ∈ range f

Proof state:
case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
h : IsIdempotentElem f
⊢ ∃ p, IsProj p f

Tactic:
use range f

Result:
case h
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
h : IsIdempotentElem f
⊢ IsProj (range f) f

Proof state:
case mp.h
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
p : Submodule S M
hp : IsProj p f
x : M
⊢ (f * f) x = f x

Tactic:
exact hp.map_id (f x) (hp.map_mem x)

Result:
no goals

Proof state:
case h.map_id.intro
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
h : IsIdempotentElem f
x : M
hx : x ∈ range f
y : M
hy : f y = x
⊢ f x = x

Tactic:
rw [← hy, ← mul_apply, h]

Result:
no goals

Proof state:
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
⊢ (∃ p, IsProj p f) ↔ IsIdempotentElem f

Tactic:
constructor

Result:
case mp
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
⊢ (∃ p, IsProj p f) → IsIdempotentElem f

case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
⊢ IsIdempotentElem f → ∃ p, IsProj p f

Proof state:
case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
⊢ IsIdempotentElem f → ∃ p, IsProj p f

Tactic:
intro h

Result:
case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
h : IsIdempotentElem f
⊢ ∃ p, IsProj p f

Proof state:
case mp
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
⊢ (∃ p, IsProj p f) → IsIdempotentElem f

Tactic:
intro ⟨p, hp⟩

Result:
case mp
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
p : Submodule S M
hp : IsProj p f
⊢ IsIdempotentElem f