Theorem: Lean4Axiomatic.Rational.div_substR (Lean4Axiomatic/Rational/Reciprocation.lean)

State before:
ℕ ℤ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
p₁ p₂ q : ℚ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
⊢ p₁ ≃ p₂ → q / p₁ ≃ q / p₂
Tactic:
intro (_ : p₁ ≃ p₂)
State after:
ℕ ℤ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
p₁ p₂ q : ℚ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
x✝ : p₁ ≃ p₂
⊢ q / p₁ ≃ q / p₂

State before:
ℕ ℤ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
p₁ p₂ q : ℚ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
x✝ : p₁ ≃ p₂
⊢ q / p₁ ≃ q / p₂
Tactic:
calc
  q / p₁   ≃ _ := div_mul_recip
  q * p₁⁻¹ ≃ _ := mul_substR (recip_subst ‹p₁ ≃ p₂›)
  q * p₂⁻¹ ≃ _ := eqv_symm div_mul_recip
  q / p₂   ≃ _ := eqv_refl
State after:
no goals