[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
S : Type ?u.27
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : Distrib S
f : R → S
hf : Injective f
add : ∀ (x y : R), f (x + y) = f x + f y
mul : ∀ (x y : R), f (x * y) = f x * f y
x y z : R
⊢ f (x * (y + z)) = f (x * y + x * z)
[PROOFSTEP]
simp only [*, left_distrib]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
S : Type ?u.27
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : Distrib S
f : R → S
hf : Injective f
add : ∀ (x y : R), f (x + y) = f x + f y
mul : ∀ (x y : R), f (x * y) = f x * f y
x y z : R
⊢ f ((x + y) * z) = f (x * z + y * z)
[PROOFSTEP]
simp only [*, right_distrib]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
S : Type ?u.1511
inst✝² : Distrib R
inst✝¹ : Add S
inst✝ : Mul S
f : R → S
hf : Surjective f
add : ∀ (x y : R), f (x + y) = f x + f y
mul : ∀ (x y : R), f (x * y) = f x * f y
x y z : R
⊢ f x * (f y + f z) = f x * f y + f x * f z
[PROOFSTEP]
simp only [← add, ← mul, left_distrib]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
S : Type ?u.1511
inst✝² : Distrib R
inst✝¹ : Add S
inst✝ : Mul S
f : R → S
hf : Surjective f
add : ∀ (x y : R), f (x + y) = f x + f y
mul : ∀ (x y : R), f (x * y) = f x * f y
x y z : R
⊢ (f x + f y) * f z = f x * f z + f y * f z
[PROOFSTEP]
simp only [← add, ← mul, right_distrib]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝³ : Mul α
inst✝² : HasDistribNeg α
inst✝¹ : Neg β
inst✝ : Mul β
f : β → α
hf : Injective f
neg : ∀ (a : β), f (-a) = -f a
mul : ∀ (a b : β), f (a * b) = f a * f b
src✝¹ : InvolutiveNeg β := Injective.involutiveNeg f hf neg
src✝ : Mul β := inst✝
x y : β
⊢ f (-x * y) = f (-(x * y))
[PROOFSTEP]
erw [neg, mul, neg, neg_mul, mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝³ : Mul α
inst✝² : HasDistribNeg α
inst✝¹ : Neg β
inst✝ : Mul β
f : β → α
hf : Injective f
neg : ∀ (a : β), f (-a) = -f a
mul : ∀ (a b : β), f (a * b) = f a * f b
src✝¹ : InvolutiveNeg β := Injective.involutiveNeg f hf neg
src✝ : Mul β := inst✝
x y : β
⊢ f (x * -y) = f (-(x * y))
[PROOFSTEP]
erw [neg, mul, neg, mul_neg, mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝³ : Mul α
inst✝² : HasDistribNeg α
inst✝¹ : Neg β
inst✝ : Mul β
f : α → β
hf : Surjective f
neg : ∀ (a : α), f (-a) = -f a
mul : ∀ (a b : α), f (a * b) = f a * f b
src✝¹ : InvolutiveNeg β := Surjective.involutiveNeg f hf neg
src✝ : Mul β := inst✝
x y : α
⊢ -f x * f y = -(f x * f y)
[PROOFSTEP]
erw [← neg, ← mul, neg_mul, neg, mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝³ : Mul α
inst✝² : HasDistribNeg α
inst✝¹ : Neg β
inst✝ : Mul β
f : α → β
hf : Surjective f
neg : ∀ (a : α), f (-a) = -f a
mul : ∀ (a b : α), f (a * b) = f a * f b
src✝¹ : InvolutiveNeg β := Surjective.involutiveNeg f hf neg
src✝ : Mul β := inst✝
x y : α
⊢ f x * -f y = -(f x * f y)
[PROOFSTEP]
erw [← neg, ← mul, mul_neg, neg, mul]
