-- Mathlib/RingTheory/Idempotents.lean
theorem isIdempotentElem_one_sub_one_sub_pow_pow
    (x : R) (n : ℕ) (hx : (x - x ^ 2) ^ n = 0) :
    IsIdempotentElem (1 - (1 - x ^ n) ^ n)

Proof state:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
⊢ Polynomial.X ^ n ∣ P

Tactic:
have := sub_dvd_pow_sub_pow 1 ((1 : Polynomial ℤ) - Polynomial.X ^ n) n

Result:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
this : 1 - (1 - Polynomial.X ^ n) ∣ 1 ^ n - (1 - Polynomial.X ^ n) ^ n
⊢ Polynomial.X ^ n ∣ P

Proof state:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
H₁ : Polynomial.X ^ n ∣ P
⊢ (Polynomial.X - Polynomial.X ^ 2) ^ n ∣ P - P ^ 2

Tactic:
have H₂ : (1 - .X) ^ n ∣ 1 - P := by
  simp only [sub_sub_cancel, P]
  simpa using pow_dvd_pow_of_dvd (sub_dvd_pow_sub_pow (α := Polynomial ℤ) 1 Polynomial.X n) n

Result:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
H₁ : Polynomial.X ^ n ∣ P
H₂ : (1 - Polynomial.X) ^ n ∣ 1 - P
⊢ (Polynomial.X - Polynomial.X ^ 2) ^ n ∣ P - P ^ 2

Proof state:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
H₁ : Polynomial.X ^ n ∣ P
⊢ (1 - Polynomial.X) ^ n ∣ 1 - P

Tactic:
simp only [sub_sub_cancel, P]

Result:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
H₁ : Polynomial.X ^ n ∣ P
⊢ (1 - Polynomial.X) ^ n ∣ (1 - Polynomial.X ^ n) ^ n

Proof state:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
this : 1 - (1 - Polynomial.X ^ n) ∣ 1 ^ n - (1 - Polynomial.X ^ n) ^ n
⊢ Polynomial.X ^ n ∣ P

Tactic:
rwa [sub_sub_cancel, one_pow] at this

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
⊢ (Polynomial.X - Polynomial.X ^ 2) ^ n ∣ P - P ^ 2

Tactic:
have H₁ : .X ^ n ∣ P := by
  have := sub_dvd_pow_sub_pow 1 ((1 : Polynomial ℤ) - Polynomial.X ^ n) n
  rwa [sub_sub_cancel, one_pow] at this

Result:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
H₁ : Polynomial.X ^ n ∣ P
⊢ (Polynomial.X - Polynomial.X ^ 2) ^ n ∣ P - P ^ 2

Proof state:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
H₁ : Polynomial.X ^ n ∣ P
H₂ : (1 - Polynomial.X) ^ n ∣ 1 - P
this : Polynomial.X ^ n * (1 - Polynomial.X) ^ n ∣ P * (1 - P)
⊢ (Polynomial.X - Polynomial.X ^ 2) ^ n ∣ P - P ^ 2

Tactic:
simpa only [← mul_pow, mul_sub, mul_one, ← pow_two] using this

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
this✝ : (Polynomial.X - Polynomial.X ^ 2) ^ n ∣ P - P ^ 2
this : (Polynomial.aeval x) ((Polynomial.X - Polynomial.X ^ 2) ^ n) ∣ (Polynomial.aeval x) (P - P ^ 2)
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)

Tactic:
simp only [map_pow, map_sub, Polynomial.aeval_X, hx, map_one, zero_dvd_iff, P] at this

Result:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
this✝ : (Polynomial.X - Polynomial.X ^ 2) ^ n ∣ P - P ^ 2
this : 1 - (1 - x ^ n) ^ n - (1 - (1 - x ^ n) ^ n) ^ 2 = 0
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)

Proof state:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
H₁ : Polynomial.X ^ n ∣ P
H₂ : (1 - Polynomial.X) ^ n ∣ 1 - P
⊢ (Polynomial.X - Polynomial.X ^ 2) ^ n ∣ P - P ^ 2

Tactic:
have := mul_dvd_mul H₁ H₂

Result:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
H₁ : Polynomial.X ^ n ∣ P
H₂ : (1 - Polynomial.X) ^ n ∣ 1 - P
this : Polynomial.X ^ n * (1 - Polynomial.X) ^ n ∣ P * (1 - P)
⊢ (Polynomial.X - Polynomial.X ^ 2) ^ n ∣ P - P ^ 2

Proof state:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
this✝ : (Polynomial.X - Polynomial.X ^ 2) ^ n ∣ P - P ^ 2
this : 1 - (1 - x ^ n) ^ n - (1 - (1 - x ^ n) ^ n) ^ 2 = 0
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)

Tactic:
rwa [sub_eq_zero, eq_comm, pow_two] at this

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)

Tactic:
have : (.X - .X ^ 2) ^ n ∣ P - P ^ 2 := by
  have H₁ : .X ^ n ∣ P := by
    have := sub_dvd_pow_sub_pow 1 ((1 : Polynomial ℤ) - Polynomial.X ^ n) n
    rwa [sub_sub_cancel, one_pow] at this
  have H₂ : (1 - .X) ^ n ∣ 1 - P := by
    simp only [sub_sub_cancel, P]
    simpa using pow_dvd_pow_of_dvd (sub_dvd_pow_sub_pow (α := Polynomial ℤ) 1 Polynomial.X n) n
  have := mul_dvd_mul H₁ H₂
  simpa only [← mul_pow, mul_sub, mul_one, ← pow_two] using this

Result:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
this : (Polynomial.X - Polynomial.X ^ 2) ^ n ∣ P - P ^ 2
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)

Proof state:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)

Tactic:
let P : Polynomial ℤ := 1 - (1 - .X ^ n) ^ n

Result:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)

Proof state:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
this : (Polynomial.X - Polynomial.X ^ 2) ^ n ∣ P - P ^ 2
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)

Tactic:
have := map_dvd (Polynomial.aeval x) this

Result:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
this✝ : (Polynomial.X - Polynomial.X ^ 2) ^ n ∣ P - P ^ 2
this : (Polynomial.aeval x) ((Polynomial.X - Polynomial.X ^ 2) ^ n) ∣ (Polynomial.aeval x) (P - P ^ 2)
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)

Proof state:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n
H₁ : Polynomial.X ^ n ∣ P
⊢ (1 - Polynomial.X) ^ n ∣ (1 - Polynomial.X ^ n) ^ n

Tactic:
simpa using pow_dvd_pow_of_dvd (sub_dvd_pow_sub_pow (α := Polynomial ℤ) 1 Polynomial.X n) n

Result:
no goals