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
h1 : ¬HPow.hPow (β := ℕ) λ 2 ∣ S'.a + S'.b
h2 : ¬HPow.hPow (β := ℕ) λ 2 ∣ S'.a + (↑η : 𝓞 K) * S'.b
h3 : ¬HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
⊢ emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)

Tactic:
rw [← emultiplicity_lt_iff_not_dvd] at h1 h2 h3

Premises used: emultiplicity_lt_iff_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
h1 : ¬HPow.hPow (β := ℕ) λ 2 ∣ S'.a + S'.b
h2 : ¬HPow.hPow (β := ℕ) λ 2 ∣ S'.a + (↑η : 𝓞 K) * S'.b
h3 : ¬HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
h1₁ : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
⊢ emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)

Tactic:
rw [← emultiplicity_lt_iff_not_dvd] at h1 h2 h3

Premises used: emultiplicity_lt_iff_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
h1 : ¬HPow.hPow (β := ℕ) λ 2 ∣ S'.a + S'.b
h2 : ¬HPow.hPow (β := ℕ) λ 2 ∣ S'.a + (↑η : 𝓞 K) * S'.b
h3 : ¬HPow.hPow (β := ℕ) λ 2 ∣ S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b
h1₁ : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2₁ : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
⊢ emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)

Tactic:
rw [← emultiplicity_lt_iff_not_dvd] at h1 h2 h3

Premises used: emultiplicity_lt_iff_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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
ht : emultiplicity λ (S'.a + S'.b) = ⊤
⊢ False

Tactic:
simp [ht] at h1
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
⊢ FiniteMultiplicity λ (S'.a + S'.b)

Tactic:
have h1' : FiniteMultiplicity (hζ.toInteger - 1) (S'.a + S'.b) :=
    finiteMultiplicity_iff_emultiplicity_ne_top.2 (fun ht ↦ by simp [ht] at h1)
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
⊢ FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)

Tactic:
finiteMultiplicity_iff_emultiplicity_ne_top.2 (fun ht ↦ ?_)

Premises used: Iff.mpr, finiteMultiplicity_iff_emultiplicity_ne_top
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
refine : ∀ (ht : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) = ⊤), False
⊢ FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)

Tactic:
refine finiteMultiplicity_iff_emultiplicity_ne_top.2 (fun ht ↦ ?_)

Premises used: Iff.mpr, finiteMultiplicity_iff_emultiplicity_ne_top
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
ht : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) = ⊤
⊢ emultiplicity λ (S'.a + hζ.toInteger * S'.b) = ⊤

Tactic:
rw [coe_eta] at ht

Premises used: IsCyclotomicExtension.Rat.Three.coe_eta
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
ht : emultiplicity λ (S'.a + hζ.toInteger * S'.b) = ⊤
⊢ False

Tactic:
simp [ht] at h2
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
⊢ FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)

Tactic:
have h2' : FiniteMultiplicity (hζ.toInteger - 1) (S'.a + η * S'.b) := by
    refine finiteMultiplicity_iff_emultiplicity_ne_top.2 (fun ht ↦ ?_)
    rw [coe_eta] at ht
    simp [ht] at h2
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
⊢ FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)

Tactic:
finiteMultiplicity_iff_emultiplicity_ne_top.2 (fun ht ↦ ?_)

Premises used: Iff.mpr, finiteMultiplicity_iff_emultiplicity_ne_top
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
refine : ∀ (ht : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) = ⊤), False
⊢ FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)

Tactic:
refine finiteMultiplicity_iff_emultiplicity_ne_top.2 (fun ht ↦ ?_)

Premises used: Iff.mpr, finiteMultiplicity_iff_emultiplicity_ne_top
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
ht : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) = ⊤
⊢ emultiplicity λ (S'.a + HPow.hPow (β := ℕ) hζ.toInteger 2 * S'.b) = ⊤

Tactic:
rw [coe_eta] at ht

Premises used: IsCyclotomicExtension.Rat.Three.coe_eta
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
ht : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) hζ.toInteger 2 * S'.b) = ⊤
⊢ False

Tactic:
simp [ht] at h3
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
⊢ FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)

Tactic:
have h3' : FiniteMultiplicity (hζ.toInteger - 1) (S'.a + η ^ 2 * S'.b) := by
    refine finiteMultiplicity_iff_emultiplicity_ne_top.2 (fun ht ↦ ?_)
    rw [coe_eta] at ht
    simp [ht] at h3
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
⊢ multiplicity λ (S'.a + S'.b) < 2

Tactic:
rw [h1'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h1

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_lt
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
h1₁ : multiplicity λ (S'.a + S'.b) < 2
⊢ emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)

