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
S' : Solution hζ
hS' : S'.multiplicity = S.Solution'_descent.multiplicity
⊢ ∃ (S₁ : Solution hζ), S₁.multiplicity < S.multiplicity

Tactic:
⟨S', hS' ▸ Solution'_descent_multiplicity_lt S⟩

Premises used: Eq.rec, _private.0.FermatLastTheoremForThreeGen.Solution.Solution'_descent_multiplicity_lt, Exists.intro, Eq.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
S' : Solution hζ
hS' : S'.multiplicity = S.Solution'_descent.multiplicity
⊢ ∃ (S₁ : Solution hζ), S₁.multiplicity < S.multiplicity

Tactic:
exact ⟨S', hS' ▸ Solution'_descent_multiplicity_lt S⟩
-- 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
obtain :
  ∀ (S' : Solution hζ) (hS' : S'.multiplicity = S.Solution'_descent.multiplicity),
    ∃ (S₁ : Solution hζ), S₁.multiplicity < S.multiplicity
⊢ ∃ (S₁ : Solution hζ), S₁.multiplicity < S.multiplicity

Tactic:
classical
  obtain ⟨S', hS'⟩ := exists_Solution_of_Solution' (Solution'_descent S)
  exact ⟨S', hS' ▸ Solution'_descent_multiplicity_lt S⟩

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.Solution'_descent, _private.0.FermatLastTheoremForThreeGen.exists_Solution_of_Solution'
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type := CyclotomicField 3 ℚ
hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯
⊢ NumberField K

Tactic:
have : NumberField K := IsCyclotomicExtension.numberField {3} ℚ _
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type := CyclotomicField 3 ℚ
hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯
this : NumberField K
apply : FermatLastTheoremForThreeGen hζ
⊢ FermatLastTheoremFor 3

Tactic:
apply FermatLastTheoremForThree_of_FermatLastTheoremThreeGen hζ

Premises used: _private.0.FermatLastTheoremForThree_of_FermatLastTheoremThreeGen
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type := CyclotomicField 3 ℚ
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ζ :=
  { a := a, b := b, c := c, u := u, ha := ha, hb := hb, hc := hc, coprime := coprime, hcdvd := hcdvd, H := H }
obtain : ∀ (S : FermatLastTheoremForThreeGen.Solution hζ), False
⊢ False

Tactic:
obtain ⟨S, -⟩ := FermatLastTheoremForThreeGen.exists_Solution_of_Solution' S'

Premises used: _private.0.FermatLastTheoremForThreeGen.exists_Solution_of_Solution'
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type := CyclotomicField 3 ℚ
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ζ :=
  { a := a, b := b, c := c, u := u, ha := ha, hb := hb, hc := hc, coprime := coprime, hcdvd := hcdvd, H := H }
S : FermatLastTheoremForThreeGen.Solution hζ
obtain : ∀ (Smin : FermatLastTheoremForThreeGen.Solution hζ) (hSmin : Smin.isMinimal), False
⊢ False

Tactic:
obtain ⟨Smin, hSmin⟩ := S.exists_minimal

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.exists_minimal
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type := CyclotomicField 3 ℚ
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ζ :=
  { a := a, b := b, c := c, u := u, ha := ha, hb := hb, hc := hc, coprime := coprime, hcdvd := hcdvd, H := H }
S Smin : FermatLastTheoremForThreeGen.Solution hζ
hSmin : Smin.isMinimal
obtain : ∀ (Sfin : FermatLastTheoremForThreeGen.Solution hζ) (hSfin : Sfin.multiplicity < Smin.multiplicity), False
⊢ False

Tactic:
obtain ⟨Sfin, hSfin⟩ := Smin.exists_Solution_multiplicity_lt

Premises used: _private.0.FermatLastTheoremForThreeGen.Solution.exists_Solution_multiplicity_lt
-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
K : Type := CyclotomicField 3 ℚ
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ζ :=
  { a := a, b := b, c := c, u := u, ha := ha, hb := hb, hc := hc, coprime := coprime, hcdvd := hcdvd, H := H }
