awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.FLT.Three
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) * λ * 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

Premises used: IsCyclotomicExtension.Rat.Three.eta_sq, sub_eq_iff_eq_add
-- Module: Mathlib.NumberTheory.FLT.Three
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'
rw : λ * k * -(↑η : 𝓞 K) + (↑η : 𝓞 K) * λ * k' = λ * ((k - k') * -(↑η : 𝓞 K))
⊢ S.b = λ * ((k - k') * -(↑η : 𝓞 K))

Tactic:
rw [hk]
-- Module: Mathlib.NumberTheory.FLT.Three
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'
⊢ λ * k * -(↑η : 𝓞 K) + (↑η : 𝓞 K) * λ * k' = λ * ((k - k') * -(↑η : 𝓞 K))

Tactic:
ring
-- Module: Mathlib.NumberTheory.FLT.Three
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
suffices : p ∣ λ
⊢ Associated p λ

Tactic:
suffices p_lam : p ∣ λ from hp.associated_of_dvd hζ.zeta_sub_one_prime' p_lam
-- Module: Mathlib.NumberTheory.FLT.Three
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 ∣ 1 * S.a + 1 * S.b

Tactic:
rw [← one_mul S.a, ← one_mul S.b] at hpab

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.a, _private.0.FermatLastTheoremForThreeGen.Solution'.b, _private.0.FermatLastTheoremForThreeGen.Solution.toSolution', one_mul
-- Module: Mathlib.NumberTheory.FLT.Three
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
hpab₁ : p ∣ 1 * S.a + 1 * S.b
⊢ p ∣ S.a + (↑η : 𝓞 K) * S.b

Tactic:
rw [← one_mul S.a, ← one_mul S.b] at hpab

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.a, _private.0.FermatLastTheoremForThreeGen.Solution'.b, _private.0.FermatLastTheoremForThreeGen.Solution.toSolution', one_mul
-- Module: Mathlib.NumberTheory.FLT.Three
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 ∣ 1 * S.a + (↑η : 𝓞 K) * S.b

Tactic:
rw [← one_mul S.a] at hpaηb

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.a, _private.0.FermatLastTheoremForThreeGen.Solution.toSolution', one_mul
-- Module: Mathlib.NumberTheory.FLT.Three
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 ∣ (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
-- Module: Mathlib.NumberTheory.FLT.Three
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
rwa : ∀ (this : p ∣ ((↑η : 𝓞 K) - HMul.hMul (α := 𝓞 K) 1 1) * @gcd _ CommSemiring.toCommMonoidWithZero _ S.a S.b), p ∣ λ
rwa₁ : ∀ (this : p ∣ ((↑η : 𝓞 K) - 1) * @gcd _ CommSemiring.toCommMonoidWithZero _ S.a S.b), p ∣ λ
rwa₂ : ∀ (this : p ∣ λ * @gcd _ CommSemiring.toCommMonoidWithZero _ S.a S.b), p ∣ λ
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : p ∣ λ), p ∣ λ
⊢ p ∣ λ

Tactic:
rwa [one_mul, one_mul, coe_eta, IsUnit.dvd_mul_right <| (gcd_isUnit_iff _ _).2 S.coprime] at this

Premises used: Iff.mpr, IsCyclotomicExtension.Rat.Three.coe_eta, gcd_isUnit_iff, _private.0.FermatLastTheoremForThreeGen.Solution'.coprime, IsUnit.dvd_mul_right, _private.0.FermatLastTheoremForThreeGen.Solution.toSolution', one_mul
-- Module: Mathlib.NumberTheory.FLT.Three
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ηsqb : p ∣ S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
suffices : p ∣ λ
⊢ Associated p λ

Tactic:
suffices p_lam : p ∣ λ from hp.associated_of_dvd hζ.zeta_sub_one_prime' p_lam
-- Module: Mathlib.NumberTheory.FLT.Three
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ηsqb : p ∣ S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
⊢ p ∣ 1 * S.a + 1 * S.b

