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
this : (S.multiplicity - 1) * 3 + 1 = 3 * S.multiplicity - 2
⊢ HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * (↑S.u₁ : 𝓞 K) * (↑S.u₂⁻¹ : 𝓞 K) *
        HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 *
      (λ * (↑S.u₂ : 𝓞 K) * (↑η : 𝓞 K)) =
    HPow.hPow (β := ℕ) S.X 3 * ((↑S.u₂ : 𝓞 K) * (↑S.u₂⁻¹ : 𝓞 K)) * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 3 * (↑S.u₁ : 𝓞 K)) *
      (λ ^ ((S.multiplicity - 1) * 3) * λ)

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
this : (S.multiplicity - 1) * 3 + 1 = 3 * S.multiplicity - 2
⊢ HPow.hPow (β := ℕ) S.X 3 * ((↑S.u₂ : 𝓞 K) * (↑S.u₂⁻¹ : 𝓞 K)) * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 3 * (↑S.u₁ : 𝓞 K)) *
      (λ ^ ((S.multiplicity - 1) * 3) * λ) =
    HPow.hPow (β := ℕ) S.X 3 * (↑S.u₁ : 𝓞 K) * λ ^ (3 * S.multiplicity - 2)

Tactic:
simp [hζ.toInteger_cube_eq_one, ← pow_succ, this]

Premises used: pow_succ, IsPrimitiveRoot.toInteger_cube_eq_one
-- 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
this : (S.multiplicity - 1) * 3 + 1 = 3 * S.multiplicity - 2
calc :
  (↑(HPow.hPow (β := ℕ) η 2 * S.u₁ * S.u₂⁻¹) : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 *
      (λ * (↑S.u₂ : 𝓞 K) * (↑η : 𝓞 K)) =
    HPow.hPow (β := ℕ) S.X 3 * ((↑S.u₂ : 𝓞 K) * (↑S.u₂⁻¹ : 𝓞 K)) * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 3 * (↑S.u₁ : 𝓞 K)) *
      (λ ^ ((S.multiplicity - 1) * 3) * λ)
calc₁ :
  HPow.hPow (β := ℕ) S.X 3 * ((↑S.u₂ : 𝓞 K) * (↑S.u₂⁻¹ : 𝓞 K)) * (HPow.hPow (β := ℕ) (↑η : 𝓞 K) 3 * (↑S.u₁ : 𝓞 K)) *
      (λ ^ ((S.multiplicity - 1) * 3) * λ) =
    HPow.hPow (β := ℕ) S.X 3 * (↑S.u₁ : 𝓞 K) * λ ^ (3 * S.multiplicity - 2)
