Theorem: LoVe.exist_distinct_fin4_of_neq (LoVe/Homework/Homework7.lean)

State before:
isLt✝¹ : 0 < 4
isLt✝ : 1 < 4
x✝ : { val := 0, isLt := isLt✝¹ } ≠ { val := 1, isLt := isLt✝ }
⊢ { val := 0, isLt := isLt✝¹ } ≠ 2 ∧
    2 ≠ { val := 1, isLt := isLt✝ } ∧ { val := 0, isLt := isLt✝¹ } ≠ 3 ∧ 3 ≠ { val := 1, isLt := isLt✝ } ∧ 2 ≠ 3
Tactic:
fin_neq
State after:
no goals

State before:
isLt✝¹ : 0 < 4
isLt✝ : 2 < 4
x✝ : { val := 0, isLt := isLt✝¹ } ≠ { val := 2, isLt := isLt✝ }
⊢ { val := 0, isLt := isLt✝¹ } ≠ 1 ∧
    1 ≠ { val := 2, isLt := isLt✝ } ∧ { val := 0, isLt := isLt✝¹ } ≠ 3 ∧ 3 ≠ { val := 2, isLt := isLt✝ } ∧ 1 ≠ 3
Tactic:
fin_neq
State after:
no goals

State before:
isLt✝¹ : 0 < 4
isLt✝ : 3 < 4
x✝ : { val := 0, isLt := isLt✝¹ } ≠ { val := 3, isLt := isLt✝ }
⊢ { val := 0, isLt := isLt✝¹ } ≠ 1 ∧
    1 ≠ { val := 3, isLt := isLt✝ } ∧ { val := 0, isLt := isLt✝¹ } ≠ 2 ∧ 2 ≠ { val := 3, isLt := isLt✝ } ∧ 1 ≠ 2
Tactic:
fin_neq
State after:
no goals

State before:
isLt✝¹ : 1 < 4
isLt✝ : 0 < 4
x✝ : { val := 1, isLt := isLt✝¹ } ≠ { val := 0, isLt := isLt✝ }
⊢ { val := 1, isLt := isLt✝¹ } ≠ 2 ∧
    2 ≠ { val := 0, isLt := isLt✝ } ∧ { val := 1, isLt := isLt✝¹ } ≠ 3 ∧ 3 ≠ { val := 0, isLt := isLt✝ } ∧ 2 ≠ 3
Tactic:
fin_neq
State after:
no goals

State before:
isLt✝¹ : 1 < 4
isLt✝ : 2 < 4
x✝ : { val := 1, isLt := isLt✝¹ } ≠ { val := 2, isLt := isLt✝ }
⊢ { val := 1, isLt := isLt✝¹ } ≠ 0 ∧
    0 ≠ { val := 2, isLt := isLt✝ } ∧ { val := 1, isLt := isLt✝¹ } ≠ 3 ∧ 3 ≠ { val := 2, isLt := isLt✝ } ∧ 0 ≠ 3
Tactic:
fin_neq
State after:
no goals

State before:
isLt✝¹ : 1 < 4
isLt✝ : 3 < 4
x✝ : { val := 1, isLt := isLt✝¹ } ≠ { val := 3, isLt := isLt✝ }
⊢ { val := 1, isLt := isLt✝¹ } ≠ 0 ∧
    0 ≠ { val := 3, isLt := isLt✝ } ∧ { val := 1, isLt := isLt✝¹ } ≠ 2 ∧ 2 ≠ { val := 3, isLt := isLt✝ } ∧ 0 ≠ 2
Tactic:
fin_neq
State after:
no goals

State before:
isLt✝¹ : 2 < 4
isLt✝ : 0 < 4
x✝ : { val := 2, isLt := isLt✝¹ } ≠ { val := 0, isLt := isLt✝ }
⊢ { val := 2, isLt := isLt✝¹ } ≠ 1 ∧
    1 ≠ { val := 0, isLt := isLt✝ } ∧ { val := 2, isLt := isLt✝¹ } ≠ 3 ∧ 3 ≠ { val := 0, isLt := isLt✝ } ∧ 1 ≠ 3
Tactic:
fin_neq
State after:
no goals

State before:
isLt✝¹ : 2 < 4
isLt✝ : 1 < 4
x✝ : { val := 2, isLt := isLt✝¹ } ≠ { val := 1, isLt := isLt✝ }
⊢ { val := 2, isLt := isLt✝¹ } ≠ 0 ∧
    0 ≠ { val := 1, isLt := isLt✝ } ∧ { val := 2, isLt := isLt✝¹ } ≠ 3 ∧ 3 ≠ { val := 1, isLt := isLt✝ } ∧ 0 ≠ 3
Tactic:
fin_neq
State after:
no goals

State before:
isLt✝¹ : 2 < 4
isLt✝ : 3 < 4
x✝ : { val := 2, isLt := isLt✝¹ } ≠ { val := 3, isLt := isLt✝ }
⊢ { val := 2, isLt := isLt✝¹ } ≠ 0 ∧
    0 ≠ { val := 3, isLt := isLt✝ } ∧ { val := 2, isLt := isLt✝¹ } ≠ 1 ∧ 1 ≠ { val := 3, isLt := isLt✝ } ∧ 0 ≠ 1
Tactic:
fin_neq
State after:
no goals

State before:
isLt✝¹ : 3 < 4
isLt✝ : 0 < 4
x✝ : { val := 3, isLt := isLt✝¹ } ≠ { val := 0, isLt := isLt✝ }
⊢ { val := 3, isLt := isLt✝¹ } ≠ 1 ∧
    1 ≠ { val := 0, isLt := isLt✝ } ∧ { val := 3, isLt := isLt✝¹ } ≠ 2 ∧ 2 ≠ { val := 0, isLt := isLt✝ } ∧ 1 ≠ 2
Tactic:
fin_neq
State after:
no goals

State before:
isLt✝¹ : 3 < 4
isLt✝ : 1 < 4
x✝ : { val := 3, isLt := isLt✝¹ } ≠ { val := 1, isLt := isLt✝ }
⊢ { val := 3, isLt := isLt✝¹ } ≠ 0 ∧
    0 ≠ { val := 1, isLt := isLt✝ } ∧ { val := 3, isLt := isLt✝¹ } ≠ 2 ∧ 2 ≠ { val := 1, isLt := isLt✝ } ∧ 0 ≠ 2
Tactic:
fin_neq
State after:
no goals

State before:
isLt✝¹ : 3 < 4
isLt✝ : 2 < 4
x✝ : { val := 3, isLt := isLt✝¹ } ≠ { val := 2, isLt := isLt✝ }
⊢ { val := 3, isLt := isLt✝¹ } ≠ 0 ∧
    0 ≠ { val := 2, isLt := isLt✝ } ∧ { val := 3, isLt := isLt✝¹ } ≠ 1 ∧ 1 ≠ { val := 2, isLt := isLt✝ } ∧ 0 ≠ 1
Tactic:
fin_neq
State after:
no goals