Tactic:
rw [← one_mul S.a, ← one_mul S.b] at hpab

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.a, _private.0.FermatLastTheoremForThreeGen.Solution'.b, _private.0.FermatLastTheoremForThreeGen.Solution.toSolution', one_mul
-- Module: Mathlib.NumberTheory.FLT.Three
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ηsqb : p ∣ S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
hpab₁ : p ∣ 1 * S.a + 1 * S.b
⊢ p ∣ S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b

Tactic:
rw [← one_mul S.a, ← one_mul S.b] at hpab

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.a, _private.0.FermatLastTheoremForThreeGen.Solution'.b, _private.0.FermatLastTheoremForThreeGen.Solution.toSolution', one_mul
-- Module: Mathlib.NumberTheory.FLT.Three
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ηsqb : p ∣ S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
⊢ p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b

Tactic:
rw [← one_mul S.a] at hpaηsqb

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.a, _private.0.FermatLastTheoremForThreeGen.Solution.toSolution', one_mul
-- Module: Mathlib.NumberTheory.FLT.Three
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ηsqb : p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
⊢ p ∣
    (1 * HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - HMul.hMul (α := 𝓞 K) 1 1) *
      @gcd _ CommSemiring.toCommMonoidWithZero _ S.a S.b

Tactic:
have := dvd_mul_sub_mul_mul_gcd_of_dvd hpab hpaηsqb
-- Module: Mathlib.NumberTheory.FLT.Three
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ηsqb : p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
this :
  p ∣
    (1 * HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - HMul.hMul (α := 𝓞 K) 1 1) *
      @gcd _ CommSemiring.toCommMonoidWithZero _ S.a S.b
⊢ p ∣ -(HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - 1)

Tactic:
rw [one_mul, mul_one, IsUnit.dvd_mul_right <| (gcd_isUnit_iff _ _).2 S.coprime, ← dvd_neg] at this

Premises used: Iff.mpr, gcd_isUnit_iff, dvd_neg, _private.0.FermatLastTheoremForThreeGen.Solution'.coprime, mul_one, IsUnit.dvd_mul_right, _private.0.FermatLastTheoremForThreeGen.Solution.toSolution', one_mul
-- Module: Mathlib.NumberTheory.FLT.Three
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ηsqb : p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
this : p ∣ -(HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - 1)
⊢ p ∣ -(HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - 1) * (↑η : 𝓞 K)

Tactic:
dvd_mul_of_dvd_left this η

Premises used: IsPrimitiveRoot.toInteger_isPrimitiveRoot, dvd_mul_of_dvd_left, Units.val, IsPrimitiveRoot.isUnit, IsUnit.unit
-- Module: Mathlib.NumberTheory.FLT.Three
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ηsqb : p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
this : p ∣ -(HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - 1)
h : λ = -(HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - 1) * (↑η : 𝓞 K)
⊢ p ∣ λ

Tactic:
convert! dvd_mul_of_dvd_left this η using 1
-- Module: Mathlib.NumberTheory.FLT.Three
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ηsqb : p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
this : p ∣ -(HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - 1)
h : λ = 1 * hζ.toInteger - (-(-hζ.toInteger - 1) - 1 * hζ.toInteger)
⊢ λ = -(HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - 1) * (↑η : 𝓞 K)

Tactic:
rw [eta_sq, neg_sub, sub_mul, sub_mul, neg_mul, ← pow_two, eta_sq, coe_eta]

Premises used: neg_sub, pow_two, IsCyclotomicExtension.Rat.Three.coe_eta, IsCyclotomicExtension.Rat.Three.eta_sq, sub_mul, neg_mul
-- Module: Mathlib.NumberTheory.FLT.Three
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ηsqb : p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
this : p ∣ -(HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - 1)
⊢ λ = 1 * hζ.toInteger - (-(-hζ.toInteger - 1) - 1 * hζ.toInteger)

Tactic:
ring
-- Module: Mathlib.NumberTheory.FLT.Three
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
hpaηb : p ∣ S.a + (↑η : 𝓞 K) * S.b
hpaηsqb : p ∣ S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
suffices : p ∣ λ
⊢ Associated p λ

Tactic:
suffices p_lam : p ∣ λ from hp.associated_of_dvd hζ.zeta_sub_one_prime' p_lam
-- Module: Mathlib.NumberTheory.FLT.Three
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
hpaηb : p ∣ S.a + (↑η : 𝓞 K) * S.b
hpaηsqb : p ∣ S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
⊢ p ∣ 1 * S.a + (↑η : 𝓞 K) * S.b

