Theorem: Lean4Axiomatic.Rational.div_substL (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 (q ≄ 0)
⊢ p₁ ≃ p₂ → p₁ / q ≃ p₂ / q
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 (q ≄ 0)
x✝ : p₁ ≃ p₂
⊢ p₁ / q ≃ p₂ / q

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 (q ≄ 0)
x✝ : p₁ ≃ p₂
⊢ p₁ / q ≃ p₂ / q
Tactic:
calc
  p₁ / q   ≃ _ := div_mul_recip
  p₁ * q⁻¹ ≃ _ := mul_substL ‹p₁ ≃ p₂›
  p₂ * q⁻¹ ≃ _ := eqv_symm div_mul_recip
  p₂ / q   ≃ _ := eqv_refl
State after:
no goals