⊢ (↑(HPow.hPow (β := ℕ) η 2 * S.u₁ * S.u₂⁻¹) : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 *
      (λ * (↑S.u₂ : 𝓞 K) * (↑η : 𝓞 K)) =
    HPow.hPow (β := ℕ) S.X 3 * (↑S.u₁ : 𝓞 K) * λ ^ (3 * S.multiplicity - 2)

Tactic:
calc _ = S.X^3 *(S.u₂*S.u₂⁻¹)*(η^3*S.u₁)*(λ^((S.multiplicity-1)*3)*λ) := by push_cast; ring
    _ = S.X^3*S.u₁*λ^(3*S.multiplicity-2) := by simp [hζ.toInteger_cube_eq_one, ← pow_succ, this]

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.multiplicity, HMul.hMul, _private.0.FermatLastTheoremForThreeGen.Solution.X, HSub.hSub, _private.0.FermatLastTheoremForThreeGen.Solution.u₁, Inv.inv, OfNat.ofNat, _private.0.FermatLastTheoremForThreeGen.Solution.u₂
-- 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
⊢ HPow.hPow (β := ℕ) S.Y 3 * (λ * (↑S.u₂ : 𝓞 K) * (↑η : 𝓞 K)) =
    HPow.hPow (β := ℕ) S.Y 3 * (↑S.u₂ : 𝓞 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
refine_3 :
  HPow.hPow (β := ℕ) S.Z 3 * (↑S.u₃ : 𝓞 K) * λ * HPow.hPow (β := ℕ) hζ.toInteger 2 * (↑S.u₂ : 𝓞 K) =
    hζ.toInteger * (↑S.u₃ : 𝓞 K) * HPow.hPow (β := ℕ) S.Z 3 * (λ * (↑S.u₂ : 𝓞 K) * hζ.toInteger)
⊢ (↑S.u₄ : 𝓞 K) * HPow.hPow (β := ℕ) S.Z 3 * (λ * (↑S.u₂ : 𝓞 K) * (↑η : 𝓞 K)) =
    HPow.hPow (β := ℕ) S.Z 3 * (↑S.u₃ : 𝓞 K) * λ * HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2

Tactic:
simp only [u₄_def, inv_eq_one_div, mul_div_assoc', mul_one, val_div_eq_divp, Units.val_mul,
      IsUnit.unit_spec, divp_mul_eq_mul_divp, divp_eq_iff_mul_eq]

Premises used: divp_eq_iff_mul_eq, mul_div_assoc', inv_eq_one_div, divp_mul_eq_mul_divp, mul_one, IsUnit.unit_spec, _private.0.FermatLastTheoremForThreeGen.Solution.u₄_def, Units.val_mul, val_div_eq_divp
-- 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
⊢ HPow.hPow (β := ℕ) S.Z 3 * (↑S.u₃ : 𝓞 K) * λ * HPow.hPow (β := ℕ) hζ.toInteger 2 * (↑S.u₂ : 𝓞 K) =
    hζ.toInteger * (↑S.u₃ : 𝓞 K) * HPow.hPow (β := ℕ) S.Z 3 * (λ * (↑S.u₂ : 𝓞 K) * 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
h :
  (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 =
    HPow.hPow (β := ℕ) λ 2 * (λ ^ (3 * S.multiplicity - 5) * (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) S.X 3)
⊢ HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3

Tactic:
use λ^(3*S.multiplicity-5)*S.u₅*(S.X^3)

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.multiplicity, HMul.hMul, _private.0.FermatLastTheoremForThreeGen.Solution.X, HSub.hSub, HPow.hPow, _private.0.FermatLastTheoremForThreeGen.Solution.u₅, OfNat.ofNat
-- 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
this : 2 ≤ S.multiplicity
⊢ 3 * (S.multiplicity - 1) = 2 + (3 * S.multiplicity - 5)

Tactic:
lia
-- 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
⊢ 3 * (S.multiplicity - 1) = 2 + (3 * S.multiplicity - 5)

Tactic:
have : 3*(S.multiplicity-1) = 2+(3*S.multiplicity-5) := by have := S.two_le_multiplicity; lia
-- 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
this : 3 * (S.multiplicity - 1) = 2 + (3 * S.multiplicity - 5)
⊢ (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 =
    λ ^ (3 * (S.multiplicity - 1)) * (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) S.X 3

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
this : 3 * (S.multiplicity - 1) = 2 + (3 * S.multiplicity - 5)
rw :
  λ ^ (2 + (3 * S.multiplicity - 5)) * (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) S.X 3 =
    HPow.hPow (β := ℕ) λ 2 * λ ^ (3 * S.multiplicity - 5) * (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) S.X 3
rw₁ rw₂ :
  HPow.hPow (β := ℕ) λ 2 * λ ^ (3 * S.multiplicity - 5) * (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) S.X 3 =
    HPow.hPow (β := ℕ) λ 2 * λ ^ (3 * S.multiplicity - 5) * (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) S.X 3
⊢ λ ^ (3 * (S.multiplicity - 1)) * (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) S.X 3 =
    HPow.hPow (β := ℕ) λ 2 * λ ^ (3 * S.multiplicity - 5) * (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) S.X 3

Tactic:
rw [this, pow_add]

Premises used: pow_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
this : 3 * (S.multiplicity - 1) = 2 + (3 * S.multiplicity - 5)
⊢ HPow.hPow (β := ℕ) λ 2 * λ ^ (3 * S.multiplicity - 5) * (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) S.X 3 =
    HPow.hPow (β := ℕ) λ 2 * (λ ^ (3 * S.multiplicity - 5) * (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) S.X 3)

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
this : 3 * (S.multiplicity - 1) = 2 + (3 * S.multiplicity - 5)
calc :
  (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 =
    λ ^ (3 * (S.multiplicity - 1)) * (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) S.X 3
calc₁ :
  λ ^ (3 * (S.multiplicity - 1)) * (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) S.X 3 =
    HPow.hPow (β := ℕ) λ 2 * λ ^ (3 * S.multiplicity - 5) * (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) S.X 3
calc₂ :
  HPow.hPow (β := ℕ) λ 2 * λ ^ (3 * S.multiplicity - 5) * (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) S.X 3 =
    HPow.hPow (β := ℕ) λ 2 * (λ ^ (3 * S.multiplicity - 5) * (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) S.X 3)
⊢ (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 =
    HPow.hPow (β := ℕ) λ 2 * (λ ^ (3 * S.multiplicity - 5) * (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) S.X 3)

Tactic:
calc _ = λ^(3*(S.multiplicity-1))*S.u₅*S.X^3 := by ring
  _ = λ^2*λ^(3*S.multiplicity-5)*S.u₅*S.X^3 := by rw [this, pow_add]
  _ = λ^2*(λ^(3*S.multiplicity-5)*S.u₅*S.X^3) := by ring

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.multiplicity, HMul.hMul, _private.0.FermatLastTheoremForThreeGen.Solution.X, HSub.hSub, _private.0.FermatLastTheoremForThreeGen.Solution.u₅, OfNat.ofNat
-- 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
⊢ HPow.hPow (β := ℕ) λ 4 = HPow.hPow (β := ℕ) λ 2 * HPow.hPow (β := ℕ) λ 2

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
⊢ HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4

Tactic:
have : λ ^ 2 ∣ λ ^ 4 := ⟨λ ^ 2, by 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
⊢ HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3

Tactic:
have h := S.lambda_sq_div_u₅_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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
h : HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3
hcong : ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)
⊢ S.u₄ = 1 ∨ S.u₄ = -1

Tactic:
apply IsCyclotomicExtension.Rat.Three.eq_one_or_neg_one_of_unit_of_congruent hζ

Premises used: IsCyclotomicExtension.Rat.Three.eq_one_or_neg_one_of_unit_of_congruent
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
h : HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3
hcong :
  ∀ (X : 𝓞 K) (hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X),
    ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
rcases h with ⟨X, hX⟩

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.X
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
hcong :
  ∀ (HY : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Y 3 - 1),
    ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)
hcong₁ :
  ∀ (HY : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Y 3 + 1),
    ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
rcases lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd hζ S.lambda_not_dvd_Y with
    HY | HY

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_Y, IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HY : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Y 3 - 1
hcong :
  ∀ (HZ : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Z 3 - 1),
    ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)
hcong₁ :
  ∀ (HZ : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Z 3 + 1),
    ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
rcases lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd
      hζ S.lambda_not_dvd_Z with HZ | HZ

Premises used: IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd, _private.0.FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_Z
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HY : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Y 3 + 1
hcong :
  ∀ (HZ : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Z 3 - 1),
    ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)
hcong₁ :
  ∀ (HZ : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Z 3 + 1),
    ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
rcases lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd
      hζ S.lambda_not_dvd_Z with HZ | HZ

Premises used: IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd, _private.0.FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_Z
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HY : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Y 3 - 1
HZ : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Z 3 - 1
⊢ HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Y 3 - 1

Tactic:
replace HY := this.trans HY
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HY : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Y 3 - 1
HZ : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Z 3 + 1
⊢ HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Y 3 - 1

Tactic:
replace HY := this.trans HY
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HY : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Y 3 + 1
HZ : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Z 3 - 1
⊢ HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Y 3 + 1

Tactic:
replace HY := this.trans HY
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HY : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Y 3 + 1
HZ : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Z 3 + 1
⊢ HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Y 3 + 1

Tactic:
replace HY := this.trans HY
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HZ : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Z 3 - 1
HY : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Y 3 - 1
⊢ HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Z 3 - 1

Tactic:
replace HZ :=
      this.trans HZ
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HZ : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Z 3 + 1
HY : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Y 3 - 1
⊢ HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Z 3 + 1

Tactic:
replace HZ :=
      this.trans HZ
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HZ : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Z 3 - 1
HY : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Y 3 + 1
⊢ HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Z 3 - 1

Tactic:
replace HZ :=
      this.trans HZ
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HZ : HPow.hPow (β := ℕ) λ 4 ∣ HPow.hPow (β := ℕ) S.Z 3 + 1
HY : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Y 3 + 1
⊢ HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Z 3 + 1

Tactic:
replace HZ :=
      this.trans HZ
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HY : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Y 3 - 1
HZ : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Z 3 - 1
hcong :
  ∀ (Y : 𝓞 K) (hY : HPow.hPow (β := ℕ) S.Y 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Y),
    ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
rcases HY with ⟨Y, hY⟩

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.Y
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HY : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Y 3 - 1
HZ : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Z 3 + 1
hcong :
  ∀ (Y : 𝓞 K) (hY : HPow.hPow (β := ℕ) S.Y 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Y),
    ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
rcases HY with ⟨Y, hY⟩

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.Y
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HY : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Y 3 + 1
HZ : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Z 3 - 1
hcong :
  ∀ (Y : 𝓞 K) (hY : HPow.hPow (β := ℕ) S.Y 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Y),
    ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
rcases HY with ⟨Y, hY⟩

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.Y
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HY : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Y 3 + 1
HZ : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Z 3 + 1
hcong :
  ∀ (Y : 𝓞 K) (hY : HPow.hPow (β := ℕ) S.Y 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Y),
    ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
rcases HY with ⟨Y, hY⟩

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.Y
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HZ : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Z 3 - 1
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Y
hcong :
  ∀ (Z : 𝓞 K) (hZ : HPow.hPow (β := ℕ) S.Z 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Z),
    ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
rcases HZ with ⟨Z, hZ⟩

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.Z
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HZ : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Z 3 + 1
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Y
hcong :
  ∀ (Z : 𝓞 K) (hZ : HPow.hPow (β := ℕ) S.Z 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Z),
    ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
rcases HZ with ⟨Z, hZ⟩

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.Z
-- 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
this : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) λ 4
X : 𝓞 K
hX : (↑S.u₅ : 𝓞 K) * HPow.hPow (β := ℕ) (λ ^ (S.multiplicity - 1) * S.X) 3 = HPow.hPow (β := ℕ) λ 2 * X
HZ : HPow.hPow (β := ℕ) λ 2 ∣ HPow.hPow (β := ℕ) S.Z 3 - 1
Y : 𝓞 K
hY : HPow.hPow (β := ℕ) S.Y 3 + 1 = HPow.hPow (β := ℕ) λ 2 * Y
hcong :
  ∀ (Z : 𝓞 K) (hZ : HPow.hPow (β := ℕ) S.Z 3 - 1 = HPow.hPow (β := ℕ) λ 2 * Z),
    ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)
⊢ ∃ (n : ℤ), HPow.hPow (β := ℕ) λ 2 ∣ (↑S.u₄ : 𝓞 K) - (↑n : 𝓞 K)

Tactic:
rcases HZ with ⟨Z, hZ⟩

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.Z