internlm/Lean-Github huggingface dataset:
Theorem: dvd_iff_nat_dvd
Proof state before:
case h
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
lc : ℕplus := { val := c, property := (_ : c ≠ 0) }
⊢ b = a * lc
Tactic:
rw [Subtype.ext_iff]
Proof state after:
case h
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
lc : ℕplus := { val := c, property := (_ : c ≠ 0) }
⊢ ↑b = ↑(a * lc)
Theorem: dvd_iff_nat_dvd
Proof state before:
case h
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
lc : ℕplus := { val := c, property := (_ : c ≠ 0) }
⊢ ↑b = ↑(a * lc)
Tactic:
exact hc
Proof state after:
no goals
Theorem: r3_not_weak_order
Proof state before:
⊢ ¬WeakOrder R3
Tactic:
intro hwo
Proof state after:
hwo : WeakOrder R3
⊢ False
Theorem: r3_not_weak_order
Proof state before:
hwo : WeakOrder R3
⊢ False
Tactic:
simp_rw [WeakOrder, PartialOrder', R3] at hwo
Proof 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
Theorem: r3_not_weak_order
Proof 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
Proof 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
Theorem: r3_not_weak_order
Proof 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)
Proof 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
Theorem: r3_not_weak_order
Proof 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
Proof 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
Theorem: r3_not_weak_order
Proof 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⟩
Proof 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
Theorem: r3_not_weak_order
Proof 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
Proof 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
Theorem: r3_not_weak_order
Proof 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⟩
Proof 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
Theorem: r3_not_weak_order
Proof 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
Proof 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
Theorem: r3_not_weak_order
Proof 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
Proof state after:
no goals
Theorem: r3_not_weak_order
Proof 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
Proof 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
Theorem: r3_not_weak_order
Proof 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⟩
Proof 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
Theorem: r3_not_weak_order
Proof 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
Proof 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
Theorem: r3_not_weak_order
Proof 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⟩
Proof 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
Theorem: r3_not_weak_order
Proof 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
Proof 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
Theorem: r3_not_weak_order
Proof 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
Proof state after:
no goals
Theorem: r3_not_strict_order
Proof state before:
⊢ ¬StrictOrder R3
Tactic:
intro hso
Proof state after:
hso : StrictOrder R3
⊢ False
Theorem: r3_not_strict_order
Proof state before:
hso : StrictOrder R3
⊢ False
Tactic:
rw [StrictOrder] at hso
Proof state after:
hso : ∀ (a b c : ℕplus), (R3 a b → R3 b c → R3 a c) ∧ Trichotomy (R3 a b) (R3 b a) (a = b)
⊢ False
Theorem: r3_not_strict_order
Proof state before:
hso : ∀ (a b c : ℕplus), (R3 a b → R3 b c → R3 a c) ∧ Trichotomy (R3 a b) (R3 b a) (a = b)
⊢ False
Tactic:
specialize hso 2 3 1
Proof state after:
hso : (R3 2 3 → R3 3 1 → R3 2 1) ∧ Trichotomy (R3 2 3) (R3 3 2) (2 = 3)
⊢ False
Theorem: r3_not_strict_order
Proof state before:
hso : (R3 2 3 → R3 3 1 → R3 2 1) ∧ Trichotomy (R3 2 3) (R3 3 2) (2 = 3)
⊢ False
Tactic:
rcases hso with ⟨_, (⟨_, _, heq⟩ | ⟨_, hdvd3, _⟩ | ⟨hdvd2, _, _⟩)⟩
Proof state after:
case intro.inl.intro.intro
left✝² : R3 2 3 → R3 3 1 → R3 2 1
left✝¹ : ¬R3 2 3
left✝ : ¬R3 3 2
heq : 2 = 3
⊢ False

case intro.inr.inl.intro.intro
left✝¹ : R3 2 3 → R3 3 1 → R3 2 1
left✝ : ¬R3 2 3
hdvd3 : R3 3 2
right✝ : ¬2 = 3
⊢ False