Tactic:
rw [h1'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h1

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_lt
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
h1₁ : multiplicity λ (S'.a + S'.b) < 2
h2₁ : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
⊢ emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)

Tactic:
rw [h1'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h1

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_lt
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
h1₁ : multiplicity λ (S'.a + S'.b) < 2
h2₁ : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3₁ : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
⊢ FiniteMultiplicity λ (S'.a + S'.b)

Tactic:
rw [h1'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h1

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_lt
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
h1₁ : multiplicity λ (S'.a + S'.b) < 2
h2₁ : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3₁ : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1'₁ : FiniteMultiplicity λ (S'.a + S'.b)
⊢ FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)

Tactic:
rw [h1'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h1

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_lt
-- 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
h1 : emultiplicity λ (S'.a + S'.b) < (↑2 : ℕ∞)
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
h1₁ : multiplicity λ (S'.a + S'.b) < 2
h2₁ : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3₁ : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1'₁ : FiniteMultiplicity λ (S'.a + S'.b)
h2'₁ : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
⊢ FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)

Tactic:
rw [h1'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h1

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_lt
-- 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
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
⊢ multiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < 2

Tactic:
rw [h2'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h2

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_lt
-- 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
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
h2₁ : multiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < 2
⊢ emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)

Tactic:
rw [h2'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h2

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_lt
-- 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
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
h2₁ : multiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < 2
h3₁ : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
⊢ FiniteMultiplicity λ (S'.a + S'.b)

Tactic:
rw [h2'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h2

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_lt
-- 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
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
h2₁ : multiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < 2
h3₁ : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1'₁ : FiniteMultiplicity λ (S'.a + S'.b)
⊢ FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)

Tactic:
rw [h2'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h2

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_lt
-- 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
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : emultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < (↑2 : ℕ∞)
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
h2₁ : multiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < 2
h3₁ : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1'₁ : FiniteMultiplicity λ (S'.a + S'.b)
h2'₁ : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
⊢ FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)

Tactic:
rw [h2'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h2

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_lt
-- 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
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < 2
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
⊢ multiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < 2

Tactic:
rw [h3'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h3

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_lt
-- 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
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < 2
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
h3₁ : multiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < 2
⊢ FiniteMultiplicity λ (S'.a + S'.b)

Tactic:
rw [h3'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h3

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_lt
-- 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
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < 2
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
h3₁ : multiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < 2
h1'₁ : FiniteMultiplicity λ (S'.a + S'.b)
⊢ FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)

Tactic:
rw [h3'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h3

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_lt
-- 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
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < 2
h3 : emultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < (↑2 : ℕ∞)
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
h3₁ : multiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < 2
h1'₁ : FiniteMultiplicity λ (S'.a + S'.b)
h2'₁ : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
⊢ FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)

Tactic:
rw [h3'.emultiplicity_eq_multiplicity, Nat.cast_lt] at h3

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, Nat.cast_lt
-- 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
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < 2
h3 : multiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < 2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
⊢ HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) λ 2) 3 ∣ (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3

Tactic:
have := (pow_dvd_pow_of_dvd (lambda_sq_dvd_c S') 3).mul_left S'.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
h1 : multiplicity λ (S'.a + S'.b) < 2
h2 : multiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) < 2
h3 : multiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b) < 2
h1' : FiniteMultiplicity λ (S'.a + S'.b)
h2' : FiniteMultiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b)
h3' : FiniteMultiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)
this : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) λ 2) 3 ∣ (↑S'.u : 𝓞 K) * HPow.hPow (β := ℕ) S'.c 3
⊢ HMul.hMul (α := ℕ) 2 3 ≤
    multiplicity λ (S'.a + S'.b) + multiplicity λ (S'.a + (↑η : 𝓞 K) * S'.b) +
      multiplicity λ (S'.a + HPow.hPow (β := ℕ) (↑η : 𝓞 K) 2 * S'.b)

Tactic:
rw [← pow_mul, ← S'.H, a_cube_add_b_cube_eq_mul, pow_dvd_iff_le_emultiplicity,
    emultiplicity_mul hζ.zeta_sub_one_prime', emultiplicity_mul hζ.zeta_sub_one_prime',
      h1'.emultiplicity_eq_multiplicity, h2'.emultiplicity_eq_multiplicity,
      h3'.emultiplicity_eq_multiplicity, ← Nat.cast_add, ← Nat.cast_add, Nat.cast_le] at this

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, _private.0.FermatLastTheoremForThreeGen.Solution'.H, pow_mul, pow_dvd_iff_le_emultiplicity, Nat.cast_add, Nat.cast_le, _private.0.FermatLastTheoremForThreeGen.a_cube_add_b_cube_eq_mul, emultiplicity_mul, IsPrimitiveRoot.zeta_sub_one_prime'