awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
pos : ∀ (h₁ : 0 < a) (h₂ : 0 < b), LE.le (α := SignType) 1 1
pos₁ : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : b < 0), LE.le (α := SignType) 1 (-1)
neg : ∀ (h₁ : 0 < a) (h₂ : ¬0 < b) (h₃ : ¬b < 0), LE.le (α := SignType) 1 0
pos₂ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : 0 < b), LE.le (α := SignType) (-1) 1
pos₃ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : ¬0 < b) (_ : b < 0), LE.le (α := SignType) (-1) (-1)
neg₁ : ∀ (h₁ : ¬0 < a) (h₄ : a < 0) (_ : ¬0 < b) (_ : ¬b < 0), LE.le (α := SignType) (-1) 0
pos₄ : ∀ (h₁ : ¬0 < a) (h₄ : ¬a < 0) (h₂ : 0 < b), LE.le (α := SignType) 0 1
pos₅ : ∀ (h₁ : ¬0 < a) (h₄ : ¬a < 0) (h₂ : ¬0 < b) (h₃ : b < 0), LE.le (α := SignType) 0 (-1)
neg₂ : ∀ (h₁ : ¬0 < a) (h₄ : ¬a < 0) (h₂ : ¬0 < b) (h₃ : ¬b < 0), LE.le (α := SignType) 0 0
⊢ LE.le (α := SignType) (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)

Tactic:
split_ifs with h₁ h₂ h₃ h₄ _ _ h₂ h₃
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : 0 < b
⊢ LE.le (α := SignType) 1 1

Tactic:
constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : 0 < b
⊢ LE.le (α := SignType) 1 1

Tactic:
try constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_ : 0 < b
⊢ LE.le (α := SignType) (-1) 1

Tactic:
constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_ : 0 < b
⊢ LE.le (α := SignType) (-1) 1

Tactic:
try constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
__1 : ¬0 < b
_ : b < 0
⊢ LE.le (α := SignType) (-1) (-1)

Tactic:
constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
__1 : ¬0 < b
_ : b < 0
⊢ LE.le (α := SignType) (-1) (-1)

Tactic:
try constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
__1 : ¬0 < b
_ : ¬b < 0
⊢ LE.le (α := SignType) (-1) 0

Tactic:
constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
__1 : ¬0 < b
_ : ¬b < 0
⊢ LE.le (α := SignType) (-1) 0

Tactic:
try constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : 0 < b
⊢ LE.le (α := SignType) 0 1

Tactic:
constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : 0 < b
⊢ LE.le (α := SignType) 0 1

Tactic:
try constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ LE.le (α := SignType) 0 0

Tactic:
constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ LE.le (α := SignType) 0 0

Tactic:
try constructor
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : b < 0
⊢ LE.le (α := SignType) 1 (-1)

Tactic:
cases lt_irrefl 0 (h₁.trans <| h.trans_lt h₃)

Premises used: lt_irrefl, LT.lt.trans, OfNat.ofNat, LE.le.trans_lt
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ LE.le (α := SignType) 1 0

Tactic:
cases h₂ (h₁.trans_le h)

Premises used: LT.lt.trans_le
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a_1 a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : b < 0
⊢ LE.le (α := SignType) 0 (-1)

Tactic:
cases h₄ (h.trans_lt h₃)

Premises used: LE.le.trans_lt
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType)
    (if 0 < a then 1 else if a < 0 then -1 else 0 : SignType)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) 0 : SignType) (0 : SignType)

Tactic:
simp [sign_apply]

Premises used: sign_apply
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
ha : 0 < a
rwa : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) 1
rwa₁ : Eq (α := SignType) 1 1
hc : 0 < a
rwa₂ : Eq (α := SignType) 1 1
hc₁ hc₂ hc₃ : 0 < a
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)

Tactic:
rwa [sign_apply, if_pos]

Premises used: if_pos, sign_apply
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
ha : a < 0
rwa : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (-1)
rwa₁ : Eq (α := SignType) (if a < 0 then -1 else 0) (-1)
rwa₂ : Eq (α := SignType) (-1) (-1)
hc : a < 0
rwa₃ : Eq (α := SignType) (-1) (-1)
hc₁ hc₂ hc₃ : a < 0
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)

Tactic:
rwa [sign_apply, if_neg <| asymm ha, if_pos]

