Theorem: Lean4Axiomatic.Rational.recip_compat_mul (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 q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
⊢ (p * q)⁻¹ ≃ p⁻¹ * q⁻¹
Tactic:
have inv_p : 1 ≃ p * p⁻¹ := eqv_symm mul_inverseR
State after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
inv_p : 1 ≃ p * p⁻¹
⊢ (p * q)⁻¹ ≃ p⁻¹ * q⁻¹

State before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
inv_p : 1 ≃ p * p⁻¹
⊢ (p * q)⁻¹ ≃ p⁻¹ * q⁻¹
Tactic:
have inv_q : 1 ≃ q * q⁻¹ := eqv_symm mul_inverseR
State after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
inv_p : 1 ≃ p * p⁻¹
inv_q : 1 ≃ q * q⁻¹
⊢ (p * q)⁻¹ ≃ p⁻¹ * q⁻¹

State before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
inv_p : 1 ≃ p * p⁻¹
inv_q : 1 ≃ q * q⁻¹
⊢ (p * q)⁻¹ ≃ p⁻¹ * q⁻¹
Tactic:
have swap_middle : (p * p⁻¹) * (q * q⁻¹) ≃ (p * q) * (p⁻¹ * q⁻¹) :=
  AA.expr_xxfxxff_lr_swap_rl
State after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
inv_p : 1 ≃ p * p⁻¹
inv_q : 1 ≃ q * q⁻¹
swap_middle : p * p⁻¹ * (q * q⁻¹) ≃ p * q * (p⁻¹ * q⁻¹)
⊢ (p * q)⁻¹ ≃ p⁻¹ * q⁻¹

State before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
inv_p : 1 ≃ p * p⁻¹
inv_q : 1 ≃ q * q⁻¹
swap_middle : p * p⁻¹ * (q * q⁻¹) ≃ p * q * (p⁻¹ * q⁻¹)
⊢ (p * q)⁻¹ ≃ p⁻¹ * q⁻¹
Tactic:
calc
  (p * q)⁻¹                           ≃ _ := eqv_symm mul_identR
  (p * q)⁻¹ * 1                       ≃ _ := mul_substR (eqv_symm mul_identR)
  (p * q)⁻¹ * (1 * 1)                 ≃ _ := mul_substR (mul_substL inv_p)
  (p * q)⁻¹ * ((p * p⁻¹) * 1)         ≃ _ := mul_substR (mul_substR inv_q)
  (p * q)⁻¹ * ((p * p⁻¹) * (q * q⁻¹)) ≃ _ := mul_substR swap_middle
  (p * q)⁻¹ * ((p * q) * (p⁻¹ * q⁻¹)) ≃ _ := eqv_symm mul_assoc
  ((p * q)⁻¹ * (p * q)) * (p⁻¹ * q⁻¹) ≃ _ := mul_substL mul_inverseL
  1 * (p⁻¹ * q⁻¹)                     ≃ _ := mul_identL
  p⁻¹ * q⁻¹                           ≃ _ := eqv_refl
State after:
no goals