awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
let let₁ let₂ let₃ : FermatLastTheoremFor 3
⊢ FermatLastTheoremFor 3
have let₄ : let K := CyclotomicField 3 ℚ;
∀ (this : NumberField K), FermatLastTheoremFor 3
Tactic: classical
  let K := CyclotomicField 3 ℚ
  let hζ := IsCyclotomicExtension.zeta_spec 3 ℚ K
  have : NumberField K := IsCyclotomicExtension.numberField {3} ℚ _
  apply FermatLastTheoremForThree_of_FermatLastTheoremThreeGen hζ
  intro a b c u hc ha hb hcdvd coprime H
  let S' : FermatLastTheoremForThreeGen.Solution' hζ :=
  { a := a
    b := b
    c := c
    u := u
    ha := ha
    hb := hb
    hc := hc
    coprime := coprime
    hcdvd := hcdvd
    H := H }
  obtain ⟨S, -⟩ := FermatLastTheoremForThreeGen.exists_Solution_of_Solution' S'
  obtain ⟨Smin, hSmin⟩ := S.exists_minimal
  obtain ⟨Sfin, hSfin⟩ := Smin.exists_Solution_multiplicity_lt
  linarith [hSmin Sfin]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
let let₁ let₂ let₃ : FermatLastTheoremFor 3
let₄ :
  let K := CyclotomicField 3 ℚ;
  ∀ (this : NumberField K), FermatLastTheoremFor 3
⊢ FermatLastTheoremFor 3
have let₅ : let K := CyclotomicField 3 ℚ;
let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := sorry;
∀ (this : NumberField K), FermatLastTheoremForThreeGen hζ
Tactic: classical
  let K := CyclotomicField 3 ℚ
  let hζ := IsCyclotomicExtension.zeta_spec 3 ℚ K
  have : NumberField K := IsCyclotomicExtension.numberField {3} ℚ _
  apply FermatLastTheoremForThree_of_FermatLastTheoremThreeGen hζ
  intro a b c u hc ha hb hcdvd coprime H
  let S' : FermatLastTheoremForThreeGen.Solution' hζ :=
  { a := a
    b := b
    c := c
    u := u
    ha := ha
    hb := hb
    hc := hc
    coprime := coprime
    hcdvd := hcdvd
    H := H }
  obtain ⟨S, -⟩ := FermatLastTheoremForThreeGen.exists_Solution_of_Solution' S'
  obtain ⟨Smin, hSmin⟩ := S.exists_minimal
  obtain ⟨Sfin, hSfin⟩ := Smin.exists_Solution_multiplicity_lt
  linarith [hSmin Sfin]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
let let₁ let₂ let₃ : FermatLastTheoremFor 3
let₄ :
  let K := CyclotomicField 3 ℚ;
  ∀ (this : NumberField K), FermatLastTheoremFor 3
let₅ :
  let K := CyclotomicField 3 ℚ;
  let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯;
  ∀ (this : NumberField K), FermatLastTheoremForThreeGen hζ
⊢ FermatLastTheoremFor 3
have let₆ : let K := CyclotomicField 3 ℚ;
let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := sorry;
∀ (this : NumberField K) (a b c : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers K)ˣ) (hc : c ≠ 0)
  (ha : ¬hζ.toInteger - 1 ∣ a) (hb : ¬hζ.toInteger - 1 ∣ b) (hcdvd : hζ.toInteger - 1 ∣ c) (coprime : IsCoprime a b)
  (H : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = (↑u : NumberField.RingOfIntegers K) * HPow.hPow (β := ℕ) c 3),
  False
Tactic: classical
  let K := CyclotomicField 3 ℚ
  let hζ := IsCyclotomicExtension.zeta_spec 3 ℚ K
  have : NumberField K := IsCyclotomicExtension.numberField {3} ℚ _
  apply FermatLastTheoremForThree_of_FermatLastTheoremThreeGen hζ
  intro a b c u hc ha hb hcdvd coprime H
  let S' : FermatLastTheoremForThreeGen.Solution' hζ :=
  { a := a
    b := b
    c := c
    u := u
    ha := ha
    hb := hb
    hc := hc
    coprime := coprime
    hcdvd := hcdvd
    H := H }
  obtain ⟨S, -⟩ := FermatLastTheoremForThreeGen.exists_Solution_of_Solution' S'
  obtain ⟨Smin, hSmin⟩ := S.exists_minimal
  obtain ⟨Sfin, hSfin⟩ := Smin.exists_Solution_multiplicity_lt
  linarith [hSmin Sfin]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
