awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : DecidableEq α
s : Finset α
f : α → ℤ
refine_1 :
  card.{u} (α := (_ : ↥s) × ℕ) (Finset.sigma (α := fun (x : ↥s) ↦ ℕ) univ fun (a : ↥s) ↦ range (f (↑a : α)).natAbs) =
    ∑ a ∈ s, (f a).natAbs
refine_2 :
  ∀ a ∈ s,
    (∑ b ∈ Finset.sigma (α := fun (x : ↥s) ↦ ℕ) univ fun (a : ↥s) ↦ range (f (↑a : α)).natAbs,
        if (fun (a : (_ : ↥s) × ℕ) ↦ (↑(a.fst (β := fun (x : ↥s) ↦ ℕ)) : α)) b = a then
          (↑((fun (a : (_ : ↥s) × ℕ) ↦
                  ((sign : (a : ℤ) → SignType) (f (↑(a.fst (β := fun (x : ↥s) ↦ ℕ)) : α)) : SignType))
                b) :
            ℤ)
        else 0) =
      f a
⊢ ∃ (β : Type u) (t : Finset β) (sgn : β → SignType) (g : β → α),
    (∀ (b : β), g b ∈ s) ∧ #t = ∑ a ∈ s, (f a).natAbs ∧ ∀ a ∈ s, (∑ b ∈ t, if g b = a then (↑(sgn b) : ℤ) else 0) = f a

Tactic:
refine
    ⟨(Σ _ : { x // x ∈ s }, ℕ), Finset.univ.sigma fun a => range (f a).natAbs,
      fun a => sign (f a.1), fun a => a.1, fun a => a.1.2, ?_, ?_⟩
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : DecidableEq α
s : Finset α
f : α → ℤ
⊢ card.{u} (α := (_ : ↥s) × ℕ) (Finset.sigma (α := fun (x : ↥s) ↦ ℕ) univ fun (a : ↥s) ↦ range (f (↑a : α)).natAbs) =
    ∑ a ∈ s, (f a).natAbs

Tactic:
simp [sum_attach (f := fun a => (f a).natAbs)]

Premises used: Finset.sum_attach, Int.natAbs
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : DecidableEq α
s : Finset α
f : α → ℤ
x : α
hx : x ∈ s
⊢ (∑ b ∈ Finset.sigma (α := fun (x : ↥s) ↦ ℕ) univ fun (a : ↥s) ↦ range (f (↑a : α)).natAbs,
      if (fun (a : (_ : ↥s) × ℕ) ↦ (↑(a.fst (β := fun (x : ↥s) ↦ ℕ)) : α)) b = x then
        (↑((fun (a : (_ : ↥s) × ℕ) ↦
                ((sign : (a : ℤ) → SignType) (f (↑(a.fst (β := fun (x : ↥s) ↦ ℕ)) : α)) : SignType))
              b) :
          ℤ)
      else 0) =
    f x

Tactic:
simp [sum_sigma, hx, ← Int.sign_eq_sign, Int.sign_mul_abs, mul_comm |f _|,
      sum_attach (s := s) (f := fun y => if y = x then f y else 0)]

Premises used: abs, Finset.sum_sigma, Finset.sum_attach, mul_comm, Int.sign_eq_sign, OfNat.ofNat, Eq, Int.sign_mul_abs, ite
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : DecidableEq α
s : Finset α
f : α → ℤ
β : Type u
t : Finset β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
ht : #t = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b ∈ t, if g b = a then (↑(sgn b) : ℤ) else 0) = f a
⊢ Fintype.card.{u} ↥t = ∑ a ∈ s, (f a).natAbs

Tactic:
simp [ht]
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Nonempty α
inst_1 : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
obtain :
  ∀ (β : Type u) (w : Fintype β) (sgn : β → SignType) (g : β → α) (hg : ∀ (b : β), g b ∈ s)
    (hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs)
    (hf : ∀ a ∈ s, (∑ b : β, if g b = a then (↑(sgn b) : ℤ) else 0) = f a),
    ∃ (β : Type u) (x : Fintype β) (sgn : β → SignType) (g : β → α),
      (∀ (b : β), g b ∉ s → sgn b = 0) ∧
        Fintype.card β = n ∧ ∀ a ∈ s, (∑ i : β, if g i = a then (↑(sgn i) : ℤ) else 0) = f a
⊢ ∃ (β : Type u) (x : Fintype β) (sgn : β → SignType) (g : β → α),
    (∀ (b : β), g b ∉ s → sgn b = 0) ∧
      Fintype.card β = n ∧ ∀ a ∈ s, (∑ i : β, if g i = a then (↑(sgn i) : ℤ) else 0) = f a

Tactic:
obtain ⟨β, _, sgn, g, hg, hβ, hf⟩ := exists_signed_sum s f

Premises used: exists_signed_sum
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Nonempty α
inst_1 : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u
w : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b : β, if g b = a then (↑(sgn b) : ℤ) else 0) = f a
⊢ Fintype.card.{u} (β ⊕ Fin (n - ∑ i ∈ s, (f i).natAbs)) = n

Tactic:
simp [hβ, h]
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Nonempty α
inst_1 : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u
w : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b : β, if g b = a then (↑(sgn b) : ℤ) else 0) = f a
a : α
ha : a ∈ s
⊢ (∑ i : β ⊕ Fin (n - ∑ i ∈ s, (f i).natAbs),
      if Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) i = a then (↑(Sum.elim sgn 0 i) : ℤ)
      else 0) =
    f a

