[GOAL]
x : SignType
⊢ x ∈ ↑[zero, neg, pos]
[PROOFSTEP]
cases x
[GOAL]
case zero
⊢ zero ∈ ↑[zero, neg, pos]
[PROOFSTEP]
simp only
[GOAL]
case neg
⊢ neg ∈ ↑[zero, neg, pos]
[PROOFSTEP]
simp only
[GOAL]
case pos
⊢ pos ∈ ↑[zero, neg, pos]
[PROOFSTEP]
simp only
[GOAL]
a b : SignType
⊢ Decidable (SignType.LE a b)
[PROOFSTEP]
cases a
[GOAL]
case zero
b : SignType
⊢ Decidable (SignType.LE SignType.zero b)
[PROOFSTEP]
cases b
[GOAL]
case neg
b : SignType
⊢ Decidable (SignType.LE neg b)
[PROOFSTEP]
cases b
[GOAL]
case pos
b : SignType
⊢ Decidable (SignType.LE pos b)
[PROOFSTEP]
cases b
[GOAL]
case zero.zero
⊢ Decidable (SignType.LE SignType.zero SignType.zero)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case zero.zero
⊢ Decidable (SignType.LE SignType.zero SignType.zero)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ SignType.LE SignType.zero SignType.zero
[PROOFSTEP]
constructor
[GOAL]
case zero.neg
⊢ Decidable (SignType.LE SignType.zero neg)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case zero.neg
⊢ Decidable (SignType.LE SignType.zero neg)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ SignType.LE SignType.zero neg
[PROOFSTEP]
constructor
[GOAL]
case zero.neg
⊢ Decidable (SignType.LE SignType.zero neg)
[PROOFSTEP]
exact isFalse (by rintro ⟨_⟩)
[GOAL]
⊢ ¬SignType.LE SignType.zero neg
[PROOFSTEP]
rintro ⟨_⟩
[GOAL]
case zero.pos
⊢ Decidable (SignType.LE SignType.zero pos)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case zero.pos
⊢ Decidable (SignType.LE SignType.zero pos)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ SignType.LE SignType.zero pos
[PROOFSTEP]
constructor
[GOAL]
case neg.zero
⊢ Decidable (SignType.LE neg SignType.zero)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case neg.zero
⊢ Decidable (SignType.LE neg SignType.zero)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ SignType.LE neg SignType.zero
[PROOFSTEP]
constructor
[GOAL]
case neg.neg
⊢ Decidable (SignType.LE neg neg)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case neg.neg
⊢ Decidable (SignType.LE neg neg)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ SignType.LE neg neg
[PROOFSTEP]
constructor
[GOAL]
case neg.pos
⊢ Decidable (SignType.LE neg pos)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case neg.pos
⊢ Decidable (SignType.LE neg pos)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ SignType.LE neg pos
[PROOFSTEP]
constructor
[GOAL]
case pos.zero
⊢ Decidable (SignType.LE pos SignType.zero)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case pos.zero
⊢ Decidable (SignType.LE pos SignType.zero)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ SignType.LE pos SignType.zero
[PROOFSTEP]
constructor
[GOAL]
case pos.zero
⊢ Decidable (SignType.LE pos SignType.zero)
[PROOFSTEP]
exact isFalse (by rintro ⟨_⟩)
[GOAL]
⊢ ¬SignType.LE pos SignType.zero
[PROOFSTEP]
rintro ⟨_⟩
[GOAL]
case pos.neg
⊢ Decidable (SignType.LE pos neg)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case pos.neg
⊢ Decidable (SignType.LE pos neg)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ SignType.LE pos neg
[PROOFSTEP]
constructor
[GOAL]
case pos.neg
⊢ Decidable (SignType.LE pos neg)
[PROOFSTEP]
exact isFalse (by rintro ⟨_⟩)
[GOAL]
⊢ ¬SignType.LE pos neg
[PROOFSTEP]
rintro ⟨_⟩
[GOAL]
case pos.pos
⊢ Decidable (SignType.LE pos pos)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case pos.pos
⊢ Decidable (SignType.LE pos pos)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ SignType.LE pos pos
[PROOFSTEP]
constructor
[GOAL]
a b : SignType
⊢ Decidable (a = b)
[PROOFSTEP]
cases a
[GOAL]
case zero
b : SignType
⊢ Decidable (zero = b)
[PROOFSTEP]
cases b
[GOAL]
case neg
b : SignType
⊢ Decidable (neg = b)
[PROOFSTEP]
cases b
[GOAL]
case pos
b : SignType
⊢ Decidable (pos = b)
[PROOFSTEP]
cases b
[GOAL]
case zero.zero
⊢ Decidable (zero = zero)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case zero.zero
⊢ Decidable (zero = zero)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ zero = zero
[PROOFSTEP]
constructor
[GOAL]
case zero.neg
⊢ Decidable (zero = neg)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case zero.neg
⊢ Decidable (zero = neg)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ zero = neg
[PROOFSTEP]
constructor
[GOAL]
case zero.neg
⊢ Decidable (zero = neg)
[PROOFSTEP]
exact isFalse (by rintro ⟨_⟩)
[GOAL]
⊢ ¬zero = neg
[PROOFSTEP]
rintro ⟨_⟩
[GOAL]
case zero.pos
⊢ Decidable (zero = pos)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case zero.pos
⊢ Decidable (zero = pos)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ zero = pos
[PROOFSTEP]
constructor
[GOAL]
case zero.pos
⊢ Decidable (zero = pos)
[PROOFSTEP]
exact isFalse (by rintro ⟨_⟩)
[GOAL]
⊢ ¬zero = pos
[PROOFSTEP]
rintro ⟨_⟩
[GOAL]
case neg.zero
⊢ Decidable (neg = zero)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case neg.zero
⊢ Decidable (neg = zero)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ neg = zero
[PROOFSTEP]
constructor
[GOAL]
case neg.zero
⊢ Decidable (neg = zero)
[PROOFSTEP]
exact isFalse (by rintro ⟨_⟩)
[GOAL]
⊢ ¬neg = zero
[PROOFSTEP]
rintro ⟨_⟩
[GOAL]
case neg.neg
⊢ Decidable (neg = neg)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case neg.neg
⊢ Decidable (neg = neg)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ neg = neg
[PROOFSTEP]
constructor
[GOAL]
case neg.pos
⊢ Decidable (neg = pos)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case neg.pos
⊢ Decidable (neg = pos)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ neg = pos
[PROOFSTEP]
constructor
[GOAL]
case neg.pos
⊢ Decidable (neg = pos)
[PROOFSTEP]
exact isFalse (by rintro ⟨_⟩)
[GOAL]
⊢ ¬neg = pos
[PROOFSTEP]
rintro ⟨_⟩
[GOAL]
case pos.zero
⊢ Decidable (pos = zero)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case pos.zero
⊢ Decidable (pos = zero)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ pos = zero
[PROOFSTEP]
constructor
[GOAL]
case pos.zero
⊢ Decidable (pos = zero)
[PROOFSTEP]
exact isFalse (by rintro ⟨_⟩)
[GOAL]
⊢ ¬pos = zero
[PROOFSTEP]
rintro ⟨_⟩
[GOAL]
case pos.neg
⊢ Decidable (pos = neg)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case pos.neg
⊢ Decidable (pos = neg)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ pos = neg
[PROOFSTEP]
constructor
[GOAL]
case pos.neg
⊢ Decidable (pos = neg)
[PROOFSTEP]
exact isFalse (by rintro ⟨_⟩)
[GOAL]
⊢ ¬pos = neg
[PROOFSTEP]
rintro ⟨_⟩
[GOAL]
case pos.pos
⊢ Decidable (pos = pos)
[PROOFSTEP]
first
| exact isTrue (by constructor)
| exact isFalse (by rintro ⟨_⟩)
[GOAL]
case pos.pos
⊢ Decidable (pos = pos)
[PROOFSTEP]
exact isTrue (by constructor)
[GOAL]
⊢ pos = pos
[PROOFSTEP]
constructor
[GOAL]
⊢ ∀ (a b : SignType), a * b = b * a
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩
[GOAL]
case zero.zero
⊢ zero * zero = zero * zero
[PROOFSTEP]
rfl
[GOAL]
case zero.neg
⊢ zero * neg = neg * zero
[PROOFSTEP]
rfl
[GOAL]
case zero.pos
⊢ zero * pos = pos * zero
[PROOFSTEP]
rfl
[GOAL]
case neg.zero
⊢ neg * zero = zero * neg
[PROOFSTEP]
rfl
[GOAL]
case neg.neg
⊢ neg * neg = neg * neg
[PROOFSTEP]
rfl
[GOAL]
case neg.pos
⊢ neg * pos = pos * neg
[PROOFSTEP]
rfl
[GOAL]
case pos.zero
⊢ pos * zero = zero * pos
[PROOFSTEP]
rfl
[GOAL]
case pos.neg
⊢ pos * neg = neg * pos
[PROOFSTEP]
rfl
[GOAL]
case pos.pos
⊢ pos * pos = pos * pos
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a b c : SignType), a * b * c = a * (b * c)
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ ⟨⟩
[GOAL]
case zero.zero.zero
⊢ zero * zero * zero = zero * (zero * zero)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case zero.zero.neg
⊢ zero * zero * neg = zero * (zero * neg)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case zero.zero.pos
⊢ zero * zero * pos = zero * (zero * pos)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case zero.neg.zero
⊢ zero * neg * zero = zero * (neg * zero)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case zero.neg.neg
⊢ zero * neg * neg = zero * (neg * neg)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case zero.neg.pos
⊢ zero * neg * pos = zero * (neg * pos)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case zero.pos.zero
⊢ zero * pos * zero = zero * (pos * zero)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case zero.pos.neg
⊢ zero * pos * neg = zero * (pos * neg)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case zero.pos.pos
⊢ zero * pos * pos = zero * (pos * pos)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case neg.zero.zero
⊢ neg * zero * zero = neg * (zero * zero)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case neg.zero.neg
⊢ neg * zero * neg = neg * (zero * neg)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case neg.zero.pos
⊢ neg * zero * pos = neg * (zero * pos)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case neg.neg.zero
⊢ neg * neg * zero = neg * (neg * zero)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case neg.neg.neg
⊢ neg * neg * neg = neg * (neg * neg)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case neg.neg.pos
⊢ neg * neg * pos = neg * (neg * pos)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case neg.pos.zero
⊢ neg * pos * zero = neg * (pos * zero)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case neg.pos.neg
⊢ neg * pos * neg = neg * (pos * neg)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case neg.pos.pos
⊢ neg * pos * pos = neg * (pos * pos)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case pos.zero.zero
⊢ pos * zero * zero = pos * (zero * zero)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case pos.zero.neg
⊢ pos * zero * neg = pos * (zero * neg)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case pos.zero.pos
⊢ pos * zero * pos = pos * (zero * pos)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case pos.neg.zero
⊢ pos * neg * zero = pos * (neg * zero)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case pos.neg.neg
⊢ pos * neg * neg = pos * (neg * neg)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case pos.neg.pos
⊢ pos * neg * pos = pos * (neg * pos)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case pos.pos.zero
⊢ pos * pos * zero = pos * (pos * zero)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case pos.pos.neg
⊢ pos * pos * neg = pos * (pos * neg)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
case pos.pos.pos
⊢ pos * pos * pos = pos * (pos * pos)
[PROOFSTEP]
rfl
  /- We can define a `Field` instance on `SignType`, but it's not mathematically sensible,
  so we only define the `CommGroupWithZero`. -/