let let₁ let₂ let₃ : FermatLastTheoremFor 3
let₄ :
  let K := CyclotomicField 3 ℚ;
  ∀ (this : NumberField K), FermatLastTheoremFor 3
let₅ :
  let K := CyclotomicField 3 ℚ;
  let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯;
  ∀ (this : NumberField K), FermatLastTheoremForThreeGen hζ
let₆ :
  let K := CyclotomicField 3 ℚ;
  let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯;
  ∀ (this : NumberField K) (a b c : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers K)ˣ) (hc : c ≠ 0)
    (ha : ¬hζ.toInteger - 1 ∣ a) (hb : ¬hζ.toInteger - 1 ∣ b) (hcdvd : hζ.toInteger - 1 ∣ c) (coprime : IsCoprime a b)
    (H :
      HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = (↑u : NumberField.RingOfIntegers K) * HPow.hPow (β := ℕ) c 3),
    False
let₇ :
  let K := CyclotomicField 3 ℚ;
  let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯;
  ∀ (this : NumberField K) (a b c : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers K)ˣ) (hc : c ≠ 0)
    (ha : ¬hζ.toInteger - 1 ∣ a) (hb : ¬hζ.toInteger - 1 ∣ b) (hcdvd : hζ.toInteger - 1 ∣ c) (coprime : IsCoprime a b)
    (H :
      HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = (↑u : NumberField.RingOfIntegers K) * HPow.hPow (β := ℕ) c 3),
    False
⊢ FermatLastTheoremFor 3
have let₈ : let K := CyclotomicField 3 ℚ;
let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := sorry;
∀ (this : NumberField K) (a b c : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers K)ˣ) (hc : c ≠ 0)
  (ha : ¬hζ.toInteger - 1 ∣ a) (hb : ¬hζ.toInteger - 1 ∣ b) (hcdvd : hζ.toInteger - 1 ∣ c) (coprime : IsCoprime a b)
  (H : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = (↑u : NumberField.RingOfIntegers K) * HPow.hPow (β := ℕ) c 3)
  (S : FermatLastTheoremForThreeGen.Solution hζ), False
Tactic: classical
  let K := CyclotomicField 3 ℚ
  let hζ := IsCyclotomicExtension.zeta_spec 3 ℚ K
  have : NumberField K := IsCyclotomicExtension.numberField {3} ℚ _
  apply FermatLastTheoremForThree_of_FermatLastTheoremThreeGen hζ
  intro a b c u hc ha hb hcdvd coprime H
  let S' : FermatLastTheoremForThreeGen.Solution' hζ :=
  { a := a
    b := b
    c := c
    u := u
    ha := ha
    hb := hb
    hc := hc
    coprime := coprime
    hcdvd := hcdvd
    H := H }
  obtain ⟨S, -⟩ := FermatLastTheoremForThreeGen.exists_Solution_of_Solution' S'
  obtain ⟨Smin, hSmin⟩ := S.exists_minimal
  obtain ⟨Sfin, hSfin⟩ := Smin.exists_Solution_multiplicity_lt
  linarith [hSmin Sfin]
-- Lean 4 proof step from Mathlib.NumberTheory.FLT.Three (goal)
Goal:
let let₁ let₂ let₃ : FermatLastTheoremFor 3
let₄ :
  let K := CyclotomicField 3 ℚ;
  ∀ (this : NumberField K), FermatLastTheoremFor 3
let₅ :
  let K := CyclotomicField 3 ℚ;
  let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯;
  ∀ (this : NumberField K), FermatLastTheoremForThreeGen hζ
let₆ :
  let K := CyclotomicField 3 ℚ;
  let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯;
  ∀ (this : NumberField K) (a b c : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers K)ˣ) (hc : c ≠ 0)
    (ha : ¬hζ.toInteger - 1 ∣ a) (hb : ¬hζ.toInteger - 1 ∣ b) (hcdvd : hζ.toInteger - 1 ∣ c) (coprime : IsCoprime a b)
    (H :
      HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = (↑u : NumberField.RingOfIntegers K) * HPow.hPow (β := ℕ) c 3),
    False