Tactic:
rw [← one_mul S.a] at hpaηb

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.a, _private.0.FermatLastTheoremForThreeGen.Solution.toSolution', one_mul
-- Module: Mathlib.NumberTheory.FLT.Three
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
hpaηb : p ∣ S.a + (↑η : 𝓞 K) * S.b
hpaηsqb : p ∣ S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
hpaηb₁ : p ∣ 1 * S.a + (↑η : 𝓞 K) * S.b
⊢ p ∣ S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b

Tactic:
rw [← one_mul S.a] at hpaηb

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.a, _private.0.FermatLastTheoremForThreeGen.Solution.toSolution', one_mul
-- Module: Mathlib.NumberTheory.FLT.Three
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
hpaηb : p ∣ 1 * S.a + (↑η : 𝓞 K) * S.b
hpaηsqb : p ∣ S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
⊢ p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b

Tactic:
rw [← one_mul S.a] at hpaηsqb

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution'.a, _private.0.FermatLastTheoremForThreeGen.Solution.toSolution', one_mul
-- Module: Mathlib.NumberTheory.FLT.Three
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
hpaηb : p ∣ 1 * S.a + (↑η : 𝓞 K) * S.b
hpaηsqb : p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
⊢ p ∣ (1 * HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K) * 1) * @gcd _ CommSemiring.toCommMonoidWithZero _ S.a S.b

Tactic:
have := dvd_mul_sub_mul_mul_gcd_of_dvd hpaηb hpaηsqb
-- Module: Mathlib.NumberTheory.FLT.Three
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
hpaηb : p ∣ 1 * S.a + (↑η : 𝓞 K) * S.b
hpaηsqb : p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
this : p ∣ (1 * HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K) * 1) * @gcd _ CommSemiring.toCommMonoidWithZero _ S.a S.b
⊢ p ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K)

Tactic:
rw [one_mul, mul_one, IsUnit.dvd_mul_right <| (gcd_isUnit_iff _ _).2 S.coprime] at this

Premises used: Iff.mpr, gcd_isUnit_iff, _private.0.FermatLastTheoremForThreeGen.Solution'.coprime, mul_one, IsUnit.dvd_mul_right, _private.0.FermatLastTheoremForThreeGen.Solution.toSolution', one_mul
-- Module: Mathlib.NumberTheory.FLT.Three
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
hpaηb : p ∣ 1 * S.a + (↑η : 𝓞 K) * S.b
hpaηsqb : p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
this : p ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K)
⊢ p ∣ (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K)) * (↑η : 𝓞 K) * (↑η : 𝓞 K)

Tactic:
(dvd_mul_of_dvd_left (dvd_mul_of_dvd_left this η) η)

Premises used: IsPrimitiveRoot.toInteger_isPrimitiveRoot, dvd_mul_of_dvd_left, Units.val, IsPrimitiveRoot.isUnit, IsUnit.unit
-- Module: Mathlib.NumberTheory.FLT.Three
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
hpaηb : p ∣ 1 * S.a + (↑η : 𝓞 K) * S.b
hpaηsqb : p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
this : p ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K)
h : λ = (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K)) * (↑η : 𝓞 K) * (↑η : 𝓞 K)
⊢ p ∣ λ

Tactic:
convert! (dvd_mul_of_dvd_left (dvd_mul_of_dvd_left this η) η) using 1
-- Module: Mathlib.NumberTheory.FLT.Three
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
hpaηb : p ∣ 1 * S.a + (↑η : 𝓞 K) * S.b
hpaηsqb : p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
this : p ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K)
h : (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K)) * (↑η : 𝓞 K) * (↑η : 𝓞 K) = λ
⊢ λ = (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K)) * (↑η : 𝓞 K) * (↑η : 𝓞 K)

