u : Lean.Level
R✝ : Type ?u.353952
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ (a₁ ^ a₂ * a₃)⁻¹ = a₃⁻¹ * (a₁⁻¹ ^ a₂ * Nat.rawCast 1)
u : Lean.Level
R✝ : Type ?u.353952
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a₁ : R
a₂ : ℕ
a₃ b₁ b₃ c : R
x✝² : a₁⁻¹ = b₁
x✝¹ : a₃⁻¹ = b₃
x✝ : b₃ * (b₁ ^ a₂ * Nat.rawCast 1) = c
⊢ (a₁ ^ a₂ * a₃)⁻¹ = c
subst_vars
no goals
u : Lean.Level
R✝ : Type ?u.353952
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ (a₁ ^ a₂ * a₃)⁻¹ = a₃⁻¹ * (a₁⁻¹ ^ a₂ * Nat.rawCast 1)
simp