Theorem: infinity_of_primes₂ (FormalBook/Chapter_01.lean)

State before:
k n : ℕ
h : k < n
⊢ (F n).Coprime (F k)
Tactic:
let m := (F n).gcd (F k)
State after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
⊢ (F n).Coprime (F k)

State before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
⊢ (F n).Coprime (F k)
Tactic:
have h_n : m ∣ F n := (F n).gcd_dvd_left (F k)
State after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
⊢ (F n).Coprime (F k)

State before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
⊢ (F n).Coprime (F k)
Tactic:
have h_k : m ∣ F k := (F n).gcd_dvd_right (F k)
State after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
⊢ (F n).Coprime (F k)

State before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
⊢ (F n).Coprime (F k)
Tactic:
have h_m : m ∣ 2 :=  by
  have h_m_prod : m ∣ (∏ k in range n, F k) :=
    dvd_trans h_k (dvd_prod_of_mem F (mem_range.mpr h))
  have h_prod : (∏ k in range n, F k) + 2 = F n := by
    rw [fermat_product, Nat.sub_add_cancel]
    refine' le_of_lt _
    simp [fermat_bounded]
  refine' (Nat.dvd_add_right h_m_prod).mp _
  rw [h_prod]
  exact h_n
State after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
⊢ (F n).Coprime (F k)

State before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
⊢ (F n).Coprime (F k)
Tactic:
cases' (dvd_prime prime_two).mp h_m with h_one h_two
State after:
case inl
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_one : m = 1
⊢ (F n).Coprime (F k)

case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
⊢ (F n).Coprime (F k)

State before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
⊢ m ∣ 2
Tactic:
have h_m_prod : m ∣ (∏ k in range n, F k) :=
  dvd_trans h_k (dvd_prod_of_mem F (mem_range.mpr h))
State after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
⊢ m ∣ 2

State before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
⊢ m ∣ 2
Tactic:
have h_prod : (∏ k in range n, F k) + 2 = F n := by
  rw [fermat_product, Nat.sub_add_cancel]
  refine' le_of_lt _
  simp [fermat_bounded]
State after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
h_prod : ∏ k ∈ range n, F k + 2 = F n
⊢ m ∣ 2

State before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
h_prod : ∏ k ∈ range n, F k + 2 = F n
⊢ m ∣ 2
Tactic:
refine' (Nat.dvd_add_right h_m_prod).mp _
State after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
h_prod : ∏ k ∈ range n, F k + 2 = F n
⊢ m ∣ ∏ k ∈ range n, F k + 2

State before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
h_prod : ∏ k ∈ range n, F k + 2 = F n
⊢ m ∣ ∏ k ∈ range n, F k + 2
Tactic:
rw [h_prod]
State after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
h_prod : ∏ k ∈ range n, F k + 2 = F n
⊢ m ∣ F n

State before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
h_prod : ∏ k ∈ range n, F k + 2 = F n
⊢ m ∣ F n
Tactic:
exact h_n
State after:
no goals

State before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
⊢ ∏ k ∈ range n, F k + 2 = F n
Tactic:
rw [fermat_product, Nat.sub_add_cancel]
State after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
⊢ 2 ≤ F n

State before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
⊢ 2 ≤ F n
Tactic:
refine' le_of_lt _
State after:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
⊢ 2 < F n

State before:
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
⊢ 2 < F n
Tactic:
simp [fermat_bounded]
State after:
no goals

State before:
case inl
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_one : m = 1
⊢ (F n).Coprime (F k)
Tactic:
exact h_one
State after:
no goals

State before:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
⊢ (F n).Coprime (F k)
Tactic:
by_contra
State after:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
x✝ : ¬(F n).Coprime (F k)
⊢ False

State before:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
x✝ : ¬(F n).Coprime (F k)
⊢ False
Tactic:
rw [h_two] at h_n
State after:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : 2 ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
x✝ : ¬(F n).Coprime (F k)
⊢ False

State before:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : 2 ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
x✝ : ¬(F n).Coprime (F k)
⊢ False
Tactic:
have h_even : Even (F n) := even_iff_two_dvd.mpr h_n
State after:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : 2 ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
x✝ : ¬(F n).Coprime (F k)
h_even : Even (F n)
⊢ False

State before:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : 2 ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
x✝ : ¬(F n).Coprime (F k)
h_even : Even (F n)
⊢ False
Tactic:
have h_odd : Odd (F n) := fermat_odd
State after:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : 2 ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
x✝ : ¬(F n).Coprime (F k)
h_even : Even (F n)
h_odd : Odd (F n)
⊢ False

State before:
case inr
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : 2 ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
h_two : m = 2
x✝ : ¬(F n).Coprime (F k)
h_even : Even (F n)
h_odd : Odd (F n)
⊢ False
Tactic:
exact (odd_iff_not_even.mp h_odd) h_even
State after:
no goals