[GOAL]
a : SignType
⊢ 1 * a = a
[PROOFSTEP]
cases a
[GOAL]
case zero
⊢ 1 * zero = zero
[PROOFSTEP]
rfl
[GOAL]
case neg
⊢ 1 * neg = neg
[PROOFSTEP]
rfl
[GOAL]
case pos
⊢ 1 * pos = pos
[PROOFSTEP]
rfl
[GOAL]
a : SignType
⊢ a * 1 = a
[PROOFSTEP]
cases a
[GOAL]
case zero
⊢ zero * 1 = zero
[PROOFSTEP]
rfl
[GOAL]
case neg
⊢ neg * 1 = neg
[PROOFSTEP]
rfl
[GOAL]
case pos
⊢ pos * 1 = pos
[PROOFSTEP]
rfl
[GOAL]
a : SignType
⊢ 0 * a = 0
[PROOFSTEP]
cases a
[GOAL]
case zero
⊢ 0 * zero = 0
[PROOFSTEP]
rfl
[GOAL]
case neg
⊢ 0 * neg = 0
[PROOFSTEP]
rfl
[GOAL]
case pos
⊢ 0 * pos = 0
[PROOFSTEP]
rfl
[GOAL]
a : SignType
⊢ a * 0 = 0
[PROOFSTEP]
cases a
[GOAL]
case zero
⊢ zero * 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case neg
⊢ neg * 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case pos
⊢ pos * 0 = 0
[PROOFSTEP]
rfl
[GOAL]
⊢ 0 ≠ 1
[PROOFSTEP]
rintro ⟨_⟩
[GOAL]
a : SignType
ha : a ≠ 0
⊢ a * a⁻¹ = 1
[PROOFSTEP]
cases a
[GOAL]
case zero
ha : zero ≠ 0
⊢ zero * zero⁻¹ = 1
[PROOFSTEP]
trivial
[GOAL]
case neg
ha : neg ≠ 0
⊢ neg * neg⁻¹ = 1
[PROOFSTEP]
trivial
[GOAL]
case pos
ha : pos ≠ 0
⊢ pos * pos⁻¹ = 1
[PROOFSTEP]
trivial
[GOAL]
a b : SignType
x✝¹ : a ≤ b
x✝ : b ≤ a
⊢ a = b
[PROOFSTEP]
cases a
[GOAL]
case zero
b : SignType
x✝¹ : zero ≤ b
x✝ : b ≤ zero
⊢ zero = b
[PROOFSTEP]
cases b
[GOAL]
case neg
b : SignType
x✝¹ : neg ≤ b
x✝ : b ≤ neg
⊢ neg = b
[PROOFSTEP]
cases b
[GOAL]
case pos
b : SignType
x✝¹ : pos ≤ b
x✝ : b ≤ pos
⊢ pos = b
[PROOFSTEP]
cases b
[GOAL]
case zero.zero
x✝¹ x✝ : zero ≤ zero
⊢ zero = zero
[PROOFSTEP]
trivial
[GOAL]
case zero.neg
x✝¹ : zero ≤ neg
x✝ : neg ≤ zero
⊢ zero = neg
[PROOFSTEP]
trivial
[GOAL]
case zero.pos
x✝¹ : zero ≤ pos
x✝ : pos ≤ zero
⊢ zero = pos
[PROOFSTEP]
trivial
[GOAL]
case neg.zero
x✝¹ : neg ≤ zero
x✝ : zero ≤ neg
⊢ neg = zero
[PROOFSTEP]
trivial
[GOAL]
case neg.neg
x✝¹ x✝ : neg ≤ neg
⊢ neg = neg
[PROOFSTEP]
trivial
[GOAL]
case neg.pos
x✝¹ : neg ≤ pos
x✝ : pos ≤ neg
⊢ neg = pos
[PROOFSTEP]
trivial
[GOAL]
case pos.zero
x✝¹ : pos ≤ zero
x✝ : zero ≤ pos
⊢ pos = zero
[PROOFSTEP]
trivial
[GOAL]
case pos.neg
x✝¹ : pos ≤ neg
x✝ : neg ≤ pos
⊢ pos = neg
[PROOFSTEP]
trivial
[GOAL]
case pos.pos
x✝¹ x✝ : pos ≤ pos
⊢ pos = pos
[PROOFSTEP]
trivial
[GOAL]
a b c : SignType
x✝¹ : a ≤ b
x✝ : b ≤ c
⊢ a ≤ c
[PROOFSTEP]
cases a
[GOAL]
case zero
b c : SignType
x✝¹ : b ≤ c
x✝ : zero ≤ b
⊢ zero ≤ c
[PROOFSTEP]
cases b
[GOAL]
case neg
b c : SignType
x✝¹ : b ≤ c
x✝ : neg ≤ b
⊢ neg ≤ c
[PROOFSTEP]
cases b
[GOAL]
case pos
b c : SignType
x✝¹ : b ≤ c
x✝ : pos ≤ b
⊢ pos ≤ c
[PROOFSTEP]
cases b
[GOAL]
case zero.zero
c : SignType
x✝¹ : zero ≤ c
x✝ : zero ≤ zero
⊢ zero ≤ c
[PROOFSTEP]
cases c
[GOAL]
case zero.neg
c : SignType
x✝¹ : neg ≤ c
x✝ : zero ≤ neg
⊢ zero ≤ c
[PROOFSTEP]
cases c
[GOAL]
case zero.pos
c : SignType
x✝¹ : pos ≤ c
x✝ : zero ≤ pos
⊢ zero ≤ c
[PROOFSTEP]
cases c
[GOAL]
case neg.zero
c : SignType
x✝¹ : zero ≤ c
x✝ : neg ≤ zero
⊢ neg ≤ c
[PROOFSTEP]
cases c
[GOAL]
case neg.neg
c : SignType
x✝¹ : neg ≤ c
x✝ : neg ≤ neg
⊢ neg ≤ c
[PROOFSTEP]
cases c
[GOAL]
case neg.pos
c : SignType
x✝¹ : pos ≤ c
x✝ : neg ≤ pos
⊢ neg ≤ c
[PROOFSTEP]
cases c
[GOAL]
case pos.zero
c : SignType
x✝¹ : zero ≤ c
x✝ : pos ≤ zero
⊢ pos ≤ c
[PROOFSTEP]
cases c
[GOAL]
case pos.neg
c : SignType
x✝¹ : neg ≤ c
x✝ : pos ≤ neg
⊢ pos ≤ c
[PROOFSTEP]
cases c
[GOAL]
case pos.pos
c : SignType
x✝¹ : pos ≤ c
x✝ : pos ≤ pos
⊢ pos ≤ c
[PROOFSTEP]
cases c
[GOAL]
case zero.zero.zero
x✝¹ x✝ : zero ≤ zero
⊢ zero ≤ zero
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case zero.zero.zero
x✝¹ x✝ : zero ≤ zero
⊢ zero ≤ zero
[PROOFSTEP]
tauto
[GOAL]
case zero.zero.neg
x✝¹ : zero ≤ zero
x✝ : zero ≤ neg
⊢ zero ≤ neg
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case zero.zero.neg
x✝¹ : zero ≤ zero
x✝ : zero ≤ neg
⊢ zero ≤ neg
[PROOFSTEP]
tauto
[GOAL]
case zero.zero.pos
x✝¹ : zero ≤ zero
x✝ : zero ≤ pos
⊢ zero ≤ pos
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case zero.zero.pos
x✝¹ : zero ≤ zero
x✝ : zero ≤ pos
⊢ zero ≤ pos
[PROOFSTEP]
tauto
[GOAL]
case zero.neg.zero
x✝¹ : zero ≤ neg
x✝ : neg ≤ zero
⊢ zero ≤ zero
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case zero.neg.zero
x✝¹ : zero ≤ neg
x✝ : neg ≤ zero
⊢ zero ≤ zero
[PROOFSTEP]
tauto
[GOAL]
case zero.neg.neg
x✝¹ : zero ≤ neg
x✝ : neg ≤ neg
⊢ zero ≤ neg
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case zero.neg.neg
x✝¹ : zero ≤ neg
x✝ : neg ≤ neg
⊢ zero ≤ neg
[PROOFSTEP]
tauto
[GOAL]
case zero.neg.pos
x✝¹ : zero ≤ neg
x✝ : neg ≤ pos
⊢ zero ≤ pos
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case zero.neg.pos
x✝¹ : zero ≤ neg
x✝ : neg ≤ pos
⊢ zero ≤ pos
[PROOFSTEP]
tauto
[GOAL]
case zero.pos.zero
x✝¹ : zero ≤ pos
x✝ : pos ≤ zero
⊢ zero ≤ zero
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case zero.pos.zero
x✝¹ : zero ≤ pos
x✝ : pos ≤ zero
⊢ zero ≤ zero
[PROOFSTEP]
tauto
[GOAL]
case zero.pos.neg
x✝¹ : zero ≤ pos
x✝ : pos ≤ neg
⊢ zero ≤ neg
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case zero.pos.neg
x✝¹ : zero ≤ pos
x✝ : pos ≤ neg
⊢ zero ≤ neg
[PROOFSTEP]
tauto
[GOAL]
case zero.pos.pos
x✝¹ : zero ≤ pos
x✝ : pos ≤ pos
⊢ zero ≤ pos
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case zero.pos.pos
x✝¹ : zero ≤ pos
x✝ : pos ≤ pos
⊢ zero ≤ pos
[PROOFSTEP]
tauto
[GOAL]
case neg.zero.zero
x✝¹ : neg ≤ zero
x✝ : zero ≤ zero
⊢ neg ≤ zero
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case neg.zero.zero
x✝¹ : neg ≤ zero
x✝ : zero ≤ zero
⊢ neg ≤ zero
[PROOFSTEP]
tauto
[GOAL]
case neg.zero.neg
x✝¹ : neg ≤ zero
x✝ : zero ≤ neg
⊢ neg ≤ neg
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case neg.zero.neg
x✝¹ : neg ≤ zero
x✝ : zero ≤ neg
⊢ neg ≤ neg
[PROOFSTEP]
tauto
[GOAL]
case neg.zero.pos
x✝¹ : neg ≤ zero
x✝ : zero ≤ pos
⊢ neg ≤ pos
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case neg.zero.pos
x✝¹ : neg ≤ zero
x✝ : zero ≤ pos
⊢ neg ≤ pos
[PROOFSTEP]
tauto
[GOAL]
case neg.zero.pos
x✝¹ : neg ≤ zero
x✝ : zero ≤ pos
⊢ neg ≤ pos
[PROOFSTEP]
constructor
[GOAL]
case neg.neg.zero
x✝¹ : neg ≤ neg
x✝ : neg ≤ zero
⊢ neg ≤ zero
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case neg.neg.zero
x✝¹ : neg ≤ neg
x✝ : neg ≤ zero
⊢ neg ≤ zero
[PROOFSTEP]
tauto
[GOAL]
case neg.neg.neg
x✝¹ x✝ : neg ≤ neg
⊢ neg ≤ neg
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case neg.neg.neg
x✝¹ x✝ : neg ≤ neg
⊢ neg ≤ neg
[PROOFSTEP]
tauto
[GOAL]
case neg.neg.pos
x✝¹ : neg ≤ neg
x✝ : neg ≤ pos
⊢ neg ≤ pos
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case neg.neg.pos
x✝¹ : neg ≤ neg
x✝ : neg ≤ pos
⊢ neg ≤ pos
[PROOFSTEP]
tauto
[GOAL]
case neg.pos.zero
x✝¹ : neg ≤ pos
x✝ : pos ≤ zero
⊢ neg ≤ zero
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case neg.pos.zero
x✝¹ : neg ≤ pos
x✝ : pos ≤ zero
⊢ neg ≤ zero
[PROOFSTEP]
tauto
[GOAL]
case neg.pos.neg
x✝¹ : neg ≤ pos
x✝ : pos ≤ neg
⊢ neg ≤ neg
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case neg.pos.neg
x✝¹ : neg ≤ pos
x✝ : pos ≤ neg
⊢ neg ≤ neg
[PROOFSTEP]
tauto
[GOAL]
case neg.pos.pos
x✝¹ : neg ≤ pos
x✝ : pos ≤ pos
⊢ neg ≤ pos
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case neg.pos.pos
x✝¹ : neg ≤ pos
x✝ : pos ≤ pos
⊢ neg ≤ pos
[PROOFSTEP]
tauto
[GOAL]
case pos.zero.zero
x✝¹ : pos ≤ zero
x✝ : zero ≤ zero
⊢ pos ≤ zero
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case pos.zero.zero
x✝¹ : pos ≤ zero
x✝ : zero ≤ zero
⊢ pos ≤ zero
[PROOFSTEP]
tauto
[GOAL]
case pos.zero.neg
x✝¹ : pos ≤ zero
x✝ : zero ≤ neg
⊢ pos ≤ neg
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case pos.zero.neg
x✝¹ : pos ≤ zero
x✝ : zero ≤ neg
⊢ pos ≤ neg
[PROOFSTEP]
tauto
[GOAL]
case pos.zero.pos
x✝¹ : pos ≤ zero
x✝ : zero ≤ pos
⊢ pos ≤ pos
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case pos.zero.pos
x✝¹ : pos ≤ zero
x✝ : zero ≤ pos
⊢ pos ≤ pos
[PROOFSTEP]
tauto
[GOAL]
case pos.neg.zero
x✝¹ : pos ≤ neg
x✝ : neg ≤ zero
⊢ pos ≤ zero
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case pos.neg.zero
x✝¹ : pos ≤ neg
x✝ : neg ≤ zero
⊢ pos ≤ zero
[PROOFSTEP]
tauto
[GOAL]
case pos.neg.neg
x✝¹ : pos ≤ neg
x✝ : neg ≤ neg
⊢ pos ≤ neg
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case pos.neg.neg
x✝¹ : pos ≤ neg
x✝ : neg ≤ neg
⊢ pos ≤ neg
[PROOFSTEP]
tauto
[GOAL]
case pos.neg.pos
x✝¹ : pos ≤ neg
x✝ : neg ≤ pos
⊢ pos ≤ pos
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case pos.neg.pos
x✝¹ : pos ≤ neg
x✝ : neg ≤ pos
⊢ pos ≤ pos
[PROOFSTEP]
tauto
[GOAL]
case pos.pos.zero
x✝¹ : pos ≤ pos
x✝ : pos ≤ zero
⊢ pos ≤ zero
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case pos.pos.zero
x✝¹ : pos ≤ pos
x✝ : pos ≤ zero
⊢ pos ≤ zero
[PROOFSTEP]
tauto
[GOAL]
case pos.pos.neg
x✝¹ : pos ≤ pos
x✝ : pos ≤ neg
⊢ pos ≤ neg
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case pos.pos.neg
x✝¹ : pos ≤ pos
x✝ : pos ≤ neg
⊢ pos ≤ neg
[PROOFSTEP]
tauto
[GOAL]
case pos.pos.pos
x✝¹ x✝ : pos ≤ pos
⊢ pos ≤ pos
[PROOFSTEP]
first
| tauto
| constructor
[GOAL]
case pos.pos.pos
x✝¹ x✝ : pos ≤ pos
⊢ pos ≤ pos
[PROOFSTEP]
tauto
[GOAL]
a : SignType
⊢ a ≤ a
[PROOFSTEP]
cases a
[GOAL]
case zero
⊢ zero ≤ zero
[PROOFSTEP]
constructor
[GOAL]
case neg
⊢ neg ≤ neg
[PROOFSTEP]
constructor
[GOAL]
case pos
⊢ pos ≤ pos
[PROOFSTEP]
constructor
[GOAL]
a b : SignType
⊢ a ≤ b ∨ b ≤ a
[PROOFSTEP]
cases a
[GOAL]
case zero
b : SignType
⊢ zero ≤ b ∨ b ≤ zero
[PROOFSTEP]
cases b
[GOAL]
case neg
b : SignType
⊢ neg ≤ b ∨ b ≤ neg
[PROOFSTEP]
cases b
[GOAL]
case pos
b : SignType
⊢ pos ≤ b ∨ b ≤ pos
[PROOFSTEP]
cases b
[GOAL]
case zero.zero
⊢ zero ≤ zero ∨ zero ≤ zero
[PROOFSTEP]
first
| left; constructor
| right; constructor
[GOAL]
case zero.zero
⊢ zero ≤ zero ∨ zero ≤ zero
[PROOFSTEP]
left
[GOAL]
case zero.zero.h
⊢ zero ≤ zero
[PROOFSTEP]
constructor
[GOAL]
case zero.neg
⊢ zero ≤ neg ∨ neg ≤ zero
[PROOFSTEP]
first
| left; constructor
| right; constructor
[GOAL]
case zero.neg
⊢ zero ≤ neg ∨ neg ≤ zero
[PROOFSTEP]
left
[GOAL]
case zero.neg.h
⊢ zero ≤ neg
[PROOFSTEP]
constructor
[GOAL]
case zero.neg
⊢ zero ≤ neg ∨ neg ≤ zero
[PROOFSTEP]
right
[GOAL]
case zero.neg.h
⊢ neg ≤ zero
[PROOFSTEP]
constructor
[GOAL]
case zero.pos
⊢ zero ≤ pos ∨ pos ≤ zero
[PROOFSTEP]
first
| left; constructor
| right; constructor
[GOAL]
case zero.pos
⊢ zero ≤ pos ∨ pos ≤ zero
[PROOFSTEP]
left
[GOAL]
case zero.pos.h
⊢ zero ≤ pos
[PROOFSTEP]
constructor
[GOAL]
case neg.zero
⊢ neg ≤ zero ∨ zero ≤ neg
[PROOFSTEP]
first
| left; constructor
| right; constructor
[GOAL]
case neg.zero
⊢ neg ≤ zero ∨ zero ≤ neg
[PROOFSTEP]
left
[GOAL]
case neg.zero.h
⊢ neg ≤ zero
[PROOFSTEP]
constructor
[GOAL]
case neg.neg
⊢ neg ≤ neg ∨ neg ≤ neg
[PROOFSTEP]
first
| left; constructor
| right; constructor
[GOAL]
case neg.neg
⊢ neg ≤ neg ∨ neg ≤ neg
[PROOFSTEP]
left
[GOAL]
case neg.neg.h
⊢ neg ≤ neg
[PROOFSTEP]
constructor
[GOAL]
case neg.pos
⊢ neg ≤ pos ∨ pos ≤ neg
[PROOFSTEP]
first
| left; constructor
| right; constructor
[GOAL]
case neg.pos
⊢ neg ≤ pos ∨ pos ≤ neg
[PROOFSTEP]
left
[GOAL]
case neg.pos.h
⊢ neg ≤ pos
[PROOFSTEP]
constructor
[GOAL]
case pos.zero
⊢ pos ≤ zero ∨ zero ≤ pos
[PROOFSTEP]
first
| left; constructor
| right; constructor
[GOAL]
case pos.zero
⊢ pos ≤ zero ∨ zero ≤ pos
[PROOFSTEP]
left
[GOAL]
case pos.zero.h
⊢ pos ≤ zero
[PROOFSTEP]
constructor
[GOAL]
case pos.zero
⊢ pos ≤ zero ∨ zero ≤ pos
[PROOFSTEP]
right
[GOAL]
case pos.zero.h
⊢ zero ≤ pos
[PROOFSTEP]
constructor
[GOAL]
case pos.neg
⊢ pos ≤ neg ∨ neg ≤ pos
[PROOFSTEP]
first
| left; constructor
| right; constructor
[GOAL]
case pos.neg
⊢ pos ≤ neg ∨ neg ≤ pos
[PROOFSTEP]
left
[GOAL]
case pos.neg.h
⊢ pos ≤ neg
[PROOFSTEP]
constructor
[GOAL]
case pos.neg
⊢ pos ≤ neg ∨ neg ≤ pos
[PROOFSTEP]
right
[GOAL]
case pos.neg.h
⊢ neg ≤ pos
[PROOFSTEP]
constructor
[GOAL]
case pos.pos
⊢ pos ≤ pos ∨ pos ≤ pos
[PROOFSTEP]
first
| left; constructor
| right; constructor
[GOAL]
case pos.pos
⊢ pos ≤ pos ∨ pos ≤ pos
[PROOFSTEP]
left
[GOAL]
case pos.pos.h
⊢ pos ≤ pos
[PROOFSTEP]
constructor
[GOAL]
x : SignType
⊢ - -x = x
[PROOFSTEP]
cases x
[GOAL]
case zero
⊢ - -zero = zero
[PROOFSTEP]
rfl
[GOAL]
case neg
⊢ - -neg = neg
[PROOFSTEP]
rfl
[GOAL]
case pos
⊢ - -pos = pos
[PROOFSTEP]
rfl
[GOAL]
x y : SignType
⊢ -x * y = -(x * y)
[PROOFSTEP]
cases x
[GOAL]
case zero
y : SignType
⊢ -zero * y = -(zero * y)
[PROOFSTEP]
cases y
[GOAL]
case neg
y : SignType
⊢ -neg * y = -(neg * y)
[PROOFSTEP]
cases y
[GOAL]
case pos
y : SignType
⊢ -pos * y = -(pos * y)
[PROOFSTEP]
cases y
[GOAL]
case zero.zero
⊢ -zero * zero = -(zero * zero)
[PROOFSTEP]
rfl
[GOAL]
case zero.neg
⊢ -zero * neg = -(zero * neg)
[PROOFSTEP]
rfl
[GOAL]
case zero.pos
⊢ -zero * pos = -(zero * pos)
[PROOFSTEP]
rfl
[GOAL]
case neg.zero
⊢ -neg * zero = -(neg * zero)
[PROOFSTEP]
rfl
[GOAL]
case neg.neg
⊢ -neg * neg = -(neg * neg)
[PROOFSTEP]
rfl
[GOAL]
case neg.pos
⊢ -neg * pos = -(neg * pos)
[PROOFSTEP]
rfl
[GOAL]
case pos.zero
⊢ -pos * zero = -(pos * zero)
[PROOFSTEP]
rfl
[GOAL]
case pos.neg
⊢ -pos * neg = -(pos * neg)
[PROOFSTEP]
rfl
[GOAL]
case pos.pos
⊢ -pos * pos = -(pos * pos)
[PROOFSTEP]
rfl
[GOAL]
x y : SignType
⊢ x * -y = -(x * y)
[PROOFSTEP]
cases x
[GOAL]
case zero
y : SignType
⊢ zero * -y = -(zero * y)
[PROOFSTEP]
cases y
[GOAL]
case neg
y : SignType
⊢ neg * -y = -(neg * y)
[PROOFSTEP]
cases y
[GOAL]
case pos
y : SignType
⊢ pos * -y = -(pos * y)
[PROOFSTEP]
cases y
[GOAL]
case zero.zero
⊢ zero * -zero = -(zero * zero)
[PROOFSTEP]
rfl
[GOAL]
case zero.neg
⊢ zero * -neg = -(zero * neg)
[PROOFSTEP]
rfl
[GOAL]
case zero.pos
⊢ zero * -pos = -(zero * pos)
[PROOFSTEP]
rfl
[GOAL]
case neg.zero
⊢ neg * -zero = -(neg * zero)
[PROOFSTEP]
rfl
[GOAL]
case neg.neg
⊢ neg * -neg = -(neg * neg)
[PROOFSTEP]
rfl
[GOAL]
case neg.pos
⊢ neg * -pos = -(neg * pos)
[PROOFSTEP]
rfl
[GOAL]
case pos.zero
⊢ pos * -zero = -(pos * zero)
[PROOFSTEP]
rfl
[GOAL]
case pos.neg
⊢ pos * -neg = -(pos * neg)
[PROOFSTEP]
rfl
[GOAL]
case pos.pos
⊢ pos * -pos = -(pos * pos)
[PROOFSTEP]
rfl
[GOAL]
a : SignType
⊢ 0 < 3
[PROOFSTEP]
simp
[GOAL]
a : SignType
⊢ 1 < 3
[PROOFSTEP]
simp
[GOAL]
a : SignType
⊢ 2 < 3
[PROOFSTEP]
simp
[GOAL]
a : SignType
⊢ (fun a =>
        match a with
        | { val := 0, isLt := isLt } => 0
        | { val := 1, isLt := isLt } => 1
        | { val := 2, isLt := isLt } => -1
        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
      ((fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) })
        a) =
    a
