awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sign.Basic
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
⊢ (↑(zero * neg) : α) = HMul.hMul (α := α) (↑zero : α) (↑neg : α)

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Premises used: SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Data.Sign.Basic
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
⊢ (↑(zero * pos) : α) = HMul.hMul (α := α) (↑zero : α) (↑pos : α)

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Premises used: SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Data.Sign.Basic
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
⊢ (↑(neg * zero) : α) = HMul.hMul (α := α) (↑neg : α) (↑zero : α)

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Premises used: SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Data.Sign.Basic
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
⊢ (↑(neg * neg) : α) = HMul.hMul (α := α) (↑neg : α) (↑neg : α)

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Premises used: SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Data.Sign.Basic
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
⊢ (↑(neg * pos) : α) = HMul.hMul (α := α) (↑neg : α) (↑pos : α)

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Premises used: SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Data.Sign.Basic
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
⊢ (↑(pos * zero) : α) = HMul.hMul (α := α) (↑pos : α) (↑zero : α)

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Premises used: SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Data.Sign.Basic
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
⊢ (↑(pos * neg) : α) = HMul.hMul (α := α) (↑pos : α) (↑neg : α)

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Premises used: SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Data.Sign.Basic
Goal:
α_1 : Type u
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
⊢ (↑(pos * pos) : α) = HMul.hMul (α := α) (↑pos : α) (↑pos : α)

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Premises used: SignType.neg_eq_neg_one, SignType.zero_eq_zero, SignType.pos_eq_one
-- Module: Mathlib.Data.Sign.Basic
Goal:
⊢ Eq (α := Finset SignType) Finset.univ {0, -1, 1}

Tactic:
decide
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u_1
f : SignType → α
rw : (↑(Finset.image f {0, -1, 1}) : Set α) = {f zero, f neg, f pos}
⊢ Set.range f = {f zero, f neg, f pos}

Tactic:
rw [← Fintype.coe_image_univ, univ_eq]

Premises used: Fintype.coe_image_univ, SignType.univ_eq
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u_1
f : SignType → α
classical : (↑(Finset.image f {0, -1, 1}) : Set α) = {f zero, f neg, f pos}
⊢ Set.range f = {f zero, f neg, f pos}

Tactic:
classical rw [← Fintype.coe_image_univ, univ_eq]

Premises used: Fintype.coe_image_univ, SignType.univ_eq
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u_1
f : SignType → α
⊢ (↑(Finset.image f {0, -1, 1}) : Set α) = {f zero, f neg, f pos}

Tactic:
simp [Finset.coe_insert]

Premises used: Finset.coe_insert
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u_1
f : SignType → α
⊢ (↑(Finset.image f {0, -1, 1}) : Set α) = {f zero, f neg, f pos}

Tactic:
classical simp [Finset.coe_insert]

Premises used: Finset.coe_insert
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u_1
inst : MulZeroOneClass α
inst_1 : HasDistribNeg α
a b : SignType
⊢ (↑(a * b) : α) = HMul.hMul (α := α) (↑a : α) (↑b : α)

Tactic:
map_mul SignType.castHom _ _

Premises used: SignType.cast, SignType.castHom, map_mul
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u_1
inst : MonoidWithZero α
inst_1 : HasDistribNeg α
a : SignType
k : ℕ
⊢ (↑(a ^ k) : α) = HPow.hPow (α := α) (↑a : α) k

Tactic:
map_pow SignType.castHom _ _

Premises used: SignType.cast, SignType.castHom, map_pow
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : HasDistribNeg α
a : SignType
k : ℤ
⊢ (↑(a ^ k) : α) = HPow.hPow (α := α) (↑a : α) k

Tactic:
map_zpow₀ SignType.castHom _ _

Premises used: SignType.cast, SignType.castHom, map_zpow₀
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
inst_3 : Nontrivial α
inst_4 : DecidableLT α
n : ℤ
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) (↑n : α) : SignType) ((sign : (a : ℤ) → SignType) n : SignType)

Tactic:
simp only [sign_apply, Int.cast_pos, Int.cast_lt_zero]

Premises used: Int.cast_lt_zero, sign_apply, Int.cast_pos
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
inl :
  ∀ (hx : x < 0),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
inr :
  ∀ (hx : x = 0),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
inr₁ :
  ∀ (hx : 0 < x),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)

Tactic:
rcases lt_trichotomy x 0 with (hx | hx | hx)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : x < 0
inl :
  ∀ (hy : y < 0),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
inl₁ :
  ∀ (hy : y = 0),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
inl₂ :
  ∀ (hy : 0 < y),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)

Tactic:
rcases lt_trichotomy y 0 with (hy | hy | hy)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : x = 0
inr :
  ∀ (hy : y < 0),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
inr₁ :
  ∀ (hy : y = 0),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
inr₂ :
  ∀ (hy : 0 < y),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)