Tactic:
simp [hf _ ha]
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Nonempty α
inst_1 : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u
w : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b : β, if g b = a then (↑(sgn b) : ℤ) else 0) = f a
i :
  ∀ (b : β ⊕ Fin (n - ∑ i ∈ s, (f i).natAbs)),
    Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) b ∉ s → Sum.elim sgn 0 b = 0
⊢ ∃ (β : Type u) (x : Fintype β) (sgn : β → SignType) (g : β → α),
    (∀ (b : β), g b ∉ s → sgn b = 0) ∧
      Fintype.card β = n ∧ ∀ a ∈ s, (∑ i : β, if g i = a then (↑(sgn i) : ℤ) else 0) = f a

Tactic:
refine
    ⟨β ⊕ (Fin (n - ∑ i ∈ s, (f i).natAbs)), inferInstance, Sum.elim sgn 0,
      Sum.elim g (Classical.arbitrary (Fin (n - Finset.sum s fun i => Int.natAbs (f i)) → α)),
        ?_, by simp [hβ, h], fun a ha => by simp [hf _ ha]⟩
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Nonempty α
inst_1 : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u
w : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b : β, if g b = a then (↑(sgn b) : ℤ) else 0) = f a
b : β
hb :
  Sum.elim (β := Fin (n - ∑ i ∈ s, (f i).natAbs)) g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α))
      (Sum.inl b) ∉
    s
⊢ Sum.elim (β := Fin (n - ∑ i ∈ s, (f i).natAbs)) sgn 0 (Sum.inl b) = 0

Tactic:
cases hb (hg _)
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Nonempty α
inst_1 : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i ∈ s, (f i).natAbs ≤ n
β : Type u
w : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a ∈ s, (f a).natAbs
hf : ∀ a ∈ s, (∑ b : β, if g b = a then (↑(sgn b) : ℤ) else 0) = f a
b : Fin (n - ∑ i ∈ s, (f i).natAbs)
hb : Sum.elim g (Classical.arbitrary (Fin (n - ∑ i ∈ s, (f i).natAbs) → α)) (Sum.inr b) ∉ s
⊢ Sum.elim sgn 0 (Sum.inr b) = 0

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ zero = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ neg = -1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ pos = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
zero : SignType.zero = -1 ∨ SignType.zero = 0 ∨ SignType.zero = 1
neg : SignType.neg = -1 ∨ SignType.neg = 0 ∨ SignType.neg = 1
pos : SignType.pos = -1 ∨ SignType.pos = 0 ∨ SignType.pos = 1
⊢ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
cases a
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ zero = -1 ∨ zero = 0 ∨ zero = 1

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ neg = -1 ∨ neg = 0 ∨ neg = 1

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ pos = -1 ∨ pos = 0 ∨ pos = 1

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
a b : SignType
zero : Decidable (SignType.zero ≤ b)
neg : Decidable (SignType.neg ≤ b)
pos : Decidable (SignType.pos ≤ b)
⊢ Decidable (a ≤ b)