[PROOFSTEP]
cases a
[GOAL]
case zero
⊢ (fun a =>
        match a with
        | { val := 0, isLt := isLt } => 0
        | { val := 1, isLt := isLt } => 1
        | { val := 2, isLt := isLt } => -1
        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
      ((fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) })
        zero) =
    zero
[PROOFSTEP]
rfl
[GOAL]
case neg
⊢ (fun a =>
        match a with
        | { val := 0, isLt := isLt } => 0
        | { val := 1, isLt := isLt } => 1
        | { val := 2, isLt := isLt } => -1
        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
      ((fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) })
        neg) =
    neg
[PROOFSTEP]
rfl
[GOAL]
case pos
⊢ (fun a =>
        match a with
        | { val := 0, isLt := isLt } => 0
        | { val := 1, isLt := isLt } => 1
        | { val := 2, isLt := isLt } => -1
        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
      ((fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) })
        pos) =
    pos
[PROOFSTEP]
rfl
[GOAL]
a : Fin 3
isLt✝ : 0 < 3
⊢ (fun a =>
        match a with
        | zero => { val := 0, isLt := (_ : 0 < 3) }
        | pos => { val := 1, isLt := (_ : 1 < 3) }
        | neg => { val := 2, isLt := (_ : 2 < 3) })
      ((fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
        { val := 0, isLt := isLt✝ }) =
    { val := 0, isLt := isLt✝ }
[PROOFSTEP]
simp
[GOAL]
a : Fin 3
isLt✝ : 1 < 3
⊢ (fun a =>
        match a with
        | zero => { val := 0, isLt := (_ : 0 < 3) }
        | pos => { val := 1, isLt := (_ : 1 < 3) }
        | neg => { val := 2, isLt := (_ : 2 < 3) })
      ((fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
        { val := 1, isLt := isLt✝ }) =
    { val := 1, isLt := isLt✝ }
[PROOFSTEP]
simp
[GOAL]
a : Fin 3
isLt✝ : 2 < 3
⊢ (fun a =>
        match a with
        | zero => { val := 0, isLt := (_ : 0 < 3) }
        | pos => { val := 1, isLt := (_ : 1 < 3) }
        | neg => { val := 2, isLt := (_ : 2 < 3) })
      ((fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
        { val := 2, isLt := isLt✝ }) =
    { val := 2, isLt := isLt✝ }
[PROOFSTEP]
simp
[GOAL]
a : Fin 3
n : ℕ
h : n + 3 < 3
⊢ (fun a =>
        match a with
        | zero => { val := 0, isLt := (_ : 0 < 3) }
        | pos => { val := 1, isLt := (_ : 1 < 3) }
        | neg => { val := 2, isLt := (_ : 2 < 3) })
      ((fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
        { val := n + 3, isLt := h }) =
    { val := n + 3, isLt := h }
[PROOFSTEP]
simp at h 
[GOAL]
a b : SignType
⊢ Equiv.toFun
      {
        toFun := fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) },
        invFun := fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
        left_inv :=
          (_ :
            ∀ (a : SignType),
              (fun a =>
                    match a with
                    | { val := 0, isLt := isLt } => 0
                    | { val := 1, isLt := isLt } => 1
                    | { val := 2, isLt := isLt } => -1
                    | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                  ((fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    a) =
                a),
        right_inv :=
          (_ :
            ∀ (a : Fin 3),
              (fun a =>
                    match a with
                    | zero => { val := 0, isLt := (_ : 0 < 3) }
                    | pos => { val := 1, isLt := (_ : 1 < 3) }
                    | neg => { val := 2, isLt := (_ : 2 < 3) })
                  ((fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    a) =
                a) }
      (a * b) =
    Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        a *
      Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        b
[PROOFSTEP]
cases a
[GOAL]
case zero
b : SignType
⊢ Equiv.toFun
      {
        toFun := fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) },
        invFun := fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
        left_inv :=
          (_ :
            ∀ (a : SignType),
              (fun a =>
                    match a with
                    | { val := 0, isLt := isLt } => 0
                    | { val := 1, isLt := isLt } => 1
                    | { val := 2, isLt := isLt } => -1
                    | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                  ((fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    a) =
                a),
        right_inv :=
          (_ :
            ∀ (a : Fin 3),
              (fun a =>
                    match a with
                    | zero => { val := 0, isLt := (_ : 0 < 3) }
                    | pos => { val := 1, isLt := (_ : 1 < 3) }
                    | neg => { val := 2, isLt := (_ : 2 < 3) })
                  ((fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    a) =
                a) }
      (zero * b) =
    Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        zero *
      Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        b
[PROOFSTEP]
cases b
[GOAL]
case neg
b : SignType
⊢ Equiv.toFun
      {
        toFun := fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) },
        invFun := fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
        left_inv :=
          (_ :
            ∀ (a : SignType),
              (fun a =>
                    match a with
                    | { val := 0, isLt := isLt } => 0
                    | { val := 1, isLt := isLt } => 1
                    | { val := 2, isLt := isLt } => -1
                    | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                  ((fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    a) =
                a),
        right_inv :=
          (_ :
            ∀ (a : Fin 3),
              (fun a =>
                    match a with
                    | zero => { val := 0, isLt := (_ : 0 < 3) }
                    | pos => { val := 1, isLt := (_ : 1 < 3) }
                    | neg => { val := 2, isLt := (_ : 2 < 3) })
                  ((fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    a) =
                a) }
      (neg * b) =
    Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        neg *
      Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        b
[PROOFSTEP]
cases b
[GOAL]
case pos
b : SignType
⊢ Equiv.toFun
      {
        toFun := fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) },
        invFun := fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
        left_inv :=
          (_ :
            ∀ (a : SignType),
              (fun a =>
                    match a with
                    | { val := 0, isLt := isLt } => 0
                    | { val := 1, isLt := isLt } => 1
                    | { val := 2, isLt := isLt } => -1
                    | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                  ((fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    a) =
                a),
        right_inv :=
          (_ :
            ∀ (a : Fin 3),
              (fun a =>
                    match a with
                    | zero => { val := 0, isLt := (_ : 0 < 3) }
                    | pos => { val := 1, isLt := (_ : 1 < 3) }
                    | neg => { val := 2, isLt := (_ : 2 < 3) })
                  ((fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    a) =
                a) }
      (pos * b) =
    Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        pos *
      Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        b
[PROOFSTEP]
cases b
[GOAL]
case zero.zero
⊢ Equiv.toFun
      {
        toFun := fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) },
        invFun := fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
        left_inv :=
          (_ :
            ∀ (a : SignType),
              (fun a =>
                    match a with
                    | { val := 0, isLt := isLt } => 0
                    | { val := 1, isLt := isLt } => 1
                    | { val := 2, isLt := isLt } => -1
                    | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                  ((fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    a) =
                a),
        right_inv :=
          (_ :
            ∀ (a : Fin 3),
              (fun a =>
                    match a with
                    | zero => { val := 0, isLt := (_ : 0 < 3) }
                    | pos => { val := 1, isLt := (_ : 1 < 3) }
                    | neg => { val := 2, isLt := (_ : 2 < 3) })
                  ((fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    a) =
                a) }
      (zero * zero) =
    Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        zero *
      Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        zero
[PROOFSTEP]
simp
[GOAL]
case zero.neg
⊢ Equiv.toFun
      {
        toFun := fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) },
        invFun := fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
        left_inv :=
          (_ :
            ∀ (a : SignType),
              (fun a =>
                    match a with
                    | { val := 0, isLt := isLt } => 0
                    | { val := 1, isLt := isLt } => 1
                    | { val := 2, isLt := isLt } => -1
                    | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                  ((fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    a) =
                a),
        right_inv :=
          (_ :
            ∀ (a : Fin 3),
              (fun a =>
                    match a with
                    | zero => { val := 0, isLt := (_ : 0 < 3) }
                    | pos => { val := 1, isLt := (_ : 1 < 3) }
                    | neg => { val := 2, isLt := (_ : 2 < 3) })
                  ((fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    a) =
                a) }
      (zero * neg) =
    Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        zero *
      Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        neg
[PROOFSTEP]
simp
[GOAL]
case zero.pos
⊢ Equiv.toFun
      {
        toFun := fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) },
        invFun := fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
        left_inv :=
          (_ :
            ∀ (a : SignType),
              (fun a =>
                    match a with
                    | { val := 0, isLt := isLt } => 0
                    | { val := 1, isLt := isLt } => 1
                    | { val := 2, isLt := isLt } => -1
                    | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                  ((fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    a) =
                a),
        right_inv :=
          (_ :
            ∀ (a : Fin 3),
              (fun a =>
                    match a with
                    | zero => { val := 0, isLt := (_ : 0 < 3) }
                    | pos => { val := 1, isLt := (_ : 1 < 3) }
                    | neg => { val := 2, isLt := (_ : 2 < 3) })
                  ((fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    a) =
                a) }
      (zero * pos) =
    Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        zero *
      Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        pos
[PROOFSTEP]
simp
[GOAL]
case neg.zero
⊢ Equiv.toFun
      {
        toFun := fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) },
        invFun := fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
        left_inv :=
          (_ :
            ∀ (a : SignType),
              (fun a =>
                    match a with
                    | { val := 0, isLt := isLt } => 0
                    | { val := 1, isLt := isLt } => 1
                    | { val := 2, isLt := isLt } => -1
                    | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                  ((fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    a) =
                a),
        right_inv :=
          (_ :
            ∀ (a : Fin 3),
              (fun a =>
                    match a with
                    | zero => { val := 0, isLt := (_ : 0 < 3) }
                    | pos => { val := 1, isLt := (_ : 1 < 3) }
                    | neg => { val := 2, isLt := (_ : 2 < 3) })
                  ((fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    a) =
                a) }
      (neg * zero) =
    Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        neg *
      Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        zero
[PROOFSTEP]
simp
[GOAL]
case neg.neg
⊢ Equiv.toFun
      {
        toFun := fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) },
        invFun := fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
        left_inv :=
          (_ :
            ∀ (a : SignType),
              (fun a =>
                    match a with
                    | { val := 0, isLt := isLt } => 0
                    | { val := 1, isLt := isLt } => 1
                    | { val := 2, isLt := isLt } => -1
                    | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                  ((fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    a) =
                a),
        right_inv :=
          (_ :
            ∀ (a : Fin 3),
              (fun a =>
                    match a with
                    | zero => { val := 0, isLt := (_ : 0 < 3) }
                    | pos => { val := 1, isLt := (_ : 1 < 3) }
                    | neg => { val := 2, isLt := (_ : 2 < 3) })
                  ((fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    a) =
                a) }
      (neg * neg) =
    Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        neg *
      Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        neg
[PROOFSTEP]
simp
[GOAL]
case neg.pos
⊢ Equiv.toFun
      {
        toFun := fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) },
        invFun := fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
        left_inv :=
          (_ :
            ∀ (a : SignType),
              (fun a =>
                    match a with
                    | { val := 0, isLt := isLt } => 0
                    | { val := 1, isLt := isLt } => 1
                    | { val := 2, isLt := isLt } => -1
                    | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                  ((fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    a) =
                a),
        right_inv :=
          (_ :
            ∀ (a : Fin 3),
              (fun a =>
                    match a with
                    | zero => { val := 0, isLt := (_ : 0 < 3) }
                    | pos => { val := 1, isLt := (_ : 1 < 3) }
                    | neg => { val := 2, isLt := (_ : 2 < 3) })
                  ((fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    a) =
                a) }
      (neg * pos) =
    Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        neg *
      Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        pos
[PROOFSTEP]
simp
[GOAL]
case pos.zero
⊢ Equiv.toFun
      {
        toFun := fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) },
        invFun := fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
        left_inv :=
          (_ :
            ∀ (a : SignType),
              (fun a =>
                    match a with
                    | { val := 0, isLt := isLt } => 0
                    | { val := 1, isLt := isLt } => 1
                    | { val := 2, isLt := isLt } => -1
                    | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                  ((fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    a) =
                a),
        right_inv :=
          (_ :
            ∀ (a : Fin 3),
              (fun a =>
                    match a with
                    | zero => { val := 0, isLt := (_ : 0 < 3) }
                    | pos => { val := 1, isLt := (_ : 1 < 3) }
                    | neg => { val := 2, isLt := (_ : 2 < 3) })
                  ((fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    a) =
                a) }
      (pos * zero) =
    Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        pos *
      Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        zero
[PROOFSTEP]
simp
[GOAL]
case pos.neg
⊢ Equiv.toFun
      {
        toFun := fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) },
        invFun := fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
        left_inv :=
          (_ :
            ∀ (a : SignType),
              (fun a =>
                    match a with
                    | { val := 0, isLt := isLt } => 0
                    | { val := 1, isLt := isLt } => 1
                    | { val := 2, isLt := isLt } => -1
                    | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                  ((fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    a) =
                a),
        right_inv :=
          (_ :
            ∀ (a : Fin 3),
              (fun a =>
                    match a with
                    | zero => { val := 0, isLt := (_ : 0 < 3) }
                    | pos => { val := 1, isLt := (_ : 1 < 3) }
                    | neg => { val := 2, isLt := (_ : 2 < 3) })
                  ((fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    a) =
                a) }
      (pos * neg) =
    Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        pos *
      Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        neg
[PROOFSTEP]
simp
[GOAL]
case pos.pos
⊢ Equiv.toFun
      {
        toFun := fun a =>
          match a with
          | zero => { val := 0, isLt := (_ : 0 < 3) }
          | pos => { val := 1, isLt := (_ : 1 < 3) }
          | neg => { val := 2, isLt := (_ : 2 < 3) },
        invFun := fun a =>
          match a with
          | { val := 0, isLt := isLt } => 0
          | { val := 1, isLt := isLt } => 1
          | { val := 2, isLt := isLt } => -1
          | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
        left_inv :=
          (_ :
            ∀ (a : SignType),
              (fun a =>
                    match a with
                    | { val := 0, isLt := isLt } => 0
                    | { val := 1, isLt := isLt } => 1
                    | { val := 2, isLt := isLt } => -1
                    | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                  ((fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    a) =
                a),
        right_inv :=
          (_ :
            ∀ (a : Fin 3),
              (fun a =>
                    match a with
                    | zero => { val := 0, isLt := (_ : 0 < 3) }
                    | pos => { val := 1, isLt := (_ : 1 < 3) }
                    | neg => { val := 2, isLt := (_ : 2 < 3) })
                  ((fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    a) =
                a) }
      (pos * pos) =
    Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        pos *
      Equiv.toFun
        {
          toFun := fun a =>
            match a with
            | zero => { val := 0, isLt := (_ : 0 < 3) }
            | pos => { val := 1, isLt := (_ : 1 < 3) }
            | neg => { val := 2, isLt := (_ : 2 < 3) },
          invFun := fun a =>
            match a with
            | { val := 0, isLt := isLt } => 0
            | { val := 1, isLt := isLt } => 1
            | { val := 2, isLt := isLt } => -1
            | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False),
          left_inv :=
            (_ :
              ∀ (a : SignType),
                (fun a =>
                      match a with
                      | { val := 0, isLt := isLt } => 0
                      | { val := 1, isLt := isLt } => 1
                      | { val := 2, isLt := isLt } => -1
                      | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                    ((fun a =>
                        match a with
                        | zero => { val := 0, isLt := (_ : 0 < 3) }
                        | pos => { val := 1, isLt := (_ : 1 < 3) }
                        | neg => { val := 2, isLt := (_ : 2 < 3) })
                      a) =
                  a),
          right_inv :=
            (_ :
              ∀ (a : Fin 3),
                (fun a =>
                      match a with
                      | zero => { val := 0, isLt := (_ : 0 < 3) }
                      | pos => { val := 1, isLt := (_ : 1 < 3) }
                      | neg => { val := 2, isLt := (_ : 2 < 3) })
                    ((fun a =>
                        match a with
                        | { val := 0, isLt := isLt } => 0
                        | { val := 1, isLt := isLt } => 1
                        | { val := 2, isLt := isLt } => -1
                        | { val := Nat.succ (Nat.succ (Nat.succ n)), isLt := h } => False.elim (_ : False))
                      a) =
                  a) }
        pos
[PROOFSTEP]
simp
[GOAL]
a : SignType
⊢ 0 ≤ a ↔ a = 0 ∨ a = 1
[PROOFSTEP]
cases a
[GOAL]
case zero
⊢ 0 ≤ zero ↔ zero = 0 ∨ zero = 1
[PROOFSTEP]
decide
[GOAL]
case neg
⊢ 0 ≤ neg ↔ neg = 0 ∨ neg = 1
[PROOFSTEP]
decide
[GOAL]
case pos
⊢ 0 ≤ pos ↔ pos = 0 ∨ pos = 1
[PROOFSTEP]
decide
[GOAL]
a : SignType
⊢ 0 ≤ a ↔ a ≠ -1
[PROOFSTEP]
cases a
[GOAL]
case zero
⊢ 0 ≤ zero ↔ zero ≠ -1
[PROOFSTEP]
decide
[GOAL]
case neg
⊢ 0 ≤ neg ↔ neg ≠ -1
[PROOFSTEP]
decide
[GOAL]
case pos
⊢ 0 ≤ pos ↔ pos ≠ -1
[PROOFSTEP]
decide
[GOAL]
a : SignType
⊢ -1 < a ↔ 0 ≤ a
[PROOFSTEP]
cases a
[GOAL]
case zero
⊢ -1 < zero ↔ 0 ≤ zero
[PROOFSTEP]
decide
[GOAL]
case neg
⊢ -1 < neg ↔ 0 ≤ neg
[PROOFSTEP]
decide
[GOAL]
case pos
⊢ -1 < pos ↔ 0 ≤ pos
[PROOFSTEP]
decide
[GOAL]
a : SignType
⊢ a ≤ 0 ↔ a = -1 ∨ a = 0
[PROOFSTEP]
cases a
[GOAL]
case zero
⊢ zero ≤ 0 ↔ zero = -1 ∨ zero = 0
[PROOFSTEP]
decide
[GOAL]
case neg
⊢ neg ≤ 0 ↔ neg = -1 ∨ neg = 0
[PROOFSTEP]
decide
[GOAL]
case pos
⊢ pos ≤ 0 ↔ pos = -1 ∨ pos = 0
[PROOFSTEP]
decide
[GOAL]
a : SignType
⊢ a ≤ 0 ↔ a ≠ 1
[PROOFSTEP]
cases a
[GOAL]
case zero
⊢ zero ≤ 0 ↔ zero ≠ 1
[PROOFSTEP]
decide
[GOAL]
case neg
⊢ neg ≤ 0 ↔ neg ≠ 1
[PROOFSTEP]
decide
[GOAL]
case pos
⊢ pos ≤ 0 ↔ pos ≠ 1
[PROOFSTEP]
decide
[GOAL]
a : SignType
⊢ a < 1 ↔ a ≤ 0
[PROOFSTEP]
cases a
[GOAL]
case zero
⊢ zero < 1 ↔ zero ≤ 0
[PROOFSTEP]
decide
[GOAL]
case neg
⊢ neg < 1 ↔ neg ≤ 0
[PROOFSTEP]
decide
[GOAL]
case pos
⊢ pos < 1 ↔ pos ≤ 0
[PROOFSTEP]
decide
[GOAL]
a : SignType
⊢ a < 0 ↔ a = -1
[PROOFSTEP]
cases a
[GOAL]
case zero
⊢ zero < 0 ↔ zero = -1
[PROOFSTEP]
decide
[GOAL]
case neg
⊢ neg < 0 ↔ neg = -1
[PROOFSTEP]
decide
[GOAL]
case pos
⊢ pos < 0 ↔ pos = -1
[PROOFSTEP]
decide
[GOAL]
a : SignType
⊢ 0 < a ↔ a = 1
[PROOFSTEP]
cases a
[GOAL]
case zero
⊢ 0 < zero ↔ zero = 1
[PROOFSTEP]
decide
[GOAL]
case neg
⊢ 0 < neg ↔ neg = 1
[PROOFSTEP]
decide
[GOAL]
case pos
⊢ 0 < pos ↔ pos = 1
[PROOFSTEP]
decide
[GOAL]
a : SignType
⊢ a = -a ↔ a = 0
[PROOFSTEP]
cases a
[GOAL]
case zero
⊢ zero = -zero ↔ zero = 0
[PROOFSTEP]
decide
[GOAL]
case neg
⊢ neg = -neg ↔ neg = 0
[PROOFSTEP]
decide
[GOAL]
case pos
⊢ pos = -pos ↔ pos = 0
[PROOFSTEP]
decide
[GOAL]
a : SignType
⊢ -a = a ↔ a = 0
[PROOFSTEP]
cases a
[GOAL]
case zero
⊢ -zero = zero ↔ zero = 0
[PROOFSTEP]
decide
[GOAL]
case neg
⊢ -neg = neg ↔ neg = 0
[PROOFSTEP]
decide
[GOAL]
case pos
⊢ -pos = pos ↔ pos = 0
[PROOFSTEP]
decide
[GOAL]
α : Type ?u.34903
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
x y : SignType
⊢ ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } (x * y) =
    ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } x *
      ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } y
[PROOFSTEP]
cases x
[GOAL]
case zero
α : Type ?u.34903
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
y : SignType
⊢ ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } (zero * y) =
    ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } zero *
      ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } y
[PROOFSTEP]
cases y
[GOAL]
case neg
α : Type ?u.34903
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
y : SignType
⊢ ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } (neg * y) =
    ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } neg *
      ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } y
[PROOFSTEP]
cases y
[GOAL]
case pos
α : Type ?u.34903
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
y : SignType
⊢ ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } (pos * y) =
    ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } pos *
      ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } y
[PROOFSTEP]
cases y
[GOAL]
case zero.zero
α : Type ?u.34903
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } (zero * zero) =
    ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } zero *
      ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } zero
[PROOFSTEP]
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]
[GOAL]
case zero.neg
α : Type ?u.34903
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } (zero * neg) =
    ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } zero *
      ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } neg
