case pos
n b : ℕ
h : ProbablePrime n b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : 2 ≤ n
⊢ Nat.coprime n b

case neg
n b : ℕ
h : ProbablePrime n b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ Nat.coprime n b
n b : ℕ
h : ProbablePrime n b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
⊢ Nat.coprime n b
by_cases h₃ : 2 ≤ n
case pos.H
n b : ℕ
h : ProbablePrime n b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : 2 ≤ n
⊢ ∀ (k : ℕ), Nat.Prime k → k ∣ n → ¬k ∣ b
case pos
n b : ℕ
h : ProbablePrime n b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : 2 ≤ n
⊢ Nat.coprime n b
apply Nat.coprime_of_dvd
case pos.H.intro.intro
k : ℕ
hk : Nat.Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : ProbablePrime (k * m) (k * j)
⊢ False
case pos.H
n b : ℕ
h : ProbablePrime n b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : 2 ≤ n
⊢ ∀ (k : ℕ), Nat.Prime k → k ∣ n → ¬k ∣ b
rintro k hk ⟨m, rfl⟩ ⟨j, rfl⟩
case pos.H.intro.intro
k : ℕ
hk : Nat.Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : ProbablePrime (k * m) (k * j)
⊢ k ∣ 1
case pos.H.intro.intro
k : ℕ
hk : Nat.Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : ProbablePrime (k * m) (k * j)
⊢ False
apply Nat.Prime.not_dvd_one hk
case pos.H.intro.intro
k : ℕ
hk : Nat.Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ 1
case pos.H.intro.intro
k : ℕ
hk : Nat.Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : ProbablePrime (k * m) (k * j)
⊢ k ∣ 1
replace h := dvd_of_mul_right_dvd h
case pos.H.intro.intro
k : ℕ
hk : Nat.Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ (k * j) ^ (k * m - 1)
case pos.H.intro.intro
k : ℕ
hk : Nat.Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ 1
rw [Nat.dvd_add_iff_right h, Nat.sub_add_cancel (Nat.one_le_pow _ _ h₂)]
case pos.H.intro.intro
k : ℕ
hk : Nat.Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k * m - 1 ≠ 0
case pos.H.intro.intro
k : ℕ
hk : Nat.Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ (k * j) ^ (k * m - 1)
refine' dvd_of_mul_right_dvd (dvd_pow_self (k * j) _)
no goals
case pos.H.intro.intro
k : ℕ
hk : Nat.Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k * m - 1 ≠ 0
linarith [tsub_pos_of_lt (one_lt_two.trans_le h₃)]
case neg
n b : ℕ
h : ProbablePrime n b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ Nat.coprime 1 b
case neg
n b : ℕ
h : ProbablePrime n b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ Nat.coprime n b
rw [show n = 1 by linarith]
no goals
case neg
n b : ℕ
h : ProbablePrime n b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ Nat.coprime 1 b
norm_num
no goals
n b : ℕ
h : ProbablePrime n b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ n = 1
linarith