let₇ :
  let K := CyclotomicField 3 ℚ;
  let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯;
  ∀ (this : NumberField K) (a b c : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers K)ˣ) (hc : c ≠ 0)
    (ha : ¬hζ.toInteger - 1 ∣ a) (hb : ¬hζ.toInteger - 1 ∣ b) (hcdvd : hζ.toInteger - 1 ∣ c) (coprime : IsCoprime a b)
    (H :
      HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = (↑u : NumberField.RingOfIntegers K) * HPow.hPow (β := ℕ) c 3),
    False
let₈ :
  let K := CyclotomicField 3 ℚ;
  let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯;
  ∀ (this : NumberField K) (a b c : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers K)ˣ) (hc : c ≠ 0)
    (ha : ¬hζ.toInteger - 1 ∣ a) (hb : ¬hζ.toInteger - 1 ∣ b) (hcdvd : hζ.toInteger - 1 ∣ c) (coprime : IsCoprime a b)
    (H : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = (↑u : NumberField.RingOfIntegers K) * HPow.hPow (β := ℕ) c 3)
    (S : FermatLastTheoremForThreeGen.Solution hζ), False
⊢ FermatLastTheoremFor 3
have let₉ : let K := CyclotomicField 3 ℚ;
let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := sorry;
∀ (this : NumberField K) (a b c : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers K)ˣ) (hc : c ≠ 0)
  (ha : ¬hζ.toInteger - 1 ∣ a) (hb : ¬hζ.toInteger - 1 ∣ b) (hcdvd : hζ.toInteger - 1 ∣ c) (coprime : IsCoprime a b)
  (H : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = (↑u : NumberField.RingOfIntegers K) * HPow.hPow (β := ℕ) c 3)
  (S Smin : FermatLastTheoremForThreeGen.Solution hζ) (hSmin : Smin.isMinimal), False
Tactic: classical
  let K := CyclotomicField 3 ℚ
  let hζ := IsCyclotomicExtension.zeta_spec 3 ℚ K
  have : NumberField K := IsCyclotomicExtension.numberField {3} ℚ _
  apply FermatLastTheoremForThree_of_FermatLastTheoremThreeGen hζ
  intro a b c u hc ha hb hcdvd coprime H
  let S' : FermatLastTheoremForThreeGen.Solution' hζ :=
  { a := a
    b := b
    c := c
    u := u
    ha := ha
    hb := hb
    hc := hc
    coprime := coprime
    hcdvd := hcdvd
    H := H }
  obtain ⟨S, -⟩ := FermatLastTheoremForThreeGen.exists_Solution_of_Solution' S'
  obtain ⟨Smin, hSmin⟩ := S.exists_minimal
  obtain ⟨Sfin, hSfin⟩ := Smin.exists_Solution_multiplicity_lt
  linarith [hSmin Sfin]
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
p : ℕ
h : Prime p
⊢ ¬p.Pseudoperfect
have rw : p = 0 ∨ ∀ s ⊆ p.properDivisors, ∑ i ∈ s, i ≠ p
Tactic: rw [not_pseudoperfect_iff_forall]
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
p : ℕ
h : Prime p
⊢ p = 0 ∨ ∀ s ⊆ p.properDivisors, ∑ i ∈ s, i ≠ p
have refine : ∀ (s : Finset ℕ) (hs : s ⊆ p.properDivisors), LE.le (α := ℕ) (∑ i ∈ s, i) 1
Tactic: refine Or.inr fun s hs ↦ ne_of_lt (lt_of_le_of_lt ?_ h.one_lt)
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (hypothesis)
Goal:
p : ℕ
h : Prime p
s : Finset ℕ
hs : s ⊆ p.properDivisors
⊢ LE.le (α := ℕ) (∑ i ∈ s, i) 1
have hs₁ : s ⊆ {1}
Tactic: rw [Prime.properDivisors h] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n m : ℕ
h : Prime n
⊢ (n ^ m).Deficient
have inl : (HPow.hPow (β := ℕ) n 0).Deficient
Tactic: rcases Nat.eq_zero_or_pos m with (rfl | _)
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n m : ℕ
h : Prime n
inl : (HPow.hPow (β := ℕ) n 0).Deficient
⊢ (n ^ m).Deficient
have inr : m > 0 → (n ^ m).Deficient
Tactic: rcases Nat.eq_zero_or_pos m with (rfl | _)
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n m : ℕ
h : Prime n
h_1 : m > 0
⊢ (n ^ m).Deficient
have inr : ∑ i ∈ map { toFun := fun (x : ℕ) ↦ n ^ x, inj' := sorry : ℕ ↪ ℕ } (range m), i < n ^ m
Tactic: rw [Deficient, properDivisors_prime_pow h]
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n m : ℕ
h : Prime n
h_1 : m > 0
⊢ ∑ i ∈ map { toFun := fun (x : ℕ) ↦ n ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range m), i < n ^ m
have x : Eq (α := ℕ) (∑ x ∈ map { toFun := fun (x : ℕ) ↦ n ^ x, inj' := sorry : ℕ ↪ ℕ } (range m), x) (∑ i ∈ range m, n ^ i)
Tactic: calc
      ∑ x ∈ Finset.map ⟨(n ^ ·), Nat.pow_right_injective h.two_le⟩ (range m), x
        = ∑ i ∈ range m, n ^ i := by simp
      _ = (n ^ m - 1) / (n - 1) := (Nat.geomSum_eq (Prime.two_le h) _)
      _ ≤ (n ^ m - 1) := Nat.div_le_self (n ^ m - 1) (n - 1)
      _ < n ^ m := sub_lt (pow_pos (Prime.pos h) m) (Nat.one_pos)
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n : ℕ
h : IsPrimePow n
⊢ n.Deficient
have obtain : ∀ (p k : ℕ) (hp : _root_.Prime p), (p ^ k).Deficient
Tactic: obtain ⟨p, k, hp, -, rfl⟩ := h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
⊢ Set.Infinite (α := ℕ) {n : ℕ | n.Deficient}
have rw : ∀ (a : ℕ), ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | n.Deficient} b ∧ a < b
Tactic: rw [Set.infinite_iff_exists_gt]
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
a : ℕ
⊢ ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | n.Deficient} b ∧ a < b
have obtain : ∀ (b : ℕ) (h1 : a.succ ≤ b) (h2 : Prime b), ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | n.Deficient} b ∧ a < b
Tactic: obtain ⟨b, h1, h2⟩ := exists_infinite_primes a.succ
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
⊢ Set.Infinite (α := ℕ) {n : ℕ | Even n ∧ n.Deficient}
have rw : ∀ (a : ℕ), ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Deficient} b ∧ a < b
Tactic: rw [Set.infinite_iff_exists_gt]
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n : ℕ
⊢ ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Deficient} b ∧ n < b
have h : Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Deficient} (HPow.hPow (α := ℕ) 2 (n + 1)) ∧
  n < HPow.hPow (α := ℕ) 2 (n + 1)