Tactic:
symm
-- Module: Mathlib.NumberTheory.FLT.Three
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
hpaηb : p ∣ 1 * S.a + (↑η : 𝓞 K) * S.b
hpaηsqb : p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
this : p ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K)
rw :
  (-(↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - 1 - (↑η : 𝓞 K)) * (↑η : 𝓞 K) * (↑η : 𝓞 K) =
    (-(↑η : 𝓞 K) - 1 - (↑η : 𝓞 K)) * (-(↑η : 𝓞 K) - 1)
rw₁ :
  (-(↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - 1 - (↑η : 𝓞 K)) * ((↑η : 𝓞 K) * (↑η : 𝓞 K)) =
    (-(↑η : 𝓞 K) - 1 - (↑η : 𝓞 K)) * (-(↑η : 𝓞 K) - 1)
rw₂ :
  (-(↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - 1 - (↑η : 𝓞 K)) * HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 =
    (-(↑η : 𝓞 K) - 1 - (↑η : 𝓞 K)) * (-(↑η : 𝓞 K) - 1)
rw₃ rw₄ :
  (-(↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - 1 - (↑η : 𝓞 K)) *
      (-(↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) - 1) =
    (-(↑η : 𝓞 K) - 1 - (↑η : 𝓞 K)) * (-(↑η : 𝓞 K) - 1)
⊢ (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K)) * (↑η : 𝓞 K) * (↑η : 𝓞 K) =
    (-(↑η : 𝓞 K) - 1 - (↑η : 𝓞 K)) * (-(↑η : 𝓞 K) - 1)

Tactic:
rw [eta_sq, mul_assoc, ← pow_two, eta_sq]

Premises used: pow_two, mul_assoc, IsCyclotomicExtension.Rat.Three.eta_sq
-- Module: Mathlib.NumberTheory.FLT.Three
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
hpaηb : p ∣ 1 * S.a + (↑η : 𝓞 K) * S.b
hpaηsqb : p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
this : p ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K)
⊢ (-(↑η : 𝓞 K) - 1 - (↑η : 𝓞 K)) * (-(↑η : 𝓞 K) - 1) = 2 * HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + 3 * (↑η : 𝓞 K) + 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.FLT.Three
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
hpaηb : p ∣ 1 * S.a + (↑η : 𝓞 K) * S.b
hpaηsqb : p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
this : p ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K)
rw : 2 * (-hζ.toInteger - 1) + 3 * hζ.toInteger + 1 = λ
⊢ 2 * HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + 3 * (↑η : 𝓞 K) + 1 = λ

Tactic:
rw [eta_sq, coe_eta]

Premises used: IsCyclotomicExtension.Rat.Three.coe_eta, IsCyclotomicExtension.Rat.Three.eta_sq
-- Module: Mathlib.NumberTheory.FLT.Three
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
hpaηb : p ∣ 1 * S.a + (↑η : 𝓞 K) * S.b
hpaηsqb : p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
this : p ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K)
⊢ 2 * (-hζ.toInteger - 1) + 3 * hζ.toInteger + 1 = λ

Tactic:
ring
-- Module: Mathlib.NumberTheory.FLT.Three
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
hpaηb : p ∣ 1 * S.a + (↑η : 𝓞 K) * S.b
hpaηsqb : p ∣ 1 * S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b
this : p ∣ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K)
calc :
  (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K)) * (↑η : 𝓞 K) * (↑η : 𝓞 K) =
    (-(↑η : 𝓞 K) - 1 - (↑η : 𝓞 K)) * (-(↑η : 𝓞 K) - 1)
calc₁ : (-(↑η : 𝓞 K) - 1 - (↑η : 𝓞 K)) * (-(↑η : 𝓞 K) - 1) = 2 * HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + 3 * (↑η : 𝓞 K) + 1
calc₂ : 2 * HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 + 3 * (↑η : 𝓞 K) + 1 = λ
⊢ (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 - (↑η : 𝓞 K)) * (↑η : 𝓞 K) * (↑η : 𝓞 K) = λ

Tactic:
calc _ = (-η.1 - 1 - η) * (-η - 1) := by rw [eta_sq, mul_assoc, ← pow_two, eta_sq]
  _ = 2 * η.1 ^ 2 + 3 * η + 1 := by ring
  _ = λ := by rw [eta_sq, coe_eta]; ring
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
⊢ S.a + (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) * S.b = (hζ.toInteger - 1) * S.y

Tactic:
(lambda_dvd_a_add_eta_mul_b S).choose_spec

