mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero
⊢ zero ≤ zero

pp: case neg
⊢ neg ≤ neg

pp: case pos
⊢ pos ≤ pos

Tactic:
<;>

Goal state after:
case zero
⊢ zero ≤ zero

case neg
⊢ neg ≤ neg

case pos
⊢ pos ≤ pos
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero
⊢ - -zero = zero

pp: case neg
⊢ - -neg = neg

pp: case pos
⊢ - -pos = pos

Tactic:
<;>

Goal state after:
case zero
⊢ - -zero = zero

case neg
⊢ - -neg = neg

case pos
⊢ - -pos = pos
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero.zero
⊢ -zero * zero = -(zero * zero)

pp: case zero.neg
⊢ -zero * neg = -(zero * neg)

pp: case zero.pos
⊢ -zero * pos = -(zero * pos)

pp: case neg.zero
⊢ -neg * zero = -(neg * zero)

pp: case neg.neg
⊢ -neg * neg = -(neg * neg)

pp: case neg.pos
⊢ -neg * pos = -(neg * pos)

pp: case pos.zero
⊢ -pos * zero = -(pos * zero)

pp: case pos.neg
⊢ -pos * neg = -(pos * neg)

pp: case pos.pos
⊢ -pos * pos = -(pos * pos)

Tactic:
<;>

Goal state after:
case zero.zero
⊢ -zero * zero = -(zero * zero)

case zero.neg
⊢ -zero * neg = -(zero * neg)

case zero.pos
⊢ -zero * pos = -(zero * pos)

case neg.zero
⊢ -neg * zero = -(neg * zero)

case neg.neg
⊢ -neg * neg = -(neg * neg)

case neg.pos
⊢ -neg * pos = -(neg * pos)

case pos.zero
⊢ -pos * zero = -(pos * zero)

case pos.neg
⊢ -pos * neg = -(pos * neg)

case pos.pos
⊢ -pos * pos = -(pos * pos)
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero.zero
⊢ zero * -zero = -(zero * zero)

pp: case zero.neg
⊢ zero * -neg = -(zero * neg)

pp: case zero.pos
⊢ zero * -pos = -(zero * pos)

pp: case neg.zero
⊢ neg * -zero = -(neg * zero)

pp: case neg.neg
⊢ neg * -neg = -(neg * neg)

pp: case neg.pos
⊢ neg * -pos = -(neg * pos)

pp: case pos.zero
⊢ pos * -zero = -(pos * zero)

pp: case pos.neg
⊢ pos * -neg = -(pos * neg)

pp: case pos.pos
⊢ pos * -pos = -(pos * pos)

Tactic:
<;>

Goal state after:
case zero.zero
⊢ zero * -zero = -(zero * zero)

case zero.neg
⊢ zero * -neg = -(zero * neg)

case zero.pos
⊢ zero * -pos = -(zero * pos)

case neg.zero
⊢ neg * -zero = -(neg * zero)

case neg.neg
⊢ neg * -neg = -(neg * neg)

case neg.pos
⊢ neg * -pos = -(neg * pos)

case pos.zero
⊢ pos * -zero = -(pos * zero)

case pos.neg
⊢ pos * -neg = -(pos * neg)

case pos.pos
⊢ pos * -pos = -(pos * pos)
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case zero
k : ℕ
⊢ (zero * zero) ^ k * zero = zero

pp: case neg
k : ℕ
⊢ (neg * neg) ^ k * neg = neg

pp: case pos
k : ℕ
⊢ (pos * pos) ^ k * pos = pos

Tactic:
<;>

Goal state after:
case zero
k : ℕ
⊢ (zero * zero) ^ k * zero = zero

case neg
k : ℕ
⊢ (neg * neg) ^ k * neg = neg

case pos
k : ℕ
⊢ (pos * pos) ^ k * pos = pos
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case inr.zero
k : ℤ
hs : zero ≠ 0
⊢ (zero * zero) ^ k * zero = zero

pp: case inr.neg
k : ℤ
hs : neg ≠ 0
⊢ (neg * neg) ^ k * neg = neg

pp: case inr.pos
k : ℤ
hs : pos ≠ 0
⊢ (pos * pos) ^ k * pos = pos

Tactic:
<;>

Goal state after:
case inr.zero
k : ℤ
hs : zero ≠ 0
⊢ (zero * zero) ^ k * zero = zero

