Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_trichotomy (Lean4Axiomatic/Rational/Impl/Fraction/Sign.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Tactic:
have
  : AA.OneOfThree
    (p.numerator ≃ 0)
    (Positive p.numerator)
    (Negative p.numerator)
  := (Integer.sign_trichotomy p.numerator).atLeastOne
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Tactic:
match this with
| AA.OneOfThree.first (_ : p.numerator ≃ 0) =>
  have : sgn p ≃ 0 := calc
    sgn p           ≃ _ := Rel.refl
    sgn p.numerator ≃ _ := Integer.sgn_zero.mp ‹p.numerator ≃ 0›
    0               ≃ _ := Rel.refl
  exact AA.OneOfThree.first this
| AA.OneOfThree.second (_ : Positive p.numerator) =>
  have : sgn p ≃ 1 := calc
    sgn p           ≃ _ := Rel.refl
    sgn p.numerator ≃ _ := Integer.sgn_positive.mp ‹Positive p.numerator›
    1               ≃ _ := Rel.refl
  exact AA.OneOfThree.second this
| AA.OneOfThree.third (_ : Negative p.numerator) =>
  have : sgn p ≃ -1 := calc
    sgn p           ≃ _ := Rel.refl
    sgn p.numerator ≃ _ := Integer.sgn_negative.mp ‹Negative p.numerator›
    (-1)            ≃ _ := Rel.refl
  exact AA.OneOfThree.third this
State after:
no goals

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
a✝ : p.numerator ≃ 0
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Tactic:
have : sgn p ≃ 0 := calc
  sgn p           ≃ _ := Rel.refl
  sgn p.numerator ≃ _ := Integer.sgn_zero.mp ‹p.numerator ≃ 0›
  0               ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this✝ : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
a✝ : p.numerator ≃ 0
this : sgn p ≃ 0
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this✝ : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
a✝ : p.numerator ≃ 0
this : sgn p ≃ 0
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Tactic:
exact AA.OneOfThree.first this
State after:
no goals

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
b✝ : Positive p.numerator
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Tactic:
have : sgn p ≃ 1 := calc
  sgn p           ≃ _ := Rel.refl
  sgn p.numerator ≃ _ := Integer.sgn_positive.mp ‹Positive p.numerator›
  1               ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this✝ : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
b✝ : Positive p.numerator
this : sgn p ≃ 1
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this✝ : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
b✝ : Positive p.numerator
this : sgn p ≃ 1
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Tactic:
exact AA.OneOfThree.second this
State after:
no goals

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
c✝ : Negative p.numerator
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Tactic:
have : sgn p ≃ -1 := calc
  sgn p           ≃ _ := Rel.refl
  sgn p.numerator ≃ _ := Integer.sgn_negative.mp ‹Negative p.numerator›
  (-1)            ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this✝ : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
c✝ : Negative p.numerator
this : sgn p ≃ -1
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this✝ : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
c✝ : Negative p.numerator
this : sgn p ≃ -1
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Tactic:
exact AA.OneOfThree.third this
State after:
no goals