[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a b : α
u : αˣ
⊢ -↑u * -↑u⁻¹ = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a b : α
u : αˣ
⊢ -↑u⁻¹ * -↑u = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a✝ b a : α
u : αˣ
⊢ -(a /ₚ u) = -a /ₚ u
[PROOFSTEP]
simp only [divp, neg_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b✝ a b : α
u : αˣ
⊢ a /ₚ u + b /ₚ u = (a + b) /ₚ u
[PROOFSTEP]
simp only [divp, add_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b✝ a b : α
u : αˣ
⊢ a /ₚ u - b /ₚ u = (a - b) /ₚ u
[PROOFSTEP]
rw [sub_eq_add_neg, sub_eq_add_neg, neg_divp, divp_add_divp_same]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b✝ a b : α
u : αˣ
⊢ a + b /ₚ u = (a * ↑u + b) /ₚ u
[PROOFSTEP]
simp only [divp, add_mul, Units.mul_inv_cancel_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b✝ a b : α
u : αˣ
⊢ a - b /ₚ u = (a * ↑u - b) /ₚ u
[PROOFSTEP]
simp only [divp, sub_mul, Units.mul_inv_cancel_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b✝ a b : α
u : αˣ
⊢ a /ₚ u + b = (a + b * ↑u) /ₚ u
[PROOFSTEP]
simp only [divp, add_mul, Units.mul_inv_cancel_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b✝ a b : α
u : αˣ
⊢ a /ₚ u - b = (a - b * ↑u) /ₚ u
[PROOFSTEP]
simp only [divp, sub_mul, sub_right_inj]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b✝ a b : α
u : αˣ
⊢ b = b * ↑u * ↑u⁻¹
[PROOFSTEP]
rw [mul_assoc, Units.mul_inv, mul_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a /ₚ u₁ + b /ₚ u₂ = (a * ↑u₂ + ↑u₁ * b) /ₚ (u₁ * u₂)
[PROOFSTEP]
simp only [divp, add_mul, mul_inv_rev, val_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + b * ↑u₂⁻¹ = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₁ * b * (↑u₂⁻¹ * ↑u₁⁻¹)
[PROOFSTEP]
rw [mul_comm (↑u₁ * b), mul_comm b]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)
[PROOFSTEP]
rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one, mul_one]
  -- porting note: `assoc_rw` not ported: `assoc_rw [mul_inv, mul_inv, mul_one, mul_one]`
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : CommRing α
a b : α
u₁ u₂ : αˣ
⊢ a /ₚ u₁ - b /ₚ u₂ = (a * ↑u₂ - ↑u₁ * b) /ₚ (u₁ * u₂)
[PROOFSTEP]
simp only [sub_eq_add_neg, neg_divp, divp_add_divp, mul_neg]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Semiring R
a : Rˣ
b : R
⊢ ↑a + b = ↑a * (1 + ↑a⁻¹ * b)
[PROOFSTEP]
rw [mul_add, mul_one, ← mul_assoc, Units.mul_inv, one_mul]