Tactic: use 2 ^ (n + 1)
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n : ℕ
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Deficient} (HPow.hPow (α := ℕ) 2 (n + 1)) ∧
    n < HPow.hPow (α := ℕ) 2 (n + 1)
have h : Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Deficient} (HPow.hPow (α := ℕ) 2 (n + 1))
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n : ℕ
h : Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Deficient} (HPow.hPow (α := ℕ) 2 (n + 1))
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Deficient} (HPow.hPow (α := ℕ) 2 (n + 1)) ∧
    n < HPow.hPow (α := ℕ) 2 (n + 1)
have h₁ : n < HPow.hPow (α := ℕ) 2 (n + 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n : ℕ
⊢ HPow.hPow (α := ℕ) 2 (n + 1) = HPow.hPow (α := ℕ) 2 n + HPow.hPow (α := ℕ) 2 n
have rw : HPow.hPow (α := ℕ) 2 n * 2 = HPow.hPow (α := ℕ) 2 n + HPow.hPow (α := ℕ) 2 n
Tactic: rw [pow_succ, mul_two]
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n : ℕ
rw : HPow.hPow (α := ℕ) 2 n * 2 = HPow.hPow (α := ℕ) 2 n + HPow.hPow (α := ℕ) 2 n
⊢ HPow.hPow (α := ℕ) 2 (n + 1) = HPow.hPow (α := ℕ) 2 n + HPow.hPow (α := ℕ) 2 n
have rw₁ : HPow.hPow (α := ℕ) 2 n + HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n + HPow.hPow (α := ℕ) 2 n
Tactic: rw [pow_succ, mul_two]
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
⊢ Set.Infinite (α := ℕ) {n : ℕ | Odd n ∧ n.Deficient}
have rw : ∀ (a : ℕ), ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Odd n ∧ n.Deficient} b ∧ a < b
Tactic: rw [Set.infinite_iff_exists_gt]
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n : ℕ
⊢ ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Odd n ∧ n.Deficient} b ∧ n < b
have obtain : ∀ (p : ℕ),
  max (n + 1) 3 ≤ p → ∀ (h2 : Prime p), ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Odd n ∧ n.Deficient} b ∧ n < b