Premises used: Exists.choose_spec, _private.0.FermatLastTheoremForThreeGen.Solution.y, _private.0.FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_mul_b
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
⊢ S.a + HPow.hPow (β := ℕ) (↑(IsUnit.unit (a := hζ.toInteger) ⋯) : 𝓞 K) 2 * S.b = (hζ.toInteger - 1) * S.z

Tactic:
(lambda_dvd_a_add_eta_sq_mul_b S).choose_spec

Premises used: Exists.choose_spec, _private.0.FermatLastTheoremForThreeGen.Solution.z, _private.0.FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_sq_mul_b
-- Module: Mathlib.NumberTheory.FLT.Three
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 : λ ∣ S.y
⊢ ((↑η : 𝓞 K) - 1) * λ ∣ ((↑η : 𝓞 K) - 1) * S.y

Tactic:
replace h := mul_dvd_mul_left ((η : 𝓞 K) - 1) h
-- Module: Mathlib.NumberTheory.FLT.Three
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 : ((↑η : 𝓞 K) - 1) * λ ∣ ((↑η : 𝓞 K) - 1) * S.y
⊢ HPow.hPow (β := ℕ) λ 2 ∣ S.a + (↑η : 𝓞 K) * S.b

Tactic:
rw [coe_eta, ← y_spec, ← pow_two] at h

Premises used: pow_two, IsCyclotomicExtension.Rat.Three.coe_eta, _private.0.FermatLastTheoremForThreeGen.Solution.y_spec
-- Module: Mathlib.NumberTheory.FLT.Three
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 + (↑η : 𝓞 K) * S.b
⊢ False

Tactic:
lambda_sq_not_dvd_a_add_eta_mul_b _ h

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_mul_b
-- Module: Mathlib.NumberTheory.FLT.Three
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 + (↑η : 𝓞 K) * S.b
⊢ False

Tactic:
exact lambda_sq_not_dvd_a_add_eta_mul_b _ h

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_mul_b
-- Module: Mathlib.NumberTheory.FLT.Three
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 : λ ∣ S.z
⊢ ((↑η : 𝓞 K) - 1) * λ ∣ ((↑η : 𝓞 K) - 1) * S.z

Tactic:
replace h := mul_dvd_mul_left ((η : 𝓞 K) - 1) h
-- Module: Mathlib.NumberTheory.FLT.Three
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 : ((↑η : 𝓞 K) - 1) * λ ∣ ((↑η : 𝓞 K) - 1) * S.z
⊢ HPow.hPow (β := ℕ) λ 2 ∣ S.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S.b

Tactic:
rw [coe_eta, ← z_spec, ← pow_two] at h

Premises used: pow_two, IsCyclotomicExtension.Rat.Three.coe_eta, _private.0.FermatLastTheoremForThreeGen.Solution.z_spec
-- Module: Mathlib.NumberTheory.FLT.Three
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
⊢ False

Tactic:
lambda_sq_not_dvd_a_add_eta_sq_mul_b _ h

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_sq_mul_b
-- Module: Mathlib.NumberTheory.FLT.Three
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
⊢ False

Tactic:
exact lambda_sq_not_dvd_a_add_eta_sq_mul_b _ h

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_sq_mul_b
-- Module: Mathlib.NumberTheory.FLT.Three
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.multiplicity ∣ S.c

Tactic:
have h : λ ^ S.multiplicity ∣ S.c := pow_multiplicity_dvd _ _
-- Module: Mathlib.NumberTheory.FLT.Three
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 : λ ^ S.multiplicity ∣ S.c
⊢ HPow.hPow (β := ℕ) (λ ^ S.multiplicity) 3 ∣ (↑S.u : 𝓞 K) * HPow.hPow (β := ℕ) S.c 3

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.FLT.Three
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 : λ ^ S.multiplicity ∣ S.c
⊢ HPow.hPow (β := ℕ) (λ ^ S.multiplicity) 3 ∣ (↑S.u : 𝓞 K) * HPow.hPow (β := ℕ) S.c 3

Tactic:
replace h : (λ ^ multiplicity S) ^ 3 ∣ S.u * S.c ^ 3 := by simp [h]