awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ (1 - (1 - a ^ n) ^ n) * e₂ = 0
have hk₁ : 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
Cleared hypotheses: hk
-- 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
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) * e₂ = 0
have this : 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
-- 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
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
⊢ (1 - (1 - a ^ n) ^ n) * e₂ = 0
have inr : MulOpposite.unop k * (a ^ n * e₂) = 0
Tactic: rw [this, mul_assoc]
-- 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
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
⊢ MulOpposite.unop k * (a ^ n * e₂) = 0
have 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
Tactic: rcases n with - | n
Cleared hypotheses: n, hn, hk, 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₂ : 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
⊢ MulOpposite.unop k * (a ^ n * e₂) = 0
have 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
Tactic: rcases n with - | n
Cleared hypotheses: n, hn, hk, 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₂ : 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)
⊢ MulOpposite.unop k * (a ^ (n + 1) * e₂) = 0
have inr : MulOpposite.unop k * (a ^ n * a * e₂) = 0
Tactic: rw [pow_succ, mul_assoc, ha', mul_zero, mul_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)
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
⊢ MulOpposite.unop k * (a ^ (n + 1) * e₂) = 0
have inr₁ : MulOpposite.unop k * (a ^ n * (a * e₂)) = 0
Tactic: rw [pow_succ, mul_assoc, ha', mul_zero, mul_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)
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
⊢ MulOpposite.unop k * (a ^ (n + 1) * e₂) = 0
have inr₂ : MulOpposite.unop k * (a ^ n * 0) = 0
Tactic: rw [pow_succ, mul_assoc, ha', mul_zero, mul_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)
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
⊢ MulOpposite.unop k * (a ^ (n + 1) * e₂) = 0
have inr₃ : MulOpposite.unop k * 0 = 0
Tactic: rw [pow_succ, mul_assoc, ha', mul_zero, mul_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)
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
⊢ MulOpposite.unop k * (a ^ (n + 1) * e₂) = 0
have inr₄ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [pow_succ, mul_assoc, ha', mul_zero, mul_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₁ : 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
⊢ ∃ (e' : R), IsIdempotentElem e' ∧ (f : (a : R) → S) e' = e₁ ∧ e' * e₂ = 0 ∧ e₂ * e' = 0
have 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
Tactic: obtain ⟨e', h₁, rfl, h₂⟩ := exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux
    f h e₁ he he₁ e₂ he₂ he₁e₂
Cleared hypotheses: e₁, he, he₁, he₁e₂, 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
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
have refine_1 : IsIdempotentElem ((1 - e₂) * e')
Tactic: refine ⟨(1 - e₂) * 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
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')
⊢ ∃ (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
have refine_2 : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) ((1 - e₂) * e') : S) ((f : (a : R) → S) e' : S)
Tactic: refine ⟨(1 - e₂) * 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
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)
⊢ ∃ (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
have refine_3 : (1 - e₂) * e' * e₂ = 0
Tactic: refine ⟨(1 - e₂) * 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
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
⊢ ∃ (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
have refine_4 : e₂ * ((1 - e₂) * e') = 0
Tactic: refine ⟨(1 - e₂) * 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
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
⊢ IsIdempotentElem ((1 - e₂) * e')
have refine_1 : (1 - e₂) * e' * ((1 - e₂) * e') = (1 - e₂) * e'
Tactic: rw [IsIdempotentElem, mul_assoc, ← mul_assoc e', mul_sub, mul_one, h₂, sub_zero, h₁.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
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 : (1 - e₂) * e' * ((1 - e₂) * e') = (1 - e₂) * e'
⊢ IsIdempotentElem ((1 - e₂) * e')
have refine_1₁ : (1 - e₂) * (e' * ((1 - e₂) * e')) = (1 - e₂) * e'
Tactic: rw [IsIdempotentElem, mul_assoc, ← mul_assoc e', mul_sub, mul_one, h₂, sub_zero, h₁.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
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 : (1 - e₂) * e' * ((1 - e₂) * e') = (1 - e₂) * e'
refine_1₁ : (1 - e₂) * (e' * ((1 - e₂) * e')) = (1 - e₂) * e'
⊢ IsIdempotentElem ((1 - e₂) * e')
have refine_1₂ : (1 - e₂) * (e' * (1 - e₂) * e') = (1 - e₂) * e'
Tactic: rw [IsIdempotentElem, mul_assoc, ← mul_assoc e', mul_sub, mul_one, h₂, sub_zero, h₁.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
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 : (1 - e₂) * e' * ((1 - e₂) * e') = (1 - e₂) * e'
refine_1₁ : (1 - e₂) * (e' * ((1 - e₂) * e')) = (1 - e₂) * e'
refine_1₂ : (1 - e₂) * (e' * (1 - e₂) * e') = (1 - e₂) * e'
⊢ IsIdempotentElem ((1 - e₂) * e')
have refine_1₃ : (1 - e₂) * ((e' * 1 - e' * e₂) * e') = (1 - e₂) * e'
Tactic: rw [IsIdempotentElem, mul_assoc, ← mul_assoc e', mul_sub, mul_one, h₂, sub_zero, h₁.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
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 : (1 - e₂) * e' * ((1 - e₂) * e') = (1 - e₂) * e'
refine_1₁ : (1 - e₂) * (e' * ((1 - e₂) * e')) = (1 - e₂) * e'
refine_1₂ : (1 - e₂) * (e' * (1 - e₂) * e') = (1 - e₂) * e'
refine_1₃ : (1 - e₂) * ((e' * 1 - e' * e₂) * e') = (1 - e₂) * e'
⊢ IsIdempotentElem ((1 - e₂) * e')
have refine_1₄ : (1 - e₂) * ((e' - e' * e₂) * e') = (1 - e₂) * e'
Tactic: rw [IsIdempotentElem, mul_assoc, ← mul_assoc e', mul_sub, mul_one, h₂, sub_zero, h₁.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
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 : (1 - e₂) * e' * ((1 - e₂) * e') = (1 - e₂) * e'
refine_1₁ : (1 - e₂) * (e' * ((1 - e₂) * e')) = (1 - e₂) * e'
refine_1₂ : (1 - e₂) * (e' * (1 - e₂) * e') = (1 - e₂) * e'
refine_1₃ : (1 - e₂) * ((e' * 1 - e' * e₂) * e') = (1 - e₂) * e'
refine_1₄ : (1 - e₂) * ((e' - e' * e₂) * e') = (1 - e₂) * e'
⊢ IsIdempotentElem ((1 - e₂) * e')
have refine_1₅ : (1 - e₂) * ((e' - 0) * e') = (1 - e₂) * e'
Tactic: rw [IsIdempotentElem, mul_assoc, ← mul_assoc e', mul_sub, mul_one, h₂, sub_zero, h₁.eq]