Theorem: Lean4Axiomatic.Rational.Impl.Fraction.mul_substR (Lean4Axiomatic/Rational/Impl/Fraction/Multiplication.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q₁ q₂ : Fraction ℤ
⊢ q₁ ≃ q₂ → p * q₁ ≃ p * q₂
Tactic:
intro (_ : q₁ ≃ q₂)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q₁ q₂ : Fraction ℤ
x✝ : q₁ ≃ q₂
⊢ p * q₁ ≃ p * q₂

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q₁ q₂ : Fraction ℤ
x✝ : q₁ ≃ q₂
⊢ p * q₁ ≃ p * q₂
Tactic:
calc
  p * q₁ ≃ _ := mul_comm
  q₁ * p ≃ _ := mul_substL ‹q₁ ≃ q₂›
  q₂ * p ≃ _ := mul_comm
  p * q₂ ≃ _ := eqv_refl
State after:
no goals