Theorem: r3_partial_order (meetings/ex6.lean)

State before:
⊢ PartialOrder' R3
Tactic:
intros hpo b c
State after:
hpo b c : ℕplus
⊢ (R3 hpo b → R3 b c → R3 hpo c) ∧ (R3 hpo b → R3 b hpo → hpo = b)

State before:
hpo b c : ℕplus
⊢ (R3 hpo b → R3 b c → R3 hpo c) ∧ (R3 hpo b → R3 b hpo → hpo = b)
Tactic:
simp [R3]
State after:
hpo b c : ℕplus
⊢ (hpo ∣ b → b ∣ c → hpo ∣ c) ∧ (hpo ∣ b → b ∣ hpo → hpo = b)

State before:
hpo b c : ℕplus
⊢ (hpo ∣ b → b ∣ c → hpo ∣ c) ∧ (hpo ∣ b → b ∣ hpo → hpo = b)
Tactic:
constructor
State after:
case left
hpo b c : ℕplus
⊢ hpo ∣ b → b ∣ c → hpo ∣ c

case right
hpo b c : ℕplus
⊢ hpo ∣ b → b ∣ hpo → hpo = b

State before:
case left
hpo b c : ℕplus
⊢ hpo ∣ b → b ∣ c → hpo ∣ c
Tactic:
intro hdvdb hdvdc
State after:
case left
hpo b c : ℕplus
hdvdb : hpo ∣ b
hdvdc : b ∣ c
⊢ hpo ∣ c

State before:
case left
hpo b c : ℕplus
hdvdb : hpo ∣ b
hdvdc : b ∣ c
⊢ hpo ∣ c
Tactic:
rw [dvd_def] at hdvdb
State after:
case left
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdc : b ∣ c
⊢ hpo ∣ c

State before:
case left
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdc : b ∣ c
⊢ hpo ∣ c
Tactic:
rw [dvd_def] at hdvdc
State after:
case left
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdc : ∃ c_1, c = b * c_1
⊢ hpo ∣ c

State before:
case left
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdc : ∃ c_1, c = b * c_1
⊢ hpo ∣ c
Tactic:
rw [dvd_def]
State after:
case left
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdc : ∃ c_1, c = b * c_1
⊢ ∃ c_1, c = hpo * c_1

State before:
case left
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdc : ∃ c_1, c = b * c_1
⊢ ∃ c_1, c = hpo * c_1
Tactic:
rcases hdvdb with ⟨k, hk⟩
State after:
case left.intro
hpo b c : ℕplus
hdvdc : ∃ c_1, c = b * c_1
k : ℕplus
hk : b = hpo * k
⊢ ∃ c_1, c = hpo * c_1

State before:
case left.intro
hpo b c : ℕplus
hdvdc : ∃ c_1, c = b * c_1
k : ℕplus
hk : b = hpo * k
⊢ ∃ c_1, c = hpo * c_1
Tactic:
rcases hdvdc with ⟨l, hl⟩
State after:
case left.intro.intro
hpo b c k : ℕplus
hk : b = hpo * k
l : ℕplus
hl : c = b * l
⊢ ∃ c_1, c = hpo * c_1

State before:
case left.intro.intro
hpo b c k : ℕplus
hk : b = hpo * k
l : ℕplus
hl : c = b * l
⊢ ∃ c_1, c = hpo * c_1
Tactic:
rw [Subtype.ext_iff] at hk
State after:
case left.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : c = b * l
⊢ ∃ c_1, c = hpo * c_1

State before:
case left.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : c = b * l
⊢ ∃ c_1, c = hpo * c_1
Tactic:
rw [Subtype.ext_iff] at hl
State after:
case left.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : ↑c = ↑(b * l)
⊢ ∃ c_1, c = hpo * c_1

State before:
case left.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : ↑c = ↑(b * l)
⊢ ∃ c_1, c = hpo * c_1
Tactic:
use (k * l)
State after:
case h
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : ↑c = ↑(b * l)
⊢ c = hpo * (k * l)

State before:
case h
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : ↑c = ↑(b * l)
⊢ c = hpo * (k * l)
Tactic:
rw [Subtype.ext_iff]
State after:
case h
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : ↑c = ↑(b * l)
⊢ ↑c = ↑(hpo * (k * l))

State before:
case h
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : ↑c = ↑(b * l)
⊢ ↑c = ↑(hpo * (k * l))
Tactic:
simp_rw [hl, ℕplus.mul_def]
State after:
case h
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : ↑c = ↑(b * l)
⊢ ↑b * ↑l = ↑hpo * (↑k * ↑l)

State before:
case h
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : ↑c = ↑(b * l)
⊢ ↑b * ↑l = ↑hpo * (↑k * ↑l)
Tactic:
simp_rw [hk, ℕplus.mul_def]
State after:
case h
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : ↑c = ↑(b * l)
⊢ ↑hpo * ↑k * ↑l = ↑hpo * (↑k * ↑l)

State before:
case h
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : ↑c = ↑(b * l)
⊢ ↑hpo * ↑k * ↑l = ↑hpo * (↑k * ↑l)
Tactic:
exact Nat.mul_assoc hpo.val k.val l.val
State after:
no goals

