awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
rw :
  (x - HPow.hPow (β := ℕ) x 2) ^ n ∣
    (x - HPow.hPow (β := ℕ) x 2) ^ n *
      ((∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) *
        HPow.hPow (α := R) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1)) n)
h : Commute x (1 - x)
hbc : Commute (∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) ((1 - x) ^ n)
⊢ (x - HPow.hPow (β := ℕ) x 2) ^ n ∣
    (x ^ n * ∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) *
      ((1 - x) * ∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1)) ^ n
have h₁ : Commute (1 - x) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1))
Tactic: rw [Commute.mul_pow, Commute.mul_mul_mul_comm, ← Commute.mul_pow, mul_one_sub, ← pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
⊢ Commute (∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) ((1 - x) ^ n)
have hbc : ∀ x_1 ∈ Finset.range n, Commute (1 - x ^ n) x
Tactic: refine .pow_right (.sub_right (.one_right _) (.sum_left _ _ _ fun _ _ ↦ .pow_left ?_ _)) _
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (hypothesis)
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)
have this : (x - HPow.hPow (β := ℕ) x 2) ^ n ∣ 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2
Tactic: have : (x - x ^ 2) ^ n ∣ (1 - (1 - x ^ n) ^ n) - (1 - (1 - x ^ n) ^ n) ^ 2 := by
    conv_rhs => rw [pow_two, ← mul_one_sub, sub_sub_cancel]
    nth_rw 1 3 [← one_pow n]
    rw [← (Commute.one_left x).mul_geom_sum₂, ← (Commute.one_left (1 - x ^ n)).mul_geom_sum₂]
    simp only [sub_sub_cancel, one_pow, one_mul]
    rw [Commute.mul_pow, Commute.mul_mul_mul_comm, ← Commute.mul_pow, mul_one_sub, ← pow_two]
    · exact ⟨_, rfl⟩
    · simp
    · refine .pow_right (.sub_right (.one_right _) (.sum_left _ _ _ fun _ _ ↦ .pow_left ?_ _)) _
      simp
    · exact .sub_left (.one_left _) (.sum_right _ _ _ fun _ _ ↦ .pow_right rfl _)
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
this : (x - HPow.hPow (β := ℕ) x 2) ^ n ∣ 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)
have rwa : ∀ (this : 0 ∣ 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2), IsIdempotentElem (1 - (1 - x ^ n) ^ n)
Tactic: rwa [hx, zero_dvd_iff, sub_eq_zero, eq_comm, pow_two] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
this : (x - HPow.hPow (β := ℕ) x 2) ^ n ∣ 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2
rwa :
  ∀ (this : 0 ∣ 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2),
    IsIdempotentElem (1 - (1 - x ^ n) ^ n)
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)
have rwa₁ : ∀ (this : 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2 = 0), IsIdempotentElem (1 - (1 - x ^ n) ^ n)
Tactic: rwa [hx, zero_dvd_iff, sub_eq_zero, eq_comm, pow_two] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
this : (x - HPow.hPow (β := ℕ) x 2) ^ n ∣ 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2
rwa :
  ∀ (this : 0 ∣ 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2),
    IsIdempotentElem (1 - (1 - x ^ n) ^ n)
rwa₁ :
  ∀ (this : 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2 = 0),
    IsIdempotentElem (1 - (1 - x ^ n) ^ n)
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)
have rwa₂ : ∀ (this : 1 - (1 - x ^ n) ^ n = HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2), IsIdempotentElem (1 - (1 - x ^ n) ^ n)
Tactic: rwa [hx, zero_dvd_iff, sub_eq_zero, eq_comm, pow_two] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
this : (x - HPow.hPow (β := ℕ) x 2) ^ n ∣ 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2
rwa :
  ∀ (this : 0 ∣ 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2),
    IsIdempotentElem (1 - (1 - x ^ n) ^ n)
rwa₁ :
  ∀ (this : 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2 = 0),
    IsIdempotentElem (1 - (1 - x ^ n) ^ n)
rwa₂ :
  ∀ (this : 1 - (1 - x ^ n) ^ n = HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2), IsIdempotentElem (1 - (1 - x ^ n) ^ n)
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)
have rwa₃ : ∀ (this : HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2 = 1 - (1 - x ^ n) ^ n), IsIdempotentElem (1 - (1 - x ^ n) ^ n)
Tactic: rwa [hx, zero_dvd_iff, sub_eq_zero, eq_comm, pow_two] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
hx : (x - HPow.hPow (β := ℕ) x 2) ^ n = 0
this : (x - HPow.hPow (β := ℕ) x 2) ^ n ∣ 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2
rwa :
  ∀ (this : 0 ∣ 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2),
    IsIdempotentElem (1 - (1 - x ^ n) ^ n)
rwa₁ :
  ∀ (this : 1 - (1 - x ^ n) ^ n - HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2 = 0),
    IsIdempotentElem (1 - (1 - x ^ n) ^ n)