Tactic: obtain ⟨p, ⟨_, h2⟩⟩ := exists_infinite_primes (max (n + 1) 3)
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n : ℕ
⊢ n.Abundant ↔ 2 < n.abundancyIndex
have pos : ∀ (h : n = 0), n.Abundant ↔ 2 < n.abundancyIndex
Tactic: by_cases h : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n : ℕ
pos : ∀ (h : n = 0), n.Abundant ↔ 2 < n.abundancyIndex
⊢ n.Abundant ↔ 2 < n.abundancyIndex
have neg : ∀ (h : ¬n = 0), n.Abundant ↔ 2 < n.abundancyIndex
Tactic: by_cases h : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n : ℕ
h : ¬n = 0
⊢ n.Abundant ↔ 2 < n.abundancyIndex
have neg : 2 * n < ∑ i ∈ n.divisors, i ↔ HMul.hMul (α := ℚ) 2 (↑n : ℚ) < (↑(∑ i ∈ n.divisors, i) : ℚ)
Tactic: rw [abundant_iff_sum_divisors, abundancyIndex, lt_div_iff₀ (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n : ℕ
h : ¬n = 0
⊢ 2 * n < ∑ i ∈ n.divisors, i ↔ HMul.hMul (α := ℚ) 2 (↑n : ℚ) < (↑(∑ i ∈ n.divisors, i) : ℚ)
have neg : 2 * n < ∑ i ∈ n.divisors, i ↔ 2 * n < ∑ i ∈ n.divisors, i
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n m : ℕ
hn : n ≠ 0
hd : m ∣ n
⊢ m.abundancyIndex ≤ n.abundancyIndex
have obtain : ∀ (k : ℕ) (hk : n = m * k), m.abundancyIndex ≤ n.abundancyIndex
Tactic: obtain ⟨k, hk⟩ := hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (hypothesis)
Goal:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
⊢ m.abundancyIndex ≤ n.abundancyIndex
have hk0 : k ≠ 0
Tactic: have hk0 : k ≠ 0 := by grind
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ m.abundancyIndex ≤ n.abundancyIndex
have rw : HDiv.hDiv (α := ℚ) (↑(∑ i ∈ m.divisors, i) : ℚ) (↑m : ℚ) ≤
  HDiv.hDiv (α := ℚ) (↑(∑ i ∈ (m * k).divisors, i) : ℚ) (↑k : ℚ) / (↑m : ℚ)
Tactic: rw [abundancyIndex, abundancyIndex, hk, cast_mul, div_mul_eq_div_div_swap]
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ HDiv.hDiv (α := ℚ) (↑(∑ i ∈ m.divisors, i) : ℚ) (↑m : ℚ) ≤
    HDiv.hDiv (α := ℚ) (↑(∑ i ∈ (m * k).divisors, i) : ℚ) (↑k : ℚ) / (↑m : ℚ)
have refine : (↑(∑ i ∈ m.divisors, i) : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑(∑ i ∈ (m * k).divisors, i) : ℚ) (↑k : ℚ)
Tactic: refine div_le_div_of_nonneg_right ?_ m.cast_nonneg
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ (↑(∑ i ∈ m.divisors, i) : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑(∑ i ∈ (m * k).divisors, i) : ℚ) (↑k : ℚ)
have rw : LE.le (α := ℕ) (∑ i ∈ m.divisors, i * k) (∑ i ∈ (m * k).divisors, i)
Tactic: rw [le_div_iff₀ (by grind [cast_pos]), ← cast_mul, cast_le, sum_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (hypothesis)
Goal:
n m : ℕ
h : m.Abundant
hd : m ∣ n
hn : n ≠ 0
⊢ n.Abundant
have this : m.abundancyIndex ≤ n.abundancyIndex
Tactic: have := abundancyIndex_le_of_dvd hn hd
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (hypothesis)
Goal:
n m : ℕ
h : n.Abundant
hm : m ≠ 0
⊢ (m * n).Abundant
have hn : n ≠ 0
Tactic: have hn : n ≠ 0 := by grind [not_abundant_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (hypothesis)
Goal:
n m : ℕ
h : n.Abundant
hm : m ≠ 0
hn : n ≠ 0
⊢ (m * n).Abundant
have hmn : m * n ≠ 0
Tactic: have hmn : m * n ≠ 0 := mul_ne_zero hm hn
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
⊢ Set.Infinite (α := ℕ) {n : ℕ | Even n ∧ n.Abundant}
have rw : ∀ (a : ℕ), ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Abundant} b ∧ a < b
Tactic: rw [Set.infinite_iff_exists_gt]
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (hypothesis)
Goal:
a : ℕ
⊢ ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Abundant} b ∧ a < b
have ha : Abundant 12
Tactic: have ha : Abundant 12 := by decide
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
a : ℕ
ha : Abundant 12
⊢ ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Abundant} b ∧ a < b
have h : Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Abundant} (2 * (a + 1) * 12) ∧ a < 2 * (a + 1) * 12
Tactic: use (2 * (a + 1)) * 12
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
⊢ Set.Infinite (α := ℕ) {n : ℕ | Odd n ∧ n.Abundant}
have rw : ∀ (a : ℕ), ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Odd n ∧ n.Abundant} b ∧ a < b
Tactic: rw [Set.infinite_iff_exists_gt]
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (hypothesis)
Goal:
a : ℕ
⊢ ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Odd n ∧ n.Abundant} b ∧ a < b
have ha : Abundant 945
Tactic: have ha : Abundant 945 := by decide +kernel
-- Lean 4 proof step from Mathlib.NumberTheory.FactorisationProperties (goal)
Goal:
a : ℕ
ha : Abundant 945
⊢ ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Odd n ∧ n.Abundant} b ∧ a < b
have h : Membership.mem (γ := Set ℕ) {n : ℕ | Odd n ∧ n.Abundant} ((2 * a + 1) * 945) ∧ a < (2 * a + 1) * 945
Tactic: use (2 * a + 1) * 945
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (hypothesis)
Goal:
n : ℕ
⊢ n.fermatNumber ≠ 1
have this : 3 ≤ n.fermatNumber
Tactic: have := three_le_fermatNumber n
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
⊢ ∏ k ∈ range (n + 1), k.fermatNumber = (n + 1).fermatNumber - 2
have succ : HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 - HPow.hPow (α := ℕ) (β := ℕ) 1 2 =
  HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 - 2
