awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
n m : ℤ
⊢ (↑(n * m) : X q) = HMul.hMul (α := X q) (↑n : X q) (↑m : X q)
have h₁ : (↑(n * m) : X q).1 = (HMul.hMul (α := X q) (↑n : X q) (↑m : X q)).1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
n m : ℤ
h₁ : (↑(n * m) : X q).1 = (HMul.hMul (α := X q) (↑n : X q) (↑m : X q)).1
⊢ (↑(n * m) : X q) = HMul.hMul (α := X q) (↑n : X q) (↑m : X q)
have h₂ : (↑(n * m) : X q).2 = (HMul.hMul (α := X q) (↑n : X q) (↑m : X q)).2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q n : ℕ
⊢ Eq (α := X q) (↑(↑n : ℤ) : X q) (↑n : X q)
have h₁ : Eq (α := ZMod q) (↑(↑n : ℤ) : X q).1 (↑n : X q).1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q n : ℕ
h₁ : Eq (α := ZMod q) (↑(↑n : ℤ) : X q).1 (↑n : X q).1
⊢ Eq (α := X q) (↑(↑n : ℤ) : X q) (↑n : X q)
have h₂ : Eq (α := ZMod q) (↑(↑n : ℤ) : X q).2 (↑n : X q).2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
⊢ HMul.hMul (α := X q) ω ωb = 1
have dsimp : HMul.hMul (α := X q) (2, 1) (2, -1) = 1
Tactic: dsimp [ω, ωb]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
⊢ HMul.hMul (α := X q) (2, 1) (2, -1) = 1
have h₁ : (HMul.hMul (α := X q) (2, 1) (2, -1)).1 = 1.1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
h₁ : (HMul.hMul (α := X q) (2, 1) (2, -1)).1 = 1.1
⊢ HMul.hMul (α := X q) (2, 1) (2, -1) = 1
have h₂ : (HMul.hMul (α := X q) (2, 1) (2, -1)).2 = 1.2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
⊢ (HMul.hMul (α := X q) (2, 1) (2, -1)).1 = 1.1
have h₁ : HMul.hMul (α := ZMod q) 2 2 + -3 = 1
Tactic: simp
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
⊢ HMul.hMul (α := X q) ωb ω = 1
have rw : HMul.hMul (α := X q) ω ωb = 1
Tactic: rw [mul_comm, ω_mul_ωb]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
rw : HMul.hMul (α := X q) ω ωb = 1
⊢ HMul.hMul (α := X q) ωb ω = 1
have rw₁ : Eq (α := X q) 1 1
Tactic: rw [mul_comm, ω_mul_ωb]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
⊢ (↑4 : X q) = HPow.hPow (α := X q) (β := ℕ) (2, 1) 1 + HPow.hPow (α := X q) (β := ℕ) (2, -1) 1
have zero : (↑4 : X q).1 = (HPow.hPow (α := X q) (β := ℕ) (2, 1) 1 + HPow.hPow (α := X q) (β := ℕ) (2, -1) 1).1
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q : ℕ
zero : (↑4 : X q).1 = (HPow.hPow (α := X q) (β := ℕ) (2, 1) 1 + HPow.hPow (α := X q) (β := ℕ) (2, -1) 1).1
⊢ (↑4 : X q) = HPow.hPow (α := X q) (β := ℕ) (2, 1) 1 + HPow.hPow (α := X q) (β := ℕ) (2, -1) 1
have zero₁ : (↑4 : X q).2 = (HPow.hPow (α := X q) (β := ℕ) (2, 1) 1 + HPow.hPow (α := X q) (β := ℕ) (2, -1) 1).2
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
⊢ (↑(HPow.hPow (β := ℕ) (s i) 2 - 2) : X q) = HPow.hPow (α := X q) (β := ℕ) (↑(s i) : X q) 2 - 2
have push_cast : HPow.hPow (α := X q) (β := ℕ) (↑(s i) : X q) 2 - 2 = HPow.hPow (α := X q) (β := ℕ) (↑(s i) : X q) 2 - 2
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
⊢ HPow.hPow (α := X q) (β := ℕ) (↑(s i) : X q) 2 - 2 =
    HPow.hPow (β := ℕ)
        (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 -
      2
have rw : HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i))
      2 -
    2 =
  HPow.hPow (β := ℕ)
      (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 -
    2
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 * (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i) * HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
have rw : HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
        HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
      2 * HMul.hMul (α := X q) ωb ω ^ HPow.hPow (α := ℕ) 2 i -
    2 =
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
Tactic: rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
rw :
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 * HMul.hMul (α := X q) ωb ω ^ HPow.hPow (α := ℕ) 2 i -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 * (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i) * HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
have rw₁ : HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
        HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
      2 * HPow.hPow (α := X q) 1 (HPow.hPow (α := ℕ) 2 i) -
    2 =
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
Tactic: rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
rw :
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 * HMul.hMul (α := X q) ωb ω ^ HPow.hPow (α := ℕ) 2 i -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
rw₁ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 * HPow.hPow (α := X q) 1 (HPow.hPow (α := ℕ) 2 i) -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 * (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i) * HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
have rw₂ : HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
        HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
      HMul.hMul (α := X q) 2 1 -
    2 =
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
Tactic: rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
rw :
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 * HMul.hMul (α := X q) ωb ω ^ HPow.hPow (α := ℕ) 2 i -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
rw₁ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 * HPow.hPow (α := X q) 1 (HPow.hPow (α := ℕ) 2 i) -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
rw₂ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        HMul.hMul (α := X q) 2 1 -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 * (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i) * HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
have rw₃ : HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
        HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
      2 -
    2 =
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
Tactic: rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
rw :
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 * HMul.hMul (α := X q) ωb ω ^ HPow.hPow (α := ℕ) 2 i -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
rw₁ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 * HPow.hPow (α := X q) 1 (HPow.hPow (α := ℕ) 2 i) -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
rw₂ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        HMul.hMul (α := X q) 2 1 -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
rw₃ :
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 * (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i) * HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
have rw₄ : HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 =
  HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
Tactic: rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 =
    HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))