case inr.neg
k : ℤ
hs : neg ≠ 0
⊢ (neg * neg) ^ k * neg = neg

case inr.pos
k : ℤ
hs : pos ≠ 0
⊢ (pos * pos) ^ k * pos = pos
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case zero
n : ℕ
hn : Even n
hs : zero ≠ 0
⊢ zero ^ n = 1

pp: case neg
n : ℕ
hn : Even n
hs : neg ≠ 0
⊢ neg ^ n = 1

pp: case pos
n : ℕ
hn : Even n
hs : pos ≠ 0
⊢ pos ^ n = 1

Tactic:
<;>

Goal state after:
case zero
n : ℕ
hn : Even n
hs : zero ≠ 0
⊢ zero ^ n = 1

case neg
n : ℕ
hn : Even n
hs : neg ≠ 0
⊢ neg ^ n = 1

case pos
n : ℕ
hn : Even n
hs : pos ≠ 0
⊢ pos ^ n = 1
Module: Mathlib.Data.Sign.Defs

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

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

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

Tactic:
<;>

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

case neg
⊢ (fun a ↦
        match a with
        | ⟨0, isLt⟩ => 0
        | ⟨1, isLt⟩ => 1
        | ⟨2, isLt⟩ => -1)
      ((fun a ↦
          match a with
          | zero => ⟨0, fin3Equiv._proof_7⟩
          | pos => ⟨1, fin3Equiv._proof_8⟩
          | neg => ⟨2, fin3Equiv._proof_9⟩)
        neg) =
    neg

case pos
⊢ (fun a ↦
        match a with
        | ⟨0, isLt⟩ => 0
        | ⟨1, isLt⟩ => 1
        | ⟨2, isLt⟩ => -1)
      ((fun a ↦
          match a with
          | zero => ⟨0, fin3Equiv._proof_7⟩
          | pos => ⟨1, fin3Equiv._proof_8⟩
          | neg => ⟨2, fin3Equiv._proof_9⟩)
        pos) =
    pos
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case zero
z : ℤ
hz : Even z
hs : zero ≠ 0
⊢ zero ^ z = 1

pp: case neg
z : ℤ
hz : Even z
hs : neg ≠ 0
⊢ neg ^ z = 1

pp: case pos
z : ℤ
hz : Even z
hs : pos ≠ 0
⊢ pos ^ z = 1

Tactic:
<;>

Goal state after:
case zero
z : ℤ
hz : Even z
hs : zero ≠ 0
⊢ zero ^ z = 1

case neg
z : ℤ
hz : Even z
hs : neg ≠ 0
⊢ neg ^ z = 1

case pos
z : ℤ
hz : Even z
hs : pos ≠ 0
⊢ pos ^ z = 1
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
y : SignType
⊢ ↑(zero * y) = ↑zero * ↑y

pp: case neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
y : SignType
⊢ ↑(neg * y) = ↑neg * ↑y

pp: case pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
y : SignType
⊢ ↑(pos * y) = ↑pos * ↑y

Tactic:
<;>

Goal state after:
case zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
y : SignType
⊢ ↑(zero * y) = ↑zero * ↑y

case neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
y : SignType
⊢ ↑(neg * y) = ↑neg * ↑y

case pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
y : SignType
⊢ ↑(pos * y) = ↑pos * ↑y
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case zero.zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(zero * zero) = ↑zero * ↑zero

pp: case zero.neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(zero * neg) = ↑zero * ↑neg

pp: case zero.pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(zero * pos) = ↑zero * ↑pos

pp: case neg.zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(neg * zero) = ↑neg * ↑zero

pp: case neg.neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(neg * neg) = ↑neg * ↑neg

pp: case neg.pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(neg * pos) = ↑neg * ↑pos

pp: case pos.zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(pos * zero) = ↑pos * ↑zero

pp: case pos.neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(pos * neg) = ↑pos * ↑neg

pp: case pos.pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(pos * pos) = ↑pos * ↑pos

Tactic:
<;>

Goal state after:
case zero.zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(zero * zero) = ↑zero * ↑zero

case zero.neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(zero * neg) = ↑zero * ↑neg

case zero.pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(zero * pos) = ↑zero * ↑pos

case neg.zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(neg * zero) = ↑neg * ↑zero

case neg.neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(neg * neg) = ↑neg * ↑neg

case neg.pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(neg * pos) = ↑neg * ↑pos

