Theorem: exercise4_4 (LeanCourse/Assignments/Solutions/Solutions4.lean)

State before:
n : ℕ
⊢ ¬Nat.Prime n ↔ n = 0 ∨ n = 1 ∨ ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ n = a * b
Tactic:
rw [← or_assoc, ← Nat.le_one_iff_eq_zero_or_eq_one, ← not_lt, ← imp_iff_not_or, Nat.prime_def_lt']
State after:
n : ℕ
⊢ ¬(2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m < n → ¬m ∣ n) ↔ 1 < n → ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ n = a * b

State before:
n : ℕ
⊢ ¬(2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m < n → ¬m ∣ n) ↔ 1 < n → ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ n = a * b
Tactic:
push_neg
State after:
n : ℕ
⊢ (2 ≤ n → ∃ m, 2 ≤ m ∧ m < n ∧ m ∣ n) ↔ 1 < n → ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ n = a * b

State before:
n : ℕ
⊢ (2 ≤ n → ∃ m, 2 ≤ m ∧ m < n ∧ m ∣ n) ↔ 1 < n → ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ n = a * b
Tactic:
simp
State after:
n : ℕ
⊢ (2 ≤ n → ∃ m, 2 ≤ m ∧ m < n ∧ m ∣ n) ↔ 1 < n → ∃ a, 2 ≤ a ∧ ∃ x, 2 ≤ x ∧ n = a * x

State before:
n : ℕ
⊢ (2 ≤ n → ∃ m, 2 ≤ m ∧ m < n ∧ m ∣ n) ↔ 1 < n → ∃ a, 2 ≤ a ∧ ∃ x, 2 ≤ x ∧ n = a * x
Tactic:
apply imp_congr
State after:
case h₁
n : ℕ
⊢ 2 ≤ n ↔ 1 < n

case h₂
n : ℕ
⊢ (∃ m, 2 ≤ m ∧ m < n ∧ m ∣ n) ↔ ∃ a, 2 ≤ a ∧ ∃ x, 2 ≤ x ∧ n = a * x

State before:
case h₂
n : ℕ
⊢ (∃ m, 2 ≤ m ∧ m < n ∧ m ∣ n) ↔ ∃ a, 2 ≤ a ∧ ∃ x, 2 ≤ x ∧ n = a * x
Tactic:
apply exists_congr
State after:
case h₂.h
n : ℕ
⊢ ∀ (a : ℕ), 2 ≤ a ∧ a < n ∧ a ∣ n ↔ 2 ≤ a ∧ ∃ x, 2 ≤ x ∧ n = a * x

State before:
case h₂.h
n : ℕ
⊢ ∀ (a : ℕ), 2 ≤ a ∧ a < n ∧ a ∣ n ↔ 2 ≤ a ∧ ∃ x, 2 ≤ x ∧ n = a * x
Tactic:
intro k
State after:
case h₂.h
n k : ℕ
⊢ 2 ≤ k ∧ k < n ∧ k ∣ n ↔ 2 ≤ k ∧ ∃ x, 2 ≤ x ∧ n = k * x

State before:
case h₂.h
n k : ℕ
⊢ 2 ≤ k ∧ k < n ∧ k ∣ n ↔ 2 ≤ k ∧ ∃ x, 2 ≤ x ∧ n = k * x
Tactic:
apply and_congr_right
State after:
case h₂.h.h
n k : ℕ
⊢ 2 ≤ k → (k < n ∧ k ∣ n ↔ ∃ x, 2 ≤ x ∧ n = k * x)

State before:
case h₂.h.h
n k : ℕ
⊢ 2 ≤ k → (k < n ∧ k ∣ n ↔ ∃ x, 2 ≤ x ∧ n = k * x)
Tactic:
intro hk
State after:
case h₂.h.h
n k : ℕ
hk : 2 ≤ k
⊢ k < n ∧ k ∣ n ↔ ∃ x, 2 ≤ x ∧ n = k * x

State before:
case h₂.h.h
n k : ℕ
hk : 2 ≤ k
⊢ k < n ∧ k ∣ n ↔ ∃ x, 2 ≤ x ∧ n = k * x
Tactic:
rw [dvd_def, ← exists_and_left]
State after:
case h₂.h.h
n k : ℕ
hk : 2 ≤ k
⊢ (∃ x, k < n ∧ n = k * x) ↔ ∃ x, 2 ≤ x ∧ n = k * x

State before:
case h₂.h.h
n k : ℕ
hk : 2 ≤ k
⊢ (∃ x, k < n ∧ n = k * x) ↔ ∃ x, 2 ≤ x ∧ n = k * x
Tactic:
apply exists_congr
State after:
case h₂.h.h.h
n k : ℕ
hk : 2 ≤ k
⊢ ∀ (a : ℕ), k < n ∧ n = k * a ↔ 2 ≤ a ∧ n = k * a

State before:
case h₂.h.h.h
n k : ℕ
hk : 2 ≤ k
⊢ ∀ (a : ℕ), k < n ∧ n = k * a ↔ 2 ≤ a ∧ n = k * a
Tactic:
intro l
State after:
case h₂.h.h.h
n k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ k < n ∧ n = k * l ↔ 2 ≤ l ∧ n = k * l

State before:
case h₂.h.h.h
n k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ k < n ∧ n = k * l ↔ 2 ≤ l ∧ n = k * l
Tactic:
apply and_congr_left
State after:
case h₂.h.h.h.h
n k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ n = k * l → (k < n ↔ 2 ≤ l)

State before:
case h₂.h.h.h.h
n k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ n = k * l → (k < n ↔ 2 ≤ l)
Tactic:
intro h
State after:
case h₂.h.h.h.h
n k : ℕ
hk : 2 ≤ k
l : ℕ
h : n = k * l
⊢ k < n ↔ 2 ≤ l

State before:
case h₂.h.h.h.h
n k : ℕ
hk : 2 ≤ k
l : ℕ
h : n = k * l
⊢ k < n ↔ 2 ≤ l
Tactic:
subst h
State after:
case h₂.h.h.h.h
k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ k < k * l ↔ 2 ≤ l

State before:
case h₂.h.h.h.h
k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ k < k * l ↔ 2 ≤ l
Tactic:
rw [succ_le]
State after:
case h₂.h.h.h.h
k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ k < k * l ↔ 1 < l

State before:
case h₂.h.h.h.h
k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ k < k * l ↔ 1 < l
Tactic:
apply lt_mul_iff_one_lt_right
State after:
case h₂.h.h.h.h.a0
k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ 0 < k

State before:
case h₂.h.h.h.h.a0
k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ 0 < k
Tactic:
linarith
State after:
no goals

State before:
case h₁
n : ℕ
⊢ 2 ≤ n ↔ 1 < n
Tactic:
rw?
State after:
no goals