-- Mathlib/NumberTheory/MaricaSchoenheim.lean
/-- The special case of Graham's conjecture where all numbers are squarefree. -/
lemma grahamConjecture_of_squarefree {n : ℕ} (f : ℕ → ℕ) (hf' : ∀ k < n, Squarefree (f k)) :
    GrahamConjecture n f

Proof state:
case calc_3
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
a : ℕ
ha : a < n
b : ℕ
hb : b < n
c : ℕ
hc : c < n
d : ℕ
hd : d < n
⊢ ∏ p ∈ (f a).primeFactors \ (f b).primeFactors, p = ∏ p ∈ (f c).primeFactors \ (f d).primeFactors, p →
    (f a).primeFactors \ (f b).primeFactors = (f c).primeFactors \ (f d).primeFactors

Tactic:
rw [← primeFactors_div_gcd (hf' _ ha) (hf' _ hb).ne_zero, ← primeFactors_div_gcd
  (hf' _ hc) (hf' _ hd).ne_zero, prod_primeFactors_of_squarefree (hf'' _ ha _),
  prod_primeFactors_of_squarefree (hf'' _ hc _)]

Result:
case calc_3
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
a : ℕ
ha : a < n
b : ℕ
hb : b < n
c : ℕ
hc : c < n
d : ℕ
hd : d < n
⊢ f a / (f a).gcd (f b) = f c / (f c).gcd (f d) →
    (f a / (f a).gcd (f b)).primeFactors = (f c / (f c).gcd (f d)).primeFactors

Proof state:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
⊢ ∃ i < n, ∃ j < n, (f i).gcd (f j) * n ≤ f i

Tactic:
by_contra!

Result:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
⊢ False

Proof state:
case calc_1
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ n = #𝒜

Tactic:
rw [Finset.card_image_of_injOn, card_Iio]

Result:
case calc_1
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ Set.InjOn (fun n => (f n).primeFactors) ↑(Iio n)

Proof state:
case calc_3
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ Set.InjOn (fun s => ∏ p ∈ s, p) ↑(𝒜 \\ 𝒜)

Tactic:
simp only [𝒜, Set.InjOn, mem_coe, forall_mem_diffs, forall_mem_image, mem_Ioo, mem_Iio]

Result:
case calc_3
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ ∀ ⦃x : ℕ⦄,
    x < n →
      ∀ ⦃x_1 : ℕ⦄,
        x_1 < n →
          ∀ ⦃x_2 : ℕ⦄,
            x_2 < n →
              ∀ ⦃x_3 : ℕ⦄,
                x_3 < n →
                  ∏ p ∈ (f x).primeFactors \ (f x_1).primeFactors, p =
                      ∏ p ∈ (f x_2).primeFactors \ (f x_3).primeFactors, p →
                    (f x).primeFactors \ (f x_1).primeFactors = (f x_2).primeFactors \ (f x_3).primeFactors

Proof state:
case calc_2
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ ∀ ⦃x : ℕ⦄,
    x < n →
      ∀ ⦃x_1 : ℕ⦄,
        x_1 < n →
          0 < ∏ p ∈ (f x).primeFactors \ (f x_1).primeFactors, p ∧
            ∏ p ∈ (f x).primeFactors \ (f x_1).primeFactors, p < n

Tactic:
rintro i hi j hj

Result:
case calc_2
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
i : ℕ
hi : i < n
j : ℕ
hj : j < n
⊢ 0 < ∏ p ∈ (f i).primeFactors \ (f j).primeFactors, p ∧ ∏ p ∈ (f i).primeFactors \ (f j).primeFactors, p < n

Proof state:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
⊢ False

Tactic:
set 𝒜 := (Iio n).image fun n ↦ primeFactors (f n)

Result:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)
⊢ False

Proof state:
case calc_3
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ ∀ ⦃x : ℕ⦄,
    x < n →
      ∀ ⦃x_1 : ℕ⦄,
        x_1 < n →
          ∀ ⦃x_2 : ℕ⦄,
            x_2 < n →
              ∀ ⦃x_3 : ℕ⦄,
                x_3 < n →
                  ∏ p ∈ (f x).primeFactors \ (f x_1).primeFactors, p =
                      ∏ p ∈ (f x_2).primeFactors \ (f x_3).primeFactors, p →
                    (f x).primeFactors \ (f x_1).primeFactors = (f x_2).primeFactors \ (f x_3).primeFactors

Tactic:
rintro a ha b hb c hc d hd

Result:
case calc_3
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
a : ℕ
ha : a < n
b : ℕ
hb : b < n
c : ℕ
hc : c < n
d : ℕ
hd : d < n
⊢ ∏ p ∈ (f a).primeFactors \ (f b).primeFactors, p = ∏ p ∈ (f c).primeFactors \ (f d).primeFactors, p →
    (f a).primeFactors \ (f b).primeFactors = (f c).primeFactors \ (f d).primeFactors

Proof state:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n => (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ #(Ioo 0 n) = n - 1

Tactic:
rw [card_Ioo, tsub_zero]

Result:
no goals