awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sign.Defs
Goal:
a b : SignType
zero :
  (match (motive := SignType → Fin 3) SignType.zero * b with
    | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
    | SignType.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)
        | SignType.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)
        | SignType.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⟩
    | SignType.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)
        | SignType.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)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
pos :
  (match (motive := SignType → Fin 3) SignType.pos * b with
    | SignType.zero => ⟨0, fin3Equiv._proof_3⟩
    | SignType.pos => ⟨1, fin3Equiv._proof_4⟩
    | SignType.neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.pos with
        | SignType.zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.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)
        | SignType.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⟩
    | SignType.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)
        | SignType.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)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | SignType.neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)

Tactic:
cases a
-- Module: Mathlib.Data.Sign.Defs
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)
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)
⊢ (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)

Tactic:
cases b
-- Module: Mathlib.Data.Sign.Defs
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)
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)
⊢ (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)

Tactic:
cases b
-- Module: Mathlib.Data.Sign.Defs
Goal:
b : SignType
pos :
  (match (motive := SignType → Fin 3) SignType.pos * zero with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | SignType.pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.pos with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.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)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
pos₁ :
  (match (motive := SignType → Fin 3) SignType.pos * neg with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | SignType.pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.pos with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) neg with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
pos₂ :
  (match (motive := SignType → Fin 3) SignType.pos * SignType.pos with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | SignType.pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.pos with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
      (match (motive := SignType → Fin 3) SignType.pos with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)
⊢ (match (motive := SignType → Fin 3) SignType.pos * b with
    | zero => ⟨0, fin3Equiv._proof_3⟩
    | SignType.pos => ⟨1, fin3Equiv._proof_4⟩
    | neg => ⟨2, fin3Equiv._proof_5⟩) =
    HMul.hMul (α := Fin 3) (β := Fin 3)
      (match (motive := SignType → Fin 3) SignType.pos with
        | zero => (⟨0, fin3Equiv._proof_3⟩ : Fin 3)
        | SignType.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)
        | SignType.pos => (⟨1, fin3Equiv._proof_4⟩ : Fin 3)
        | neg => (⟨2, fin3Equiv._proof_5⟩ : Fin 3) :
        Fin 3)

Tactic:
cases b
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ (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:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ (match (motive := SignType → Fin 3) zero * neg 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) 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)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ (match (motive := SignType → Fin 3) zero * pos 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) 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)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ (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:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ (match (motive := SignType → Fin 3) neg * neg 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) 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)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ (match (motive := SignType → Fin 3) neg * pos 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) 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)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ (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:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ (match (motive := SignType → Fin 3) pos * neg 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) 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)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ (match (motive := SignType → Fin 3) pos * pos 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) 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)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ 0 ≤ a ↔ a = 0 ∨ a = 1

Tactic:
decide +revert
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ 0 ≤ a ↔ a ≠ -1

Tactic:
decide +revert
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ -1 < a ↔ 0 ≤ a

Tactic:
decide +revert
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ a ≤ 0 ↔ a = -1 ∨ a = 0

Tactic:
decide +revert
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ a ≤ 0 ↔ a ≠ 1

Tactic:
decide +revert
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ a < 1 ↔ a ≤ 0

Tactic:
decide +revert
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ a < 0 ↔ a = -1

Tactic:
decide +revert
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ a ≤ -1 ↔ a = -1

Tactic:
le_bot_iff

Premises used: le_bot_iff
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ 0 < a ↔ a = 1

Tactic:
decide +revert
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ 1 ≤ a ↔ a = 1

Tactic:
top_le_iff

Premises used: top_le_iff
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ -1 ≤ a

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ a ≤ 1

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ ¬a < -1

Tactic:
not_lt_bot

Premises used: not_lt_bot
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ ¬1 < a

Tactic:
not_top_lt

Premises used: not_top_lt
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ a = -a ↔ a = 0

Tactic:
decide +revert
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ -a = a ↔ a = 0

Tactic:
decide +revert
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ -a = 0 ↔ a = 0

Tactic:
decide +revert
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ LT.lt (α := SignType) (-1) 1

Tactic:
bot_lt_top

Premises used: bot_lt_top
-- Module: Mathlib.Data.Sign.Defs
Goal:
a b : SignType
⊢ -a ≤ -b ↔ b ≤ a

