simp_rw [R4] at hf
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
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