Premises used: asymm, if_pos, sign_apply, if_neg
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType) ↔ 0 < a

Tactic:
⟨fun h => ?_, fun h => sign_pos h⟩

Premises used: sign_pos, Iff.intro
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
refine : ∀ (h : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)), 0 < a
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType) ↔ 0 < a

Tactic:
refine ⟨fun h => ?_, fun h => sign_pos h⟩
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
h : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)
by_contra : ∀ (hn : ¬0 < a), False
⊢ 0 < a

Tactic:
by_contra hn
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
h : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)
hn : ¬0 < a
⊢ Eq (α := SignType) (if a < 0 then -1 else 0) 1

Tactic:
rw [sign_apply, if_neg hn] at h

Premises used: sign_apply, if_neg
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
h : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)
hn : ¬0 < a
h₁ : Eq (α := SignType) (if a < 0 then -1 else 0) 1
⊢ ¬0 < a

Tactic:
rw [sign_apply, if_neg hn] at h

Premises used: sign_apply, if_neg
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
h : Eq (α := SignType) (if a < 0 then -1 else 0) 1
hn : ¬0 < a
⊢ False

Tactic:
split_ifs at h
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType) ↔ a < 0

Tactic:
⟨fun h => ?_, fun h => sign_neg h⟩

Premises used: sign_neg, Iff.intro
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
refine : ∀ (h : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)), a < 0
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType) ↔ a < 0

Tactic:
refine ⟨fun h => ?_, fun h => sign_neg h⟩
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
h : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)
⊢ Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (-1)

Tactic:
rw [sign_apply] at h

Premises used: sign_apply
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
h : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (-1)
⊢ ¬0 < a

Tactic:
split_ifs at h
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
h : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (-1)
h₁ : ¬0 < a
⊢ a < 0

Tactic:
split_ifs at h
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
h : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) (-1)
h₁ : ¬0 < a
h₂ : a < 0
⊢ Eq (α := SignType) (-1) (-1)

Tactic:
split_ifs at h
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : Preorder α
inst_2 : DecidableLT α
a : α
h_1 : ¬0 < a
h_2 : a < 0
h : Eq (α := SignType) (-1) (-1)
⊢ a < 0

Tactic:
assumption
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
β : Type u_2
F : Type u_3
inst_2 : Zero β
inst_3 : Preorder β
inst_4 : DecidableLT β
inst_5 : FunLike F α β
inst_6 : ZeroHomClass F α β
f : F
hf : StrictMono.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
a : α
⊢ Eq (α := SignType) ((sign : (a : β) → SignType) ((f : (a : α) → β) a : β) : SignType)
    ((sign : (a : α) → SignType) a : SignType)

Tactic:
simp only [sign_apply, ← map_zero f, hf.lt_iff_lt]

Premises used: StrictMono.lt_iff_lt, map_zero, sign_apply
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a = 0

Tactic:
⟨fun h => ?_, fun h => h.symm ▸ sign_zero⟩

Premises used: sign_zero, Eq.rec, Iff.intro, Eq.symm
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
refine : ∀ (h : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType)), a = 0
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a = 0

Tactic:
refine ⟨fun h => ?_, fun h => h.symm ▸ sign_zero⟩
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
h : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType)
⊢ Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) 0

Tactic:
rw [sign_apply] at h

Premises used: sign_apply
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
h : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) 0
⊢ ¬0 < a

Tactic:
split_ifs at h with h_1 h_2
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
h : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) 0
h_1 : ¬0 < a
⊢ ¬a < 0

Tactic:
split_ifs at h with h_1 h_2
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
h : Eq (α := SignType) (if 0 < a then 1 else if a < 0 then -1 else 0) 0
h_1 : ¬0 < a
h_2 : ¬a < 0
⊢ Eq (α := SignType) 0 0

Tactic:
split_ifs at h with h_1 h_2
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
h_1 : ¬0 < a
h_2 : ¬a < 0
⊢ a = 0

Tactic:
(le_of_not_gt h_1).eq_of_not_lt h_2

Premises used: le_of_not_gt, LE.le.eq_of_not_lt
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
h_1 : ¬0 < a
h_2 : ¬a < 0
⊢ a = 0

Tactic:
exact (le_of_not_gt h_1).eq_of_not_lt h_2