S Smin : FermatLastTheoremForThreeGen.Solution hζ
hSmin : Smin.isMinimal
Sfin : FermatLastTheoremForThreeGen.Solution hζ
hSfin : Sfin.multiplicity < Smin.multiplicity
linarith :
  -1 + (HAdd.hAdd (α := ℤ) (↑Sfin.multiplicity : ℤ) 1 - (↑Smin.multiplicity : ℤ)) +
      HSub.hSub (α := ℤ) (↑Smin.multiplicity : ℤ) (↑Sfin.multiplicity : ℤ) =
    0
⊢ False

Tactic:
linarith [hSmin Sfin]
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
⊢ ¬n.Pseudoperfect ↔ n = 0 ∨ ∀ s ⊆ n.properDivisors, ∑ i ∈ s, i ≠ n

Tactic:
grind [Pseudoperfect]

Premises used: Nat.Pseudoperfect
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
⊢ Deficient 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
⊢ Deficient 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
⊢ Deficient 3

Tactic:
decide
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
⊢ ¬Abundant 0

Tactic:
decide
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
⊢ Abundant 12

Tactic:
decide
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
⊢ Weird 70

Tactic:
decide +kernel
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
hn : n ≠ 0
⊢ n.Deficient ↔ ¬n.Abundant ∧ ¬n.Perfect

Tactic:
grind [Perfect, Abundant, Deficient]

Premises used: Nat.Abundant, Nat.Deficient, Nat.Perfect
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
hn : 0 ≠ n
⊢ n.Perfect ↔ ¬n.Abundant ∧ ¬n.Deficient

Tactic:
grind [Perfect, Abundant, Deficient]

Premises used: Nat.Abundant, Nat.Deficient, Nat.Perfect
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
hn : 0 ≠ n
⊢ n.Abundant ↔ ¬n.Perfect ∧ ¬n.Deficient

Tactic:
grind [Perfect, Abundant, Deficient]

Premises used: Nat.Abundant, Nat.Deficient, Nat.Perfect
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
hn : 0 ≠ n
⊢ n.Deficient ∨ n.Abundant ∨ n.Perfect

Tactic:
grind [Perfect, Abundant, Deficient]

Premises used: Nat.Abundant, Nat.Deficient, Nat.Perfect
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
h : n.Perfect
⊢ n.Pseudoperfect

Tactic:
⟨h.2, ⟨properDivisors n, ⟨fun _ a ↦ a, h.1⟩⟩⟩

Premises used: Nat.properDivisors, And.right, And.left, And.intro, Exists.intro, Nat.Pseudoperfect
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
h : Prime n
⊢ ¬n.Abundant

Tactic:
fun h1 ↦ (h.one_lt.trans h1).ne' (sum_properDivisors_eq_one_iff_prime.mpr h)

Premises used: Iff.mpr, Nat.Prime.one_lt, Nat.sum_properDivisors_eq_one_iff_prime, LT.lt.ne', LT.lt.trans, Not
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
h : Prime n
⊢ ¬n.Weird

Tactic:
grind [Weird, h.not_abundant]

Premises used: Nat.Weird, Nat.Prime.not_abundant
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
p : ℕ
h : Prime p
rw : p = 0 ∨ ∀ s ⊆ p.properDivisors, ∑ i ∈ s, i ≠ p
⊢ ¬p.Pseudoperfect

Tactic:
rw [not_pseudoperfect_iff_forall]

Premises used: Nat.not_pseudoperfect_iff_forall
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
p : ℕ
h : Prime p
⊢ p = 0 ∨ ∀ s ⊆ p.properDivisors, ∑ i ∈ s, i ≠ p

Tactic:
Or.inr fun s hs ↦ ne_of_lt (lt_of_le_of_lt ?_ h.one_lt)

Premises used: lt_of_le_of_lt, Nat.Prime.one_lt, Nat.ne_of_lt, Or.inr
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
p : ℕ
h : Prime p
refine : ∀ (s : Finset ℕ) (hs : s ⊆ p.properDivisors), LE.le (α := ℕ) (∑ i ∈ s, i) 1
⊢ p = 0 ∨ ∀ s ⊆ p.properDivisors, ∑ i ∈ s, i ≠ p

Tactic:
refine Or.inr fun s hs ↦ ne_of_lt (lt_of_le_of_lt ?_ h.one_lt)

Premises used: lt_of_le_of_lt, Nat.Prime.one_lt, Nat.ne_of_lt, Or.inr
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
p : ℕ
h : Prime p
s : Finset ℕ
hs : s ⊆ p.properDivisors
⊢ s ⊆ {1}

