-- Mathlib/RingTheory/Idempotents.lean
/-- A family of complete orthogonal idempotents induces an isomorphism `R ≃+* ∏ R ⧸ ⟨1 - eᵢ⟩` -/
lemma CompleteOrthogonalIdempotents.bijective_pi (he : CompleteOrthogonalIdempotents e) :
    Function.Bijective (Pi.ringHom fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i}))

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s✝ : Finset I
a : I
s : Finset I
has : a ∉ s
e' : (∏ i ∈ s, (1 - e i)) * x = x
this : (1 - e a) * x = x
⊢ (∏ i ∈ insert a s, (1 - e i)) * x = x

Tactic:
simp [has, mul_assoc, e', this]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
⊢ x = 0

Tactic:
suffices ∀ s : Finset I, (∏ i ∈ s, (1 - e i)) * x = x by
  rw [← this Finset.univ, he.prod_one_sub, zero_mul]

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
⊢ ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s : Finset I
⊢ (∏ i ∈ ∅, (1 - e i)) * x = x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s : Finset I
⊢ ∀ ⦃a : I⦄ {s : Finset I}, a ∉ s → (∏ i ∈ s, (1 - e i)) * x = x → (∏ i ∈ insert a s, (1 - e i)) * x = x

Tactic:
intros a s has e'

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s✝ : Finset I
a : I
s : Finset I
has : a ∉ s
e' : (∏ i ∈ s, (1 - e i)) * x = x
⊢ (∏ i ∈ insert a s, (1 - e i)) * x = x

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
⊢ ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x

Tactic:
refine fun s ↦ Finset.induction_on s (by simp) ?_

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s : Finset I
⊢ ∀ ⦃a : I⦄ {s : Finset I}, a ∉ s → (∏ i ∈ s, (1 - e i)) * x = x → (∏ i ∈ insert a s, (1 - e i)) * x = x

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : (Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i})) x = 0
⊢ x = 0

Tactic:
simp [funext_iff, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton] at hx

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
⊢ x = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ Function.Injective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i}))

Tactic:
rw [injective_iff_map_eq_zero]

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ ∀ (a : R), (Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i})) a = 0 → a = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s✝ : Finset I
a : I
s : Finset I
has : a ∉ s
e' : (∏ i ∈ s, (1 - e i)) * x = x
⊢ (∏ i ∈ insert a s, (1 - e i)) * x = x

Tactic:
suffices (1 - e a) * x = x by simp [has, mul_assoc, e', this]

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s✝ : Finset I
a : I
s : Finset I
has : a ∉ s
e' : (∏ i ∈ s, (1 - e i)) * x = x
⊢ (1 - e a) * x = x

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ ∀ (a : R), (Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i})) a = 0 → a = 0

Tactic:
intro x hx

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : (Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i})) x = 0
⊢ x = 0

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
s✝ : Finset I
a : I
s : Finset I
has : a ∉ s
c : R
hx : ∀ (x : I), 1 - e x ∣ (1 - e a) * c
e' : (∏ i ∈ s, (1 - e i)) * ((1 - e a) * c) = (1 - e a) * c
⊢ (1 - e a) * ((1 - e a) * c) = (1 - e a) * c

Tactic:
rw [← mul_assoc, (he.idem a).one_sub.eq]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ Function.Bijective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i}))

Tactic:
classical
refine ⟨?_, he.1.surjective_pi⟩
rw [injective_iff_map_eq_zero]
intro x hx
simp [funext_iff, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton] at hx
suffices ∀ s : Finset I, (∏ i ∈ s, (1 - e i)) * x = x by
  rw [← this Finset.univ, he.prod_one_sub, zero_mul]
refine fun s ↦ Finset.induction_on s (by simp) ?_
intros a s has e'
suffices (1 - e a) * x = x by simp [has, mul_assoc, e', this]
obtain ⟨c, rfl⟩ := hx a
rw [← mul_assoc, (he.idem a).one_sub.eq]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ Function.Bijective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i}))

Tactic:
refine ⟨?_, he.1.surjective_pi⟩

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ Function.Injective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i}))

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
this : ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
⊢ x = 0

Tactic:
rw [← this Finset.univ, he.prod_one_sub, zero_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s✝ : Finset I
a : I
s : Finset I
has : a ∉ s
e' : (∏ i ∈ s, (1 - e i)) * x = x
⊢ (1 - e a) * x = x

Tactic:
obtain ⟨c, rfl⟩ := hx a

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
s✝ : Finset I
a : I
s : Finset I
has : a ∉ s
c : R
hx : ∀ (x : I), 1 - e x ∣ (1 - e a) * c
e' : (∏ i ∈ s, (1 - e i)) * ((1 - e a) * c) = (1 - e a) * c
⊢ (1 - e a) * ((1 - e a) * c) = (1 - e a) * c