Theorem: Lean4Axiomatic.Rational.abs_subst (Lean4Axiomatic/Rational/Metric.lean)

State before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p₁ p₂ : ℚ
⊢ p₁ ≃ p₂ → abs p₁ ≃ abs p₂
Tactic:
intro (_ : p₁ ≃ p₂)
State after:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p₁ p₂ : ℚ
x✝ : p₁ ≃ p₂
⊢ abs p₁ ≃ abs p₂

State before:
ℕ ℤ ℚ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Negation ℚ
inst✝⁷ : Subtraction ℚ
inst✝⁶ : Multiplication ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : MinMax ℚ
inst✝ : Metric ℚ
p₁ p₂ : ℚ
x✝ : p₁ ≃ p₂
⊢ abs p₁ ≃ abs p₂
Tactic:
calc
  abs p₁      ≃ _ := abs_sgn
  p₁ * sgn p₁ ≃ _ := mul_substL ‹p₁ ≃ p₂›
  p₂ * sgn p₁ ≃ _ := mul_substR (from_integer_subst (sgn_subst ‹p₁ ≃ p₂›))
  p₂ * sgn p₂ ≃ _ := eqv_symm abs_sgn
  abs p₂      ≃ _ := eqv_refl
State after:
no goals