Tactic:
rw [Prime.properDivisors h] at hs

Premises used: Nat.Prime.properDivisors
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
p : ℕ
h : Prime p
s : Finset ℕ
hs : s ⊆ {1}
⊢ LE.le (α := ℕ) (∑ i ∈ s, i) 1

Tactic:
simpa using Finset.sum_le_sum_of_subset hs

Premises used: Finset.sum_le_sum_of_subset
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
p : ℕ
h : Prime p
⊢ ¬p.Perfect

Tactic:
fun hp ↦ h.not_pseudoperfect hp.pseudoperfect

Premises used: Nat.Perfect.pseudoperfect, Not, Nat.Prime.not_pseudoperfect
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
h : Prime n
inl : (HPow.hPow (β := ℕ) n 0).Deficient
inr : m > 0 → (n ^ m).Deficient
⊢ (n ^ m).Deficient

Tactic:
rcases Nat.eq_zero_or_pos m with (rfl | _)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
h : Prime n
⊢ (HPow.hPow (β := ℕ) n 0).Deficient

Tactic:
simpa using deficient_one

Premises used: Nat.deficient_one
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
h : Prime n
h_1 : m > 0
inr : ∑ i ∈ map { toFun := fun (x : ℕ) ↦ n ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range m), i < n ^ m
⊢ (n ^ m).Deficient

Tactic:
rw [Deficient, properDivisors_prime_pow h]

Premises used: Nat.properDivisors_prime_pow, Nat.Deficient
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
h : Prime n
h_1 : m > 0
⊢ Eq (α := ℕ) (∑ x ∈ map { toFun := fun (x : ℕ) ↦ n ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range m), x) (∑ i ∈ range m, n ^ i)

Tactic:
simp
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
h : Prime n
h_1 : m > 0
⊢ ∑ i ∈ range m, n ^ i = (n ^ m - 1) / (n - 1)

Tactic:
(Nat.geomSum_eq (Prime.two_le h) _)

Premises used: Nat.geomSum_eq, Nat.Prime.two_le
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
h : Prime n
h_1 : m > 0
⊢ (n ^ m - 1) / (n - 1) ≤ n ^ m - 1

Tactic:
Nat.div_le_self (n ^ m - 1) (n - 1)

Premises used: HSub.hSub, Nat.div_le_self, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
h : Prime n
h_1 : m > 0
⊢ n ^ m - 1 < n ^ m

Tactic:
sub_lt (pow_pos (Prime.pos h) m) (Nat.one_pos)

Premises used: pow_pos, Nat.one_pos, Nat.sub_lt, Nat.Prime.pos
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
h : Prime n
h_1 : m > 0
x : Eq (α := ℕ) (∑ x ∈ map { toFun := fun (x : ℕ) ↦ n ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range m), x) (∑ i ∈ range m, n ^ i)
⊢ ∑ i ∈ map { toFun := fun (x : ℕ) ↦ n ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range m), i < n ^ m

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)

Premises used: pow_pos, Nat.one_pos, HSub.hSub, Finset.map, Function.Embedding.mk, Nat.sub_lt, Nat.div_le_self, Nat.Prime.pos, Nat.geomSum_eq, Finset.range, HPow.hPow, Nat.pow_right_injective, Nat.Prime.two_le, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
h : IsPrimePow n
obtain : ∀ (p k : ℕ) (hp : _root_.Prime p), (p ^ k).Deficient
⊢ n.Deficient

Tactic:
obtain ⟨p, k, hp, -, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
p k : ℕ
hp : _root_.Prime p
⊢ (p ^ k).Deficient

Tactic:
hp.nat_prime.deficient_pow

Premises used: Prime.nat_prime, Nat.Prime.deficient_pow
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
p k : ℕ
hp : _root_.Prime p
⊢ (p ^ k).Deficient

Tactic:
exact hp.nat_prime.deficient_pow

Premises used: Prime.nat_prime, Nat.Prime.deficient_pow
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
h : Prime n
⊢ n.Deficient

Tactic:
(pow_one n) ▸ h.deficient_pow

Premises used: Eq.rec, pow_one, Nat.Prime.deficient_pow
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
rw : ∀ (a : ℕ), ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | n.Deficient} b ∧ a < b
⊢ Set.Infinite (α := ℕ) {n : ℕ | n.Deficient}

