Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
hsb : sign b = -1
⊢ sign a = sign b ∨ sign a = -sign b

pp: case inl.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
hsb : sign b = 0
⊢ sign a = sign b ∨ sign a = -sign b

pp: case inl.inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
hsb : sign b = 1
⊢ sign a = sign b ∨ sign a = -sign b

pp: case inr.inl.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
hsb : sign b = -1
⊢ sign a = sign b ∨ sign a = -sign b

pp: case inr.inl.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
hsb : sign b = 0
⊢ sign a = sign b ∨ sign a = -sign b

pp: case inr.inl.inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
hsb : sign b = 1
⊢ sign a = sign b ∨ sign a = -sign b

pp: case inr.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
hsb : sign b = -1
⊢ sign a = sign b ∨ sign a = -sign b

pp: case inr.inr.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
hsb : sign b = 0
⊢ sign a = sign b ∨ sign a = -sign b

pp: case inr.inr.inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
hsb : sign b = 1
⊢ sign a = sign b ∨ sign a = -sign b

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
hsb : sign b = -1
⊢ sign a = sign b ∨ sign a = -sign b

case inl.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
hsb : sign b = 0
⊢ sign a = sign b ∨ sign a = -sign b

case inl.inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = -1
hsb : sign b = 1
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inl.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
hsb : sign b = -1
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inl.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
hsb : sign b = 0
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inl.inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 0
hsb : sign b = 1
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
hsb : sign b = -1
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inr.inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
hsb : sign b = 0
⊢ sign a = sign b ∨ sign a = -sign b

case inr.inr.inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : sign a = 1
hsb : sign b = 1
⊢ sign a = sign b ∨ sign a = -sign b