Tactic:
cases a
-- Module: Mathlib.Data.Sign.Defs
Goal:
b : SignType
zero : Decidable (SignType.zero ≤ SignType.zero)
zero₁ : Decidable (SignType.zero ≤ neg)
zero₂ : Decidable (SignType.zero ≤ pos)
⊢ Decidable (SignType.zero ≤ b)

Tactic:
cases b
-- Module: Mathlib.Data.Sign.Defs
Goal:
b : SignType
neg : Decidable (SignType.neg ≤ zero)
neg₁ : Decidable (SignType.neg ≤ SignType.neg)
neg₂ : Decidable (SignType.neg ≤ pos)
⊢ Decidable (SignType.neg ≤ b)

Tactic:
cases b
-- Module: Mathlib.Data.Sign.Defs
Goal:
b : SignType
pos : Decidable (SignType.pos ≤ zero)
pos₁ : Decidable (SignType.pos ≤ neg)
pos₂ : Decidable (SignType.pos ≤ SignType.pos)
⊢ Decidable (SignType.pos ≤ b)

Tactic:
cases b
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ zero ≤ zero

Tactic:
constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (zero ≤ zero)

Tactic:
exact isTrue (by constructor)

Premises used: Decidable.isTrue
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (zero ≤ zero)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

Premises used: Decidable.isTrue, Decidable.isFalse
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (zero ≤ neg)

Tactic:
exact isFalse (by rintro ⟨_⟩)

Premises used: Decidable.isFalse
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (zero ≤ neg)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

Premises used: Decidable.isTrue, Decidable.isFalse
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ zero ≤ pos

Tactic:
constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (zero ≤ pos)

Tactic:
exact isTrue (by constructor)

Premises used: Decidable.isTrue
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (zero ≤ pos)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

Premises used: Decidable.isTrue, Decidable.isFalse
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ neg ≤ zero

Tactic:
constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (neg ≤ zero)

Tactic:
exact isTrue (by constructor)

Premises used: Decidable.isTrue
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (neg ≤ zero)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

Premises used: Decidable.isTrue, Decidable.isFalse
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ neg ≤ neg

Tactic:
constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (neg ≤ neg)

Tactic:
exact isTrue (by constructor)

Premises used: Decidable.isTrue
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (neg ≤ neg)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

Premises used: Decidable.isTrue, Decidable.isFalse
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ neg ≤ pos

Tactic:
constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (neg ≤ pos)

Tactic:
exact isTrue (by constructor)

Premises used: Decidable.isTrue
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (neg ≤ pos)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

Premises used: Decidable.isTrue, Decidable.isFalse
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (pos ≤ zero)

Tactic:
exact isFalse (by rintro ⟨_⟩)

Premises used: Decidable.isFalse
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (pos ≤ zero)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

Premises used: Decidable.isTrue, Decidable.isFalse
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (pos ≤ neg)

Tactic:
exact isFalse (by rintro ⟨_⟩)

Premises used: Decidable.isFalse
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (pos ≤ neg)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

Premises used: Decidable.isTrue, Decidable.isFalse
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ pos ≤ pos

Tactic:
constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (pos ≤ pos)

Tactic:
exact isTrue (by constructor)

Premises used: Decidable.isTrue
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ Decidable (pos ≤ pos)

Tactic:
first | exact isTrue (by constructor) | exact isFalse (by rintro ⟨_⟩)

Premises used: Decidable.isTrue, Decidable.isFalse
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ ∀ (a b c : SignType), a * b * c = a * (b * c)