rwa₂ :
  ∀ (this : 1 - (1 - x ^ n) ^ n = HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2), IsIdempotentElem (1 - (1 - x ^ n) ^ n)
rwa₃ :
  ∀ (this : HPow.hPow (β := ℕ) (1 - (1 - x ^ n) ^ n) 2 = 1 - (1 - x ^ n) ^ n), IsIdempotentElem (1 - (1 - x ^ n) ^ n)
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)
have rwa₄ : ∀ (this : (1 - (1 - x ^ n) ^ n) * (1 - (1 - x ^ n) ^ n) = 1 - (1 - x ^ n) ^ n), IsIdempotentElem (1 - (1 - x ^ n) ^ n)
Tactic: rwa [hx, zero_dvd_iff, sub_eq_zero, eq_comm, pow_two] 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
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
he₂ : IsIdempotentElem e₂
he₁e₂ : HMul.hMul (β := S) e₁ ((f : (a : R) → S) e₂ : S) = 0
⊢ ∃ (e' : R), IsIdempotentElem e' ∧ (f : (a : R) → S) e' = e₁ ∧ e' * e₂ = 0
have obtain : ∀ (e₁ : R) (he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S))
  (he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0),
  ∃ (e' : R),
    IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0
Tactic: obtain ⟨e₁, rfl⟩ := he
Cleared hypotheses: e₁, he, he₁, he₁e₂
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
⊢ ∃ (e' : R),
    IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0
have inl : Subsingleton R →
  ∃ (e' : R),
    IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0
Tactic: cases subsingleton_or_nontrivial R
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
inl :
  Subsingleton R →
    ∃ (e' : R),
      IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0
⊢ ∃ (e' : R),
    IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0
have inr : Nontrivial R →
  ∃ (e' : R),
    IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0
Tactic: cases subsingleton_or_nontrivial R
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
have rw : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) (e₁ * e₂) : S) = (f : (a : R) → S) e₁
Tactic: rw [map_sub, map_mul, he₁e₂, sub_zero]
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
rw : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) (e₁ * e₂) : S) = (f : (a : R) → S) e₁
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
have rw₁ : HSub.hSub (α := S) ((f : (a : R) → S) e₁ : S)
    (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S)) =
  (f : (a : R) → S) e₁
Tactic: rw [map_sub, map_mul, he₁e₂, sub_zero]
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
rw : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) (e₁ * e₂) : S) = (f : (a : R) → S) e₁
rw₁ :
  HSub.hSub (α := S) ((f : (a : R) → S) e₁ : S)
      (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S)) =
    (f : (a : R) → S) e₁
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
have rw₂ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) e₁ : S) (0 : S) = (f : (a : R) → S) e₁
Tactic: rw [map_sub, map_mul, he₁e₂, sub_zero]
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
rw : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) (e₁ * e₂) : S) = (f : (a : R) → S) e₁
rw₁ :
  HSub.hSub (α := S) ((f : (a : R) → S) e₁ : S)
      (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S)) =
    (f : (a : R) → S) e₁
