Theorem: Lean4Axiomatic.Integer.sgn_idemp (Lean4Axiomatic/Integer/Sign.lean)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ sgn (sgn a) ≃ sgn a
Tactic:
have : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a) :=
  (sign_trichotomy a).atLeastOne
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ sgn (sgn a) ≃ sgn a

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
⊢ sgn (sgn a) ≃ sgn a
Tactic:
match this with
| AA.OneOfThree.first (_ : a ≃ 0) =>
  have : sgn a ≃ 0 := sgn_zero.mp ‹a ≃ 0›
  calc
    sgn (sgn a) ≃ _ := sgn_subst ‹sgn a ≃ 0›
    sgn (0 : ℤ) ≃ _ := sgn_subst (Rel.symm ‹a ≃ 0›)
    sgn a       ≃ _ := Rel.refl
| AA.OneOfThree.second (_ : Positive a) =>
  have : sgn a ≃ 1 := sgn_positive.mp ‹Positive a›
  calc
    sgn (sgn a) ≃ _ := sgn_subst ‹sgn a ≃ 1›
    sgn (1 : ℤ) ≃ _ := sgn_positive.mp one_positive
    1           ≃ _ := Rel.symm ‹sgn a ≃ 1›
    sgn a       ≃ _ := Rel.refl
| AA.OneOfThree.third (_ : Negative a) =>
  have : sgn a ≃ -1 := sgn_negative.mp ‹Negative a›
  calc
    sgn (sgn a)  ≃ _ := sgn_subst ‹sgn a ≃ -1›
    sgn (-1 : ℤ) ≃ _ := sgn_negative.mp neg_one_negative
    (-1)         ≃ _ := Rel.symm ‹sgn a ≃ -1›
    sgn a        ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
a✝ : a ≃ 0
⊢ sgn (sgn a) ≃ sgn a
Tactic:
have : sgn a ≃ 0 := sgn_zero.mp ‹a ≃ 0›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this✝ : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
a✝ : a ≃ 0
this : sgn a ≃ 0
⊢ sgn (sgn a) ≃ sgn a

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this✝ : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
a✝ : a ≃ 0
this : sgn a ≃ 0
⊢ sgn (sgn a) ≃ sgn a
Tactic:
calc
  sgn (sgn a) ≃ _ := sgn_subst ‹sgn a ≃ 0›
  sgn (0 : ℤ) ≃ _ := sgn_subst (Rel.symm ‹a ≃ 0›)
  sgn a       ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
b✝ : Positive a
⊢ sgn (sgn a) ≃ sgn a
Tactic:
have : sgn a ≃ 1 := sgn_positive.mp ‹Positive a›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this✝ : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
b✝ : Positive a
this : sgn a ≃ 1
⊢ sgn (sgn a) ≃ sgn a

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this✝ : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
b✝ : Positive a
this : sgn a ≃ 1
⊢ sgn (sgn a) ≃ sgn a
Tactic:
calc
  sgn (sgn a) ≃ _ := sgn_subst ‹sgn a ≃ 1›
  sgn (1 : ℤ) ≃ _ := sgn_positive.mp one_positive
  1           ≃ _ := Rel.symm ‹sgn a ≃ 1›
  sgn a       ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
c✝ : Negative a
⊢ sgn (sgn a) ≃ sgn a
Tactic:
have : sgn a ≃ -1 := sgn_negative.mp ‹Negative a›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this✝ : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
c✝ : Negative a
this : sgn a ≃ -1
⊢ sgn (sgn a) ≃ sgn a

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
this✝ : AA.OneOfThree (a ≃ 0) (Positive a) (Negative a)
c✝ : Negative a
this : sgn a ≃ -1
⊢ sgn (sgn a) ≃ sgn a
Tactic:
calc
  sgn (sgn a)  ≃ _ := sgn_subst ‹sgn a ≃ -1›
  sgn (-1 : ℤ) ≃ _ := sgn_negative.mp neg_one_negative
  (-1)         ≃ _ := Rel.symm ‹sgn a ≃ -1›
  sgn a        ≃ _ := Rel.refl
State after:
no goals