case intro.inr.inr.intro.intro
left✝¹ : R3 2 3 → R3 3 1 → R3 2 1
hdvd2 : R3 2 3
left✝ : ¬R3 3 2
right✝ : ¬2 = 3
⊢ False
Theorem: r3_not_strict_order
Proof state before:
case intro.inl.intro.intro
left✝² : R3 2 3 → R3 3 1 → R3 2 1
left✝¹ : ¬R3 2 3
left✝ : ¬R3 3 2
heq : 2 = 3
⊢ False
Tactic:
rw [←Subtype.coe_inj] at heq
Proof state after:
case intro.inl.intro.intro
left✝² : R3 2 3 → R3 3 1 → R3 2 1
left✝¹ : ¬R3 2 3
left✝ : ¬R3 3 2
heq : ↑2 = ↑3
⊢ False
Theorem: r3_not_strict_order
Proof state before:
case intro.inl.intro.intro
left✝² : R3 2 3 → R3 3 1 → R3 2 1
left✝¹ : ¬R3 2 3
left✝ : ¬R3 3 2
heq : ↑2 = ↑3
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: r3_not_strict_order
Proof state before:
case intro.inr.inl.intro.intro
left✝¹ : R3 2 3 → R3 3 1 → R3 2 1
left✝ : ¬R3 2 3
hdvd3 : R3 3 2
right✝ : ¬2 = 3
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: r3_not_strict_order
Proof state before:
case intro.inr.inr.intro.intro
left✝¹ : R3 2 3 → R3 3 1 → R3 2 1
hdvd2 : R3 2 3
left✝ : ¬R3 3 2
right✝ : ¬2 = 3
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: r3_partial_order
Proof state before:
⊢ PartialOrder' R3
Tactic:
intros hpo b c
Proof state after:
hpo b c : ℕplus
⊢ (R3 hpo b → R3 b c → R3 hpo c) ∧ (R3 hpo b → R3 b hpo → hpo = b)
Theorem: r3_partial_order
Proof 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]
Proof state after:
hpo b c : ℕplus
⊢ (hpo ∣ b → b ∣ c → hpo ∣ c) ∧ (hpo ∣ b → b ∣ hpo → hpo = b)
Theorem: r3_partial_order
Proof state before:
hpo b c : ℕplus
⊢ (hpo ∣ b → b ∣ c → hpo ∣ c) ∧ (hpo ∣ b → b ∣ hpo → hpo = b)
Tactic:
constructor
Proof 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
Theorem: r3_partial_order
Proof state before:
case left
hpo b c : ℕplus
⊢ hpo ∣ b → b ∣ c → hpo ∣ c
Tactic:
intro hdvdb hdvdc
Proof state after:
case left
hpo b c : ℕplus
hdvdb : hpo ∣ b
hdvdc : b ∣ c
⊢ hpo ∣ c
Theorem: r3_partial_order
Proof state before:
case left
hpo b c : ℕplus
hdvdb : hpo ∣ b
hdvdc : b ∣ c
⊢ hpo ∣ c
Tactic:
rw [dvd_def] at hdvdb
Proof state after:
case left
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdc : b ∣ c
⊢ hpo ∣ c
Theorem: r3_partial_order
Proof state before:
case left
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdc : b ∣ c
⊢ hpo ∣ c
Tactic:
rw [dvd_def] at hdvdc
Proof state after:
case left
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdc : ∃ c_1, c = b * c_1
⊢ hpo ∣ c
Theorem: r3_partial_order
Proof 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]
Proof 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
Theorem: r3_partial_order
Proof 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⟩
Proof 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
Theorem: r3_partial_order
Proof 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⟩
Proof 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
Theorem: r3_partial_order
Proof 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
Proof 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
Theorem: r3_partial_order
Proof 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
Proof 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
Theorem: r3_partial_order
Proof 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)
Proof state after:
case h
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : ↑c = ↑(b * l)
⊢ c = hpo * (k * l)
Theorem: r3_partial_order
Proof 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]
Proof state after:
case h
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : ↑c = ↑(b * l)
⊢ ↑c = ↑(hpo * (k * l))
Theorem: r3_partial_order
Proof 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]
Proof state after:
case h
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : ↑c = ↑(b * l)
⊢ ↑b * ↑l = ↑hpo * (↑k * ↑l)
Theorem: r3_partial_order
Proof 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]
Proof 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)
Theorem: r3_partial_order
Proof 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
Proof state after:
no goals
Theorem: r3_partial_order
Proof state before:
case right
hpo b c : ℕplus
⊢ hpo ∣ b → b ∣ hpo → hpo = b
Tactic:
intro hdvdb hdvdhpo
Proof state after:
case right
hpo b c : ℕplus
hdvdb : hpo ∣ b
hdvdhpo : b ∣ hpo
⊢ hpo = b
Theorem: r3_partial_order
Proof state before:
case right
hpo b c : ℕplus
hdvdb : hpo ∣ b
hdvdhpo : b ∣ hpo
⊢ hpo = b
Tactic:
rw [dvd_def] at hdvdb
Proof state after:
case right
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdhpo : b ∣ hpo
⊢ hpo = b
Theorem: r3_partial_order
Proof state before:
case right
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdhpo : b ∣ hpo
⊢ hpo = b
Tactic:
rw [dvd_def] at hdvdhpo
Proof state after:
case right
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdhpo : ∃ c, hpo = b * c
⊢ hpo = b
Theorem: r3_partial_order
Proof 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⟩
Proof state after:
case right.intro
hpo b c : ℕplus
hdvdhpo : ∃ c, hpo = b * c
k : ℕplus
hk : b = hpo * k
⊢ hpo = b
Theorem: r3_partial_order
Proof 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⟩
Proof state after:
case right.intro.intro
hpo b c k : ℕplus
hk : b = hpo * k
l : ℕplus
hl : hpo = b * l
⊢ hpo = b
Theorem: r3_partial_order
Proof 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
Proof 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
Theorem: r3_partial_order
Proof 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
Proof state after:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : hpo = b * l
⊢ hpo = b
Theorem: r3_partial_order
Proof 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
Proof 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
Theorem: r3_partial_order
Proof 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
Proof state after:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo = ↑b * ↑l
⊢ hpo = b
Theorem: r3_partial_order
Proof 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]
Proof state after:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo = ↑b * ↑l
⊢ ↑hpo = ↑b
Theorem: r3_partial_order
Proof 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
Proof state after:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo = ↑hpo * ↑k * ↑l
⊢ ↑hpo = ↑b
Theorem: r3_partial_order
Proof 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
Proof state after:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo * ↑k * ↑l = ↑hpo
⊢ ↑hpo = ↑b
Theorem: r3_partial_order
Proof 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
Proof state after:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑k = 1 ∧ ↑l = 1
⊢ ↑hpo = ↑b
Theorem: r3_partial_order
Proof 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
Proof state after:
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * 1
l : ℕplus
hl : ↑k = 1 ∧ ↑l = 1
⊢ ↑hpo = ↑b
Theorem: r3_partial_order
Proof 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
Proof state after:
case right.intro.intro
hpo b c k l : ℕplus
hl : ↑k = 1 ∧ ↑l = 1
hk : ↑b = ↑hpo
⊢ ↑hpo = ↑b
Theorem: r3_partial_order
Proof state before:
case right.intro.intro
hpo b c k l : ℕplus
hl : ↑k = 1 ∧ ↑l = 1
hk : ↑b = ↑hpo
⊢ ↑hpo = ↑b
Tactic:
symm
Proof state after:
case right.intro.intro
hpo b c k l : ℕplus
hl : ↑k = 1 ∧ ↑l = 1
hk : ↑b = ↑hpo
⊢ ↑b = ↑hpo
Theorem: r3_partial_order
Proof 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
Proof state after:
no goals
Theorem: r4_weak_order
Proof state before:
⊢ WeakOrder R4
Tactic:
simp only [WeakOrder, PartialOrder', R4]
Proof 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
Theorem: r4_weak_order
Proof 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
Proof 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
Theorem: r4_weak_order
Proof 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
Proof state after:
case left
a b c : ↑VeryDiv
⊢ (↑a ∣ ↑b → ↑b ∣ ↑c → ↑a ∣ ↑c) ∧ (↑a ∣ ↑b → ↑b ∣ ↑a → a = b)
Theorem: r4_weak_order
Proof state before:
case left
a b c : ↑VeryDiv
⊢ (↑a ∣ ↑b → ↑b ∣ ↑c → ↑a ∣ ↑c) ∧ (↑a ∣ ↑b → ↑b ∣ ↑a → a = b)
Tactic:
constructor
Proof 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
Theorem: r4_weak_order
Proof state before:
case left.left
a b c : ↑VeryDiv
⊢ ↑a ∣ ↑b → ↑b ∣ ↑c → ↑a ∣ ↑c
Tactic:
exact Nat.dvd_trans
Proof state after:
no goals
Theorem: r4_weak_order
Proof state before:
case left.right
a b c : ↑VeryDiv
⊢ ↑a ∣ ↑b → ↑b ∣ ↑a → a = b
Tactic:
simp_rw [←SetCoe.ext_iff]
Proof state after:
case left.right
a b c : ↑VeryDiv
⊢ ↑a ∣ ↑b → ↑b ∣ ↑a → ↑a = ↑b
Theorem: r4_weak_order
Proof state before:
case left.right
a b c : ↑VeryDiv
⊢ ↑a ∣ ↑b → ↑b ∣ ↑a → ↑a = ↑b
Tactic:
exact Nat.dvd_antisymm
Proof state after:
no goals
Theorem: r4_weak_order
Proof state before:
case right

⊢ ∀ (a b : ↑VeryDiv), ↑a ∣ ↑b ∨ ↑b ∣ ↑a
Tactic:
intros a b
Proof state after:
case right
a b : ↑VeryDiv
⊢ ↑a ∣ ↑b ∨ ↑b ∣ ↑a
Theorem: r4_weak_order
Proof state before:
case right
a b : ↑VeryDiv
⊢ ↑a ∣ ↑b ∨ ↑b ∣ ↑a
Tactic:
rcases a with ⟨a, ha⟩
Proof state after:
case right.mk
b : ↑VeryDiv
a : ℕ
ha : a ∈ VeryDiv
⊢ ↑{ val := a, property := ha } ∣ ↑b ∨ ↑b ∣ ↑{ val := a, property := ha }
Theorem: r4_weak_order
Proof 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⟩
Proof 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 }
Theorem: r4_weak_order
Proof 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 *
Proof 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
Theorem: r4_weak_order
Proof 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 *
Proof 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
Theorem: r4_weak_order
Proof 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
Proof 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
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inl.inr.inl

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

⊢ 2 ∣ 6
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inl.inr.inl.h

⊢ 2 ∣ 6
Tactic:
use 3
Proof state after:
no goals
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inl.inr.inr.inl

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

⊢ 2 ∣ 30
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inl.inr.inr.inl.h

⊢ 2 ∣ 30
Tactic:
use 15
Proof state after:
no goals
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inl.inr.inr.inr

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

⊢ 2 ∣ 210
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inl.inr.inr.inr.h

⊢ 2 ∣ 210
Tactic:
use 105
Proof state after:
no goals
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inl.inl

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

⊢ 2 ∣ 6
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inl.inl.h

⊢ 2 ∣ 6
Tactic:
use 3
Proof state after:
no goals
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inl.inr.inl

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

⊢ 2 ∣ 30
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inl.inr.inl.h

⊢ 2 ∣ 30
Tactic:
use 15
Proof state after:
no goals
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inl.inr.inr

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

⊢ 2 ∣ 210
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inl.inr.inr.h

⊢ 2 ∣ 210
Tactic:
use 105
Proof state after:
no goals