rw₂ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) e₁ : S) (0 : S) = (f : (a : R) → S) e₁
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
have rw₃ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₁ : S)
Tactic: rw [map_sub, map_mul, he₁e₂, sub_zero]
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
⊢ ∃ (e' : R),
    IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0
have ha : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
Tactic: have ha : f a = f e₁ := by rw [map_sub, map_mul, he₁e₂, sub_zero]
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
⊢ a * e₂ = 0
have rw : e₁ * e₂ - e₁ * e₂ * e₂ = 0
Tactic: rw [sub_mul, mul_assoc, he₂.eq, sub_self]
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
rw : e₁ * e₂ - e₁ * e₂ * e₂ = 0
⊢ a * e₂ = 0
have rw₁ : e₁ * e₂ - e₁ * (e₂ * e₂) = 0
Tactic: rw [sub_mul, mul_assoc, he₂.eq, sub_self]
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
rw : e₁ * e₂ - e₁ * e₂ * e₂ = 0
rw₁ : e₁ * e₂ - e₁ * (e₂ * e₂) = 0
⊢ a * e₂ = 0
have rw₂ : e₁ * e₂ - e₁ * e₂ = 0
Tactic: rw [sub_mul, mul_assoc, he₂.eq, sub_self]
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
rw : e₁ * e₂ - e₁ * e₂ * e₂ = 0
rw₁ : e₁ * e₂ - e₁ * (e₂ * e₂) = 0
rw₂ : e₁ * e₂ - e₁ * e₂ = 0
⊢ a * e₂ = 0
have rw₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [sub_mul, mul_assoc, he₂.eq, sub_self]
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
⊢ ∃ (e' : R),
    IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0
have ha' : a * e₂ = 0
Tactic: have ha' : a * e₂ = 0 := by rw [sub_mul, mul_assoc, he₂.eq, sub_self]
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
ha' : a * e₂ = 0
⊢ ∃ (e' : R),
    IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0
have hx' : Membership.mem (γ := Ideal R) (RingHom.ker f) (a - HPow.hPow (β := ℕ) a 2)
Tactic: have hx' : a - a ^ 2 ∈ RingHom.ker f := by
    simp [RingHom.mem_ker, pow_two, ha, he₁.eq]
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
ha' : a * e₂ = 0
hx' : Membership.mem (γ := Ideal R) (RingHom.ker f) (a - HPow.hPow (β := ℕ) a 2)
⊢ ∃ (e' : R),
    IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0
have inr : ∀ (n : ℕ) (hn : (a - HPow.hPow (β := ℕ) a 2) ^ n = 0),
  ∃ (e' : R),
    IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0
Tactic: obtain ⟨n, hn⟩ := h _ hx'
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
ha' : a * e₂ = 0
hx' : Membership.mem (γ := Ideal R) (RingHom.ker f) (a - HPow.hPow (β := ℕ) a 2)
n : ℕ
hn : (a - HPow.hPow (β := ℕ) a 2) ^ n = 0
⊢ ∃ (e' : R),
    IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0
have inr : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (1 - (1 - a ^ n) ^ n) : S) ((f : (a : R) → S) e₁ : S)
Tactic: refine ⟨_, isIdempotentElem_one_sub_one_sub_pow_pow _ _ hn, ?_, ?_⟩
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
ha' : a * e₂ = 0
hx' : Membership.mem (γ := Ideal R) (RingHom.ker f) (a - HPow.hPow (β := ℕ) a 2)
n : ℕ
hn : (a - HPow.hPow (β := ℕ) a 2) ^ n = 0
inr : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (1 - (1 - a ^ n) ^ n) : S) ((f : (a : R) → S) e₁ : S)
⊢ ∃ (e' : R),
    IsIdempotentElem e' ∧ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₁ : S) ∧ e' * e₂ = 0
have inr₁ : (1 - (1 - a ^ n) ^ n) * e₂ = 0
Tactic: refine ⟨_, isIdempotentElem_one_sub_one_sub_pow_pow _ _ hn, ?_, ?_⟩
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
ha' : a * e₂ = 0
hx' : Membership.mem (γ := Ideal R) (RingHom.ker f) (a - HPow.hPow (β := ℕ) a 2)
n : ℕ
hn : (a - HPow.hPow (β := ℕ) a 2) ^ n = 0
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (1 - (1 - a ^ n) ^ n) : S) ((f : (a : R) → S) e₁ : S)
have inr : ∀ (hn : HPow.hPow (β := ℕ) (a - HPow.hPow (β := ℕ) a 2) 0 = 0),
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (1 - HPow.hPow (β := ℕ) (1 - HPow.hPow (β := ℕ) a 0) 0) : S)
    ((f : (a : R) → S) e₁ : S)
Tactic: rcases n with - | n
Cleared hypotheses: n, hn
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
ha' : a * e₂ = 0
hx' : Membership.mem (γ := Ideal R) (RingHom.ker f) (a - HPow.hPow (β := ℕ) a 2)
n : ℕ
hn : (a - HPow.hPow (β := ℕ) a 2) ^ n = 0
inr :
  ∀ (hn : HPow.hPow (β := ℕ) (a - HPow.hPow (β := ℕ) a 2) 0 = 0),
    Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (1 - HPow.hPow (β := ℕ) (1 - HPow.hPow (β := ℕ) a 0) 0) : S)
      ((f : (a : R) → S) e₁ : S)
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (1 - (1 - a ^ n) ^ n) : S) ((f : (a : R) → S) e₁ : S)
have inr₁ : ∀ (n : ℕ) (hn : (a - HPow.hPow (β := ℕ) a 2) ^ (n + 1) = 0),
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (1 - (1 - a ^ (n + 1)) ^ (n + 1)) : S) ((f : (a : R) → S) e₁ : S)
Tactic: rcases n with - | n
Cleared hypotheses: n, hn
-- 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
h : ∀ (x : R), Membership.mem (γ := Ideal R) (RingHom.ker f) x → IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem.{u_2} (M := S) ((f : (a : R) → S) e₁ : S)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₂ : S) = 0
h_1 : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)
ha' : a * e₂ = 0
hx' : Membership.mem (γ := Ideal R) (RingHom.ker f) (a - HPow.hPow (β := ℕ) a 2)
n : ℕ
hn : (a - HPow.hPow (β := ℕ) a 2) ^ n = 0
⊢ (1 - (1 - a ^ n) ^ n) * e₂ = 0
have inr : ∀ (k : Rᵐᵒᵖ) (hk : HPow.hPow (α := Rᵐᵒᵖ) 1 n - MulOpposite.op (1 - a ^ n) ^ n = (1 - MulOpposite.op (1 - a ^ n)) * k),
  (1 - (1 - a ^ n) ^ n) * e₂ = 0
Tactic: obtain ⟨k, hk⟩ := (Commute.one_left (MulOpposite.op <| 1 - a ^ n)).sub_dvd_pow_sub_pow n