awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
zero :
  (fun (a : Fin 3) ↦
        (match (motive := Fin 3 → SignType) a with
          | ⟨0, isLt⟩ => 0
          | ⟨1, isLt⟩ => 1
          | ⟨2, isLt⟩ => -1 :
          SignType))
      ((fun (a : SignType) ↦
          (match (motive := SignType → Fin 3) a with
            | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
            | pos => ⟨1, fin3Equiv._proof_4⟩
            | neg => ⟨2, fin3Equiv._proof_5⟩ :
            Fin 3))
        SignType.zero) =
    SignType.zero
⊢ (fun (a : Fin 3) ↦
        (match (motive := Fin 3 → SignType) a with
          | ⟨0, isLt⟩ => 0
          | ⟨1, isLt⟩ => 1
          | ⟨2, isLt⟩ => -1 :
          SignType))
      ((fun (a : SignType) ↦
          (match (motive := SignType → Fin 3) a with
            | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
            | pos => ⟨1, fin3Equiv._proof_4⟩
            | neg => ⟨2, fin3Equiv._proof_5⟩ :
            Fin 3))
        a) =
    a
have neg : (fun (a : Fin 3) ↦
      (match (motive := Fin 3 → SignType) a with
        | ⟨0, isLt⟩ => 0
        | ⟨1, isLt⟩ => 1
        | ⟨2, isLt⟩ => -1 :
        SignType))
    ((fun (a : SignType) ↦
        (match (motive := SignType → Fin 3) a with
          | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
          | pos => ⟨1, fin3Equiv._proof_4⟩
          | neg => ⟨2, fin3Equiv._proof_5⟩ :
          Fin 3))
      neg) =
  neg
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a : SignType
zero :
  (fun (a : Fin 3) ↦
        (match (motive := Fin 3 → SignType) a with
          | ⟨0, isLt⟩ => 0
          | ⟨1, isLt⟩ => 1
          | ⟨2, isLt⟩ => -1 :
          SignType))
      ((fun (a : SignType) ↦
          (match (motive := SignType → Fin 3) a with
            | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
            | pos => ⟨1, fin3Equiv._proof_4⟩
            | SignType.neg => ⟨2, fin3Equiv._proof_5⟩ :
            Fin 3))
        SignType.zero) =
    SignType.zero
neg :
  (fun (a : Fin 3) ↦
        (match (motive := Fin 3 → SignType) a with
          | ⟨0, isLt⟩ => 0
          | ⟨1, isLt⟩ => 1
          | ⟨2, isLt⟩ => -1 :
          SignType))
      ((fun (a : SignType) ↦
          (match (motive := SignType → Fin 3) a with
            | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
            | pos => ⟨1, fin3Equiv._proof_4⟩
            | SignType.neg => ⟨2, fin3Equiv._proof_5⟩ :
            Fin 3))
        SignType.neg) =
    SignType.neg
⊢ (fun (a : Fin 3) ↦
        (match (motive := Fin 3 → SignType) a with
          | ⟨0, isLt⟩ => 0
          | ⟨1, isLt⟩ => 1
          | ⟨2, isLt⟩ => -1 :
          SignType))
      ((fun (a : SignType) ↦
          (match (motive := SignType → Fin 3) a with
            | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
            | pos => ⟨1, fin3Equiv._proof_4⟩
            | SignType.neg => ⟨2, fin3Equiv._proof_5⟩ :
            Fin 3))
        a) =
    a
