How to reduce the compilation time of this line?

Stream: new members

[chenjulang]

Check the line "<;> apply And.intro;apply Eq.refl;exact Prod.mk_eq_zero.mp rfl".
To apply the same tactics on 18 Goals, this line costs over minutes,
Any ideas how to speed it up ?

lemma ft_valid
  : ∀x : RubiksSuperType,
  FaceTurn x → x ∈ ValidCube
  :=
    by
      intro x hx
      cases hx with
      | _ =>
        -- method 1:
        -- simp [ValidCube, U, D, R, L, F, B, U2, D2, R2, L2, F2, B2, U', D', R', L', F', B']
        -- repeat' apply And.intro
        -- all_goals apply Eq.refl

        -- method 2:
        simp only [ValidCube, U, D, R, L, F, B, U2, D2, R2, L2, F2, B2, U', D', R', L', F', B']
        <;> apply And.intro;apply Eq.refl;exact Prod.mk_eq_zero.mp rfl
        done

[chenjulang]

The 18 Goals:

18 goals
case U
⊢ ({ permute := cyclePieces [0, 1, 2, 3], orient := 0 }, { permute := cyclePieces [0, 1, 2, 3], orient := 0 }) ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case D
⊢ ({ permute := cyclePieces [4, 5, 6, 7], orient := 0 }, { permute := cyclePieces [4, 5, 6, 7], orient := 0 }) ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case R
⊢ ({ permute := cyclePieces [1, 6, 5, 2], orient := Orient 8 3 [(1, 1), (6, 2), (5, 1), (2, 2)] },
    { permute := cyclePieces [1, 9, 5, 10], orient := 0 }) ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case L
⊢ ({ permute := cyclePieces [0, 3, 4, 7], orient := Orient 8 3 [(0, 2), (3, 1), (4, 2), (7, 1)] },
    { permute := cyclePieces [3, 11, 7, 8], orient := 0 }) ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case F
⊢ ({ permute := cyclePieces [2, 5, 4, 3], orient := Orient 8 3 [(2, 1), (5, 2), (4, 1), (3, 2)] },
    { permute := cyclePieces [2, 10, 4, 11], orient := Orient 12 2 [(2, 1), (10, 1), (4, 1), (11, 1)] }) ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case B
⊢ ({ permute := cyclePieces [0, 7, 6, 1], orient := Orient 8 3 [(0, 1), (7, 2), (6, 1), (1, 2)] },
    { permute := cyclePieces [0, 8, 6, 9], orient := Orient 12 2 [(0, 1), (8, 1), (6, 1), (9, 1)] }) ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case U2
⊢ ({ permute := cyclePieces [0, 1, 2, 3], orient := 0 }, { permute := cyclePieces [0, 1, 2, 3], orient := 0 }) ^ 2 ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case D2
⊢ ({ permute := cyclePieces [4, 5, 6, 7], orient := 0 }, { permute := cyclePieces [4, 5, 6, 7], orient := 0 }) ^ 2 ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case R2
⊢ ({ permute := cyclePieces [1, 6, 5, 2], orient := Orient 8 3 [(1, 1), (6, 2), (5, 1), (2, 2)] },
      { permute := cyclePieces [1, 9, 5, 10], orient := 0 }) ^
    2 ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case L2
⊢ ({ permute := cyclePieces [0, 3, 4, 7], orient := Orient 8 3 [(0, 2), (3, 1), (4, 2), (7, 1)] },
      { permute := cyclePieces [3, 11, 7, 8], orient := 0 }) ^
    2 ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case F2
⊢ ({ permute := cyclePieces [2, 5, 4, 3], orient := Orient 8 3 [(2, 1), (5, 2), (4, 1), (3, 2)] },
      { permute := cyclePieces [2, 10, 4, 11], orient := Orient 12 2 [(2, 1), (10, 1), (4, 1), (11, 1)] }) ^
    2 ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case B2
⊢ ({ permute := cyclePieces [0, 7, 6, 1], orient := Orient 8 3 [(0, 1), (7, 2), (6, 1), (1, 2)] },
      { permute := cyclePieces [0, 8, 6, 9], orient := Orient 12 2 [(0, 1), (8, 1), (6, 1), (9, 1)] }) ^
    2 ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case U'
⊢ ({ permute := cyclePieces [0, 1, 2, 3], orient := 0 }, { permute := cyclePieces [0, 1, 2, 3], orient := 0 })⁻¹ ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case D'
⊢ ({ permute := cyclePieces [4, 5, 6, 7], orient := 0 }, { permute := cyclePieces [4, 5, 6, 7], orient := 0 })⁻¹ ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case R'
⊢ ({ permute := cyclePieces [1, 6, 5, 2], orient := Orient 8 3 [(1, 1), (6, 2), (5, 1), (2, 2)] },
      { permute := cyclePieces [1, 9, 5, 10], orient := 0 })⁻¹ ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case L'
⊢ ({ permute := cyclePieces [0, 3, 4, 7], orient := Orient 8 3 [(0, 2), (3, 1), (4, 2), (7, 1)] },
      { permute := cyclePieces [3, 11, 7, 8], orient := 0 })⁻¹ ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case F'
⊢ ({ permute := cyclePieces [2, 5, 4, 3], orient := Orient 8 3 [(2, 1), (5, 2), (4, 1), (3, 2)] },
      { permute := cyclePieces [2, 10, 4, 11], orient := Orient 12 2 [(2, 1), (10, 1), (4, 1), (11, 1)] })⁻¹ ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}
case B'
⊢ ({ permute := cyclePieces [0, 7, 6, 1], orient := Orient 8 3 [(0, 1), (7, 2), (6, 1), (1, 2)] },
      { permute := cyclePieces [0, 8, 6, 9], orient := Orient 12 2 [(0, 1), (8, 1), (6, 1), (9, 1)] })⁻¹ ∈
  {c |
    sign c.1.permute = sign c.2.permute ∧
      Finset.sum {0, 1, 2, 3, 4, 5, 6, 7} c.1.orient = 0 ∧
        Finset.sum {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} c.2.orient = 0}