Tactic:
rw [Set.infinite_iff_exists_gt]

Premises used: Set.infinite_iff_exists_gt
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
a : ℕ
obtain :
  ∀ (b : ℕ) (h1 : a.succ ≤ b) (h2 : Prime b), ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | n.Deficient} b ∧ a < b
⊢ ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | n.Deficient} b ∧ a < b

Tactic:
obtain ⟨b, h1, h2⟩ := exists_infinite_primes a.succ

Premises used: Nat.succ, Nat.exists_infinite_primes
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
a b : ℕ
h1 : a.succ ≤ b
h2 : Prime b
⊢ ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | n.Deficient} b ∧ a < b

Tactic:
⟨b, h2.deficient, h1⟩

Premises used: And.intro, Exists.intro, Nat.Prime.deficient
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
a b : ℕ
h1 : a.succ ≤ b
h2 : Prime b
⊢ ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | n.Deficient} b ∧ a < b

Tactic:
exact ⟨b, h2.deficient, h1⟩
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
rw : ∀ (a : ℕ), ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Deficient} b ∧ a < b
⊢ Set.Infinite (α := ℕ) {n : ℕ | Even n ∧ n.Deficient}

Tactic:
rw [Set.infinite_iff_exists_gt]

Premises used: Set.infinite_iff_exists_gt
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
h :
  Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Deficient} (HPow.hPow (α := ℕ) 2 (n + 1)) ∧
    n < HPow.hPow (α := ℕ) 2 (n + 1)
⊢ ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Deficient} b ∧ n < b

Tactic:
use 2 ^ (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
h : Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Deficient} (HPow.hPow (α := ℕ) 2 (n + 1))
h₁ : n < HPow.hPow (α := ℕ) 2 (n + 1)
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Deficient} (HPow.hPow (α := ℕ) 2 (n + 1)) ∧
    n < HPow.hPow (α := ℕ) 2 (n + 1)

Tactic:
constructor
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
rw : HPow.hPow (α := ℕ) 2 n * 2 = HPow.hPow (α := ℕ) 2 n + HPow.hPow (α := ℕ) 2 n
rw₁ rw₂ : HPow.hPow (α := ℕ) 2 n + HPow.hPow (α := ℕ) 2 n = HPow.hPow (α := ℕ) 2 n + HPow.hPow (α := ℕ) 2 n
⊢ HPow.hPow (α := ℕ) 2 (n + 1) = HPow.hPow (α := ℕ) 2 n + HPow.hPow (α := ℕ) 2 n

Tactic:
rw [pow_succ, mul_two]

Premises used: pow_succ, mul_two
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | Even n ∧ n.Deficient} (HPow.hPow (α := ℕ) 2 (n + 1))

Tactic:
exact ⟨⟨2 ^ n, by rw [pow_succ, mul_two]⟩, prime_two.deficient_pow⟩
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
⊢ n ≤ HPow.hPow (α := ℕ) 2 n

Tactic:
Nat.le_of_lt n.lt_two_pow_self

Premises used: Nat.le_of_lt, Nat.lt_two_pow_self
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
⊢ HPow.hPow (α := ℕ) 2 n < HPow.hPow (α := ℕ) 2 (n + 1)

Tactic:
(Nat.pow_lt_pow_iff_right (Nat.one_lt_two)).mpr (lt_add_one n)

Premises used: Iff.mpr, Nat.one_lt_two, lt_add_one, Nat.pow_lt_pow_iff_right
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
⊢ n < HPow.hPow (α := ℕ) 2 (n + 1)

Tactic:
calc
      n ≤ 2 ^ n := Nat.le_of_lt n.lt_two_pow_self
      _ < 2 ^ (n + 1) := (Nat.pow_lt_pow_iff_right (Nat.one_lt_two)).mpr (lt_add_one n)

Premises used: Iff.mpr, Nat.one_lt_two, lt_add_one, Nat.le_of_lt, HAdd.hAdd, Nat.lt_two_pow_self, Nat.pow_lt_pow_iff_right, OfNat.ofNat
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
rw : ∀ (a : ℕ), ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Odd n ∧ n.Deficient} b ∧ a < b
⊢ Set.Infinite (α := ℕ) {n : ℕ | Odd n ∧ n.Deficient}

