awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Idempotents
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 : 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:
exact ⟨_, Subsingleton.elim _ _, rfl, Subsingleton.elim _ _⟩
-- Module: Mathlib.RingTheory.Idempotents
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₁
rw₃ rw₄ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e₁ : S) ((f : (a : R) → S) e₁ : S)
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) e₁ : S)

Tactic:
rw [map_sub, map_mul, he₁e₂, sub_zero]

Premises used: map_sub, sub_zero, map_mul
-- Module: Mathlib.RingTheory.Idempotents
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)

Tactic:
have ha : f a = f e₁ := by rw [map_sub, map_mul, he₁e₂, sub_zero]
-- Module: Mathlib.RingTheory.Idempotents
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
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ a * e₂ = 0

Tactic:
rw [sub_mul, mul_assoc, he₂.eq, sub_self]

Premises used: sub_self, mul_assoc, sub_mul, IsIdempotentElem.eq
-- Module: Mathlib.RingTheory.Idempotents
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

Tactic:
have ha' : a * e₂ = 0 := by rw [sub_mul, mul_assoc, he₂.eq, sub_self]
-- Module: Mathlib.RingTheory.Idempotents
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
⊢ Membership.mem (γ := Ideal R) (RingHom.ker f) (a - HPow.hPow (β := ℕ) a 2)

Tactic:
simp [RingHom.mem_ker, pow_two, ha, he₁.eq]

Premises used: pow_two, RingHom.mem_ker, IsIdempotentElem.eq
-- Module: Mathlib.RingTheory.Idempotents
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
⊢ 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]
-- Module: Mathlib.RingTheory.Idempotents
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)
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
⊢ ∃ (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'
-- Module: Mathlib.RingTheory.Idempotents
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

Tactic:
⟨_, isIdempotentElem_one_sub_one_sub_pow_pow _ _ hn, ?_, ?_⟩

Premises used: isIdempotentElem_one_sub_one_sub_pow_pow, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Idempotents
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)
inr₁ : (1 - (1 - a ^ n) ^ n) * 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

Tactic:
refine ⟨_, isIdempotentElem_one_sub_one_sub_pow_pow _ _ hn, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Idempotents
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)
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)
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (1 - (1 - a ^ n) ^ n) : S) ((f : (a : R) → S) e₁ : S)

Tactic:
rcases n with - | n
-- Module: Mathlib.RingTheory.Idempotents
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)
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:
simp at hn
-- Module: Mathlib.RingTheory.Idempotents
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 + 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:
simp only [map_sub, map_one, map_pow, ha, he₁.pow_succ_eq,
      he₁.one_sub.pow_succ_eq, sub_sub_cancel]

Premises used: IsIdempotentElem.one_sub, map_sub, IsIdempotentElem.pow_succ_eq, map_pow, sub_sub_cancel, map_one
-- Module: Mathlib.RingTheory.Idempotents
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 :
  ∀ (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
⊢ (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

Premises used: HSub.hSub, Commute.sub_dvd_pow_sub_pow, HPow.hPow, OfNat.ofNat, MulOpposite.op, Commute.one_left
-- Module: Mathlib.RingTheory.Idempotents
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
k : Rᵐᵒᵖ
hk : HPow.hPow (α := Rᵐᵒᵖ) 1 n - MulOpposite.op (1 - a ^ n) ^ n = (1 - MulOpposite.op (1 - a ^ n)) * k
⊢ MulOpposite.unop (HPow.hPow (α := Rᵐᵒᵖ) 1 n - MulOpposite.op (1 - a ^ n) ^ n) =
    MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ n)) * k)

Tactic:
apply_fun MulOpposite.unop at hk

Premises used: MulOpposite.unop
-- Module: Mathlib.RingTheory.Idempotents
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
k : Rᵐᵒᵖ
hk :
  MulOpposite.unop (HPow.hPow (α := Rᵐᵒᵖ) 1 n - MulOpposite.op (1 - a ^ n) ^ n) =
    MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ n)) * k)
⊢ 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n

Tactic:
simpa using hk
-- Module: Mathlib.RingTheory.Idempotents
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
k : Rᵐᵒᵖ
hk :
  MulOpposite.unop (HPow.hPow (α := Rᵐᵒᵖ) 1 n - MulOpposite.op (1 - a ^ n) ^ n) =
    MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ n)) * k)
⊢ 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n

Tactic:
have : 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n := by simpa using hk
-- Module: Mathlib.RingTheory.Idempotents
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
k : Rᵐᵒᵖ
hk :
  MulOpposite.unop (HPow.hPow (α := Rᵐᵒᵖ) 1 n - MulOpposite.op (1 - a ^ n) ^ n) =
    MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ n)) * k)
this : 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n
inr : MulOpposite.unop k * (a ^ n * e₂) = 0
⊢ (1 - (1 - a ^ n) ^ n) * e₂ = 0

Tactic:
rw [this, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Idempotents
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
k : Rᵐᵒᵖ
hk :
  MulOpposite.unop (HPow.hPow (α := Rᵐᵒᵖ) 1 n - MulOpposite.op (1 - a ^ n) ^ n) =
    MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ n)) * k)
this : 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n
inr :
  ∀ (hn : HPow.hPow (β := ℕ) (a - HPow.hPow (β := ℕ) a 2) 0 = 0)
    (hk :
      MulOpposite.unop
          (HPow.hPow (α := Rᵐᵒᵖ) (β := ℕ) 1 0 - HPow.hPow (β := ℕ) (MulOpposite.op (1 - HPow.hPow (β := ℕ) a 0)) 0) =
        MulOpposite.unop ((1 - MulOpposite.op (1 - HPow.hPow (β := ℕ) a 0)) * k))
    (this : 1 - HPow.hPow (β := ℕ) (1 - HPow.hPow (β := ℕ) a 0) 0 = MulOpposite.unop k * HPow.hPow (β := ℕ) a 0),
    MulOpposite.unop k * (HPow.hPow (β := ℕ) a 0 * e₂) = 0
