case pos
n : ℕ
n1 : n ≠ 1
n0 : n = 0
⊢ Nat.minFacProp n (minFac n)

case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
⊢ Nat.minFacProp n (minFac n)
n : ℕ
n1 : n ≠ 1
⊢ Nat.minFacProp n (minFac n)
by_cases n0 : n = 0
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
⊢ Nat.minFacProp n (minFac n)
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
⊢ Nat.minFacProp n (minFac n)
have n2 : 2 ≤ n := by
  revert n0 n1
  rcases n with (_ | _ | _) <;> simp [succ_le_succ]
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
⊢ Nat.minFacProp n (if 2 ∣ n then 2 else minFacAux n 3)
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
⊢ Nat.minFacProp n (minFac n)
simp [minFac_eq]
case pos
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ Nat.minFacProp n 2

case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ Nat.minFacProp n (minFacAux n 3)
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
⊢ Nat.minFacProp n (if 2 ∣ n then 2 else minFacAux n 3)
by_cases d2 : 2 ∣ n <;> simp [d2]
no goals
case pos
n : ℕ
n1 : n ≠ 1
n0 : n = 0
⊢ Nat.minFacProp n (minFac n)
simp [n0, minFacProp, GE.ge]
n : ℕ
⊢ n ≠ 1 → ¬n = 0 → 2 ≤ n
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
⊢ 2 ≤ n
revert n0 n1
no goals
n : ℕ
⊢ n ≠ 1 → ¬n = 0 → 2 ≤ n
rcases n with (_ | _ | _) <;> simp [succ_le_succ]
no goals
case pos
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ Nat.minFacProp n 2
exact ⟨le_rfl, d2, fun k k2 _ => k2⟩
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
⊢ 2 = m → 2 ∣ n
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ Nat.minFacProp n (minFacAux n 3)
refine'
  minFacAux_has_prop n2 3 0 rfl fun m m2 d => (Nat.eq_or_lt_of_le m2).resolve_left (mt _ d2)
no goals
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
⊢ 2 = m → 2 ∣ n
exact fun e => e.symm ▸ d