have pos : (fun (a : Fin 3) ↦
      (match (motive := Fin 3 → SignType) a with
        | ⟨0, isLt⟩ => 0
        | ⟨1, isLt⟩ => 1
        | ⟨2, isLt⟩ => -1 :
        SignType))
    ((fun (a : SignType) ↦
        (match (motive := SignType → Fin 3) a with
          | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
          | pos => ⟨1, fin3Equiv._proof_4⟩
          | SignType.neg => ⟨2, fin3Equiv._proof_5⟩ :
          Fin 3))
      pos) =
  pos
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a b : SignType
⊢ (match (motive := SignType → Fin 3) a * b with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) a with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) b with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
have zero : (match (motive := SignType → Fin 3) zero * b with
  | zero => ⟨0, fin3Equiv._proof_3⟩
  | pos => ⟨1, fin3Equiv._proof_4⟩
  | neg => ⟨2, fin3Equiv._proof_5⟩) =
  HMul.hMul (α := Fin 3) (β := Fin 3)
    (match (motive := SignType → Fin 3) zero with
      | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
    (match (motive := SignType → Fin 3) b with
      | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a b : SignType
zero :
  (match (motive := SignType → Fin 3) SignType.zero * b with
    | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.zero with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) b with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
⊢ (match (motive := SignType → Fin 3) a * b with
    | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) a with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) b with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
have neg : (match (motive := SignType → Fin 3) neg * b with
  | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
  | pos => ⟨1, fin3Equiv._proof_4⟩
  | neg => ⟨2, fin3Equiv._proof_5⟩) =
  HMul.hMul (α := Fin 3) (β := Fin 3)
    (match (motive := SignType → Fin 3) neg with
      | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
    (match (motive := SignType → Fin 3) b with
      | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
a b : SignType
zero :
  (match (motive := SignType → Fin 3) SignType.zero * b with
    | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | SignType.neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.zero with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) b with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
neg :
  (match (motive := SignType → Fin 3) SignType.neg * b with
    | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | SignType.neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.neg with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) b with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
⊢ (match (motive := SignType → Fin 3) a * b with
    | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | SignType.neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) a with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) b with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
have pos : (match (motive := SignType → Fin 3) pos * b with
  | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
  | pos => ⟨1, fin3Equiv._proof_4⟩
  | SignType.neg => ⟨2, fin3Equiv._proof_5⟩) =
  HMul.hMul (α := Fin 3) (β := Fin 3)
    (match (motive := SignType → Fin 3) pos with
      | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
    (match (motive := SignType → Fin 3) b with
      | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
⊢ (match (motive := SignType → Fin 3) zero * b with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) zero with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) b with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
have zero : (match (motive := SignType → Fin 3) zero * zero with
  | zero => ⟨0, fin3Equiv._proof_3⟩
  | pos => ⟨1, fin3Equiv._proof_4⟩
  | neg => ⟨2, fin3Equiv._proof_5⟩) =
  HMul.hMul (α := Fin 3) (β := Fin 3)
    (match (motive := SignType → Fin 3) zero with
      | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
    (match (motive := SignType → Fin 3) zero with
      | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
zero :
  (match (motive := SignType → Fin 3) SignType.zero * SignType.zero with
    | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.zero with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) SignType.zero with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
⊢ (match (motive := SignType → Fin 3) SignType.zero * b with
    | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.zero with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) b with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
have zero₁ : (match (motive := SignType → Fin 3) SignType.zero * neg with
  | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
  | pos => ⟨1, fin3Equiv._proof_4⟩
  | neg => ⟨2, fin3Equiv._proof_5⟩) =
  HMul.hMul (α := Fin 3) (β := Fin 3)
    (match (motive := SignType → Fin 3) SignType.zero with
      | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
    (match (motive := SignType → Fin 3) neg with
      | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
zero :
  (match (motive := SignType → Fin 3) SignType.zero * SignType.zero with
    | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.zero with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) SignType.zero with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
zero₁ :
  (match (motive := SignType → Fin 3) SignType.zero * neg with
    | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.zero with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) neg with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
⊢ (match (motive := SignType → Fin 3) SignType.zero * b with
    | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.zero with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) b with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
have zero₂ : (match (motive := SignType → Fin 3) SignType.zero * pos with
  | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
  | pos => ⟨1, fin3Equiv._proof_4⟩
  | neg => ⟨2, fin3Equiv._proof_5⟩) =
  HMul.hMul (α := Fin 3) (β := Fin 3)
    (match (motive := SignType → Fin 3) SignType.zero with
      | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
    (match (motive := SignType → Fin 3) pos with
      | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
⊢ (match (motive := SignType → Fin 3) neg * b with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) neg with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) b with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
have neg : (match (motive := SignType → Fin 3) neg * zero with
  | zero => ⟨0, fin3Equiv._proof_3⟩
  | pos => ⟨1, fin3Equiv._proof_4⟩
  | neg => ⟨2, fin3Equiv._proof_5⟩) =
  HMul.hMul (α := Fin 3) (β := Fin 3)
    (match (motive := SignType → Fin 3) neg with
      | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
    (match (motive := SignType → Fin 3) zero with
      | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
neg :
  (match (motive := SignType → Fin 3) SignType.neg * zero with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | SignType.neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.neg with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) zero with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
⊢ (match (motive := SignType → Fin 3) SignType.neg * b with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | SignType.neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.neg with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) b with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
have neg₁ : (match (motive := SignType → Fin 3) SignType.neg * SignType.neg with
  | zero => ⟨0, fin3Equiv._proof_3⟩
  | pos => ⟨1, fin3Equiv._proof_4⟩
  | SignType.neg => ⟨2, fin3Equiv._proof_5⟩) =
  HMul.hMul (α := Fin 3) (β := Fin 3)
    (match (motive := SignType → Fin 3) SignType.neg with
      | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
    (match (motive := SignType → Fin 3) SignType.neg with
      | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
neg :
  (match (motive := SignType → Fin 3) SignType.neg * zero with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | SignType.neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.neg with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) zero with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
neg₁ :
  (match (motive := SignType → Fin 3) SignType.neg * SignType.neg with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | SignType.neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.neg with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) SignType.neg with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
⊢ (match (motive := SignType → Fin 3) SignType.neg * b with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | SignType.neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.neg with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) b with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
have neg₂ : (match (motive := SignType → Fin 3) SignType.neg * pos with
  | zero => ⟨0, fin3Equiv._proof_3⟩
  | pos => ⟨1, fin3Equiv._proof_4⟩
  | SignType.neg => ⟨2, fin3Equiv._proof_5⟩) =
  HMul.hMul (α := Fin 3) (β := Fin 3)
    (match (motive := SignType → Fin 3) SignType.neg with
      | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
    (match (motive := SignType → Fin 3) pos with
      | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sign.Defs (goal)
Goal:
b : SignType
⊢ (match (motive := SignType → Fin 3) pos * b with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) pos with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) b with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
have pos : (match (motive := SignType → Fin 3) pos * zero with
  | zero => ⟨0, fin3Equiv._proof_3⟩
  | pos => ⟨1, fin3Equiv._proof_4⟩
  | neg => ⟨2, fin3Equiv._proof_5⟩) =
  HMul.hMul (α := Fin 3) (β := Fin 3)
    (match (motive := SignType → Fin 3) pos with
      | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
    (match (motive := SignType → Fin 3) zero with
      | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
      | pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
      | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
      Fin 3)
Tactic: cases b
Cleared hypotheses: b