case pos.zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(pos * zero) = ↑pos * ↑zero

case pos.neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(pos * neg) = ↑pos * ↑neg

case pos.pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(pos * pos) = ↑pos * ↑pos
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case zero.zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(zero * zero) = ↑zero * ↑zero

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Goal state after:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case zero.neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(zero * neg) = ↑zero * ↑neg

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Goal state after:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case zero.pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(zero * pos) = ↑zero * ↑pos

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Goal state after:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case neg.zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(neg * zero) = ↑neg * ↑zero

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Goal state after:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case neg.neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(neg * neg) = ↑neg * ↑neg

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Goal state after:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case neg.pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(neg * pos) = ↑neg * ↑pos

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Goal state after:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case pos.zero
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(pos * zero) = ↑pos * ↑zero

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Goal state after:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case pos.neg
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(pos * neg) = ↑pos * ↑neg

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Goal state after:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case pos.pos
α✝ : Type u
α : Type ?u.4
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ↑(pos * pos) = ↑pos * ↑pos

Tactic:
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]

Goal state after:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x < 0
⊢ sign (x * y) = sign x * sign y

pp: case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x = 0
⊢ sign (x * y) = sign x * sign y

pp: case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : 0 < x
⊢ sign (x * y) = sign x * sign y

Tactic:
<;>

Goal state after:
case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x < 0
⊢ sign (x * y) = sign x * sign y

case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x = 0
⊢ sign (x * y) = sign x * sign y

case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : 0 < x
⊢ sign (x * y) = sign x * sign y
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case inl.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x < 0
hy : y < 0
⊢ sign (x * y) = sign x * sign y

pp: case inl.inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x < 0
hy : y = 0
⊢ sign (x * y) = sign x * sign y

pp: case inl.inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x < 0
hy : 0 < y
⊢ sign (x * y) = sign x * sign y

pp: case inr.inl.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x = 0
hy : y < 0
⊢ sign (x * y) = sign x * sign y

pp: case inr.inl.inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x = 0
hy : y = 0
⊢ sign (x * y) = sign x * sign y

pp: case inr.inl.inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x = 0
hy : 0 < y
⊢ sign (x * y) = sign x * sign y

pp: case inr.inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : 0 < x
hy : y < 0
⊢ sign (x * y) = sign x * sign y

pp: case inr.inr.inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : 0 < x
hy : y = 0
⊢ sign (x * y) = sign x * sign y

pp: case inr.inr.inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : 0 < x
hy : 0 < y
⊢ sign (x * y) = sign x * sign y

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x < 0
hy : y < 0
⊢ sign (x * y) = sign x * sign y

case inl.inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x < 0
hy : y = 0
⊢ sign (x * y) = sign x * sign y

case inl.inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x < 0
hy : 0 < y
⊢ sign (x * y) = sign x * sign y

case inr.inl.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x = 0
hy : y < 0
⊢ sign (x * y) = sign x * sign y

case inr.inl.inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x = 0
hy : y = 0
⊢ sign (x * y) = sign x * sign y

case inr.inl.inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : x = 0
hy : 0 < y
⊢ sign (x * y) = sign x * sign y

case inr.inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : 0 < x
hy : y < 0
⊢ sign (x * y) = sign x * sign y

case inr.inr.inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : 0 < x
hy : y = 0
⊢ sign (x * y) = sign x * sign y

case inr.inr.inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
hx : 0 < x
hy : 0 < y
⊢ sign (x * y) = sign x * sign y
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ ↑(sign x) * |x| = x

pp: case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ ↑(sign 0) * |0| = 0

pp: case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ ↑(sign x) * |x| = x

Tactic:
<;>

Goal state after:
case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ ↑(sign x) * |x| = x

case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ ↑(sign 0) * |0| = 0

case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ ↑(sign x) * |x| = x
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ |x| * ↑(sign x) = x

pp: case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ |0| * ↑(sign 0) = 0

pp: case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ |x| * ↑(sign x) = x

Tactic:
<;>

Goal state after:
case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ |x| * ↑(sign x) = x

case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ |0| * ↑(sign 0) = 0

case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ |x| * ↑(sign x) = x
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ ↑(sign x) * x = |x|

pp: case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ ↑(sign 0) * 0 = |0|

pp: case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ ↑(sign x) * x = |x|

Tactic:
<;>

Goal state after:
case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ ↑(sign x) * x = |x|

