Theorem: r4_weak_order (meetings/ex6.lean)

State before:
⊢ WeakOrder R4
Tactic:
simp only [WeakOrder, PartialOrder', R4]
State after:
⊢ (∀ (a b c : ↑VeryDiv), (↑a ∣ ↑b → ↑b ∣ ↑c → ↑a ∣ ↑c) ∧ (↑a ∣ ↑b → ↑b ∣ ↑a → a = b)) ∧
    ∀ (a b : ↑VeryDiv), ↑a ∣ ↑b ∨ ↑b ∣ ↑a

State before:
⊢ (∀ (a b c : ↑VeryDiv), (↑a ∣ ↑b → ↑b ∣ ↑c → ↑a ∣ ↑c) ∧ (↑a ∣ ↑b → ↑b ∣ ↑a → a = b)) ∧
    ∀ (a b : ↑VeryDiv), ↑a ∣ ↑b ∨ ↑b ∣ ↑a
Tactic:
constructor
State after:
case left

⊢ ∀ (a b c : ↑VeryDiv), (↑a ∣ ↑b → ↑b ∣ ↑c → ↑a ∣ ↑c) ∧ (↑a ∣ ↑b → ↑b ∣ ↑a → a = b)

case right

⊢ ∀ (a b : ↑VeryDiv), ↑a ∣ ↑b ∨ ↑b ∣ ↑a

State before:
case left

⊢ ∀ (a b c : ↑VeryDiv), (↑a ∣ ↑b → ↑b ∣ ↑c → ↑a ∣ ↑c) ∧ (↑a ∣ ↑b → ↑b ∣ ↑a → a = b)
Tactic:
intros a b c
State after:
case left
a b c : ↑VeryDiv
⊢ (↑a ∣ ↑b → ↑b ∣ ↑c → ↑a ∣ ↑c) ∧ (↑a ∣ ↑b → ↑b ∣ ↑a → a = b)

State before:
case left
a b c : ↑VeryDiv
⊢ (↑a ∣ ↑b → ↑b ∣ ↑c → ↑a ∣ ↑c) ∧ (↑a ∣ ↑b → ↑b ∣ ↑a → a = b)
Tactic:
constructor
State after:
case left.left
a b c : ↑VeryDiv
⊢ ↑a ∣ ↑b → ↑b ∣ ↑c → ↑a ∣ ↑c

case left.right
a b c : ↑VeryDiv
⊢ ↑a ∣ ↑b → ↑b ∣ ↑a → a = b

State before:
case left.left
a b c : ↑VeryDiv
⊢ ↑a ∣ ↑b → ↑b ∣ ↑c → ↑a ∣ ↑c
Tactic:
exact Nat.dvd_trans
State after:
no goals

State before:
case left.right
a b c : ↑VeryDiv
⊢ ↑a ∣ ↑b → ↑b ∣ ↑a → a = b
Tactic:
simp_rw [←SetCoe.ext_iff]
State after:
case left.right
a b c : ↑VeryDiv
⊢ ↑a ∣ ↑b → ↑b ∣ ↑a → ↑a = ↑b

State before:
case left.right
a b c : ↑VeryDiv
⊢ ↑a ∣ ↑b → ↑b ∣ ↑a → ↑a = ↑b
Tactic:
exact Nat.dvd_antisymm
State after:
no goals

State before:
case right

⊢ ∀ (a b : ↑VeryDiv), ↑a ∣ ↑b ∨ ↑b ∣ ↑a
Tactic:
intros a b
State after:
case right
a b : ↑VeryDiv
⊢ ↑a ∣ ↑b ∨ ↑b ∣ ↑a

State before:
case right
a b : ↑VeryDiv
⊢ ↑a ∣ ↑b ∨ ↑b ∣ ↑a
Tactic:
rcases a with ⟨a, ha⟩
State after:
case right.mk
b : ↑VeryDiv
a : ℕ
ha : a ∈ VeryDiv
⊢ ↑{ val := a, property := ha } ∣ ↑b ∨ ↑b ∣ ↑{ val := a, property := ha }

State before:
case right.mk
b : ↑VeryDiv
a : ℕ
ha : a ∈ VeryDiv
⊢ ↑{ val := a, property := ha } ∣ ↑b ∨ ↑b ∣ ↑{ val := a, property := ha }
Tactic:
rcases b with ⟨b, hb⟩
State after:
case right.mk.mk
a : ℕ
ha : a ∈ VeryDiv
b : ℕ
hb : b ∈ VeryDiv
⊢ ↑{ val := a, property := ha } ∣ ↑{ val := b, property := hb } ∨
    ↑{ val := b, property := hb } ∣ ↑{ val := a, property := ha }

State before:
case right.mk.mk
a : ℕ
ha : a ∈ VeryDiv
b : ℕ
hb : b ∈ VeryDiv
⊢ ↑{ val := a, property := ha } ∣ ↑{ val := b, property := hb } ∨
    ↑{ val := b, property := hb } ∣ ↑{ val := a, property := ha }
Tactic:
simp_rw [VeryDiv] at *
State after:
case right.mk.mk
a : ℕ
ha : a ∈ {1, 2, 6, 30, 210}
b : ℕ
hb : b ∈ {1, 2, 6, 30, 210}
⊢ a ∣ b ∨ b ∣ a

State before:
case right.mk.mk
a : ℕ
ha : a ∈ {1, 2, 6, 30, 210}
b : ℕ
hb : b ∈ {1, 2, 6, 30, 210}
⊢ a ∣ b ∨ b ∣ a
Tactic:
simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at *
State after:
case right.mk.mk
a b : ℕ
ha : a = 1 ∨ a = 2 ∨ a = 6 ∨ a = 30 ∨ a = 210
hb : b = 1 ∨ b = 2 ∨ b = 6 ∨ b = 30 ∨ b = 210
⊢ a ∣ b ∨ b ∣ a

State before:
case right.mk.mk
a b : ℕ
ha : a = 1 ∨ a = 2 ∨ a = 6 ∨ a = 30 ∨ a = 210
hb : b = 1 ∨ b = 2 ∨ b = 6 ∨ b = 30 ∨ b = 210
⊢ a ∣ b ∨ b ∣ a
Tactic:
aesop
State after:
case right.mk.mk.inr.inr.inl.inr.inl

⊢ 2 ∣ 6 ∨ 6 ∣ 2

case right.mk.mk.inr.inr.inl.inr.inr.inl

⊢ 2 ∣ 30 ∨ 30 ∣ 2

case right.mk.mk.inr.inr.inl.inr.inr.inr

⊢ 2 ∣ 210 ∨ 210 ∣ 2

case right.mk.mk.inr.inr.inr.inl.inl

⊢ 6 ∣ 2 ∨ 2 ∣ 6

case right.mk.mk.inr.inr.inr.inl.inr.inl

⊢ 30 ∣ 2 ∨ 2 ∣ 30

case right.mk.mk.inr.inr.inr.inl.inr.inr

⊢ 210 ∣ 2 ∨ 2 ∣ 210

case right.mk.mk.inr.inr.inr.inr.inl.inr.inl

⊢ 6 ∣ 30 ∨ 30 ∣ 6

case right.mk.mk.inr.inr.inr.inr.inl.inr.inr

⊢ 6 ∣ 210 ∨ 210 ∣ 6

case right.mk.mk.inr.inr.inr.inr.inr.inl.inl

⊢ 30 ∣ 6 ∨ 6 ∣ 30

case right.mk.mk.inr.inr.inr.inr.inr.inl.inr

⊢ 210 ∣ 6 ∨ 6 ∣ 210

case right.mk.mk.inr.inr.inr.inr.inr.inr.inl.inr

⊢ 30 ∣ 210 ∨ 210 ∣ 30

case right.mk.mk.inr.inr.inr.inr.inr.inr.inr.inl

⊢ 210 ∣ 30 ∨ 30 ∣ 210

State before:
case right.mk.mk.inr.inr.inl.inr.inl

⊢ 2 ∣ 6 ∨ 6 ∣ 2
Tactic:
left
State after:
case right.mk.mk.inr.inr.inl.inr.inl.h

⊢ 2 ∣ 6

State before:
case right.mk.mk.inr.inr.inl.inr.inl.h

⊢ 2 ∣ 6
Tactic:
use 3
State after:
no goals

State before:
case right.mk.mk.inr.inr.inl.inr.inr.inl

⊢ 2 ∣ 30 ∨ 30 ∣ 2
Tactic:
left
State after:
case right.mk.mk.inr.inr.inl.inr.inr.inl.h

⊢ 2 ∣ 30

State before:
case right.mk.mk.inr.inr.inl.inr.inr.inl.h

⊢ 2 ∣ 30
Tactic:
use 15
State after:
no goals

State before:
case right.mk.mk.inr.inr.inl.inr.inr.inr

⊢ 2 ∣ 210 ∨ 210 ∣ 2
Tactic:
left
State after:
case right.mk.mk.inr.inr.inl.inr.inr.inr.h

⊢ 2 ∣ 210

State before:
case right.mk.mk.inr.inr.inl.inr.inr.inr.h

⊢ 2 ∣ 210
Tactic:
use 105
State after:
no goals

State before:
case right.mk.mk.inr.inr.inr.inl.inl

⊢ 6 ∣ 2 ∨ 2 ∣ 6
Tactic:
right
State after:
case right.mk.mk.inr.inr.inr.inl.inl.h

⊢ 2 ∣ 6

State before:
case right.mk.mk.inr.inr.inr.inl.inl.h

⊢ 2 ∣ 6
Tactic:
use 3
State after:
no goals

State before:
case right.mk.mk.inr.inr.inr.inl.inr.inl

⊢ 30 ∣ 2 ∨ 2 ∣ 30
Tactic:
right
State after:
case right.mk.mk.inr.inr.inr.inl.inr.inl.h

⊢ 2 ∣ 30

State before:
case right.mk.mk.inr.inr.inr.inl.inr.inl.h

⊢ 2 ∣ 30
Tactic:
use 15
State after:
no goals

State before:
case right.mk.mk.inr.inr.inr.inl.inr.inr

⊢ 210 ∣ 2 ∨ 2 ∣ 210
Tactic:
right
State after:
case right.mk.mk.inr.inr.inr.inl.inr.inr.h

⊢ 2 ∣ 210

State before:
case right.mk.mk.inr.inr.inr.inl.inr.inr.h

⊢ 2 ∣ 210
Tactic:
use 105
State after:
no goals

State before:
case right.mk.mk.inr.inr.inr.inr.inl.inr.inl

⊢ 6 ∣ 30 ∨ 30 ∣ 6
Tactic:
left
State after:
case right.mk.mk.inr.inr.inr.inr.inl.inr.inl.h

⊢ 6 ∣ 30

State before:
case right.mk.mk.inr.inr.inr.inr.inl.inr.inl.h

⊢ 6 ∣ 30
Tactic:
use 5
State after:
no goals

State before:
case right.mk.mk.inr.inr.inr.inr.inl.inr.inr

⊢ 6 ∣ 210 ∨ 210 ∣ 6
Tactic:
left
State after:
case right.mk.mk.inr.inr.inr.inr.inl.inr.inr.h

⊢ 6 ∣ 210

State before:
case right.mk.mk.inr.inr.inr.inr.inl.inr.inr.h

⊢ 6 ∣ 210
Tactic:
use 35
State after:
no goals

State before:
case right.mk.mk.inr.inr.inr.inr.inr.inl.inl

⊢ 30 ∣ 6 ∨ 6 ∣ 30
Tactic:
right
State after:
case right.mk.mk.inr.inr.inr.inr.inr.inl.inl.h

⊢ 6 ∣ 30

State before:
case right.mk.mk.inr.inr.inr.inr.inr.inl.inl.h

⊢ 6 ∣ 30
Tactic:
use 5
State after:
no goals

State before:
case right.mk.mk.inr.inr.inr.inr.inr.inl.inr

⊢ 210 ∣ 6 ∨ 6 ∣ 210
Tactic:
right
State after:
case right.mk.mk.inr.inr.inr.inr.inr.inl.inr.h

⊢ 6 ∣ 210

State before:
case right.mk.mk.inr.inr.inr.inr.inr.inl.inr.h

⊢ 6 ∣ 210
Tactic:
use 35
State after:
no goals

State before:
case right.mk.mk.inr.inr.inr.inr.inr.inr.inl.inr

⊢ 30 ∣ 210 ∨ 210 ∣ 30
Tactic:
left
State after:
case right.mk.mk.inr.inr.inr.inr.inr.inr.inl.inr.h

⊢ 30 ∣ 210

State before:
case right.mk.mk.inr.inr.inr.inr.inr.inr.inl.inr.h

⊢ 30 ∣ 210
Tactic:
use 7
State after:
no goals

State before:
case right.mk.mk.inr.inr.inr.inr.inr.inr.inr.inl

⊢ 210 ∣ 30 ∨ 30 ∣ 210
Tactic:
right
State after:
case right.mk.mk.inr.inr.inr.inr.inr.inr.inr.inl.h

⊢ 30 ∣ 210

State before:
case right.mk.mk.inr.inr.inr.inr.inr.inr.inr.inl.h

⊢ 30 ∣ 210
Tactic:
use 7
State after:
no goals