Theorem: r3_not_weak_order (meetings/ex6.lean)

State before:
⊢ ¬WeakOrder R3
Tactic:
intro hwo
State after:
hwo : WeakOrder R3
⊢ False

State before:
hwo : WeakOrder R3
⊢ False
Tactic:
simp_rw [WeakOrder, PartialOrder', R3] at hwo
State after:
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
⊢ False

State before:
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
⊢ False
Tactic:
have hf := hwo.2 2 3
State after:
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
hf : 2 ∣ 3 ∨ 3 ∣ 2
⊢ False

State before:
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
hf : 2 ∣ 3 ∨ 3 ∣ 2
⊢ False
Tactic:
rcases hf with (hdvd3 | hdvd2)
State after:
case inl
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
hdvd3 : 2 ∣ 3
⊢ False

case inr
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
hdvd2 : 3 ∣ 2
⊢ False

State before:
case inl
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
hdvd3 : 2 ∣ 3
⊢ False
Tactic:
rw [dvd_def] at hdvd3
State after:
case inl
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
hdvd3 : ∃ c, 3 = 2 * c
⊢ False

State before:
case inl
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
hdvd3 : ∃ c, 3 = 2 * c
⊢ False
Tactic:
rcases hdvd3 with ⟨c, hc⟩
State after:
case inl.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : 3 = 2 * c
⊢ False

State before:
case inl.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : 3 = 2 * c
⊢ False
Tactic:
rw [Subtype.ext_iff] at hc
State after:
case inl.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : ↑3 = ↑(2 * c)
⊢ False

State before:
case inl.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : ↑3 = ↑(2 * c)
⊢ False
Tactic:
have hdvd : ∃ c : ℕ, (3 : ℕ) = 2 * c := ⟨c.val, hc⟩
State after:
case inl.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : ↑3 = ↑(2 * c)
hdvd : ∃ c, 3 = 2 * c
⊢ False

State before:
case inl.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : ↑3 = ↑(2 * c)
hdvd : ∃ c, 3 = 2 * c
⊢ False
Tactic:
rw [←dvd_def] at hdvd
State after:
case inl.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : ↑3 = ↑(2 * c)
hdvd : 2 ∣ 3
⊢ False

State before:
case inl.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : ↑3 = ↑(2 * c)
hdvd : 2 ∣ 3
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case inr
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
hdvd2 : 3 ∣ 2
⊢ False
Tactic:
rw [dvd_def] at hdvd2
State after:
case inr
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
hdvd2 : ∃ c, 2 = 3 * c
⊢ False

State before:
case inr
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
hdvd2 : ∃ c, 2 = 3 * c
⊢ False
Tactic:
rcases hdvd2 with ⟨c, hc⟩
State after:
case inr.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : 2 = 3 * c
⊢ False

State before:
case inr.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : 2 = 3 * c
⊢ False
Tactic:
rw [Subtype.ext_iff] at hc
State after:
case inr.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : ↑2 = ↑(3 * c)
⊢ False

State before:
case inr.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : ↑2 = ↑(3 * c)
⊢ False
Tactic:
have hdvd : ∃ c : ℕ, (2 : ℕ) = 3 * c := ⟨c.val, hc⟩
State after:
case inr.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : ↑2 = ↑(3 * c)
hdvd : ∃ c, 2 = 3 * c
⊢ False

State before:
case inr.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : ↑2 = ↑(3 * c)
hdvd : ∃ c, 2 = 3 * c
⊢ False
Tactic:
rw [←dvd_def] at hdvd
State after:
case inr.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : ↑2 = ↑(3 * c)
hdvd : 3 ∣ 2
⊢ False

State before:
case inr.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : ↑2 = ↑(3 * c)
hdvd : 3 ∣ 2
⊢ False
Tactic:
contradiction
State after:
no goals