Tactic:
decide +revert
-- Module: Mathlib.Data.Sign.Defs
Goal:
a b : SignType
⊢ -a < -b ↔ b < a

Tactic:
decide +revert
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Neg α
β : Type u_2
inst_3 : One β
inst_4 : Neg β
inst_5 : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
s : SignType
zero : f (↑SignType.zero : α) = (↑SignType.zero : β)
neg : f (↑SignType.neg : α) = (↑SignType.neg : β)
pos : f (↑SignType.pos : α) = (↑SignType.pos : β)
⊢ f (↑s : α) = (↑s : β)

Tactic:
cases s
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Neg α
β : Type u_2
inst_3 : One β
inst_4 : Neg β
inst_5 : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
⊢ f (↑zero : α) = (↑zero : β)

Tactic:
simp only [SignType.cast, h₁, h₂, h₃]

Premises used: SignType.cast
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Neg α
β : Type u_2
inst_3 : One β
inst_4 : Neg β
inst_5 : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
⊢ f (↑neg : α) = (↑neg : β)

Tactic:
simp only [SignType.cast, h₁, h₂, h₃]

Premises used: SignType.cast
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Neg α
β : Type u_2
inst_3 : One β
inst_4 : Neg β
inst_5 : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
⊢ f (↑pos : α) = (↑pos : β)

Tactic:
simp only [SignType.cast, h₁, h₂, h₃]

Premises used: SignType.cast
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : AddGroupWithOne α
inst_1 : One β
inst_2 : SubtractionMonoid β
inst_3 : FunLike F α β
inst_4 : AddMonoidHomClass F α β
inst_5 : OneHomClass F α β
f : F
s : SignType
h₁ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)
h₂ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)
h₃ : Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (-1) : β) (-1 : β)
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (↑s : α) : β) ((↑s : β) : β)

Tactic:
apply map_cast'

Premises used: SignType.map_cast'
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : AddGroupWithOne α
inst_1 : One β
inst_2 : SubtractionMonoid β
inst_3 : FunLike F α β
inst_4 : AddMonoidHomClass F α β
inst_5 : OneHomClass F α β
f : F
s : SignType
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : AddGroupWithOne α
inst_1 : One β
inst_2 : SubtractionMonoid β
inst_3 : FunLike F α β
inst_4 : AddMonoidHomClass F α β
inst_5 : OneHomClass F α β
f : F
s : SignType
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_2
β : Type u_3
F : Type u_4
inst : AddGroupWithOne α
inst_1 : One β
inst_2 : SubtractionMonoid β
inst_3 : FunLike F α β
inst_4 : AddMonoidHomClass F α β
inst_5 : OneHomClass F α β
f : F
s : SignType
⊢ Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) (-1) : β) (-1 : β)

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Neg α
⊢ Eq.{u_1 + 1} (α := α) (↑0 : α) 0

Tactic:
rfl

Premises used: SignType.cast, rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Neg α
⊢ Eq.{u_1 + 1} (α := α) (↑1 : α) 1

Tactic:
rfl

Premises used: SignType.cast, rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Neg α
⊢ Eq.{u_1 + 1} (α := α) (↑(-1) : α) (-1)

Tactic:
rfl

Premises used: SignType.cast, rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_2
inst : One α
inst_1 : SubtractionMonoid α
s : SignType
zero : Eq.{u_2 + 1} (α := α) (↑(-SignType.zero) : α) (-(↑SignType.zero : α))
neg : Eq.{u_2 + 1} (α := α) (↑(-SignType.neg) : α) (-(↑SignType.neg : α))
pos : Eq.{u_2 + 1} (α := α) (↑(-SignType.pos) : α) (-(↑SignType.pos : α))
⊢ Eq.{u_2 + 1} (α := α) (↑(-s) : α) (-(↑s : α))

Tactic:
cases s
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_2
inst : One α
inst_1 : SubtractionMonoid α
⊢ Eq.{u_2 + 1} (α := α) (↑(-zero) : α) (-(↑zero : α))

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_2
inst : One α
inst_1 : SubtractionMonoid α
⊢ Eq.{u_2 + 1} (α := α) (↑(-neg) : α) (-(↑neg : α))

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_2
inst : One α
inst_1 : SubtractionMonoid α
⊢ Eq.{u_2 + 1} (α := α) (↑(-pos) : α) (-(↑pos : α))

Tactic:
simp