Tactic:
decide
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
zero : 1 * SignType.zero = SignType.zero
neg : 1 * SignType.neg = SignType.neg
pos : 1 * SignType.pos = SignType.pos
⊢ 1 * a = a

Tactic:
cases a
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ 1 * zero = zero

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ 1 * neg = neg

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ 1 * pos = pos

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
zero : SignType.zero * 1 = SignType.zero
neg : SignType.neg * 1 = SignType.neg
pos : SignType.pos * 1 = SignType.pos
⊢ a * 1 = a

Tactic:
cases a
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ zero * 1 = zero

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ neg * 1 = neg

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ pos * 1 = pos

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ ∀ (a b : SignType), a * b = b * a

Tactic:
decide
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
zero : 0 * SignType.zero = 0
neg : 0 * SignType.neg = 0
pos : 0 * SignType.pos = 0
⊢ 0 * a = 0

Tactic:
cases a
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ 0 * zero = 0

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ 0 * neg = 0

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ 0 * pos = 0

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
zero : SignType.zero * 0 = 0
neg : SignType.neg * 0 = 0
pos : SignType.pos * 0 = 0
⊢ a * 0 = 0

Tactic:
cases a
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ zero * 0 = 0

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ neg * 0 = 0

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ pos * 0 = 0

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
ha : a ≠ 0
zero : ∀ (ha : SignType.zero ≠ 0), SignType.zero * id SignType.zero = 1
neg : ∀ (ha : SignType.neg ≠ 0), SignType.neg * id SignType.neg = 1
pos : ∀ (ha : SignType.pos ≠ 0), SignType.pos * id SignType.pos = 1
⊢ a * id a = 1

Tactic:
cases a
-- Module: Mathlib.Data.Sign.Defs
Goal:
ha : zero ≠ 0
⊢ zero * id zero = 1

Tactic:
trivial
-- Module: Mathlib.Data.Sign.Defs
Goal:
ha : neg ≠ 0
⊢ neg * id neg = 1

Tactic:
trivial
-- Module: Mathlib.Data.Sign.Defs
Goal:
ha : pos ≠ 0
⊢ pos * id pos = 1

Tactic:
trivial
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
zero : SignType.zero ≤ SignType.zero
neg : SignType.neg ≤ SignType.neg
pos : SignType.pos ≤ SignType.pos
⊢ a ≤ a

Tactic:
cases a
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ ∀ (a b c : SignType), a ≤ b → b ≤ c → a ≤ c

Tactic:
decide
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ ∀ (a b : SignType), a ≤ b → b ≤ a → a = b

Tactic:
decide
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ ∀ (a b : SignType), a ≤ b ∨ b ≤ a

Tactic:
decide
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ ∀ (a : SignType), -1 ≤ a

Tactic:
LE.of_neg

Premises used: SignType.LE.of_neg
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ ∀ (a : SignType), -1 ≤ a

Tactic:
exact LE.of_neg

Premises used: SignType.LE.of_neg
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ - -zero = zero

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ - -neg = neg

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ - -pos = pos

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ -zero * zero = -(zero * zero)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ -zero * neg = -(zero * neg)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ -zero * pos = -(zero * pos)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ -neg * zero = -(neg * zero)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ -neg * neg = -(neg * neg)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ -neg * pos = -(neg * pos)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ -pos * zero = -(pos * zero)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ -pos * neg = -(pos * neg)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ -pos * pos = -(pos * pos)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ zero * -zero = -(zero * zero)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ zero * -neg = -(zero * neg)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ zero * -pos = -(zero * pos)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ neg * -zero = -(neg * zero)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ neg * -neg = -(neg * neg)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ neg * -pos = -(neg * pos)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ pos * -zero = -(pos * zero)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ pos * -neg = -(pos * neg)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ pos * -pos = -(pos * pos)

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ LT.lt (α := ℕ) 0 3

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ LT.lt (α := ℕ) 1 3

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : SignType
⊢ LT.lt (α := ℕ) 2 3

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
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⟩
            | SignType.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⟩
            | SignType.pos => ⟨1, fin3Equiv._proof_4⟩
            | SignType.neg => ⟨2, fin3Equiv._proof_5⟩ :
            Fin 3))
        SignType.neg) =
    SignType.neg
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⟩
            | SignType.pos => ⟨1, fin3Equiv._proof_4⟩
            | SignType.neg => ⟨2, fin3Equiv._proof_5⟩ :
            Fin 3))
        SignType.pos) =
    SignType.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⟩
            | SignType.pos => ⟨1, fin3Equiv._proof_4⟩
            | SignType.neg => ⟨2, fin3Equiv._proof_5⟩ :
            Fin 3))
        a) =
    a

