[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : RightDistribClass R
a b c d : R
⊢ (a + b + c) * d = a * d + b * d + c * d
[PROOFSTEP]
simp [right_distrib]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ (a + 1) * b = a * b + b
[PROOFSTEP]
rw [add_mul, one_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : LeftDistribClass α
a b : α
⊢ a * (b + 1) = a * b + a
[PROOFSTEP]
rw [mul_add, mul_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ (1 + a) * b = b + a * b
[PROOFSTEP]
rw [add_mul, one_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : LeftDistribClass α
a b : α
⊢ a * (1 + b) = a + a * b
[PROOFSTEP]
rw [mul_add, mul_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonAssocSemiring α
n : α
⊢ 1 * n + 1 * n = n + n
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonAssocSemiring α
n : α
⊢ n * 1 + n * 1 = n + n
[PROOFSTEP]
rw [mul_one]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : Mul α
P : Prop
inst✝ : Decidable P
a b c : α
⊢ (a * if P then b else c) = if P then a * b else a * c
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : Mul α
P : Prop
inst✝ : Decidable P
a b c : α
h✝ : P
⊢ a * b = a * b
[PROOFSTEP]
rfl
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : Mul α
P : Prop
inst✝ : Decidable P
a b c : α
h✝ : ¬P
⊢ a * c = a * c
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : Mul α
P : Prop
inst✝ : Decidable P
a b c : α
⊢ (if P then a else b) * c = if P then a * c else b * c
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : Mul α
P : Prop
inst✝ : Decidable P
a b c : α
h✝ : P
⊢ a * c = a * c
[PROOFSTEP]
rfl
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : Mul α
P : Prop
inst✝ : Decidable P
a b c : α
h✝ : ¬P
⊢ b * c = b * c
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroOneClass α
P : Prop
inst✝ : Decidable P
a : α
⊢ (a * if P then 1 else 0) = if P then a else 0
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroOneClass α
P : Prop
inst✝ : Decidable P
a : α
⊢ (if P then 1 else 0) * a = if P then a else 0
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
⊢ (if P then a * b else 0) = (if P then a else 0) * b
[PROOFSTEP]
by_cases h : P
[GOAL]
case pos
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
h : P
⊢ (if P then a * b else 0) = (if P then a else 0) * b
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
h : ¬P
⊢ (if P then a * b else 0) = (if P then a else 0) * b
[PROOFSTEP]
simp [h]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
⊢ (if P then a * b else 0) = a * if P then b else 0
[PROOFSTEP]
by_cases h : P
[GOAL]
case pos
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
h : P
⊢ (if P then a * b else 0) = a * if P then b else 0
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
h : ¬P
⊢ (if P then a * b else 0) = a * if P then b else 0
[PROOFSTEP]
simp [h]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
R : Type x
α : Type u_1
inst✝² : MulZeroClass α
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b : α
⊢ (if P ∧ Q then a * b else 0) = (if P then a else 0) * if Q then b else 0
[PROOFSTEP]
simp only [← ite_and, ite_mul, mul_ite, mul_zero, zero_mul, and_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : CommSemiring α
a✝ b✝ c a b : α
⊢ (a + b) * (a + b) = a * a + 2 * a * b + b * b
[PROOFSTEP]
simp only [two_mul, add_mul, mul_add, add_assoc, mul_comm b]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
a b : α
⊢ -a * -b = a * b
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
a b : α
⊢ -a * b = a * -b
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ -a = -1 * a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ a * -1 = -a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ -1 * a = -a
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : MulZeroClass α
inst✝ : HasDistribNeg α
src✝¹ : Zero α := inferInstanceAs (Zero α)
src✝ : InvolutiveNeg α := inferInstanceAs (InvolutiveNeg α)
⊢ -0 = 0
[PROOFSTEP]
rw [← zero_mul (0 : α), ← neg_mul, mul_zero, mul_zero]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ -a * b + a * b = 0
[PROOFSTEP]
rw [← right_distrib, add_left_neg, zero_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ a * -b + a * b = 0
[PROOFSTEP]
rw [← left_distrib, add_left_neg, mul_zero]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c : α
⊢ a * (b - c) = a * b - a * c
[PROOFSTEP]
simpa only [sub_eq_add_neg, neg_mul_eq_mul_neg] using mul_add a b (-c)
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c : α
⊢ (a - b) * c = a * c - b * c
[PROOFSTEP]
simpa only [sub_eq_add_neg, neg_mul_eq_neg_mul] using add_mul a (-b) c
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
⊢ a * e + c = b * e + d ↔ a * e + c = d + b * e
[PROOFSTEP]
simp [add_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c = d + b * e
⊢ a * e + c - b * e = d
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c = d + b * e
⊢ d + b * e - b * e = d
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c - b * e = d
⊢ a * e + c = d + b * e
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c - b * e = d
⊢ a * e + c = a * e + c - b * e + b * e
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
⊢ a * e + c - b * e = d ↔ (a - b) * e + c = d
[PROOFSTEP]
simp [sub_mul, sub_add_eq_add_sub]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c = b * e + d
⊢ (a - b) * e + c = a * e + c - b * e
[PROOFSTEP]
simp [sub_mul, sub_add_eq_add_sub]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c = b * e + d
⊢ a * e + c - b * e = d
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing α
a b c d e : α
h : a * e + c = b * e + d
⊢ b * e + d - b * e = d
[PROOFSTEP]
simp [@add_sub_cancel α]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonAssocRing α
a b : α
⊢ (a - 1) * b = a * b - b
[PROOFSTEP]
rw [sub_mul, one_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonAssocRing α
a b : α
⊢ a * (b - 1) = a * b - a
[PROOFSTEP]
rw [mul_sub, mul_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonAssocRing α
a b : α
⊢ (1 - a) * b = b - a * b
[PROOFSTEP]
rw [sub_mul, one_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonAssocRing α
a b : α
⊢ a * (1 - b) = a - a * b
[PROOFSTEP]
rw [mul_sub, mul_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b c d e : α
src✝ : Ring α := inst✝
a : α
⊢ 0 * a + 0 * a = 0 * a + 0
[PROOFSTEP]
rw [← add_mul, zero_add, add_zero]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b c d e : α
src✝ : Ring α := inst✝
a : α
⊢ a * 0 + a * 0 = a * 0 + 0
[PROOFSTEP]
rw [← mul_add, add_zero, add_zero]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b c d e : α
src✝ : Ring α := inst✝
a : α
⊢ 0 * a + 0 * a = 0 * a + 0
[PROOFSTEP]
rw [← add_mul, zero_add, add_zero]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Ring α
a✝ b c d e : α
src✝ : Ring α := inst✝
a : α
⊢ a * 0 + a * 0 = a * 0 + 0
[PROOFSTEP]
rw [← mul_add, add_zero, add_zero]
