-- Mathlib/RingTheory/Idempotents.lean
/-- A family of orthogonal idempotents induces an surjection `R ≃+* ∏ R ⧸ ⟨1 - eᵢ⟩` -/
lemma OrthogonalIdempotents.surjective_pi {I : Type*} [Finite I] {e : I → R}
    (he : OrthogonalIdempotents e) :
    Function.Surjective (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✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
hij : i ≠ j
⊢ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})

Tactic:
rw [Ideal.isCoprime_span_singleton_iff]

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
hij : i ≠ j
⊢ IsCoprime (1 - e i) (1 - e j)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun i j => IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : (i : I) → R ⧸ Ideal.span {1 - e i}
⊢ ∃ a, (Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i})) a = x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.quotientInfToPiQuotient_surj this x

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun i j => IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : R ⧸ ⨅ i, Ideal.span {1 - e i}
⊢ ∃ a,
    (Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i})) a =
      (Ideal.quotientInfToPiQuotient fun i => Ideal.span {1 - e i}) x

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun i j => IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : R ⧸ ⨅ i, Ideal.span {1 - e i}
⊢ ∃ a,
    (Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i})) a =
      (Ideal.quotientInfToPiQuotient fun i => Ideal.span {1 - e i}) x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun i j => IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : R
⊢ ∃ a,
    (Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i})) a =
      (Ideal.quotientInfToPiQuotient fun i => Ideal.span {1 - e i}) ((Ideal.Quotient.mk (⨅ i, Ideal.span {1 - e i})) x)

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun i j => IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : R
⊢ ∃ a,
    (Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i})) a =
      (Ideal.quotientInfToPiQuotient fun i => Ideal.span {1 - e i}) ((Ideal.Quotient.mk (⨅ i, Ideal.span {1 - e i})) x)

Tactic:
exact ⟨x, by ext i; simp [Ideal.quotientInfToPiQuotient]⟩

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun i j => IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : R
i : I
⊢ (Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i})) x i =
    (Ideal.quotientInfToPiQuotient fun i => Ideal.span {1 - e i}) ((Ideal.Quotient.mk (⨅ i, Ideal.span {1 - e i})) x) i

Tactic:
simp [Ideal.quotientInfToPiQuotient]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun i j => IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
⊢ Function.Surjective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i}))

Tactic:
intro x

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun i j => IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : (i : I) → R ⧸ Ideal.span {1 - e i}
⊢ ∃ a, (Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i})) a = x

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
hij : i ≠ j
⊢ 1 * (1 - e i) + e i * (1 - e j) = 1

Tactic:
simp [mul_sub, sub_mul, he.ortho hij]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
hij : i ≠ j
⊢ IsCoprime (1 - e i) (1 - e j)

Tactic:
exact ⟨1, e i, by simp [mul_sub, sub_mul, he.ortho hij]⟩

Result:
no goals

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

Tactic:
suffices Pairwise fun i j ↦ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j}) by
  intro x
  obtain ⟨x, rfl⟩ := Ideal.quotientInfToPiQuotient_surj this x
  obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
  exact ⟨x, by ext i; simp [Ideal.quotientInfToPiQuotient]⟩

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
⊢ Pairwise fun i j => IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
⊢ Pairwise fun i j => IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})

Tactic:
intros i j hij

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
hij : i ≠ j
⊢ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun i j => IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : R
⊢ (Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i})) x =
    (Ideal.quotientInfToPiQuotient fun i => Ideal.span {1 - e i}) ((Ideal.Quotient.mk (⨅ i, Ideal.span {1 - e i})) x)

Tactic:
ext i

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun i j => IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : R
i : I
⊢ (Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i})) x i =
    (Ideal.quotientInfToPiQuotient fun i => Ideal.span {1 - e i}) ((Ideal.Quotient.mk (⨅ i, Ideal.span {1 - e i})) x) i