Tactic:
rw [Set.infinite_iff_exists_gt]

Premises used: Set.infinite_iff_exists_gt
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
obtain :
  ∀ (p : ℕ),
    max (n + 1) 3 ≤ p → ∀ (h2 : Prime p), ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Odd n ∧ n.Deficient} b ∧ n < b
⊢ ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Odd n ∧ n.Deficient} b ∧ n < b

Tactic:
obtain ⟨p, ⟨_, h2⟩⟩ := exists_infinite_primes (max (n + 1) 3)

Premises used: HAdd.hAdd, Max.max, OfNat.ofNat, Nat.exists_infinite_primes
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n p : ℕ
left : max (n + 1) 3 ≤ p
h2 : Prime p
⊢ 2 < p

Tactic:
grind
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n p : ℕ
left : max (n + 1) 3 ≤ p
h2 : Prime p
⊢ n < p

Tactic:
grind
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n p : ℕ
left : max (n + 1) 3 ≤ p
h2 : Prime p
⊢ ∃ (b : ℕ), Membership.mem (γ := Set ℕ) {n : ℕ | Odd n ∧ n.Deficient} b ∧ n < b

Tactic:
exact ⟨p, Set.mem_setOf.mpr ⟨Prime.odd_of_ne_two h2 (Ne.symm (ne_of_lt (by grind))),
    Prime.deficient h2⟩, by grind⟩
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
⊢ n.Abundant ↔ 2 * n < ∑ i ∈ n.divisors, i

Tactic:
grind [Abundant, sum_divisors_eq_sum_properDivisors_add_self]

Premises used: Nat.sum_divisors_eq_sum_properDivisors_add_self, Nat.Abundant
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
pos : ∀ (h : n = 0), n.Abundant ↔ 2 < n.abundancyIndex
neg : ∀ (h : ¬n = 0), n.Abundant ↔ 2 < n.abundancyIndex
⊢ n.Abundant ↔ 2 < n.abundancyIndex

Tactic:
by_cases h : n = 0
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
h : n = 0
⊢ n.Abundant ↔ 2 < n.abundancyIndex

Tactic:
simp [h, Abundant, abundancyIndex]