Tactic:
rcases lt_trichotomy y 0 with (hy | hy | hy)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : 0 < x
inr :
  ∀ (hy : y < 0),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
inr₁ :
  ∀ (hy : y = 0),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
inr₂ :
  ∀ (hy : 0 < y),
    (sign : (a : α) → SignType) (x * y) =
      HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
        ((sign : (a : α) → SignType) y : SignType)
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)

Tactic:
rcases lt_trichotomy y 0 with (hy | hy | hy)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : x < 0
hy : y < 0
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, mul_pos_of_neg_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : x < 0
hy : y = 0
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, mul_pos_of_neg_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : x < 0
hy : 0 < y
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, mul_pos_of_neg_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : x = 0
hy : y < 0
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, mul_pos_of_neg_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : x = 0
hy : y = 0
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, mul_pos_of_neg_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : x = 0
hy : 0 < y
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, mul_pos_of_neg_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : 0 < x
hy : y < 0
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, mul_pos_of_neg_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : 0 < x
hy : y = 0
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, mul_pos_of_neg_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x y : α
hx : 0 < x
hy : 0 < y
⊢ (sign : (a : α) → SignType) (x * y) =
    HMul.hMul (α := SignType) (β := SignType) ((sign : (a : α) → SignType) x : SignType)
      ((sign : (a : α) → SignType) y : SignType)

Tactic:
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Premises used: mul_neg_of_neg_of_pos, mul_pos_of_neg_of_neg, mul_neg_of_pos_of_neg
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
inl : ∀ (hx : x < 0), (↑((sign : (a : α) → SignType) x) : α) * |x| = x
inr : HMul.hMul (α := α) (↑((sign : (a : α) → SignType) 0) : α) |0| = 0
inr₁ : ∀ (hx : 0 < x), (↑((sign : (a : α) → SignType) x) : α) * |x| = x
⊢ (↑((sign : (a : α) → SignType) x) : α) * |x| = x

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ (↑((sign : (a : α) → SignType) x) : α) * |x| = x

Tactic:
simp [*, abs_of_pos, abs_of_neg]

Premises used: abs_of_neg, abs_of_pos
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
⊢ HMul.hMul (α := α) (↑((sign : (a : α) → SignType) 0) : α) |0| = 0

Tactic:
simp [*, abs_of_pos, abs_of_neg]

Premises used: abs_of_neg, abs_of_pos
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ (↑((sign : (a : α) → SignType) x) : α) * |x| = x

Tactic:
simp [*, abs_of_pos, abs_of_neg]

Premises used: abs_of_neg, abs_of_pos
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
inl : ∀ (hx : x < 0), |x| * (↑((sign : (a : α) → SignType) x) : α) = x
inr : HMul.hMul (α := α) |0| (↑((sign : (a : α) → SignType) 0) : α) = 0
inr₁ : ∀ (hx : 0 < x), |x| * (↑((sign : (a : α) → SignType) x) : α) = x
⊢ |x| * (↑((sign : (a : α) → SignType) x) : α) = x

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ |x| * (↑((sign : (a : α) → SignType) x) : α) = x

Tactic:
simp [*, abs_of_pos, abs_of_neg]

Premises used: abs_of_neg, abs_of_pos
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
⊢ HMul.hMul (α := α) |0| (↑((sign : (a : α) → SignType) 0) : α) = 0

Tactic:
simp [*, abs_of_pos, abs_of_neg]

Premises used: abs_of_neg, abs_of_pos
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ |x| * (↑((sign : (a : α) → SignType) x) : α) = x

Tactic:
simp [*, abs_of_pos, abs_of_neg]

Premises used: abs_of_neg, abs_of_pos
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
inl : ∀ (hx : x < 0), (↑((sign : (a : α) → SignType) x) : α) * x = |x|
inr : HMul.hMul (α := α) (↑((sign : (a : α) → SignType) 0) : α) 0 = |0|
inr₁ : ∀ (hx : 0 < x), (↑((sign : (a : α) → SignType) x) : α) * x = |x|
⊢ (↑((sign : (a : α) → SignType) x) : α) * x = |x|

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ (↑((sign : (a : α) → SignType) x) : α) * x = |x|

Tactic:
simp [*, abs_of_pos, abs_of_neg]

Premises used: abs_of_neg, abs_of_pos
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
⊢ HMul.hMul (α := α) (↑((sign : (a : α) → SignType) 0) : α) 0 = |0|

Tactic:
simp [*, abs_of_pos, abs_of_neg]

Premises used: abs_of_neg, abs_of_pos
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ (↑((sign : (a : α) → SignType) x) : α) * x = |x|

Tactic:
simp [*, abs_of_pos, abs_of_neg]