[PROOFSTEP]
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]
[GOAL]
case zero.pos
α : Type ?u.34903
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } (zero * pos) =
    ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } zero *
      ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } pos
[PROOFSTEP]
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]
[GOAL]
case neg.zero
α : Type ?u.34903
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } (neg * zero) =
    ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } neg *
      ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } zero
[PROOFSTEP]
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]
[GOAL]
case neg.neg
α : Type ?u.34903
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } (neg * neg) =
    ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } neg *
      ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } neg
[PROOFSTEP]
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]
[GOAL]
case neg.pos
α : Type ?u.34903
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } (neg * pos) =
    ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } neg *
      ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } pos
[PROOFSTEP]
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]
[GOAL]
case pos.zero
α : Type ?u.34903
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } (pos * zero) =
    ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } pos *
      ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } zero
[PROOFSTEP]
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]
[GOAL]
case pos.neg
α : Type ?u.34903
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } (pos * neg) =
    ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } pos *
      ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } neg
[PROOFSTEP]
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]
[GOAL]
case pos.pos
α : Type ?u.34903
inst✝¹ : MulZeroOneClass α
inst✝ : HasDistribNeg α
⊢ ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } (pos * pos) =
    ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } pos *
      ZeroHom.toFun { toFun := cast, map_zero' := (_ : ↑0 = ↑0) } pos
[PROOFSTEP]
simp [zero_eq_zero, pos_eq_one, neg_eq_neg_one]
[GOAL]
⊢ Finset.univ = {0, -1, 1}
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
f : SignType → α
⊢ Set.range f = {f zero, f neg, f pos}
[PROOFSTEP]
classical rw [← Fintype.coe_image_univ, univ_eq]
[GOAL]
α : Type u_1
f : SignType → α
⊢ Set.range f = {f zero, f neg, f pos}
[PROOFSTEP]
rw [← Fintype.coe_image_univ, univ_eq]
[GOAL]
α : Type u_1
f : SignType → α
⊢ ↑(Finset.image f {0, -1, 1}) = {f zero, f neg, f pos}
[PROOFSTEP]
classical simp [Finset.coe_insert]
[GOAL]
α : Type u_1
f : SignType → α
⊢ ↑(Finset.image f {0, -1, 1}) = {f zero, f neg, f pos}
[PROOFSTEP]
simp [Finset.coe_insert]
[GOAL]
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
⊢ (fun a => if 0 < a then 1 else if a < 0 then -1 else 0) a ≤ (fun a => if 0 < a then 1 else if a < 0 then -1 else 0) b
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
⊢ (if 0 < a then 1 else if a < 0 then -1 else 0) ≤ if 0 < b then 1 else if b < 0 then -1 else 0
[PROOFSTEP]
split_ifs with h₁ h₂ h₃ h₄ _ _ h₂ h₃
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : 0 < b
⊢ 1 ≤ 1
[PROOFSTEP]
try constructor
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : 0 < b
⊢ 1 ≤ 1
[PROOFSTEP]
constructor
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : b < 0
⊢ 1 ≤ -1
[PROOFSTEP]
try constructor
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : b < 0
⊢ 1 ≤ -1
[PROOFSTEP]
constructor
[GOAL]
case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 1 ≤ 0
[PROOFSTEP]
try constructor
[GOAL]
case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 1 ≤ 0
[PROOFSTEP]
constructor
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_ : 0 < b
⊢ -1 ≤ 1
[PROOFSTEP]
try constructor
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_ : 0 < b
⊢ -1 ≤ 1
[PROOFSTEP]
constructor
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_✝ : ¬0 < b
_ : b < 0
⊢ -1 ≤ -1
[PROOFSTEP]
try constructor
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_✝ : ¬0 < b
_ : b < 0
⊢ -1 ≤ -1
[PROOFSTEP]
constructor
[GOAL]
case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_✝ : ¬0 < b
_ : ¬b < 0
⊢ -1 ≤ 0
[PROOFSTEP]
try constructor
[GOAL]
case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_✝ : ¬0 < b
_ : ¬b < 0
⊢ -1 ≤ 0
[PROOFSTEP]
constructor
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : 0 < b
⊢ 0 ≤ 1
[PROOFSTEP]
try constructor
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : 0 < b
⊢ 0 ≤ 1
[PROOFSTEP]
constructor
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : b < 0
⊢ 0 ≤ -1
[PROOFSTEP]
try constructor
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : b < 0
⊢ 0 ≤ -1
[PROOFSTEP]
constructor
[GOAL]
case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 0 ≤ 0
[PROOFSTEP]
try constructor
[GOAL]
case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 0 ≤ 0
[PROOFSTEP]
constructor
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : b < 0
⊢ 1 ≤ -1
[PROOFSTEP]
cases lt_irrefl 0 (h₁.trans <| h.trans_lt h₃)
[GOAL]
case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 1 ≤ 0
[PROOFSTEP]
cases h₂ (h₁.trans_le h)
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : b < 0
⊢ 0 ≤ -1
[PROOFSTEP]
cases h₄ (h.trans_lt h₃)
[GOAL]
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
⊢ ↑sign 0 = 0
[PROOFSTEP]
simp [sign_apply]
[GOAL]
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
ha : 0 < a
⊢ ↑sign a = 1
[PROOFSTEP]
rwa [sign_apply, if_pos]
[GOAL]
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
ha : a < 0
⊢ ↑sign a = -1
[PROOFSTEP]
rwa [sign_apply, if_neg <| asymm ha, if_pos]
[GOAL]
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
⊢ ↑sign a = 1 ↔ 0 < a
[PROOFSTEP]
refine' ⟨fun h => _, fun h => sign_pos h⟩
[GOAL]
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
h : ↑sign a = 1
⊢ 0 < a
[PROOFSTEP]
by_contra hn
[GOAL]
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
h : ↑sign a = 1
hn : ¬0 < a
⊢ False
[PROOFSTEP]
rw [sign_apply, if_neg hn] at h 
[GOAL]
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
h : (if a < 0 then -1 else 0) = 1
hn : ¬0 < a
⊢ False
[PROOFSTEP]
split_ifs at h 
[GOAL]
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
⊢ ↑sign a = -1 ↔ a < 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => sign_neg h⟩
[GOAL]
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
h : ↑sign a = -1
⊢ a < 0
[PROOFSTEP]
rw [sign_apply] at h 
[GOAL]
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = -1
⊢ a < 0
[PROOFSTEP]
split_ifs at h 
[GOAL]
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x < x_1
a : α
h✝¹ : ¬0 < a
h✝ : a < 0
h : -1 = -1
⊢ a < 0
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
⊢ ↑sign a = 0 ↔ a = 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.symm ▸ sign_zero⟩
[GOAL]
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : ↑sign a = 0
⊢ a = 0
[PROOFSTEP]
rw [sign_apply] at h 
[GOAL]
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = 0
⊢ a = 0
[PROOFSTEP]
split_ifs at h  with h_1 h_2
[GOAL]
case neg
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h_1 : ¬0 < a
h_2 : ¬a < 0
h : 0 = 0
⊢ a = 0
[PROOFSTEP]
cases' h
[GOAL]
case neg.refl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h_1 : ¬0 < a
h_2 : ¬a < 0
⊢ a = 0
[PROOFSTEP]
exact (le_of_not_lt h_1).eq_of_not_lt h_2
[GOAL]
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
⊢ 0 ≤ ↑sign a ↔ 0 ≤ a
[PROOFSTEP]
rcases lt_trichotomy 0 a with (h | h | h)
[GOAL]
case inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 < a
⊢ 0 ≤ ↑sign a ↔ 0 ≤ a
[PROOFSTEP]
simp [h, h.le]
[GOAL]
case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 = a
⊢ 0 ≤ ↑sign a ↔ 0 ≤ a
[PROOFSTEP]
simp [← h]
[GOAL]
case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : a < 0
⊢ 0 ≤ ↑sign a ↔ 0 ≤ a
[PROOFSTEP]
simp [h, h.not_le]
[GOAL]
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
⊢ ↑sign a ≤ 0 ↔ a ≤ 0
[PROOFSTEP]
rcases lt_trichotomy 0 a with (h | h | h)
[GOAL]
case inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 < a
⊢ ↑sign a ≤ 0 ↔ a ≤ 0
[PROOFSTEP]
simp [h, h.not_le]
[GOAL]
case inr.inl
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : 0 = a
⊢ ↑sign a ≤ 0 ↔ a ≤ 0
[PROOFSTEP]
simp [← h]
[GOAL]
case inr.inr
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : a < 0
⊢ ↑sign a ≤ 0 ↔ a ≤ 0
[PROOFSTEP]
simp [h, h.le]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b x y : α
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
[PROOFSTEP]
rcases lt_trichotomy x 0 with (hx | hx | hx)
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedRing α
a b x y : α
hx : x < 0
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
[PROOFSTEP]
rcases lt_trichotomy y 0 with (hy | hy | hy)
[GOAL]
case inr.inl
α : Type u_1
inst✝ : LinearOrderedRing α
a b x y : α
hx : x = 0
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
[PROOFSTEP]
rcases lt_trichotomy y 0 with (hy | hy | hy)
[GOAL]
case inr.inr
α : Type u_1
inst✝ : LinearOrderedRing α
a b x y : α
hx : 0 < x
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
[PROOFSTEP]
rcases lt_trichotomy y 0 with (hy | hy | hy)
[GOAL]
case inl.inl
α : Type u_1
inst✝ : LinearOrderedRing α
a b x y : α
hx : x < 0
hy : y < 0
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
[PROOFSTEP]
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case inl.inr.inl
α : Type u_1
inst✝ : LinearOrderedRing α
a b x y : α
hx : x < 0
hy : y = 0
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
[PROOFSTEP]
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case inl.inr.inr
α : Type u_1
inst✝ : LinearOrderedRing α
a b x y : α
hx : x < 0
hy : 0 < y
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
[PROOFSTEP]
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case inr.inl.inl
α : Type u_1
inst✝ : LinearOrderedRing α
a b x y : α
hx : x = 0
hy : y < 0
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
[PROOFSTEP]
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case inr.inl.inr.inl
α : Type u_1
inst✝ : LinearOrderedRing α
a b x y : α
hx : x = 0
hy : y = 0
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
[PROOFSTEP]
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case inr.inl.inr.inr
α : Type u_1
inst✝ : LinearOrderedRing α
a b x y : α
hx : x = 0
hy : 0 < y
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
[PROOFSTEP]
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case inr.inr.inl
α : Type u_1
inst✝ : LinearOrderedRing α
a b x y : α
hx : 0 < x
hy : y < 0
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
[PROOFSTEP]
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case inr.inr.inr.inl
α : Type u_1
inst✝ : LinearOrderedRing α
a b x y : α
hx : 0 < x
hy : y = 0
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
[PROOFSTEP]
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
case inr.inr.inr.inr
α : Type u_1
inst✝ : LinearOrderedRing α
a b x y : α
hx : 0 < x
hy : 0 < y
⊢ ↑sign (x * y) = ↑sign x * ↑sign y
[PROOFSTEP]
simp [hx, hy, mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b x : α
⊢ ↑(↑sign x) * |x| = x
[PROOFSTEP]
rcases lt_trichotomy x 0 with (hx | rfl | hx)
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedRing α
a b x : α
hx : x < 0
⊢ ↑(↑sign x) * |x| = x
[PROOFSTEP]
rw [sign_neg hx, abs_of_neg hx, coe_neg_one, neg_one_mul, neg_neg]
[GOAL]
case inr.inl
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ ↑(↑sign 0) * |0| = 0
[PROOFSTEP]
rw [abs_zero, mul_zero]
[GOAL]
case inr.inr
α : Type u_1
inst✝ : LinearOrderedRing α
a b x : α
hx : 0 < x
⊢ ↑(↑sign x) * |x| = x
[PROOFSTEP]
rw [sign_pos hx, abs_of_pos hx, coe_one, one_mul]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
a b x : α
⊢ |x| * ↑(↑sign x) = x
[PROOFSTEP]
rcases lt_trichotomy x 0 with (hx | rfl | hx)
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedRing α
a b x : α
hx : x < 0
⊢ |x| * ↑(↑sign x) = x
[PROOFSTEP]
rw [sign_neg hx, abs_of_neg hx, coe_neg_one, mul_neg_one, neg_neg]
[GOAL]
case inr.inl
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ |0| * ↑(↑sign 0) = 0
[PROOFSTEP]
rw [abs_zero, zero_mul]
[GOAL]
case inr.inr
α : Type u_1
inst✝ : LinearOrderedRing α
a b x : α
hx : 0 < x
⊢ |x| * ↑(↑sign x) = x
[PROOFSTEP]
rw [sign_pos hx, abs_of_pos hx, coe_one, mul_one]
[GOAL]
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : α
⊢ ↑sign (-a) = -↑sign a
[PROOFSTEP]
simp_rw [sign_apply, Left.neg_pos_iff, Left.neg_neg_iff]
[GOAL]
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : α
⊢ (if a < 0 then 1 else if 0 < a then -1 else 0) = -if 0 < a then 1 else if a < 0 then -1 else 0
[PROOFSTEP]
split_ifs with h h'
[GOAL]
case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : α
h : a < 0
h' : 0 < a
⊢ False
[PROOFSTEP]
exact False.elim (lt_asymm h h')
[GOAL]
case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : α
h : a < 0
h' : ¬0 < a
⊢ 1 = - -1
[PROOFSTEP]
simp
[GOAL]
case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : α
⊢ ↑sign (-a) = -↑sign a
[PROOFSTEP]
simp_rw [sign_apply, Right.neg_pos_iff, Right.neg_neg_iff]
[GOAL]
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : α
⊢ (if a < 0 then 1 else if 0 < a then -1 else 0) = -if 0 < a then 1 else if a < 0 then -1 else 0
[PROOFSTEP]
split_ifs with h h'
[GOAL]
case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : α
h : a < 0
h' : 0 < a
⊢ False
[PROOFSTEP]
exact False.elim (lt_asymm h h')
[GOAL]
case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : α
h : a < 0
h' : ¬0 < a
⊢ 1 = - -1
[PROOFSTEP]
simp
[GOAL]
case pos
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : α
h : ¬a < 0
h✝ : 0 < a
⊢ -1 = -1
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
a : α
h : ¬a < 0
h✝ : ¬0 < a
⊢ 0 = -0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
t : SignType
h : ∀ (i : ι), i ∈ s → ↑sign (f i) = t
⊢ ↑sign (∑ i in s, f i) = t
[PROOFSTEP]
cases t
[GOAL]
case zero
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → ↑sign (f i) = zero
⊢ ↑sign (∑ i in s, f i) = zero
[PROOFSTEP]
simp_rw [zero_eq_zero, sign_eq_zero_iff] at h ⊢
[GOAL]
case zero
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → f i = 0
⊢ ∑ i in s, f i = 0
[PROOFSTEP]
exact Finset.sum_eq_zero h
[GOAL]
case neg
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → ↑sign (f i) = neg
⊢ ↑sign (∑ i in s, f i) = neg
[PROOFSTEP]
simp_rw [neg_eq_neg_one, sign_eq_neg_one_iff] at h ⊢
[GOAL]
case neg
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → f i < 0
⊢ ∑ i in s, f i < 0
[PROOFSTEP]
exact Finset.sum_neg h hs
[GOAL]
case pos
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → ↑sign (f i) = pos
⊢ ↑sign (∑ i in s, f i) = pos
[PROOFSTEP]
simp_rw [pos_eq_one, sign_eq_one_iff] at h ⊢
[GOAL]
case pos
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
ι : Type u_2
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
h : ∀ (i : ι), i ∈ s → 0 < f i
⊢ 0 < ∑ i in s, f i
[PROOFSTEP]
exact Finset.sum_pos h hs
[GOAL]
α : Type u_1
n : ℤ
⊢ sign n = ↑(↑SignType.sign n)
[PROOFSTEP]
obtain (n | _) | _ := n
[GOAL]
case ofNat.zero
α : Type u_1
⊢ sign (ofNat Nat.zero) = ↑(↑SignType.sign (ofNat Nat.zero))
[PROOFSTEP]
simp [sign, Int.sign_neg, negSucc_lt_zero]
[GOAL]
case ofNat.succ
α : Type u_1
n✝ : ℕ
⊢ sign (ofNat (Nat.succ n✝)) = ↑(↑SignType.sign (ofNat (Nat.succ n✝)))
[PROOFSTEP]
simp [sign, Int.sign_neg, negSucc_lt_zero]
[GOAL]
case negSucc
α : Type u_1
a✝ : ℕ
⊢ sign -[a✝+1] = ↑(↑SignType.sign -[a✝+1])
[PROOFSTEP]
simp [sign, Int.sign_neg, negSucc_lt_zero]
[GOAL]
α✝ α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ ∃ β t sgn g,
    (∀ (b : β), g b ∈ s) ∧
      card t = ∑ a in s, Int.natAbs (f a) ∧ ∀ (a : α), a ∈ s → (∑ b in t, if g b = a then ↑(sgn b) else 0) = f a
[PROOFSTEP]
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, _, _⟩
[GOAL]
case refine'_1
α✝ α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ card (Finset.sigma univ fun a => range (Int.natAbs (f ↑a))) = ∑ a in s, Int.natAbs (f a)
[PROOFSTEP]
simp [sum_attach (f := fun a => (f a).natAbs)]
[GOAL]
case refine'_2
α✝ α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
⊢ ∀ (a : α),
    a ∈ s →
      (∑ b in Finset.sigma univ fun a => range (Int.natAbs (f ↑a)),
          if (fun a => ↑a.fst) b = a then ↑((fun a => ↑sign (f ↑a.fst)) b) else 0) =
        f a
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_2
α✝ α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
x : α
hx : x ∈ s
⊢ (∑ b in Finset.sigma univ fun a => range (Int.natAbs (f ↑a)),
      if (fun a => ↑a.fst) b = x then ↑((fun a => ↑sign (f ↑a.fst)) b) else 0) =
    f x
[PROOFSTEP]
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)]
[GOAL]
α✝ α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
β : Type u_1
t : Finset β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
ht : card t = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), a ∈ s → (∑ b in t, if g b = a then ↑(sgn b) else 0) = f a
⊢ Fintype.card { x // x ∈ t } = ∑ a in s, Int.natAbs (f a)
[PROOFSTEP]
simp [ht]
[GOAL]
α✝ α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
⊢ ∃ β x sgn g,
    (∀ (b : β), ¬g b ∈ s → sgn b = 0) ∧
      Fintype.card β = n ∧ ∀ (a : α), a ∈ s → (∑ i : β, if g i = a then ↑(sgn i) else 0) = f a
[PROOFSTEP]
obtain ⟨β, _, sgn, g, hg, hβ, hf⟩ := exists_signed_sum s f
[GOAL]
case intro.intro.intro.intro.intro.intro
α✝ α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), a ∈ s → (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
⊢ ∃ β x sgn g,
    (∀ (b : β), ¬g b ∈ s → sgn b = 0) ∧
      Fintype.card β = n ∧ ∀ (a : α), a ∈ s → (∑ i : β, if g i = a then ↑(sgn i) else 0) = f a
[PROOFSTEP]
refine'
  ⟨Sum β (Fin (n - ∑ i in 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]⟩
[GOAL]
α✝ α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), a ∈ s → (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
⊢ Fintype.card (β ⊕ Fin (n - ∑ i in s, Int.natAbs (f i))) = n
[PROOFSTEP]
simp [hβ, h]
[GOAL]
α✝ α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), a ∈ s → (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
a : α
ha : a ∈ s
⊢ (∑ i : β ⊕ Fin (n - ∑ i in s, Int.natAbs (f i)),
      if Sum.elim g (Classical.arbitrary (Fin (n - ∑ i in s, Int.natAbs (f i)) → α)) i = a then ↑(Sum.elim sgn 0 i)
      else 0) =
    f a
[PROOFSTEP]
simp [hf _ ha]
[GOAL]
case intro.intro.intro.intro.intro.intro
α✝ α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), a ∈ s → (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
⊢ ∀ (b : β ⊕ Fin (n - ∑ i in s, Int.natAbs (f i))),
    ¬Sum.elim g (Classical.arbitrary (Fin (n - ∑ i in s, Int.natAbs (f i)) → α)) b ∈ s → Sum.elim sgn 0 b = 0
[PROOFSTEP]
rintro (b | b) hb
[GOAL]
case intro.intro.intro.intro.intro.intro.inl
α✝ α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), a ∈ s → (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
b : β
hb : ¬Sum.elim g (Classical.arbitrary (Fin (n - ∑ i in s, Int.natAbs (f i)) → α)) (Sum.inl b) ∈ s
⊢ Sum.elim sgn 0 (Sum.inl b) = 0
[PROOFSTEP]
cases hb (hg _)
[GOAL]
case intro.intro.intro.intro.intro.intro.inr
α✝ α : Type u_1
inst✝¹ : Nonempty α
inst✝ : DecidableEq α
s : Finset α
f : α → ℤ
n : ℕ
h : ∑ i in s, Int.natAbs (f i) ≤ n
β : Type u_1
w✝ : Fintype β
sgn : β → SignType
g : β → α
hg : ∀ (b : β), g b ∈ s
hβ : Fintype.card β = ∑ a in s, Int.natAbs (f a)
hf : ∀ (a : α), a ∈ s → (∑ b : β, if g b = a then ↑(sgn b) else 0) = f a
b : Fin (n - ∑ i in s, Int.natAbs (f i))
hb : ¬Sum.elim g (Classical.arbitrary (Fin (n - ∑ i in s, Int.natAbs (f i)) → α)) (Sum.inr b) ∈ s
⊢ Sum.elim sgn 0 (Sum.inr b) = 0
[PROOFSTEP]
rfl