Tactic: rw [prod_range_succ, hn, fermatNumber, fermatNumber, mul_comm,
    (show 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1 by lia), ← sq_sub_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n)) 2 - HPow.hPow (α := ℕ) (β := ℕ) 1 2 =
    HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 - 2
have succ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) - 1 = 1 + HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) - 2
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
⊢ ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
have zero : ∏ k ∈ range 0, k.fermatNumber = fermatNumber 0 - 2
Tactic: induction n with | zero => rfl | succ n hn =>
  rw [prod_range_succ, hn, fermatNumber, fermatNumber, mul_comm,
    (show 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1 by lia), ← sq_sub_sq]
  ring_nf
  lia
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
zero : ∏ k ∈ range 0, k.fermatNumber = fermatNumber 0 - 2
⊢ ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
have succ : ∀ (n : ℕ) (hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2),
  ∏ k ∈ range (n + 1), k.fermatNumber = (n + 1).fermatNumber - 2
Tactic: induction n with | zero => rfl | succ n hn =>
  rw [prod_range_succ, hn, fermatNumber, fermatNumber, mul_comm,
    (show 2 ^ 2 ^ n + 1 - 2 = 2 ^ 2 ^ n - 1 by lia), ← sq_sub_sq]
  ring_nf
  lia
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
⊢ n.fermatNumber = HAdd.hAdd (α := ℕ) (∏ k ∈ range n, k.fermatNumber) 2
have rw : 2 ≤ n.fermatNumber
Tactic: rw [prod_fermatNumber, Nat.sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
⊢ (n + 1).fermatNumber = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
have rw : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
Tactic: rw [fermatNumber, pow_succ, mul_comm, pow_mul', fermatNumber, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
rw : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
⊢ (n + 1).fermatNumber = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
have rw₁ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
Tactic: rw [fermatNumber, pow_succ, mul_comm, pow_mul', fermatNumber, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Fermat (goal)
Goal:
n : ℕ
rw : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 (n + 1)) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
rw₁ : HPow.hPow (α := ℕ) 2 (HPow.hPow (α := ℕ) 2 n * 2) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
⊢ (n + 1).fermatNumber = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
have rw₂ : HPow.hPow (α := ℕ) 2 (2 * HPow.hPow (α := ℕ) 2 n) + 1 = HPow.hPow (β := ℕ) (n.fermatNumber - 1) 2 + 1
Tactic: rw [fermatNumber, pow_succ, mul_comm, pow_mul', fermatNumber, add_tsub_cancel_right]