Theorem: Lean4Axiomatic.Rational.sgn_recip (Lean4Axiomatic/Rational/Sign.lean)

State before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
⊢ sgn (p⁻¹) ≃ sgn p
Tactic:
have : 1 ≃ sgn p * sgn p := Rel.symm sqrt1_sgn_nonzero.elim
State after:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
this : 1 ≃ sgn p * sgn p
⊢ sgn (p⁻¹) ≃ sgn p

State before:
ℕ ℤ ℚ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Core ℚ
inst✝⁷ : Addition ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Negation ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
this : 1 ≃ sgn p * sgn p
⊢ sgn (p⁻¹) ≃ sgn p
Tactic:
calc
  sgn (p⁻¹)                   ≃ _ := Rel.symm AA.identR
  sgn (p⁻¹) * 1               ≃ _ := AA.substR ‹1 ≃ sgn p * sgn p›
  sgn (p⁻¹) * (sgn p * sgn p) ≃ _ := AA.substR (Rel.symm sgn_compat_mul)
  sgn (p⁻¹) * sgn (p * p)     ≃ _ := Rel.symm sgn_compat_mul
  sgn (p⁻¹ * (p * p))         ≃ _ := sgn_subst (eqv_symm mul_assoc)
  sgn ((p⁻¹ * p) * p)         ≃ _ := sgn_subst (mul_substL mul_inverseL)
  sgn (1 * p)                 ≃ _ := sgn_subst mul_identL
  sgn p                       ≃ _ := Rel.refl
State after:
no goals