-- Mathlib/NumberTheory/FLT/Three.lean
/-- We have that `S.Solution'_descent.multiplicity = S.multiplicity - 1`. -/
lemma Solution'_descent_multiplicity : S.Solution'_descent.multiplicity = S.multiplicity - 1

Proof state:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k : 𝓞 K
hk : λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S = λ ^ (S.multiplicity - 1 + 1) * k
⊢ λ ∣ FermatLastTheoremForThreeGen.Solution.X S

Tactic:
rw [pow_succ, mul_assoc] at hk

Result:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k : 𝓞 K
hk : λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S = λ ^ (S.multiplicity - 1) * (λ * k)
⊢ λ ∣ FermatLastTheoremForThreeGen.Solution.X S

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ λ ^ (S.multiplicity - 1) ∣ S.Solution'_descent.c

Tactic:
simp [Solution'_descent]

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ (S.multiplicity - 1 + 1) ∣ S.Solution'_descent.c
⊢ λ ∣ FermatLastTheoremForThreeGen.Solution.X S

Tactic:
obtain ⟨k, hk : λ^(S.multiplicity-1)*S.X=λ^(S.multiplicity-1+1)*k⟩ := h

Result:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k : 𝓞 K
hk : λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S = λ ^ (S.multiplicity - 1 + 1) * k
⊢ λ ∣ FermatLastTheoremForThreeGen.Solution.X S

Proof state:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k : 𝓞 K
hk : λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S = λ ^ (S.multiplicity - 1) * (λ * k)
⊢ λ ∣ FermatLastTheoremForThreeGen.Solution.X S

Tactic:
simp only [mul_eq_mul_left_iff, pow_eq_zero_iff', hζ.zeta_sub_one_prime'.ne_zero, ne_eq,
  false_and, or_false] at hk

Result:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k : 𝓞 K
hk : FermatLastTheoremForThreeGen.Solution.X S = λ * k
⊢ λ ∣ FermatLastTheoremForThreeGen.Solution.X S

Proof state:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k : 𝓞 K
hk : FermatLastTheoremForThreeGen.Solution.X S = λ * k
⊢ λ ∣ FermatLastTheoremForThreeGen.Solution.X S

Tactic:
simp [hk]

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.Solution'_descent.multiplicity = S.multiplicity - 1

Tactic:
refine multiplicity_eq_of_dvd_of_not_dvd
  (by simp [Solution'_descent]) (fun h ↦ S.lambda_not_dvd_X ?_)

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ (S.multiplicity - 1 + 1) ∣ S.Solution'_descent.c
⊢ λ ∣ FermatLastTheoremForThreeGen.Solution.X S