Theorem: r4_not_strict_order (meetings/ex6.lean)

State before:
⊢ ¬StrictOrder R4
Tactic:
intro hso
State after:
hso : StrictOrder R4
⊢ False

State before:
hso : StrictOrder R4
⊢ False
Tactic:
simp_rw [StrictOrder, VeryDiv] at hso
State after:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
⊢ False

State before:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
⊢ False
Tactic:
have hf := hso ⟨1, by tauto⟩ ⟨1, by tauto⟩ ⟨1, by tauto⟩
State after:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
hf :
  (R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
        { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) } →
      R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
          { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) } →
        R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
          { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }) ∧
    Trichotomy
      (R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
        { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) })
      (R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
        { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) })
      ({ val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) } =
        { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) })
⊢ False

State before:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
hf :
  (R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
        { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) } →
      R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
          { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) } →
        R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
          { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }) ∧
    Trichotomy
      (R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
        { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) })
      (R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
        { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) })
      ({ val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) } =
        { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) })
⊢ False
Tactic:
simp_rw [R4] at hf
State after:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
hf : (1 ∣ 1 → 1 ∣ 1 → 1 ∣ 1) ∧ Trichotomy (1 ∣ 1) (1 ∣ 1) True
⊢ False

State before:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
hf : (1 ∣ 1 → 1 ∣ 1 → 1 ∣ 1) ∧ Trichotomy (1 ∣ 1) (1 ∣ 1) True
⊢ False
Tactic:
rw [Trichotomy] at hf
State after:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
hf : (1 ∣ 1 → 1 ∣ 1 → 1 ∣ 1) ∧ (¬1 ∣ 1 ∧ ¬1 ∣ 1 ∧ True ∨ ¬1 ∣ 1 ∧ 1 ∣ 1 ∧ ¬True ∨ 1 ∣ 1 ∧ ¬1 ∣ 1 ∧ ¬True)
⊢ False

State before:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
hf : (1 ∣ 1 → 1 ∣ 1 → 1 ∣ 1) ∧ (¬1 ∣ 1 ∧ ¬1 ∣ 1 ∧ True ∨ ¬1 ∣ 1 ∧ 1 ∣ 1 ∧ ¬True ∨ 1 ∣ 1 ∧ ¬1 ∣ 1 ∧ ¬True)
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
⊢ 1 ∈ {1, 2, 6, 30, 210}
Tactic:
tauto
State after:
no goals