inr₁ :
  ∀ (n : ℕ) (hn : (a - HPow.hPow (β := ℕ) a 2) ^ (n + 1) = 0)
    (hk :
      MulOpposite.unop (HPow.hPow (α := Rᵐᵒᵖ) 1 (n + 1) - MulOpposite.op (1 - a ^ (n + 1)) ^ (n + 1)) =
        MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ (n + 1))) * k))
    (this : 1 - (1 - a ^ (n + 1)) ^ (n + 1) = MulOpposite.unop k * a ^ (n + 1)),
    MulOpposite.unop k * (a ^ (n + 1) * e₂) = 0
⊢ MulOpposite.unop k * (a ^ n * e₂) = 0

Tactic:
rcases n with - | n
-- Module: Mathlib.RingTheory.Idempotents
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)
k : Rᵐᵒᵖ
hn : HPow.hPow (β := ℕ) (a - HPow.hPow (β := ℕ) a 2) 0 = 0
hk :
  MulOpposite.unop
      (HPow.hPow (α := Rᵐᵒᵖ) (β := ℕ) 1 0 - HPow.hPow (β := ℕ) (MulOpposite.op (1 - HPow.hPow (β := ℕ) a 0)) 0) =
    MulOpposite.unop ((1 - MulOpposite.op (1 - HPow.hPow (β := ℕ) a 0)) * k)
this : 1 - HPow.hPow (β := ℕ) (1 - HPow.hPow (β := ℕ) a 0) 0 = MulOpposite.unop k * HPow.hPow (β := ℕ) a 0
⊢ MulOpposite.unop k * (HPow.hPow (β := ℕ) a 0 * e₂) = 0

Tactic:
simp at hn
-- Module: Mathlib.RingTheory.Idempotents
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)
k : Rᵐᵒᵖ
n : ℕ
hn : (a - HPow.hPow (β := ℕ) a 2) ^ (n + 1) = 0
hk :
  MulOpposite.unop (HPow.hPow (α := Rᵐᵒᵖ) 1 (n + 1) - MulOpposite.op (1 - a ^ (n + 1)) ^ (n + 1)) =
    MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ (n + 1))) * k)
this : 1 - (1 - a ^ (n + 1)) ^ (n + 1) = MulOpposite.unop k * a ^ (n + 1)
inr : MulOpposite.unop k * (a ^ n * a * e₂) = 0
inr₁ : MulOpposite.unop k * (a ^ n * (a * e₂)) = 0
inr₂ : MulOpposite.unop k * (a ^ n * 0) = 0
inr₃ : MulOpposite.unop k * 0 = 0
inr₄ inr₅ : Eq.{u_1 + 1} (α := R) 0 0
⊢ MulOpposite.unop k * (a ^ (n + 1) * e₂) = 0

Tactic:
rw [pow_succ, mul_assoc, ha', mul_zero, mul_zero]

Premises used: pow_succ, mul_assoc, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.Idempotents
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
he₂e₁ : HMul.hMul (α := S) ((f : (a : R) → S) e₂ : S) e₁ = 0
obtain :
  ∀ (e' : R) (h₁ : IsIdempotentElem e') (h₂ : e' * e₂ = 0)
    (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))
    (he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0)
    (he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0),
    ∃ (e'_1 : R),
      IsIdempotentElem e'_1 ∧
        Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e'_1 : S) ((f : (a : R) → S) e' : S) ∧ e'_1 * e₂ = 0 ∧ e₂ * e'_1 = 0
⊢ ∃ (e' : R), IsIdempotentElem e' ∧ (f : (a : R) → S) e' = e₁ ∧ e' * e₂ = 0 ∧ e₂ * e' = 0

Tactic:
obtain ⟨e', h₁, rfl, h₂⟩ := exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux
    f h e₁ he he₁ e₂ he₂ he₁e₂

Premises used: exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux, rfl
-- Module: Mathlib.RingTheory.Idempotents
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
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
⊢ ∃ (e'_1 : R),
    IsIdempotentElem e'_1 ∧
      Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e'_1 : S) ((f : (a : R) → S) e' : S) ∧ e'_1 * e₂ = 0 ∧ e₂ * e'_1 = 0

Tactic:
⟨(1 - e₂) * e', ?_, ?_, ?_, ?_⟩

Premises used: HMul.hMul, HSub.hSub, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Idempotents
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
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
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)
he₁e₂ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e' : S) ((f : (a : R) → S) e₂ : S) = 0
he₂e₁ : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) e₂ : S) ((f : (a : R) → S) e' : S) = 0
refine_1 : IsIdempotentElem ((1 - e₂) * e')
refine_2 : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) ((1 - e₂) * e') : S) ((f : (a : R) → S) e' : S)
refine_3 : (1 - e₂) * e' * e₂ = 0
refine_4 : e₂ * ((1 - e₂) * e') = 0
⊢ ∃ (e'_1 : R),
    IsIdempotentElem e'_1 ∧
      Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) e'_1 : S) ((f : (a : R) → S) e' : S) ∧ e'_1 * e₂ = 0 ∧ e₂ * e'_1 = 0

Tactic:
refine ⟨(1 - e₂) * e', ?_, ?_, ?_, ?_⟩