awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
I : Type u_3
inst_2 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
⊢ ∃ (e' : I → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
have obtain : ∀ (e' : Fin (Fintype.card I) → R) (h₁ : CompleteOrthogonalIdempotents e')
  (h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Equiv.symm (Fintype.equivFin I)) : (a : Fin (Fintype.card I)) → I)),
  ∃ (e' : I → R), CompleteOrthogonalIdempotents e' ∧ (⇑f : (a : R) → S) ∘ e' = e
Tactic: obtain ⟨e', h₁, h₂⟩ := lift_of_isNilpotent_ker_aux f h
    ((equiv (Fintype.equivFin I).symm).mpr he) (fun _ ↦ he' _)
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
I : Type u_3
inst_2 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (e i)
e' : Fin (Fintype.card I) → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : (⇑f : (a : R) → S) ∘ e' = e ∘ (⇑(Equiv.symm (Fintype.equivFin I)) : (a : Fin (Fintype.card I)) → I)
⊢ (⇑f : (a : R) → S) ∘ e' ∘ (⇑(Fintype.equivFin I) : (a : I) → Fin (Fintype.card I)) = e
have h₃ : ∀ (x : I), ((⇑f : (a : R) → S) ∘ e' ∘ (⇑(Fintype.equivFin I) : (a : I) → Fin (Fintype.card I))) x = e x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
⊢ HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
have simp : e₁ - e₂ * e₁ - (e₂ * e₁ - e₂ * e₁) - (e₂ * e₁ - e₂ * (e₂ * e₁) - (e₂ * (e₂ * e₁) - e₂)) = e₁ - e₂
Tactic: simp only [pow_succ, pow_zero, mul_sub, one_mul, sub_mul, he₁.eq, he₂.eq,
      H'.eq, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
⊢ e₁ - e₂ * e₁ - (e₂ * e₁ - e₂ * e₁) - (e₂ * e₁ - e₂ * (e₂ * e₁) - (e₂ * (e₂ * e₁) - e₂)) = e₁ - e₂
have simp : e₁ - e₂ * e₁ - (e₂ * e₁ - e₂ * e₁) - (e₂ * e₁ - e₂ * e₁ - (e₂ * e₁ - e₂)) = e₁ - e₂
Tactic: simp only [← mul_assoc, he₂.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (hypothesis)
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
⊢ e₁ = e₂
have this : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
Tactic: have : (e₁ - e₂) ^ 3 = (e₁ - e₂) := by
    simp only [pow_succ, pow_zero, mul_sub, one_mul, sub_mul, he₁.eq, he₂.eq,
      H'.eq, mul_assoc]
    simp only [← mul_assoc, he₂.eq]
    abel
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
this : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
⊢ e₁ = e₂
have obtain : ∀ (n : ℕ) (hn : (e₁ - e₂) ^ n = 0), e₁ = e₂
Tactic: obtain ⟨n, hn⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
n : ℕ
⊢ (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
have zero : (e₁ - e₂) ^ (HMul.hMul (α := ℕ) 2 0 + 1) = e₁ - e₂
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
n : ℕ
zero : (e₁ - e₂) ^ (HMul.hMul (α := ℕ) 2 0 + 1) = e₁ - e₂
⊢ (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
have succ : ∀ (n : ℕ), (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂ → (e₁ - e₂) ^ (2 * (n + 1) + 1) = e₁ - e₂
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (hypothesis)
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
⊢ e₁ = e₂
have this₁ : (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
Tactic: have : (e₁ - e₂) ^ (2 * n + 1) = (e₁ - e₂) := by
    clear hn; induction n <;> simp [mul_add, add_assoc, pow_add _ (2 * _) 3, ← pow_succ, *]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this_1 : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
⊢ e₁ = e₂
have rwa : ∀ (this : (e₁ - e₂) ^ (2 * n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
Tactic: rwa [pow_succ, two_mul, pow_add, hn, zero_mul, zero_mul, eq_comm, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this_1 : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
rwa : ∀ (this : (e₁ - e₂) ^ (2 * n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
⊢ e₁ = e₂
have rwa₁ : ∀ (this : (e₁ - e₂) ^ (n + n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
Tactic: rwa [pow_succ, two_mul, pow_add, hn, zero_mul, zero_mul, eq_comm, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this_1 : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
rwa : ∀ (this : (e₁ - e₂) ^ (2 * n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₁ : ∀ (this : (e₁ - e₂) ^ (n + n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
⊢ e₁ = e₂
have rwa₂ : ∀ (this : (e₁ - e₂) ^ n * (e₁ - e₂) ^ n * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
Tactic: rwa [pow_succ, two_mul, pow_add, hn, zero_mul, zero_mul, eq_comm, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this_1 : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
rwa : ∀ (this : (e₁ - e₂) ^ (2 * n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₁ : ∀ (this : (e₁ - e₂) ^ (n + n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₂ : ∀ (this : (e₁ - e₂) ^ n * (e₁ - e₂) ^ n * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
⊢ e₁ = e₂
have rwa₃ : ∀ (this : HMul.hMul (α := R) 0 0 * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
Tactic: rwa [pow_succ, two_mul, pow_add, hn, zero_mul, zero_mul, eq_comm, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this_1 : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
rwa : ∀ (this : (e₁ - e₂) ^ (2 * n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₁ : ∀ (this : (e₁ - e₂) ^ (n + n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₂ : ∀ (this : (e₁ - e₂) ^ n * (e₁ - e₂) ^ n * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₃ : ∀ (this : HMul.hMul (α := R) 0 0 * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
⊢ e₁ = e₂
have rwa₄ : ∀ (this : 0 * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
Tactic: rwa [pow_succ, two_mul, pow_add, hn, zero_mul, zero_mul, eq_comm, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this_1 : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
rwa : ∀ (this : (e₁ - e₂) ^ (2 * n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₁ : ∀ (this : (e₁ - e₂) ^ (n + n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₂ : ∀ (this : (e₁ - e₂) ^ n * (e₁ - e₂) ^ n * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₃ : ∀ (this : HMul.hMul (α := R) 0 0 * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₄ : ∀ (this : 0 * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
⊢ e₁ = e₂
have rwa₅ : ∀ (this : 0 = e₁ - e₂), e₁ = e₂
Tactic: rwa [pow_succ, two_mul, pow_add, hn, zero_mul, zero_mul, eq_comm, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this_1 : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
rwa : ∀ (this : (e₁ - e₂) ^ (2 * n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₁ : ∀ (this : (e₁ - e₂) ^ (n + n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₂ : ∀ (this : (e₁ - e₂) ^ n * (e₁ - e₂) ^ n * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₃ : ∀ (this : HMul.hMul (α := R) 0 0 * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₄ : ∀ (this : 0 * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₅ : ∀ (this : 0 = e₁ - e₂), e₁ = e₂
⊢ e₁ = e₂
have rwa₆ : ∀ (this : e₁ - e₂ = 0), e₁ = e₂
Tactic: rwa [pow_succ, two_mul, pow_add, hn, zero_mul, zero_mul, eq_comm, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this_1 : HPow.hPow (β := ℕ) (e₁ - e₂) 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
rwa : ∀ (this : (e₁ - e₂) ^ (2 * n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₁ : ∀ (this : (e₁ - e₂) ^ (n + n) * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₂ : ∀ (this : (e₁ - e₂) ^ n * (e₁ - e₂) ^ n * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₃ : ∀ (this : HMul.hMul (α := R) 0 0 * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₄ : ∀ (this : 0 * (e₁ - e₂) = e₁ - e₂), e₁ = e₂
rwa₅ : ∀ (this : 0 = e₁ - e₂), e₁ = e₂
rwa₆ : ∀ (this : e₁ - e₂ = 0), e₁ = e₂
⊢ e₁ = e₂
have rwa₇ : ∀ (this : e₁ = e₂), e₁ = e₂
Tactic: rwa [pow_succ, two_mul, pow_add, hn, zero_mul, zero_mul, eq_comm, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
I : Type u_3
e : I → R
inst_2 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e)
⊢ CompleteOrthogonalIdempotents e
have obtain : ∀ (e' : I → R) (h₁ : CompleteOrthogonalIdempotents e')
  (h₂ : Eq (α := I → S) ((⇑f : (a : R) → S) ∘ e') ((⇑f : (a : R) → S) ∘ e)), CompleteOrthogonalIdempotents e
Tactic: obtain ⟨e', h₁, h₂⟩ := lift_of_isNilpotent_ker f h he'' (fun _ ↦ ⟨_, rfl⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
I : Type u_3
e : I → R
inst_2 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e)
e' : I → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : Eq (α := I → S) ((⇑f : (a : R) → S) ∘ e') ((⇑f : (a : R) → S) ∘ e)
⊢ e = e'
have h₃ : ∀ (i : I), e i = e' i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
I : Type u_3
e : I → R
inst_2 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e)
e' : I → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : Eq (α := I → S) ((⇑f : (a : R) → S) ∘ e') ((⇑f : (a : R) → S) ∘ e)
i : I
⊢ e i = e' i
have h₃ : Membership.mem (γ := Ideal R) (RingHom.ker f) (e i - e' i)
Tactic: refine eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute
      (he _) (h₁.idem _) (h _ ?_) ((he' i).comm _)
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
I : Type u_3
e : I → R
inst_2 : Fintype I
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents.{u_2, u_3} (R := S) ((⇑f : (a : R) → S) ∘ e)
e' : I → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : Eq (α := I → S) ((⇑f : (a : R) → S) ∘ e') ((⇑f : (a : R) → S) ∘ e)
h₃ : CompleteOrthogonalIdempotents e
⊢ CompleteOrthogonalIdempotents e
have h₄ : Eq (α := I → S) ((⇑f : (a : R) → S) ∘ e) ((⇑f : (a : R) → S) ∘ e)
Tactic: obtain rfl : e = e' := by
    ext i
    refine eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute
      (he _) (h₁.idem _) (h _ ?_) ((he' i).comm _)
    simpa [RingHom.mem_ker, sub_eq_zero] using congr_fun h₂.symm i
Cleared hypotheses: e', h₁, h₂
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e : S
he : Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) e
he' : IsIdempotentElem e
⊢ ∃! e' : R, IsIdempotentElem e' ∧ (f : (a : R) → S) e' = e
have obtain : ∀ (e' : R) (he₂ : IsIdempotentElem e')
  (he :
    Membership.mem.{u_2, u_2} (α := S) (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f)
      ((f : (a : R) → S) e' : S))
  (he' : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e' : S)),
  ∃! e'_1 : R, IsIdempotentElem e'_1 ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e'_1 : S) ((f : (a : R) → S) e' : S)
Tactic: obtain ⟨e', he₂, rfl⟩ := exists_isIdempotentElem_eq_of_ker_isNilpotent f h e he he'
Cleared hypotheses: e, he, he'
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e' : R
he₂ : IsIdempotentElem e'
he :
  Membership.mem.{u_2, u_2} (α := S) (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) ((f : (a : R) → S) e' : S)
he' : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e' : S)
x : R
h_1 :
  (fun (e'_1 : R) ↦
      IsIdempotentElem e'_1 ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e'_1 : S) ((f : (a : R) → S) e' : S))
    x
hx : IsIdempotentElem x
hx' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) e' : S)
⊢ Membership.mem (γ := Ideal R) (RingHom.ker f) (x - e')
have rw : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x - e') : S) (0 : S)
Tactic: rw [RingHom.mem_ker, map_sub, hx', sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e' : R
he₂ : IsIdempotentElem e'
he :
  Membership.mem.{u_2, u_2} (α := S) (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) ((f : (a : R) → S) e' : S)
he' : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e' : S)
x : R
h_1 :
  (fun (e'_1 : R) ↦
      IsIdempotentElem e'_1 ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e'_1 : S) ((f : (a : R) → S) e' : S))
    x
hx : IsIdempotentElem x
hx' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) e' : S)
rw : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x - e') : S) (0 : S)
⊢ Membership.mem (γ := Ideal R) (RingHom.ker f) (x - e')
have rw₁ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) e' : S) = 0
Tactic: rw [RingHom.mem_ker, map_sub, hx', sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e' : R
he₂ : IsIdempotentElem e'
he :
  Membership.mem.{u_2, u_2} (α := S) (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) ((f : (a : R) → S) e' : S)
he' : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e' : S)
x : R
h_1 :
  (fun (e'_1 : R) ↦
      IsIdempotentElem e'_1 ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e'_1 : S) ((f : (a : R) → S) e' : S))
    x
hx : IsIdempotentElem x
hx' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) e' : S)
rw : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x - e') : S) (0 : S)
rw₁ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) e' : S) = 0
⊢ Membership.mem (γ := Ideal R) (RingHom.ker f) (x - e')
have rw₂ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e' : S) = 0
Tactic: rw [RingHom.mem_ker, map_sub, hx', sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
f : R →+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e' : R
he₂ : IsIdempotentElem e'
he :
  Membership.mem.{u_2, u_2} (α := S) (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) ((f : (a : R) → S) e' : S)
he' : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e' : S)
x : R
h_1 :
  (fun (e'_1 : R) ↦
      IsIdempotentElem e'_1 ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e'_1 : S) ((f : (a : R) → S) e' : S))
    x
hx : IsIdempotentElem x
hx' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) e' : S)
rw : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x - e') : S) (0 : S)
rw₁ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) e' : S) = 0
rw₂ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e' : S) = 0
⊢ Membership.mem (γ := Ideal R) (RingHom.ker f) (x - e')
have rw₃ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [RingHom.mem_ker, map_sub, hx', sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun (i j : I) ↦ IsCoprime (R := Ideal R) (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})
⊢ ∃ (a : R),
    (Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
            Ideal.Quotient.mk (Ideal.span {1 - e i}) :
          (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
        a =
      x
have obtain : ∀ (x : HasQuotient.Quotient R (B := Ideal R) (⨅ (i : I), Ideal.span {1 - e i})),
  ∃ (a : R),
    Eq (α := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
      ((Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
              Ideal.Quotient.mk (Ideal.span {1 - e i}) :
            (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
          a :
        (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
      ((Ideal.quotientInfToPiQuotient fun (i : I) ↦ Ideal.span {1 - e i} :
            (a : R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) → (i : I) → R ⧸ Ideal.span {1 - e i})
          x :
        (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
Tactic: obtain ⟨x, rfl⟩ := Ideal.quotientInfToPiQuotient_surj this x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun (i j : I) ↦ IsCoprime (R := Ideal R) (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : HasQuotient.Quotient R (B := Ideal R) (⨅ (i : I), Ideal.span {1 - e i})
⊢ ∃ (a : R),
    Eq (α := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
      ((Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
              Ideal.Quotient.mk (Ideal.span {1 - e i}) :
            (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
          a :
        (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
      ((Ideal.quotientInfToPiQuotient fun (i : I) ↦ Ideal.span {1 - e i} :
            (a : R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) → (i : I) → R ⧸ Ideal.span {1 - e i})
          x :
        (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
have obtain : ∀ (x : R),
  ∃ (a : R),
    Eq (α := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
      ((Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
              Ideal.Quotient.mk (Ideal.span {1 - e i}) :
            (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
          a :
        (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
      ((Ideal.quotientInfToPiQuotient fun (i : I) ↦ Ideal.span {1 - e i} :
            (a : R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) → (i : I) → R ⧸ Ideal.span {1 - e i})
          ((Ideal.Quotient.mk (⨅ (i : I), Ideal.span {1 - e i}) : (a : R) → R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) x :
            HasQuotient.Quotient R (B := Ideal R) (⨅ (i : I), Ideal.span {1 - e i})) :
        (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Type u_3
inst_1 : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun (i j : I) ↦ IsCoprime (R := Ideal R) (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : R
⊢ Eq (α := (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    ((Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
            Ideal.Quotient.mk (Ideal.span {1 - e i}) :
          (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
        x :
      (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    ((Ideal.quotientInfToPiQuotient fun (i : I) ↦ Ideal.span {1 - e i} :
          (a : R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) → (i : I) → R ⧸ Ideal.span {1 - e i})
        ((Ideal.Quotient.mk (⨅ (i : I), Ideal.span {1 - e i}) : (a : R) → R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) x :
          HasQuotient.Quotient R (B := Ideal R) (⨅ (i : I), Ideal.span {1 - e i})) :
      (i : I) → HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
have h : ∀ (i : I),
  Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    ((Pi.ringHom (f := fun (i : I) ↦ HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i})) fun (i : I) ↦
            Ideal.Quotient.mk (Ideal.span {1 - e i}) :
          (a : R) → (i : I) → R ⧸ Ideal.span {1 - e i})
        x i :
      HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
    ((Ideal.quotientInfToPiQuotient fun (i : I) ↦ Ideal.span {1 - e i} :
          (a : R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) → (i : I) → R ⧸ Ideal.span {1 - e i})
        ((Ideal.Quotient.mk (⨅ (i : I), Ideal.span {1 - e i}) : (a : R) → R ⧸ ⨅ (i : I), Ideal.span {1 - e i}) x :
          HasQuotient.Quotient R (B := Ideal R) (⨅ (i : I), Ideal.span {1 - e i}))
        i :
      HasQuotient.Quotient R (B := Ideal R) (Ideal.span {1 - e i}))
Tactic: ext i