[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b c x : R
e : ℕ
pq_pf : a + b = c
⊢ x ^ e * a + x ^ e * b = x ^ e * c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b x : R
e : ℕ
⊢ x ^ e * a + x ^ e * b = x ^ e * (a + b)
[PROOFSTEP]
simp [mul_add]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b x : R
e : ℕ
h : a + b = ↑0
⊢ x ^ e * a + x ^ e * b = ↑0
[PROOFSTEP]
simp [h, ← mul_add]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
b : R
⊢ 0 + b = b
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
⊢ a + 0 = a
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ b₁ c₁ a₂ b₂ c₂ : R
x✝¹ : a₁ + b₁ = c₁
x✝ : a₂ + b₂ = c₂
⊢ a₁ + a₂ + (b₁ + b₂) = c₁ + c₂
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ b₁ a₂ b₂ : R
⊢ a₁ + a₂ + (b₁ + b₂) = a₁ + b₁ + (a₂ + b₂)
[PROOFSTEP]
simp [add_assoc, add_left_comm]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ b₁ a₂ b₂ c : R
h : IsNat (a₁ + b₁) 0
h₄ : a₂ + b₂ = c
⊢ a₁ + a₂ + (b₁ + b₂) = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ b₁ a₂ b₂ : R
h : IsNat (a₁ + b₁) 0
⊢ a₁ + a₂ + (b₁ + b₂) = a₂ + b₂
[PROOFSTEP]
rw [add_add_add_comm, h.1, Nat.cast_zero, add_pf_zero_add]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₂ b c a₁ : R
x✝ : a₂ + b = c
⊢ a₁ + a₂ + b = a₁ + c
[PROOFSTEP]
simp [*, add_assoc]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b₂ c b₁ : R
x✝ : a + b₂ = c
⊢ a + (b₁ + b₂) = b₁ + c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b₂ b₁ : R
⊢ a + (b₁ + b₂) = b₁ + (a + b₂)
[PROOFSTEP]
simp [add_left_comm]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
⊢ Nat.rawCast 1 * a = a
[PROOFSTEP]
simp [Nat.rawCast]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
⊢ a * Nat.rawCast 1 = a
[PROOFSTEP]
simp [Nat.rawCast]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₃ b c a₁ : R
a₂ : ℕ
x✝ : a₃ * b = c
⊢ a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₃ b a₁ : R
a₂ : ℕ
⊢ a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b₃ c b₁ : R
b₂ : ℕ
x✝ : a * b₃ = c
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b₃ b₁ : R
b₂ : ℕ
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃)
[PROOFSTEP]
rw [mul_left_comm]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
ea eb e : ℕ
a₂ b₂ c x : R
x✝¹ : ea + eb = e
x✝ : a₂ * b₂ = c
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
ea eb : ℕ
a₂ b₂ x : R
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)
[PROOFSTEP]
simp [pow_add, mul_mul_mul_comm]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
⊢ a * 0 = 0
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b₁ c₁ b₂ c₂ d : R
x✝² : a * b₁ = c₁
x✝¹ : a * b₂ = c₂
x✝ : c₁ + 0 + c₂ = d
⊢ a * (b₁ + b₂) = d
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b₁ b₂ : R
⊢ a * (b₁ + b₂) = a * b₁ + 0 + a * b₂
[PROOFSTEP]
simp [_root_.mul_add]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
b : R
⊢ 0 * b = 0
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ b c₁ a₂ c₂ d : R
x✝² : a₁ * b = c₁
x✝¹ : a₂ * b = c₂
x✝ : c₁ + c₂ = d
⊢ (a₁ + a₂) * b = d
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ b a₂ : R
⊢ (a₁ + a₂) * b = a₁ * b + a₂ * b
[PROOFSTEP]
simp [_root_.add_mul]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
n : ℕ
⊢ ↑(Nat.rawCast n) = Nat.rawCast n
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ : ℕ
b₁ : R
a₃ : ℕ
b₃ : R
a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₃ = b₃
⊢ ↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ a₃ a₂ : ℕ
⊢ ↑(a₁ ^ a₂ * a₃) = ↑a₁ ^ a₂ * ↑a₃
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₂ = b₂
⊢ ↑(a₁ + a₂) = b₁ + b₂
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ a₂ : ℕ
⊢ ↑(a₁ + a₂) = ↑a₁ + ↑a₂
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type ?u.195007
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b c : ℕ
x✝ : a * b = c
⊢ a • b = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type ?u.195007
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a b : ℕ
⊢ a • b = a * b
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : ℕ
a' b c : R
x✝¹ : ↑a = a'
x✝ : a' * b = c
⊢ a • b = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : ℕ
b : R
⊢ a • b = ↑a * b
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R✝ : Type ?u.203137
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a b : R
x✝ : Int.rawCast (Int.negOfNat 1) * a = b
⊢ -a = b
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.203137
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a : R
⊢ -a = Int.rawCast (Int.negOfNat 1) * a
[PROOFSTEP]
simp [Int.negOfNat]
[GOAL]
u : Lean.Level
R✝ : Type ?u.204069
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a₁ : R
a₂ : ℕ
a₃ b : R
x✝ : -a₃ = b
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.204069
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * -a₃
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R✝ : Type ?u.213000
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
⊢ -0 = 0
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R✝ : Type ?u.213479
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a₁ a₂ b₁ b₂ : R
x✝¹ : -a₁ = b₁
x✝ : -a₂ = b₂
⊢ -(a₁ + a₂) = b₁ + b₂
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.213479
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a₁ a₂ : R
⊢ -(a₁ + a₂) = -a₁ + -a₂
[PROOFSTEP]
simp [add_comm]
[GOAL]
u : Lean.Level
R✝ : Type ?u.219543
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a b c d : R
x✝¹ : -b = c
x✝ : a + c = d
⊢ a - b = d
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.219543
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a b : R
⊢ a - b = a + -b
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
b : ℕ
⊢ a ^ b = (a + 0) ^ b * Nat.rawCast 1
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
b : ℕ
⊢ a ^ b = a ^ b * Nat.rawCast 1 + 0
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type ?u.229716
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a✝ : Q(ℕ)
va : ExProd sℕ a✝
a : Q(ℕ)
value✝ : ℚ
hyp✝ : Option Expr
lit : Q(ℕ)
this : «$a» =Q Nat.rawCast «$lit»
p : Nat.ble 1 «$lit» =Q true
⊢ Option Q(0 < «$a»)
[PROOFSTEP]
exact some (q(const_pos $lit $p))
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
⊢ a ^ 1 = a
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
k : ℕ
b c : R
x✝¹ : a ^ k = b
x✝ : b * b = c
⊢ a ^ Nat.mul 2 k = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
k : ℕ
⊢ a ^ Nat.mul 2 k = a ^ k * a ^ k
[PROOFSTEP]
simp [Nat.succ_mul, pow_add]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
k : ℕ
b c d : R
x✝² : a ^ k = b
x✝¹ : b * b = c
x✝ : c * a = d
⊢ a ^ Nat.add (Nat.mul 2 k) 1 = d
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
k : ℕ
⊢ a ^ Nat.add (Nat.mul 2 k) 1 = a ^ k * a ^ k * a
[PROOFSTEP]
simp [Nat.succ_mul, pow_add]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
b : ℕ
⊢ Nat.rawCast 1 ^ b = Nat.rawCast 1
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
ea₁ b c₁ : ℕ
a₂ c₂ xa₁ : R
x✝¹ : ea₁ * b = c₁
x✝ : a₂ ^ b = c₂
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
ea₁ b : ℕ
a₂ xa₁ : R
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * a₂ ^ b
[PROOFSTEP]
simp [_root_.mul_pow, pow_mul]
[GOAL]
u : Lean.Level
R : Type ?u.271767
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
k : ℕ
⊢ Nat.rawCast k = Nat.rawCast 1 * k
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type ?u.272246
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₃ c₂ k a₁ a₂ : ℕ
x✝ : a₃ = c₂ * k
⊢ a₁ ^ a₂ * a₃ = a₁ ^ a₂ * c₂ * k
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type ?u.272246
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
c₂ k a₁ a₂ : ℕ
⊢ a₁ ^ a₂ * (c₂ * k) = a₁ ^ a₂ * c₂ * k
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
⊢ a ^ Nat.rawCast 1 = a
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
b✝ b : ℕ
x✝ : 0 < b + 1
⊢ 0 ^ (b + 1) = 0
[PROOFSTEP]
simp [pow_succ]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
b : ℕ
c : R
x✝ : a ^ b = c
⊢ (a + 0) ^ b = c + 0
[PROOFSTEP]
simp [*]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
b c k : ℕ
a d e : R
x✝² : b = c * k
x✝¹ : a ^ c = d
x✝ : d ^ k = e
⊢ a ^ b = e
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
c k : ℕ
a : R
⊢ a ^ (c * k) = (a ^ c) ^ k
[PROOFSTEP]
simp [pow_mul]
[GOAL]
u : Lean.Level
R : Type ?u.283538
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a✝ : Q(«$α»)
b : Q(ℕ)
va✝ : ExSum sα a✝
vb : ExProd sℕ b
a : Q(«$α»)
va : ExSum sα a
this : «$b» =Q Nat.rawCast 1
⊢ Q(«$a» ^ «$b» = «$a»)
[PROOFSTEP]
exact q(pow_one_cast $a)
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
⊢ a ^ 0 = Nat.rawCast 1 + 0
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
b₁ : ℕ
c₁ : R
b₂ : ℕ
c₂ d : R
x✝² : a ^ b₁ = c₁
x✝¹ : a ^ b₂ = c₂
x✝ : c₁ * c₂ = d
⊢ a ^ (b₁ + b₂) = d
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
b₁ b₂ : ℕ
⊢ a ^ (b₁ + b₂) = a ^ b₁ * a ^ b₂
[PROOFSTEP]
simp [_root_.pow_add]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
n : ℕ
e : a = ↑n
⊢ a = Nat.rawCast n + 0
[PROOFSTEP]
simp [e]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
e : a = ↑0
⊢ a = 0
[PROOFSTEP]
simp [e]
[GOAL]
u : Lean.Level
R✝ : Type ?u.333286
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
n : ℕ
R : Type u_1
inst✝ : Ring R
a : R
e : a = ↑(Int.negOfNat n)
⊢ a = Int.rawCast (Int.negOfNat n) + 0
[PROOFSTEP]
simp [e]
[GOAL]
u : Lean.Level
R✝ : Type ?u.334205
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
n : ℤ
d : ℕ
R : Type u_1
inst✝ : DivisionRing R
a : R
inv✝ : Invertible ↑d
e : a = ↑n * ⅟↑d
⊢ a = Rat.rawCast n d + 0
[PROOFSTEP]
simp [e, div_eq_mul_inv]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a a' : R
p : a = a'
⊢ a = a' ^ Nat.rawCast 1 * Nat.rawCast 1
[PROOFSTEP]
simp [*]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
⊢ a = a ^ Nat.rawCast 1 * Nat.rawCast 1 + 0
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a a' : R
p : a = a'
⊢ a = a' ^ Nat.rawCast 1 * Nat.rawCast 1 + 0
[PROOFSTEP]
simp [*]
[GOAL]
u : Lean.Level
R✝ : Type ?u.354097
α : 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
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.354097
α : 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)
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R✝ : Type ?u.357008
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a b : R
x✝ : a⁻¹ = b
⊢ (a + 0)⁻¹ = b + 0
[PROOFSTEP]
simp [*]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ : ℕ
b₁ : R
a₂ : ℕ
b₂ : R
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₂ = b₂
⊢ ↑(a₁ + a₂) = b₁ + b₂
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₁ a₂ : ℕ
⊢ ↑(a₁ + a₂) = ↑a₁ + ↑a₂
[PROOFSTEP]
simp
[GOAL]
u : Lean.Level
R✝ : Type ?u.392566
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a b c d : R
x✝¹ : b⁻¹ = c
x✝ : a * c = d
⊢ a / b = d
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.392566
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a b : R
⊢ a / b = a * b⁻¹
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' + b' = c
⊢ a + b = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a' b' : R
⊢ a' + b' = a' + b'
[PROOFSTEP]
rfl
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' * b' = c
⊢ a * b = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a' b' : R
⊢ a' * b' = a' * b'
[PROOFSTEP]
rfl
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a a' : ℕ
b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' • b' = c
⊢ a • b = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a' : ℕ
b' : R
⊢ a' • b' = a' • b'
[PROOFSTEP]
rfl
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a a' : R
b b' : ℕ
c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' ^ b' = c
⊢ a ^ b = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a' : R
b' : ℕ
⊢ a' ^ b' = a' ^ b'
[PROOFSTEP]
rfl
[GOAL]
u : Lean.Level
R✝ : Type ?u.398592
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a a' b : R
x✝¹ : a = a'
x✝ : -a' = b
⊢ -a = b
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.398592
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a' : R
⊢ -a' = -a'
[PROOFSTEP]
rfl
[GOAL]
u : Lean.Level
R✝ : Type ?u.398710
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' - b' = c
⊢ a - b = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.398710
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a' b' : R
⊢ a' - b' = a' - b'
[PROOFSTEP]
rfl
[GOAL]
u : Lean.Level
R✝ : Type ?u.398916
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a a' b : R
x✝¹ : a = a'
x✝ : a'⁻¹ = b
⊢ a⁻¹ = b
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.398916
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a' : R
⊢ a'⁻¹ = a'⁻¹
[PROOFSTEP]
rfl
[GOAL]
u : Lean.Level
R✝ : Type ?u.399091
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' / b' = c
⊢ a / b = c
[PROOFSTEP]
subst_vars
[GOAL]
u : Lean.Level
R✝ : Type ?u.399091
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : DivisionRing R
a' b' : R
⊢ a' / b' = a' / b'
[PROOFSTEP]
rfl
[GOAL]
u : Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a c b : R
x✝¹ : a = c
x✝ : b = c
⊢ a = b
[PROOFSTEP]
subst_vars
[GOAL]
u : Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
b : R
⊢ b = b
[PROOFSTEP]
rfl