Premises used: Nat.Abundant, Nat.abundancyIndex
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
h : ¬n = 0
⊢ LT.lt (α := ℚ) 0 (↑n : ℚ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
h : ¬n = 0
neg : 2 * n < ∑ i ∈ n.divisors, i ↔ HMul.hMul (α := ℚ) 2 (↑n : ℚ) < (↑(∑ i ∈ n.divisors, i) : ℚ)
⊢ n.Abundant ↔ 2 < n.abundancyIndex

Tactic:
rw [abundant_iff_sum_divisors, abundancyIndex, lt_div_iff₀ (by positivity)]

Premises used: lt_div_iff₀, Nat.abundancyIndex, Nat.abundant_iff_sum_divisors
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n : ℕ
h : ¬n = 0
neg neg₁ neg₂ neg₃ : 2 * n < ∑ i ∈ n.divisors, i ↔ 2 * n < ∑ i ∈ n.divisors, i
⊢ 2 * n < ∑ i ∈ n.divisors, i ↔ HMul.hMul (α := ℚ) 2 (↑n : ℚ) < (↑(∑ i ∈ n.divisors, i) : ℚ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
hn : n ≠ 0
hd : m ∣ n
obtain : ∀ (k : ℕ) (hk : n = m * k), m.abundancyIndex ≤ n.abundancyIndex
⊢ m.abundancyIndex ≤ n.abundancyIndex

Tactic:
obtain ⟨k, hk⟩ := hd
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
⊢ k ≠ 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
⊢ k ≠ 0

Tactic:
have hk0 : k ≠ 0 := by grind
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
rw :
  HDiv.hDiv (α := ℚ) (↑(∑ i ∈ m.divisors, i) : ℚ) (↑m : ℚ) ≤
    HDiv.hDiv (α := ℚ) (↑(∑ i ∈ (m * k).divisors, i) : ℚ) (↑k : ℚ) / (↑m : ℚ)
⊢ m.abundancyIndex ≤ n.abundancyIndex

Tactic:
rw [abundancyIndex, abundancyIndex, hk, cast_mul, div_mul_eq_div_div_swap]

Premises used: div_mul_eq_div_div_swap, Nat.cast_mul, Nat.abundancyIndex
-- Module: Mathlib.NumberTheory.FactorisationProperties
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 : ℚ)

Tactic:
div_le_div_of_nonneg_right ?_ m.cast_nonneg

Premises used: div_le_div_of_nonneg_right, Nat.cast_nonneg
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
refine : (↑(∑ i ∈ m.divisors, i) : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑(∑ i ∈ (m * k).divisors, i) : ℚ) (↑k : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑(∑ i ∈ m.divisors, i) : ℚ) (↑m : ℚ) ≤
    HDiv.hDiv (α := ℚ) (↑(∑ i ∈ (m * k).divisors, i) : ℚ) (↑k : ℚ) / (↑m : ℚ)

Tactic:
refine div_le_div_of_nonneg_right ?_ m.cast_nonneg

Premises used: div_le_div_of_nonneg_right
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ LT.lt (α := ℚ) 0 (↑k : ℚ)

Tactic:
grind [cast_pos]

Premises used: Nat.cast_pos
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
rw : LE.le (α := ℕ) (∑ i ∈ m.divisors, i * k) (∑ i ∈ (m * k).divisors, i)
⊢ (↑(∑ i ∈ m.divisors, i) : ℚ) ≤ HDiv.hDiv (α := ℚ) (↑(∑ i ∈ (m * k).divisors, i) : ℚ) (↑k : ℚ)

Tactic:
rw [le_div_iff₀ (by grind [cast_pos]), ← cast_mul, cast_le, sum_mul]

Premises used: Nat.cast_mul, Nat.cast_le, le_div_iff₀, Finset.sum_mul
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ image (fun (a : ℕ) ↦ a * k) m.divisors ⊆ (m * k).divisors

Tactic:
grind [mul_dvd_mul_iff_right hk0]

Premises used: mul_dvd_mul_iff_right
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ LE.le (α := ℕ) (∑ i ∈ m.divisors, i * k) (∑ i ∈ (m * k).divisors, i)

Tactic:
exact (sum_image (f := fun i ↦ i) (mul_left_injective₀ hk0).injOn).symm.trans_le
    (sum_le_sum_of_subset (by grind [mul_dvd_mul_iff_right hk0]))

Premises used: Function.Injective.injOn, mul_left_injective₀, Eq.trans_le, Finset.sum_le_sum_of_subset, Finset.sum_image, Eq.symm
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
h : m.Abundant
hd : m ∣ n
hn : n ≠ 0
⊢ m.abundancyIndex ≤ n.abundancyIndex

Tactic:
have := abundancyIndex_le_of_dvd hn hd
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
h : m.Abundant
hd : m ∣ n
hn : n ≠ 0
this : m.abundancyIndex ≤ n.abundancyIndex
⊢ n.Abundant

Tactic:
grind [abundant_iff_two_lt_abundancyIndex]

Premises used: Nat.abundant_iff_two_lt_abundancyIndex
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
h : n.Abundant
hm : m ≠ 0
⊢ n ≠ 0

Tactic:
grind [not_abundant_zero]

Premises used: Nat.not_abundant_zero
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
h : n.Abundant
hm : m ≠ 0
⊢ n ≠ 0

Tactic:
have hn : n ≠ 0 := by grind [not_abundant_zero]
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
h : n.Abundant
hm : m ≠ 0
hn : n ≠ 0
⊢ m * n ≠ 0

Tactic:
have hmn : m * n ≠ 0 := mul_ne_zero hm hn
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
h : n.Abundant
hm : m ≠ 0
hn : n ≠ 0
hmn : m * n ≠ 0
⊢ (m * n).Abundant

Tactic:
Abundant.of_dvd h (Nat.dvd_mul_left n m) hmn

Premises used: Nat.Abundant.of_dvd, Nat.dvd_mul_left
-- Module: Mathlib.NumberTheory.FactorisationProperties
Goal:
n m : ℕ
h : n.Abundant
hm : m ≠ 0
hn : n ≠ 0
hmn : m * n ≠ 0
⊢ (m * n).Abundant

Tactic:
exact Abundant.of_dvd h (Nat.dvd_mul_left n m) hmn

Premises used: Nat.Abundant.of_dvd, Nat.dvd_mul_left