awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
inr :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2) 3 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₁ :
  HPow.hPow (β := ℕ) S'.a 3 + (↑η : 𝓞 K) ^ HMul.hMul (α := ℕ) 2 3 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₂ :
  HPow.hPow (β := ℕ) S'.a 3 + (↑η : 𝓞 K) ^ HMul.hMul (α := ℕ) 3 2 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₃ :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 3) 2 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₄ :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) hζ.toInteger 3) 2 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
⊢ HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
have inr₅ : HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (α := 𝓞 K) (β := ℕ) 1 2 * HPow.hPow (β := ℕ) S'.b 3 =
  (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
Tactic: rw [mul_pow, ← pow_mul, mul_comm 2, pow_mul, coe_eta, hζ.toInteger_cube_eq_one, one_pow,
        one_mul, S'.H]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
inr :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2) 3 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₁ :
  HPow.hPow (β := ℕ) S'.a 3 + (↑η : 𝓞 K) ^ HMul.hMul (α := ℕ) 2 3 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₂ :
  HPow.hPow (β := ℕ) S'.a 3 + (↑η : 𝓞 K) ^ HMul.hMul (α := ℕ) 3 2 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₃ :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 3) 2 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₄ :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) hζ.toInteger 3) 2 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₅ :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (α := 𝓞 K) (β := ℕ) 1 2 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
⊢ HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
have inr₆ : HPow.hPow (β := ℕ) S'.a 3 + 1 * HPow.hPow (β := ℕ) S'.b 3 = (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
Tactic: rw [mul_pow, ← pow_mul, mul_comm 2, pow_mul, coe_eta, hζ.toInteger_cube_eq_one, one_pow,
        one_mul, S'.H]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
inr :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2) 3 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₁ :
  HPow.hPow (β := ℕ) S'.a 3 + (↑η : 𝓞 K) ^ HMul.hMul (α := ℕ) 2 3 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₂ :
  HPow.hPow (β := ℕ) S'.a 3 + (↑η : 𝓞 K) ^ HMul.hMul (α := ℕ) 3 2 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₃ :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 3) 2 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₄ :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) hζ.toInteger 3) 2 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₅ :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (α := 𝓞 K) (β := ℕ) 1 2 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₆ : HPow.hPow (β := ℕ) S'.a 3 + 1 * HPow.hPow (β := ℕ) S'.b 3 = (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
⊢ HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
have inr₇ : HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3 = (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
Tactic: rw [mul_pow, ← pow_mul, mul_comm 2, pow_mul, coe_eta, hζ.toInteger_cube_eq_one, one_pow,
        one_mul, S'.H]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
inr :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2) 3 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₁ :
  HPow.hPow (β := ℕ) S'.a 3 + (↑η : 𝓞 K) ^ HMul.hMul (α := ℕ) 2 3 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₂ :
  HPow.hPow (β := ℕ) S'.a 3 + (↑η : 𝓞 K) ^ HMul.hMul (α := ℕ) 3 2 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₃ :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 3) 2 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₄ :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) hζ.toInteger 3) 2 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₅ :
  HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (α := 𝓞 K) (β := ℕ) 1 2 * HPow.hPow (β := ℕ) S'.b 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₆ : HPow.hPow (β := ℕ) S'.a 3 + 1 * HPow.hPow (β := ℕ) S'.b 3 = (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
inr₇ : HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) S'.b 3 = (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
⊢ HPow.hPow (β := ℕ) S'.a 3 + HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) 3 =
    (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
have inr₈ : (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3 = (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
Tactic: rw [mul_pow, ← pow_mul, mul_comm 2, pow_mul, coe_eta, hζ.toInteger_cube_eq_one, one_pow,
        one_mul, S'.H]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
h_1 : λ ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
x : 𝓞 K
hx : HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b = λ * x
⊢ S'.b = λ * ((↑η : 𝓞 K) * x)
have inr : S'.b = λ * (x * (↑η : 𝓞 K))
Tactic: rw [mul_comm _ x, ← mul_assoc, ← hx, mul_comm _ S'.b, mul_assoc, ← pow_succ, coe_eta,
        hζ.toInteger_cube_eq_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
h_1 : λ ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
x : 𝓞 K
hx : HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b = λ * x
inr : S'.b = λ * (x * (↑η : 𝓞 K))
⊢ S'.b = λ * ((↑η : 𝓞 K) * x)
have inr₁ : S'.b = λ * x * (↑η : 𝓞 K)
Tactic: rw [mul_comm _ x, ← mul_assoc, ← hx, mul_comm _ S'.b, mul_assoc, ← pow_succ, coe_eta,
        hζ.toInteger_cube_eq_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
h_1 : λ ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
x : 𝓞 K
hx : HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b = λ * x
inr : S'.b = λ * (x * (↑η : 𝓞 K))
inr₁ : S'.b = λ * x * (↑η : 𝓞 K)
⊢ S'.b = λ * ((↑η : 𝓞 K) * x)
have inr₂ : S'.b = HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b * (↑η : 𝓞 K)
Tactic: rw [mul_comm _ x, ← mul_assoc, ← hx, mul_comm _ S'.b, mul_assoc, ← pow_succ, coe_eta,
        hζ.toInteger_cube_eq_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
h_1 : λ ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
x : 𝓞 K
hx : HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b = λ * x
inr : S'.b = λ * (x * (↑η : 𝓞 K))
inr₁ : S'.b = λ * x * (↑η : 𝓞 K)
inr₂ : S'.b = HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b * (↑η : 𝓞 K)
⊢ S'.b = λ * ((↑η : 𝓞 K) * x)
have inr₃ : S'.b = S'.b * HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * (↑η : 𝓞 K)
Tactic: rw [mul_comm _ x, ← mul_assoc, ← hx, mul_comm _ S'.b, mul_assoc, ← pow_succ, coe_eta,
        hζ.toInteger_cube_eq_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
h_1 : λ ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
x : 𝓞 K
hx : HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b = λ * x
inr : S'.b = λ * (x * (↑η : 𝓞 K))
inr₁ : S'.b = λ * x * (↑η : 𝓞 K)
inr₂ : S'.b = HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b * (↑η : 𝓞 K)
inr₃ : S'.b = S'.b * HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * (↑η : 𝓞 K)
⊢ S'.b = λ * ((↑η : 𝓞 K) * x)
have inr₄ : S'.b = S'.b * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * (↑η : 𝓞 K))
Tactic: rw [mul_comm _ x, ← mul_assoc, ← hx, mul_comm _ S'.b, mul_assoc, ← pow_succ, coe_eta,
        hζ.toInteger_cube_eq_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
h_1 : λ ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
x : 𝓞 K
hx : HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b = λ * x
inr : S'.b = λ * (x * (↑η : 𝓞 K))
inr₁ : S'.b = λ * x * (↑η : 𝓞 K)
inr₂ : S'.b = HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b * (↑η : 𝓞 K)
inr₃ : S'.b = S'.b * HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * (↑η : 𝓞 K)
inr₄ : S'.b = S'.b * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * (↑η : 𝓞 K))
⊢ S'.b = λ * ((↑η : 𝓞 K) * x)
have inr₅ : S'.b = S'.b * (↑η : 𝓞 K) ^ HAdd.hAdd (α := ℕ) 2 1
Tactic: rw [mul_comm _ x, ← mul_assoc, ← hx, mul_comm _ S'.b, mul_assoc, ← pow_succ, coe_eta,
        hζ.toInteger_cube_eq_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
h_1 : λ ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
x : 𝓞 K
hx : HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b = λ * x
inr : S'.b = λ * (x * (↑η : 𝓞 K))
inr₁ : S'.b = λ * x * (↑η : 𝓞 K)
inr₂ : S'.b = HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b * (↑η : 𝓞 K)
inr₃ : S'.b = S'.b * HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * (↑η : 𝓞 K)
inr₄ : S'.b = S'.b * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * (↑η : 𝓞 K))
inr₅ : S'.b = S'.b * (↑η : 𝓞 K) ^ HAdd.hAdd (α := ℕ) 2 1
⊢ S'.b = λ * ((↑η : 𝓞 K) * x)
have inr₆ : S'.b = S'.b * hζ.toInteger ^ HAdd.hAdd (α := ℕ) 2 1
Tactic: rw [mul_comm _ x, ← mul_assoc, ← hx, mul_comm _ S'.b, mul_assoc, ← pow_succ, coe_eta,
        hζ.toInteger_cube_eq_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
h_1 : λ ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
x : 𝓞 K
hx : HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b = λ * x
inr : S'.b = λ * (x * (↑η : 𝓞 K))
inr₁ : S'.b = λ * x * (↑η : 𝓞 K)
inr₂ : S'.b = HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b * (↑η : 𝓞 K)
inr₃ : S'.b = S'.b * HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * (↑η : 𝓞 K)
inr₄ : S'.b = S'.b * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * (↑η : 𝓞 K))
inr₅ : S'.b = S'.b * (↑η : 𝓞 K) ^ HAdd.hAdd (α := ℕ) 2 1
inr₆ : S'.b = S'.b * hζ.toInteger ^ HAdd.hAdd (α := ℕ) 2 1
⊢ S'.b = λ * ((↑η : 𝓞 K) * x)
have inr₇ : S'.b = S'.b * 1
Tactic: rw [mul_comm _ x, ← mul_assoc, ← hx, mul_comm _ S'.b, mul_assoc, ← pow_succ, coe_eta,
        hζ.toInteger_cube_eq_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h : HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
h_1 : λ ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
x : 𝓞 K
hx : HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b = λ * x
inr : S'.b = λ * (x * (↑η : 𝓞 K))
inr₁ : S'.b = λ * x * (↑η : 𝓞 K)
inr₂ : S'.b = HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b * (↑η : 𝓞 K)
inr₃ : S'.b = S'.b * HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * (↑η : 𝓞 K)
inr₄ : S'.b = S'.b * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * (↑η : 𝓞 K))
inr₅ : S'.b = S'.b * (↑η : 𝓞 K) ^ HAdd.hAdd (α := ℕ) 2 1
inr₆ : S'.b = S'.b * hζ.toInteger ^ HAdd.hAdd (α := ℕ) 2 1
inr₇ : S'.b = S'.b * 1
⊢ S'.b = λ * ((↑η : 𝓞 K) * x)
have inr₈ : S'.b = S'.b
Tactic: rw [mul_comm _ x, ← mul_assoc, ← hx, mul_comm _ S'.b, mul_assoc, ← pow_succ, coe_eta,
        hζ.toInteger_cube_eq_one, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ ∃ (S₁ : Solution hζ), S₁.multiplicity = S'.multiplicity
have obtain : ∀ (a b : 𝓞 K) (H : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3)
  (coprime : IsCoprime a b) (ha : ¬λ ∣ a) (hb : ¬λ ∣ b) (hab : HPow.hPow (β := ℕ) λ 2 ∣ a + b),
  ∃ (S₁ : Solution hζ), S₁.multiplicity = S'.multiplicity
Tactic: obtain ⟨a, b, H, coprime, ha, hb, hab⟩ := ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd S'
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
⊢ λ * S.b = λ * S.b
have rw : S.b * λ = S.b * λ
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
⊢ λ ∣ S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
have rw : λ ∣ S.a + S.b + HPow.hPow (β := ℕ) λ 2 * S.b + 2 * λ * S.b
Tactic: rw [show S.a + η ^ 2 * S.b = (S.a + S.b) + λ ^ 2 * S.b + 2 * λ * S.b by rw [coe_eta]; ring]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ ¬HPow.hPow (β := ℕ) λ 2 ∣ S.a + (↑η : 𝓞 K) * S.b
have simp_rw : ¬HPow.hPow (β := ℕ) λ 2 ∣ S.a + S.b + λ * S.b
Tactic: simp_rw [a_add_eta_mul_b, dvd_add_right S.hab, pow_two, mul_dvd_mul_iff_left
    hζ.zeta_sub_one_prime'.ne_zero, S.hb, not_false_eq_true]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
simp_rw : ¬HPow.hPow (β := ℕ) λ 2 ∣ S.a + S.b + λ * S.b
⊢ ¬HPow.hPow (β := ℕ) λ 2 ∣ S.a + (↑η : 𝓞 K) * S.b
have simp_rw₁ : ¬HPow.hPow (β := ℕ) λ 2 ∣ λ * S.b
Tactic: simp_rw [a_add_eta_mul_b, dvd_add_right S.hab, pow_two, mul_dvd_mul_iff_left
    hζ.zeta_sub_one_prime'.ne_zero, S.hb, not_false_eq_true]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
simp_rw : ¬HPow.hPow (β := ℕ) λ 2 ∣ S.a + S.b + λ * S.b
simp_rw₁ : ¬HPow.hPow (β := ℕ) λ 2 ∣ λ * S.b
⊢ ¬HPow.hPow (β := ℕ) λ 2 ∣ S.a + (↑η : 𝓞 K) * S.b
have simp_rw₂ : ¬λ * λ ∣ λ * S.b
Tactic: simp_rw [a_add_eta_mul_b, dvd_add_right S.hab, pow_two, mul_dvd_mul_iff_left
    hζ.zeta_sub_one_prime'.ne_zero, S.hb, not_false_eq_true]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
simp_rw : ¬HPow.hPow (β := ℕ) λ 2 ∣ S.a + S.b + λ * S.b
simp_rw₁ : ¬HPow.hPow (β := ℕ) λ 2 ∣ λ * S.b
simp_rw₂ : ¬λ * λ ∣ λ * S.b
⊢ ¬HPow.hPow (β := ℕ) λ 2 ∣ S.a + (↑η : 𝓞 K) * S.b
have simp_rw₃ : ¬λ ∣ S.b
Tactic: simp_rw [a_add_eta_mul_b, dvd_add_right S.hab, pow_two, mul_dvd_mul_iff_left
    hζ.zeta_sub_one_prime'.ne_zero, S.hb, not_false_eq_true]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
simp_rw : ¬HPow.hPow (β := ℕ) λ 2 ∣ S.a + S.b + λ * S.b
simp_rw₁ : ¬HPow.hPow (β := ℕ) λ 2 ∣ λ * S.b
simp_rw₂ : ¬λ * λ ∣ λ * S.b
simp_rw₃ : ¬λ ∣ S.b
⊢ ¬HPow.hPow (β := ℕ) λ 2 ∣ S.a + (↑η : 𝓞 K) * S.b
have simp_rw₄ : ¬False
Tactic: simp_rw [a_add_eta_mul_b, dvd_add_right S.hab, pow_two, mul_dvd_mul_iff_left
    hζ.zeta_sub_one_prime'.ne_zero, S.hb, not_false_eq_true]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
k : 𝓞 K
hk : S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b = HPow.hPow (β := ℕ) λ 2 * k
⊢ False
have rcases : ∀ (k' : 𝓞 K) (hk' : S.a + S.b = HPow.hPow (β := ℕ) λ 2 * k'), False
Tactic: rcases S.hab with ⟨k', hk'⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
k : 𝓞 K
hk : S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b = HPow.hPow (β := ℕ) λ 2 * k
k' : 𝓞 K
hk' : S.a + S.b = HPow.hPow (β := ℕ) λ 2 * k'
⊢ False
have refine : S.b = λ * ((k - k') * -(↑η : 𝓞 K))
Tactic: refine S.hb ⟨(k - k') * (-η), ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
k : 𝓞 K
hk : S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b = HPow.hPow (β := ℕ) λ 2 * k
k' : 𝓞 K
hk' : S.a + S.b = HPow.hPow (β := ℕ) λ 2 * k'
⊢ S.b = λ * ((k - k') * -(↑η : 𝓞 K))
have rw : ∀ (k' : 𝓞 K) (hk : λ * (S.b * ((↑η : 𝓞 K) + 1) + λ * k') = λ * (λ * k)) (hk' : S.a + S.b = HPow.hPow (β := ℕ) λ 2 * k'),
  S.b = λ * ((k - k') * -(↑η : 𝓞 K))
Tactic: rw [show S.a + η ^ 2 * S.b = S.a + S.b - S.b + η ^ 2 * S.b by ring, hk',
    show λ ^ 2 * k' - S.b + η ^ 2 * S.b = λ * (S.b * (η + 1) + λ * k') by rw [coe_eta]; ring,
    pow_two, mul_assoc] at hk
Cleared hypotheses: hk, k', hk'
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (hypothesis)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
k k' : 𝓞 K
hk : λ * (S.b * ((↑η : 𝓞 K) + 1) + λ * k') = λ * (λ * k)
hk' : S.a + S.b = HPow.hPow (β := ℕ) λ 2 * k'
⊢ S.b = λ * ((k - k') * -(↑η : 𝓞 K))
have hk₁ : S.b * ((↑η : 𝓞 K) + 1) + λ * k' = λ * k
Tactic: simp only [mul_eq_mul_left_iff, hζ.zeta_sub_one_prime'.ne_zero, or_false] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (hypothesis)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
k k' : 𝓞 K
hk' : S.a + S.b = HPow.hPow (β := ℕ) λ 2 * k'
hk : S.b * ((↑η : 𝓞 K) + 1) + λ * k' = λ * k
⊢ S.b = λ * ((k - k') * -(↑η : 𝓞 K))
have hk₁ : (S.b * ((↑η : 𝓞 K) + 1) + λ * k') * -(↑η : 𝓞 K) = λ * k * -(↑η : 𝓞 K)
Tactic: apply_fun (· * -↑η) at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (hypothesis)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
k k' : 𝓞 K
hk' : S.a + S.b = HPow.hPow (β := ℕ) λ 2 * k'
hk : (S.b * ((↑η : 𝓞 K) + 1) + λ * k') * -(↑η : 𝓞 K) = λ * k * -(↑η : 𝓞 K)
⊢ S.b = λ * ((k - k') * -(↑η : 𝓞 K))
have hk₁ : S.b = λ * k * -(↑η : 𝓞 K) + (↑η : 𝓞 K) * λ * k'
Tactic: rw [show (S.b * (η + 1) + λ * k') * -η = (-S.b) * (η ^ 2 + η + 1 - 1) - η * λ * k' by ring,
    eta_sq, show -S.b * (-↑η - 1 + ↑η + 1 - 1) = S.b by ring, sub_eq_iff_eq_add] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
k k' : 𝓞 K
hk' : S.a + S.b = HPow.hPow (β := ℕ) λ 2 * k'
hk : S.b = λ * k * -(↑η : 𝓞 K) + (↑η : 𝓞 K) * λ * k'
⊢ S.b = λ * ((k - k') * -(↑η : 𝓞 K))
have rw : λ * k * -(↑η : 𝓞 K) + (↑η : 𝓞 K) * λ * k' = λ * ((k - k') * -(↑η : 𝓞 K))
Tactic: rw [hk]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ S.a + S.b
hpaηb : p ∣ S.a + (↑η : 𝓞 K) * S.b
⊢ Associated p λ
have suffices : p ∣ λ
Tactic: suffices p_lam : p ∣ λ from hp.associated_of_dvd hζ.zeta_sub_one_prime' p_lam
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (hypothesis)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ S.a + S.b
hpaηb : p ∣ S.a + (↑η : 𝓞 K) * S.b
⊢ p ∣ λ
have hpab₁ : p ∣ 1 * S.a + 1 * S.b
Tactic: rw [← one_mul S.a, ← one_mul S.b] at hpab
Cleared hypotheses: hpab, hpaηb
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (hypothesis)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηb : p ∣ S.a + (↑η : 𝓞 K) * S.b
⊢ p ∣ λ
have hpaηb₁ : p ∣ 1 * S.a + (↑η : 𝓞 K) * S.b
Tactic: rw [← one_mul S.a] at hpaηb
Cleared hypotheses: hpaηb
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (hypothesis)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηb : p ∣ 1 * S.a + (↑η : 𝓞 K) * S.b
⊢ p ∣ λ
have this : p ∣ (1 * (↑η : 𝓞 K) - HMul.hMul (α := 𝓞 K) 1 1) * @gcd _ CommSemiring.toCommMonoidWithZero _ S.a S.b
Tactic: have := dvd_mul_sub_mul_mul_gcd_of_dvd hpab hpaηb
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηb : p ∣ 1 * S.a + (↑η : 𝓞 K) * S.b
this : p ∣ (1 * (↑η : 𝓞 K) - HMul.hMul (α := 𝓞 K) 1 1) * @gcd _ CommSemiring.toCommMonoidWithZero _ S.a S.b
⊢ p ∣ λ
have rwa : ∀ (this : p ∣ ((↑η : 𝓞 K) - HMul.hMul (α := 𝓞 K) 1 1) * @gcd _ CommSemiring.toCommMonoidWithZero _ S.a S.b), p ∣ λ
Tactic: rwa [one_mul, one_mul, coe_eta, IsUnit.dvd_mul_right <| (gcd_isUnit_iff _ _).2 S.coprime] at this
Cleared hypotheses: this