Premises used: le_of_not_gt, LE.le.eq_of_not_lt
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
⊢ Ne (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≠ 0

Tactic:
sign_eq_zero_iff.not

Premises used: Iff.not, sign_eq_zero_iff
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
inl : ∀ (h : 0 < a), LE.le (α := SignType) (0 : SignType) ((sign : (a : α) → SignType) a : SignType) ↔ 0 ≤ a
inr : ∀ (h : 0 = a), LE.le (α := SignType) (0 : SignType) ((sign : (a : α) → SignType) a : SignType) ↔ 0 ≤ a
inr₁ : ∀ (h : a < 0), LE.le (α := SignType) (0 : SignType) ((sign : (a : α) → SignType) a : SignType) ↔ 0 ≤ a
⊢ LE.le (α := SignType) (0 : SignType) ((sign : (a : α) → SignType) a : SignType) ↔ 0 ≤ a

Tactic:
rcases lt_trichotomy 0 a with (h | h | h)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
h : 0 < a
⊢ LE.le (α := SignType) (0 : SignType) ((sign : (a : α) → SignType) a : SignType) ↔ 0 ≤ a

Tactic:
simp [h, h.le]

Premises used: LT.lt.le
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
h : 0 = a
⊢ LE.le (α := SignType) (0 : SignType) ((sign : (a : α) → SignType) a : SignType) ↔ 0 ≤ a

Tactic:
simp [← h]
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
h : a < 0
⊢ LE.le (α := SignType) (0 : SignType) ((sign : (a : α) → SignType) a : SignType) ↔ 0 ≤ a

Tactic:
simp [h, h.not_ge]

Premises used: LT.lt.not_ge
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
inl : ∀ (h : 0 < a), LE.le (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≤ 0
inr : ∀ (h : 0 = a), LE.le (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≤ 0
inr₁ : ∀ (h : a < 0), LE.le (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≤ 0
⊢ LE.le (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≤ 0

Tactic:
rcases lt_trichotomy 0 a with (h | h | h)

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
h : 0 < a
⊢ LE.le (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≤ 0

Tactic:
simp [h, h.not_ge]

Premises used: LT.lt.not_ge
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
h : 0 = a
⊢ LE.le (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≤ 0

Tactic:
simp [← h]
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a : α
h : a < 0
⊢ LE.le (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType) ↔ a ≤ 0

Tactic:
simp [h, h.le]

Premises used: LT.lt.le
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
inl :
  ∀ (hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
inr :
  ∀ (hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
inr₁ :
  ∀ (hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)

Tactic:
rcases trichotomy (sign a) with hsa | hsa | hsa

Premises used: SignType.trichotomy, DFunLike.coe, SignType.sign
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)
inl :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (-1 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
inl₁ :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (0 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
inl₂ :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (1 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)

Tactic:
rcases trichotomy (sign b) with hsb | hsb | hsb

Premises used: SignType.trichotomy, DFunLike.coe, SignType.sign
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType)
inr :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (-1 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
inr₁ :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (0 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
inr₂ :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (1 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)

Tactic:
rcases trichotomy (sign b) with hsb | hsb | hsb

Premises used: SignType.trichotomy, DFunLike.coe, SignType.sign
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (1 : SignType)
inr :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (-1 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
inr₁ :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (0 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
inr₂ :
  ∀ (hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (1 : SignType)),
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
      Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)

Tactic:
rcases trichotomy (sign b) with hsb | hsb | hsb

Premises used: SignType.trichotomy, DFunLike.coe, SignType.sign
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)
hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (-1 : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)

Tactic:
simp_all
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)
hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (0 : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)

Tactic:
simp_all
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-1 : SignType)
hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (1 : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)

Tactic:
simp_all
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType)
hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (-1 : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)

Tactic:
simp_all
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType)
hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (0 : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)

Tactic:
simp_all
-- Module: Mathlib.Data.Sign.Defs
Goal:
α : Type u_1
inst : Zero α
inst_1 : LinearOrder α
a b : α
ha : a ≠ 0
hb : b ≠ 0
hsa : Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (0 : SignType)
hsb : Eq (α := SignType) ((sign : (a : α) → SignType) b : SignType) (1 : SignType)
⊢ Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) ((sign : (a : α) → SignType) b : SignType) ∨
    Eq (α := SignType) ((sign : (a : α) → SignType) a : SignType) (-(sign : (a : α) → SignType) b : SignType)

Tactic:
simp_all