have rw : HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i * 2) +
    HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 =
  HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))
Tactic: rw [← pow_mul, ← pow_mul, _root_.pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
rw :
  HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i * 2) +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 =
    HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 =
    HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))
have rw₁ : HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i * 2) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i * 2) =
  HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))
Tactic: rw [← pow_mul, ← pow_mul, _root_.pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
rw :
  HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i * 2) +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 =
    HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))
rw₁ :
  HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i * 2) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i * 2) =
    HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
      HPow.hPow (β := ℕ) (HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 =
    HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))
have rw₂ : HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i * 2) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i * 2) =
  HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i * 2) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i * 2)
Tactic: rw [← pow_mul, ← pow_mul, _root_.pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
ih : (↑(s i) : X q) = HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 i) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 i)
⊢ (↑(s (i + 1)) : X q) =
    HPow.hPow (α := X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) + HPow.hPow (α := X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))
have X : (↑(HPow.hPow (β := ℕ) (s i) 2 - 2) : X q) = HPow.hPow (α := X q) (β := ℕ) (↑(s i) : X q) 2 - 2
Tactic: calc
      (s (i + 1) : X q) = (s i ^ 2 - 2 : ℤ) := rfl
      _ = (s i : X q) ^ 2 - 2 := by push_cast; rfl
      _ = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 := by rw [ih]
      _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 := by ring
      _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 := by
        rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]
      _ = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1) := by rw [← pow_mul, ← pow_mul, _root_.pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
ih :
  (↑(s i) : LucasLehmer.X q) =
    HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i) +
      HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i)
X :
  (↑(HPow.hPow (β := ℕ) (s i) 2 - 2) : LucasLehmer.X q) =
    HPow.hPow (α := LucasLehmer.X q) (β := ℕ) (↑(s i) : LucasLehmer.X q) 2 - 2