State before:
case right
hpo b c : ℕplus
⊢ hpo ∣ b → b ∣ hpo → hpo = b
Tactic:
intro hdvdb hdvdhpo
State after:
case right
hpo b c : ℕplus
hdvdb : hpo ∣ b
hdvdhpo : b ∣ hpo
⊢ hpo = b

State before:
case right
hpo b c : ℕplus
hdvdb : hpo ∣ b
hdvdhpo : b ∣ hpo
⊢ hpo = b
Tactic:
rw [dvd_def] at hdvdb
State after:
case right
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdhpo : b ∣ hpo
⊢ hpo = b

State before:
case right
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdhpo : b ∣ hpo
⊢ hpo = b
Tactic:
rw [dvd_def] at hdvdhpo
State after:
case right
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdhpo : ∃ c, hpo = b * c
⊢ hpo = b

State before:
case right
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdhpo : ∃ c, hpo = b * c
⊢ hpo = b
Tactic:
rcases hdvdb with ⟨k, hk⟩
State after:
case right.intro
hpo b c : ℕplus
hdvdhpo : ∃ c, hpo = b * c
k : ℕplus
hk : b = hpo * k
⊢ hpo = b

State before:
case right.intro
hpo b c : ℕplus
hdvdhpo : ∃ c, hpo = b * c
k : ℕplus
hk : b = hpo * k
⊢ hpo = b
Tactic:
rcases hdvdhpo with ⟨l, hl⟩
State after:
case right.intro.intro
hpo b c k : ℕplus
hk : b = hpo * k
l : ℕplus
hl : hpo = b * l
⊢ hpo = b

State before:
case right.intro.intro
hpo b c k : ℕplus
hk : b = hpo * k
l : ℕplus
hl : hpo = b * l
⊢ hpo = b
Tactic:
rw [Subtype.ext_iff, ℕplus.mul_def] at hk
State after:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑{ val := ↑hpo * ↑k, property := (_ : ↑hpo * ↑k ≠ 0) }
l : ℕplus
hl : hpo = b * l
⊢ hpo = b

State before:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑{ val := ↑hpo * ↑k, property := (_ : ↑hpo * ↑k ≠ 0) }
l : ℕplus
hl : hpo = b * l
⊢ hpo = b
Tactic:
simp at hk
State after:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : hpo = b * l
⊢ hpo = b

State before:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : hpo = b * l
⊢ hpo = b
Tactic:
rw [Subtype.ext_iff, ℕplus.mul_def] at hl
State after:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo = ↑{ val := ↑b * ↑l, property := (_ : ↑b * ↑l ≠ 0) }
⊢ hpo = b

State before:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo = ↑{ val := ↑b * ↑l, property := (_ : ↑b * ↑l ≠ 0) }
⊢ hpo = b
Tactic:
simp at hl
State after:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo = ↑b * ↑l
⊢ hpo = b

State before:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo = ↑b * ↑l
⊢ hpo = b
Tactic:
rw [Subtype.ext_iff]
State after:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo = ↑b * ↑l
⊢ ↑hpo = ↑b

State before:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo = ↑b * ↑l
⊢ ↑hpo = ↑b
Tactic:
rw [hk] at hl
State after:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo = ↑hpo * ↑k * ↑l
⊢ ↑hpo = ↑b

State before:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo = ↑hpo * ↑k * ↑l
⊢ ↑hpo = ↑b
Tactic:
symm at hl
State after:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo * ↑k * ↑l = ↑hpo
⊢ ↑hpo = ↑b

State before:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo * ↑k * ↑l = ↑hpo
⊢ ↑hpo = ↑b
Tactic:
rw [Nat.mul_assoc, Nat.mul_right_eq_self_iff (Nat.zero_lt_of_ne_zero hpo.property), mul_eq_one] at hl
State after:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑k = 1 ∧ ↑l = 1
⊢ ↑hpo = ↑b

State before:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑k = 1 ∧ ↑l = 1
⊢ ↑hpo = ↑b
Tactic:
rw [hl.1] at hk
State after:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * 1
l : ℕplus
hl : ↑k = 1 ∧ ↑l = 1
⊢ ↑hpo = ↑b

State before:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * 1
l : ℕplus
hl : ↑k = 1 ∧ ↑l = 1
⊢ ↑hpo = ↑b
Tactic:
simp at hk
State after:
case right.intro.intro
hpo b c k l : ℕplus
hl : ↑k = 1 ∧ ↑l = 1
hk : ↑b = ↑hpo
⊢ ↑hpo = ↑b

State before:
case right.intro.intro
hpo b c k l : ℕplus
hl : ↑k = 1 ∧ ↑l = 1
hk : ↑b = ↑hpo
⊢ ↑hpo = ↑b
Tactic:
symm
State after:
case right.intro.intro
hpo b c k l : ℕplus
hl : ↑k = 1 ∧ ↑l = 1
hk : ↑b = ↑hpo
⊢ ↑b = ↑hpo

State before:
case right.intro.intro
hpo b c k l : ℕplus
hl : ↑k = 1 ∧ ↑l = 1
hk : ↑b = ↑hpo
⊢ ↑b = ↑hpo
Tactic:
exact hk
State after:
no goals