Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero.zero
⊢ (match zero * zero with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match zero with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match zero with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

pp: case zero.neg
⊢ (match zero * neg with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match zero with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match neg with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

pp: case zero.pos
⊢ (match zero * pos with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match zero with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match pos with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

pp: case neg.zero
⊢ (match neg * zero with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match neg with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match zero with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

pp: case neg.neg
⊢ (match neg * neg with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match neg with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match neg with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

pp: case neg.pos
⊢ (match neg * pos with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match neg with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match pos with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

pp: case pos.zero
⊢ (match pos * zero with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match pos with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match zero with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

pp: case pos.neg
⊢ (match pos * neg with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match pos with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match neg with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

pp: case pos.pos
⊢ (match pos * pos with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match pos with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match pos with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

Tactic:
<;>

Goal state after:
case zero.zero
⊢ (match zero * zero with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match zero with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match zero with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

case zero.neg
⊢ (match zero * neg with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match zero with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match neg with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

case zero.pos
⊢ (match zero * pos with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match zero with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match pos with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

case neg.zero
⊢ (match neg * zero with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match neg with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match zero with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

case neg.neg
⊢ (match neg * neg with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match neg with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match neg with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

case neg.pos
⊢ (match neg * pos with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match neg with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match pos with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

case pos.zero
⊢ (match pos * zero with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match pos with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match zero with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

case pos.neg
⊢ (match pos * neg with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match pos with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match neg with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

case pos.pos
⊢ (match pos * pos with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match pos with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match pos with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