⊢ (↑(s (i + 1)) : LucasLehmer.X q) =
    HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) +
      HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))
have X₁ : HPow.hPow (α := LucasLehmer.X q) (β := ℕ) (↑(s i) : LucasLehmer.X q) 2 - 2 =
  HPow.hPow (β := ℕ)
      (HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i) +
        HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i))
      2 -
    2
Tactic: calc
      (s (i + 1) : X q) = (s i ^ 2 - 2 : ℤ) := rfl
      _ = (s i : X q) ^ 2 - 2 := by push_cast; rfl
      _ = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 := by rw [ih]
      _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 := by ring
      _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 := by
        rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]
      _ = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1) := by rw [← pow_mul, ← pow_mul, _root_.pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
ih :
  (↑(s i) : LucasLehmer.X q) =
    HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i) +
      HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i)
X :
  (↑(HPow.hPow (β := ℕ) (s i) 2 - 2) : LucasLehmer.X q) =
    HPow.hPow (α := LucasLehmer.X q) (β := ℕ) (↑(s i) : LucasLehmer.X q) 2 - 2
X₁ :
  HPow.hPow (α := LucasLehmer.X q) (β := ℕ) (↑(s i) : LucasLehmer.X q) 2 - 2 =
    HPow.hPow (β := ℕ)
        (HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i) +
          HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i))
        2 -
      2
⊢ (↑(s (i + 1)) : LucasLehmer.X q) =
    HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) +
      HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))
have X₂ : HPow.hPow (β := ℕ)
      (HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i) +
        HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i))
      2 -
    2 =
  HPow.hPow (β := ℕ) (HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
        HPow.hPow (β := ℕ) (HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
      2 *
        (HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i) *
          HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i)) -
    2
Tactic: calc
      (s (i + 1) : X q) = (s i ^ 2 - 2 : ℤ) := rfl
      _ = (s i : X q) ^ 2 - 2 := by push_cast; rfl
      _ = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 := by rw [ih]
      _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 := by ring
      _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 := by
        rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]
      _ = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1) := by rw [← pow_mul, ← pow_mul, _root_.pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.LucasLehmer (goal)
Goal:
q i : ℕ
ih :
  (↑(s i) : LucasLehmer.X q) =
    HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i) +
      HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i)
X :
  (↑(HPow.hPow (β := ℕ) (s i) 2 - 2) : LucasLehmer.X q) =
    HPow.hPow (α := LucasLehmer.X q) (β := ℕ) (↑(s i) : LucasLehmer.X q) 2 - 2
X₁ :
  HPow.hPow (α := LucasLehmer.X q) (β := ℕ) (↑(s i) : LucasLehmer.X q) 2 - 2 =
    HPow.hPow (β := ℕ)
        (HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i) +
          HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i))
        2 -
      2
X₂ :
  HPow.hPow (β := ℕ)
        (HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i) +
          HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i))
        2 -
      2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
          HPow.hPow (β := ℕ) (HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
        2 *
          (HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i) *
            HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i)) -
      2
⊢ (↑(s (i + 1)) : LucasLehmer.X q) =
    HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 (i + 1)) +
      HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 (i + 1))
have X₃ : HPow.hPow (β := ℕ) (HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
        HPow.hPow (β := ℕ) (HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2 +
      2 *
        (HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i) *
          HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i)) -
    2 =
  HPow.hPow (β := ℕ) (HPow.hPow (α := LucasLehmer.X q) ω (HPow.hPow (α := ℕ) 2 i)) 2 +
    HPow.hPow (β := ℕ) (HPow.hPow (α := LucasLehmer.X q) ωb (HPow.hPow (α := ℕ) 2 i)) 2
Tactic: calc
      (s (i + 1) : X q) = (s i ^ 2 - 2 : ℤ) := rfl
      _ = (s i : X q) ^ 2 - 2 := by push_cast; rfl
      _ = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 := by rw [ih]
      _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 := by ring
      _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 := by
        rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]
      _ = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1) := by rw [← pow_mul, ← pow_mul, _root_.pow_succ]