Premises used: abs_of_neg, abs_of_pos
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
inl : ∀ (hx : x < 0), x * (↑((sign : (a : α) → SignType) x) : α) = |x|
inr : HMul.hMul (α := α) 0 (↑((sign : (a : α) → SignType) 0) : α) = |0|
inr₁ : ∀ (hx : 0 < x), x * (↑((sign : (a : α) → SignType) x) : α) = |x|
⊢ x * (↑((sign : (a : α) → SignType) x) : α) = |x|

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ x * (↑((sign : (a : α) → SignType) x) : α) = |x|

Tactic:
simp [*, abs_of_pos, abs_of_neg]

Premises used: abs_of_neg, abs_of_pos
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
⊢ HMul.hMul (α := α) 0 (↑((sign : (a : α) → SignType) 0) : α) = |0|

Tactic:
simp [*, abs_of_pos, abs_of_neg]

Premises used: abs_of_neg, abs_of_pos
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ x * (↑((sign : (a : α) → SignType) x) : α) = |x|

Tactic:
simp [*, abs_of_pos, abs_of_neg]

Premises used: abs_of_neg, abs_of_pos
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
x : α
n : ℕ
⊢ (sign : (a : α) → SignType) (x ^ n) = HPow.hPow (α := SignType) ((sign : (a : α) → SignType) x : SignType) n

Tactic:
map_pow signHom x n

Premises used: signHom, map_pow, ite
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
t : SignType
h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = t
zero :
  ∀ (h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = SignType.zero),
    (sign : (a : α) → SignType) (∑ i ∈ s, f i) = SignType.zero
neg :
  ∀ (h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = SignType.neg),
    (sign : (a : α) → SignType) (∑ i ∈ s, f i) = SignType.neg
pos :
  ∀ (h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = SignType.pos),
    (sign : (a : α) → SignType) (∑ i ∈ s, f i) = SignType.pos
⊢ (sign : (a : α) → SignType) (∑ i ∈ s, f i) = t

Tactic:
cases t
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = SignType.zero
zero : ∀ (h : ∀ i ∈ s, f i = 0), Eq.{u + 1} (α := α) (∑ i ∈ s, f i) 0
⊢ (sign : (a : α) → SignType) (∑ i ∈ s, f i) = SignType.zero

Tactic:
simp_rw [zero_eq_zero, sign_eq_zero_iff] at h ⊢

Premises used: SignType.zero_eq_zero, sign_eq_zero_iff
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, f i = 0
⊢ Eq.{u + 1} (α := α) (∑ i ∈ s, f i) 0

Tactic:
Finset.sum_eq_zero h

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, f i = 0
⊢ Eq.{u + 1} (α := α) (∑ i ∈ s, f i) 0

Tactic:
exact Finset.sum_eq_zero h

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = SignType.neg
neg : ∀ (h : ∀ i ∈ s, f i < 0), LT.lt.{u} (α := α) (∑ i ∈ s, f i) 0
⊢ (sign : (a : α) → SignType) (∑ i ∈ s, f i) = SignType.neg

Tactic:
simp_rw [neg_eq_neg_one, sign_eq_neg_one_iff] at h ⊢

Premises used: SignType.neg_eq_neg_one, sign_eq_neg_one_iff
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, f i < 0
⊢ LT.lt.{u} (α := α) (∑ i ∈ s, f i) 0

Tactic:
Finset.sum_neg h hs

Premises used: Finset.sum_neg
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, f i < 0
⊢ LT.lt.{u} (α := α) (∑ i ∈ s, f i) 0

Tactic:
exact Finset.sum_neg h hs

Premises used: Finset.sum_neg
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, (sign : (a : α) → SignType) (f i) = SignType.pos
pos : ∀ (h : ∀ i ∈ s, 0 < f i), LT.lt.{u} (α := α) 0 (∑ i ∈ s, f i)
⊢ (sign : (a : α) → SignType) (∑ i ∈ s, f i) = SignType.pos

Tactic:
simp_rw [pos_eq_one, sign_eq_one_iff] at h ⊢

Premises used: SignType.pos_eq_one, sign_eq_one_iff
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, 0 < f i
⊢ LT.lt.{u} (α := α) 0 (∑ i ∈ s, f i)

Tactic:
Finset.sum_pos h hs

Premises used: Finset.sum_pos
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, 0 < f i
⊢ LT.lt.{u} (α := α) 0 (∑ i ∈ s, f i)

Tactic:
exact Finset.sum_pos h hs

Premises used: Finset.sum_pos
-- Module: Mathlib.Data.Sign.Basic
Goal:
α : Type u
inst : DecidableEq α
s : Finset α
f : α → ℤ
⊢ ∃ (β : 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:
⟨(Σ _ : { 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, ?_, ?_⟩

Premises used: Finset.univ, Finset.sigma, Sigma.fst, Finset.range, Nat, And.intro, Int.natAbs, Exists.intro, Subtype.val, DFunLike.coe, SignType.sign, Sigma, Subtype.property