Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case refine_1
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ ![0, 1, 1] ≠ 0

pp: case refine_2
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ ![1, 0, 0] ≠ 0

pp: case refine_3
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ ![1, 0, 1] ≠ 0

pp: case refine_4
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ ![1, 0, 0] ≠ 0

pp: case refine_5
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ ![0, 1, 0] ≠ 0

pp: case refine_6
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ ![0, 0, 1] ≠ 0

pp: case refine_7
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ Projectivization.mk K ![0, 1, 1] ?refine_1 ∉ Projectivization.mk K ![0, 1, 0] ?refine_5 ∧
    Projectivization.mk K ![0, 1, 1] ?refine_1 ∉ Projectivization.mk K ![0, 0, 1] ?refine_6 ∧
      Projectivization.mk K ![1, 0, 0] ?refine_2 ∉ Projectivization.mk K ![1, 0, 0] ?refine_4 ∧
        Projectivization.mk K ![1, 0, 0] ?refine_2 ∈ Projectivization.mk K ![0, 1, 0] ?refine_5 ∧
          Projectivization.mk K ![1, 0, 0] ?refine_2 ∈ Projectivization.mk K ![0, 0, 1] ?refine_6 ∧
            Projectivization.mk K ![1, 0, 1] ?refine_3 ∉ Projectivization.mk K ![1, 0, 0] ?refine_4 ∧
              Projectivization.mk K ![1, 0, 1] ?refine_3 ∈ Projectivization.mk K ![0, 1, 0] ?refine_5 ∧
                Projectivization.mk K ![1, 0, 1] ?refine_3 ∉ Projectivization.mk K ![0, 0, 1] ?refine_6

Tactic:
<;>

Goal state after:
case refine_1
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ ![0, 1, 1] ≠ 0

case refine_2
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ ![1, 0, 0] ≠ 0

case refine_3
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ ![1, 0, 1] ≠ 0

case refine_4
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ ![1, 0, 0] ≠ 0

case refine_5
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ ![0, 1, 0] ≠ 0

case refine_6
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ ![0, 0, 1] ≠ 0

case refine_7
P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
⊢ Projectivization.mk K ![0, 1, 1] ?refine_1 ∉ Projectivization.mk K ![0, 1, 0] ?refine_5 ∧
    Projectivization.mk K ![0, 1, 1] ?refine_1 ∉ Projectivization.mk K ![0, 0, 1] ?refine_6 ∧
      Projectivization.mk K ![1, 0, 0] ?refine_2 ∉ Projectivization.mk K ![1, 0, 0] ?refine_4 ∧
        Projectivization.mk K ![1, 0, 0] ?refine_2 ∈ Projectivization.mk K ![0, 1, 0] ?refine_5 ∧
          Projectivization.mk K ![1, 0, 0] ?refine_2 ∈ Projectivization.mk K ![0, 0, 1] ?refine_6 ∧
            Projectivization.mk K ![1, 0, 1] ?refine_3 ∉ Projectivization.mk K ![1, 0, 0] ?refine_4 ∧
              Projectivization.mk K ![1, 0, 1] ?refine_3 ∈ Projectivization.mk K ![0, 1, 0] ?refine_5 ∧
                Projectivization.mk K ![1, 0, 1] ?refine_3 ∉ Projectivization.mk K ![0, 0, 1] ?refine_6