Tactic:
cases a
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ (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
            | zero => ⟨0, fin3Equiv._proof_3⟩
            | pos => ⟨1, fin3Equiv._proof_4⟩
            | neg => ⟨2, fin3Equiv._proof_5⟩ :
            Fin 3))
        zero) =
    zero

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ (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
            | zero => ⟨0, fin3Equiv._proof_3⟩
            | pos => ⟨1, fin3Equiv._proof_4⟩
            | neg => ⟨2, fin3Equiv._proof_5⟩ :
            Fin 3))
        neg) =
    neg

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
⊢ (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
            | zero => ⟨0, fin3Equiv._proof_3⟩
            | pos => ⟨1, fin3Equiv._proof_4⟩
            | neg => ⟨2, fin3Equiv._proof_5⟩ :
            Fin 3))
        pos) =
    pos

Tactic:
rfl
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : Fin 3
isLt : LT.lt (α := ℕ) 0 3
⊢ (fun (a : SignType) ↦
        (match (motive := SignType → Fin 3) a with
          | zero => ⟨0, fin3Equiv._proof_3⟩
          | pos => ⟨1, fin3Equiv._proof_4⟩
          | neg => ⟨2, fin3Equiv._proof_5⟩ :
          Fin 3))
      ((fun (a : Fin 3) ↦
          (match (motive := Fin 3 → SignType) a with
            | ⟨0, isLt⟩ => 0
            | ⟨1, isLt⟩ => 1
            | ⟨2, isLt⟩ => -1 :
            SignType))
        ⟨0, isLt⟩) =
    (⟨0, isLt⟩ : Fin 3)

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : Fin 3
isLt : LT.lt (α := ℕ) 1 3
⊢ (fun (a : SignType) ↦
        (match (motive := SignType → Fin 3) a with
          | zero => ⟨0, fin3Equiv._proof_3⟩
          | pos => ⟨1, fin3Equiv._proof_4⟩
          | neg => ⟨2, fin3Equiv._proof_5⟩ :
          Fin 3))
      ((fun (a : Fin 3) ↦
          (match (motive := Fin 3 → SignType) a with
            | ⟨0, isLt⟩ => 0
            | ⟨1, isLt⟩ => 1
            | ⟨2, isLt⟩ => -1 :
            SignType))
        ⟨1, isLt⟩) =
    (⟨1, isLt⟩ : Fin 3)

Tactic:
simp
-- Module: Mathlib.Data.Sign.Defs
Goal:
a : Fin 3
isLt : LT.lt (α := ℕ) 2 3
⊢ (fun (a : SignType) ↦
        (match (motive := SignType → Fin 3) a with
          | zero => ⟨0, fin3Equiv._proof_3⟩
          | pos => ⟨1, fin3Equiv._proof_4⟩
          | neg => ⟨2, fin3Equiv._proof_5⟩ :
          Fin 3))
      ((fun (a : Fin 3) ↦
          (match (motive := Fin 3 → SignType) a with
            | ⟨0, isLt⟩ => 0
            | ⟨1, isLt⟩ => 1
            | ⟨2, isLt⟩ => -1 :
            SignType))
        ⟨2, isLt⟩) =
    (⟨2, isLt⟩ : Fin 3)

Tactic:
simp