Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_substR (Lean4Axiomatic/Rational/Impl/Fraction/Addition.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₁ ≃ _ := add_comm
  q₁ + p ≃ _ := add_substL ‹q₁ ≃ q₂›
  q₂ + p ≃ _ := add_comm
  p + q₂ ≃ _ := eqv_refl
State after:
no goals