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

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
⊢ sgn 2 ≃ 1
Tactic:
have : sgn (1:ℤ) ≃ 1 := sgn_positive.mp one_positive
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
this : sgn 1 ≃ 1
⊢ sgn 2 ≃ 1

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
this : sgn 1 ≃ 1
⊢ sgn 2 ≃ 1
Tactic:
calc
  _ ≃ sgn (2:ℤ)       := Rel.refl
  _ ≃ sgn (1 + 1 : ℤ) := sgn_subst (Rel.symm add_one_one)
  _ ≃ 1               := add_preserves_sign ‹sgn (1:ℤ) ≃ 1› ‹sgn (1:ℤ) ≃ 1›
State after:
no goals