case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ ↑(sign 0) * 0 = |0|

case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ ↑(sign x) * x = |x|
Module: Mathlib.Data.Sign.Defs

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

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

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

Tactic:
<;>

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

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

case pos
b : SignType
⊢ (match pos * b with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match pos with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match b with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ x * ↑(sign x) = |x|

pp: case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ 0 * ↑(sign 0) = |0|

pp: case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ x * ↑(sign x) = |x|

Tactic:
<;>

Goal state after:
case inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : x < 0
⊢ x * ↑(sign x) = |x|

case inr.inl
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ 0 * ↑(sign 0) = |0|

case inr.inr
α : Type u
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x : α
hx : 0 < x
⊢ x * ↑(sign x) = |x|
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case zero
α : Type u_1
inst✝⁵ : Zero α
inst✝⁴ : One α
inst✝³ : Neg α
β : Type u_2
inst✝² : One β
inst✝¹ : Neg β
inst✝ : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
⊢ f ↑zero = ↑zero

pp: case neg
α : Type u_1
inst✝⁵ : Zero α
inst✝⁴ : One α
inst✝³ : Neg α
β : Type u_2
inst✝² : One β
inst✝¹ : Neg β
inst✝ : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
⊢ f ↑neg = ↑neg

pp: case pos
α : Type u_1
inst✝⁵ : Zero α
inst✝⁴ : One α
inst✝³ : Neg α
β : Type u_2
inst✝² : One β
inst✝¹ : Neg β
inst✝ : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
⊢ f ↑pos = ↑pos

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝⁵ : Zero α
inst✝⁴ : One α
inst✝³ : Neg α
β : Type u_2
inst✝² : One β
inst✝¹ : Neg β
inst✝ : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
⊢ f ↑zero = ↑zero

case neg
α : Type u_1
inst✝⁵ : Zero α
inst✝⁴ : One α
inst✝³ : Neg α
β : Type u_2
inst✝² : One β
inst✝¹ : Neg β
inst✝ : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
⊢ f ↑neg = ↑neg

case pos
α : Type u_1
inst✝⁵ : Zero α
inst✝⁴ : One α
inst✝³ : Neg α
β : Type u_2
inst✝² : One β
inst✝¹ : Neg β
inst✝ : Zero β
f : α → β
h₁ : f 1 = 1
h₂ : f 0 = 0
h₃ : f (-1) = -1
⊢ f ↑pos = ↑pos
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case h₁
α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁵ : AddGroupWithOne α
inst✝⁴ : One β
inst✝³ : SubtractionMonoid β
inst✝² : FunLike F α β
inst✝¹ : AddMonoidHomClass F α β
inst✝ : OneHomClass F α β
f : F
s : SignType
⊢ f 1 = 1

pp: case h₂
α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁵ : AddGroupWithOne α
inst✝⁴ : One β
inst✝³ : SubtractionMonoid β
inst✝² : FunLike F α β
inst✝¹ : AddMonoidHomClass F α β
inst✝ : OneHomClass F α β
f : F
s : SignType
⊢ f 0 = 0

pp: case h₃
α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁵ : AddGroupWithOne α
inst✝⁴ : One β
inst✝³ : SubtractionMonoid β
inst✝² : FunLike F α β
inst✝¹ : AddMonoidHomClass F α β
inst✝ : OneHomClass F α β
f : F
s : SignType
⊢ f (-1) = -1

Tactic:
<;>

Goal state after:
case h₁
α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁵ : AddGroupWithOne α
inst✝⁴ : One β
inst✝³ : SubtractionMonoid β
inst✝² : FunLike F α β
inst✝¹ : AddMonoidHomClass F α β
inst✝ : OneHomClass F α β
f : F
s : SignType
⊢ f 1 = 1

case h₂
α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁵ : AddGroupWithOne α
inst✝⁴ : One β
inst✝³ : SubtractionMonoid β
inst✝² : FunLike F α β
inst✝¹ : AddMonoidHomClass F α β
inst✝ : OneHomClass F α β
f : F
s : SignType
⊢ f 0 = 0

case h₃
α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁵ : AddGroupWithOne α
inst✝⁴ : One β
inst✝³ : SubtractionMonoid β
inst✝² : FunLike F α β
inst✝¹ : AddMonoidHomClass F α β
inst✝ : OneHomClass F α β
f : F
s : SignType
⊢ f (-1) = -1