Theorem: C05S03.aux (MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean)

State before:
m n : ℕ
h₀ : m ∣ n
h₁ : 2 ≤ m
h₂ : m < n
⊢ n / m ∣ n ∧ n / m < n
Tactic:
constructor
State after:
case left
m n : ℕ
h₀ : m ∣ n
h₁ : 2 ≤ m
h₂ : m < n
⊢ n / m ∣ n

case right
m n : ℕ
h₀ : m ∣ n
h₁ : 2 ≤ m
h₂ : m < n
⊢ n / m < n

State before:
case right
m n : ℕ
h₀ : m ∣ n
h₁ : 2 ≤ m
h₂ : m < n
⊢ n / m < n
Tactic:
exact Nat.div_lt_self (lt_of_le_of_lt (zero_le _) h₂) h₁
State after:
no goals

State before:
case left
m n : ℕ
h₀ : m ∣ n
h₁ : 2 ≤ m
h₂ : m < n
⊢ n / m ∣ n
Tactic:
exact Nat.div_dvd_of_dvd h₀
State after:
no goals