[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a✝ b✝ c✝ d a b c : α
⊢ (a + b) / c = a / c + b / c
[PROOFSTEP]
simp_rw [div_eq_mul_inv, add_mul]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a b c d : α
h : b ≠ 0
⊢ (b + a) / b = 1 + a / b
[PROOFSTEP]
rw [← div_self h, add_div]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a b c d : α
h : b ≠ 0
⊢ (a + b) / b = a / b + 1
[PROOFSTEP]
rw [← div_self h, add_div]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a b c d : α
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a * (a + b) * (1 / b) = 1 / a + 1 / b
[PROOFSTEP]
rw [mul_add, one_div_mul_cancel ha, add_mul, one_mul, mul_assoc, mul_one_div_cancel hb, mul_one, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a✝ b✝ c d a b : α
hc : c ≠ 0
⊢ (a + b / c) * c = a * c + b
[PROOFSTEP]
rw [right_distrib, div_mul_cancel _ hc]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a✝ b✝ c✝ d a b c : α
hc : c ≠ 0
⊢ b + a / c = (b * c + a) / c
[PROOFSTEP]
rw [add_div, mul_div_cancel _ hc]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a✝ b✝ c✝ d a b c : α
hc : c ≠ 0
⊢ a / c + b = (a + b * c) / c
[PROOFSTEP]
rwa [add_comm, add_div', add_comm]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a b c d : α
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b + c / d = (a * d + b * c) / (b * d)
[PROOFSTEP]
rw [add_div, mul_div_mul_right _ b hd, hbc.eq, hbd.eq, mul_div_mul_right c d hb]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a b c d : α
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a + 1 / b = (a + b) / (a * b)
[PROOFSTEP]
rw [(Commute.one_right a).div_add_div hab ha hb, one_mul, mul_one, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionSemiring α
a b c d : α
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ + b⁻¹ = (a + b) / (a * b)
[PROOFSTEP]
rw [inv_eq_one_div, inv_eq_one_div, hab.one_div_add_one_div ha hb]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a b : K
⊢ -1 * -1 = 1
[PROOFSTEP]
rw [neg_mul_neg, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b a : K
⊢ 1 / -a = 1 / (-1 * a)
[PROOFSTEP]
rw [neg_eq_neg_one_mul]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b a : K
⊢ 1 / (-1 * a) = 1 / a * (1 / -1)
[PROOFSTEP]
rw [one_div_mul_one_div_rev]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b a : K
⊢ 1 / a * (1 / -1) = 1 / a * -1
[PROOFSTEP]
rw [one_div_neg_one_eq_neg_one]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b a : K
⊢ 1 / a * -1 = -(1 / a)
[PROOFSTEP]
rw [mul_neg, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ b / -a = b * (1 / -a)
[PROOFSTEP]
rw [← inv_eq_one_div, division_def]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ b * (1 / -a) = b * -(1 / a)
[PROOFSTEP]
rw [one_div_neg_eq_neg_one_div]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ b * -(1 / a) = -(b * (1 / a))
[PROOFSTEP]
rw [neg_mul_eq_mul_neg]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ -(b * (1 / a)) = -(b / a)
[PROOFSTEP]
rw [mul_one_div]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ -b / a = -(b / a)
[PROOFSTEP]
rw [neg_eq_neg_one_mul, mul_div_assoc, ← neg_eq_neg_one_mul]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ -(b / a) = -b / a
[PROOFSTEP]
simp [neg_div]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b✝ a b : K
⊢ -a / -b = a / b
[PROOFSTEP]
rw [div_neg_eq_neg_div, neg_div, neg_neg]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a b : K
⊢ -a⁻¹ = (-a)⁻¹
[PROOFSTEP]
rw [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a✝ b a : K
⊢ a / -b = -(a / b)
[PROOFSTEP]
rw [← div_neg_eq_neg_div]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a b : K
⊢ (-a)⁻¹ = -a⁻¹
[PROOFSTEP]
rw [neg_inv]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹ : DivisionMonoid K
inst✝ : HasDistribNeg K
a b : K
⊢ (-1)⁻¹ = -1
[PROOFSTEP]
rw [← neg_inv, inv_one]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a✝ b c d a : K
h : a ≠ 0
⊢ a / -a = -1
[PROOFSTEP]
rw [div_neg_eq_neg_div, div_self h]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a✝ b c d a : K
h : a ≠ 0
⊢ -a / a = -1
[PROOFSTEP]
rw [neg_div, div_self h]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a✝ b✝ c✝ d a b c : K
⊢ a / c - b / c = (a - b) / c
[PROOFSTEP]
rw [sub_eq_add_neg, ← neg_div, div_add_div_same, sub_eq_add_neg]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a✝ b✝ c d a b : K
h : b ≠ 0
⊢ (b - a) / b = 1 - a / b
[PROOFSTEP]
simpa only [← @div_self _ _ b h] using (div_sub_div_same b a b).symm
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a✝ b✝ c d a b : K
h : b ≠ 0
⊢ (a - b) / b = a / b - 1
[PROOFSTEP]
simpa only [← @div_self _ _ b h] using (div_sub_div_same a b b).symm
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a✝ b✝ c d a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = a⁻¹ * (b - a) * b⁻¹
[PROOFSTEP]
rw [mul_sub, sub_mul, mul_inv_cancel_right₀ hb, inv_mul_cancel ha, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a b c d : K
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a * (b - a) * (1 / b) = 1 / a - 1 / b
[PROOFSTEP]
rw [mul_sub_left_distrib (1 / a), one_div_mul_cancel ha, mul_sub_right_distrib, one_mul, mul_assoc,
  mul_one_div_cancel hb, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b - c / d = (a * d - b * c) / (b * d)
[PROOFSTEP]
simpa only [mul_neg, neg_div, ← sub_eq_add_neg] using hbc.neg_right.div_add_div hbd hb hd
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : DivisionRing K
a b c d : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)
[PROOFSTEP]
simp only [inv_eq_one_div, (Commute.one_right a).div_sub_div hab ha hb, one_mul, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : Field K
a b : K
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ - b⁻¹ = (b - a) / (a * b)
[PROOFSTEP]
rw [inv_eq_one_div, inv_eq_one_div, div_sub_div _ _ ha hb, one_mul, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : Field K
a b c : K
hc : c ≠ 0
⊢ b - a / c = (b * c - a) / c
[PROOFSTEP]
simpa using div_sub_div b a one_ne_zero hc
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝ : Field K
a b c : K
hc : c ≠ 0
⊢ a / c - b = (a - c * b) / c
[PROOFSTEP]
simpa using div_sub_div a b hc one_ne_zero
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹⁶ : DivisionRing K
K' : Type ?u.52132
inst✝¹⁵ : Zero K'
inst✝¹⁴ : One K'
inst✝¹³ : Add K'
inst✝¹² : Mul K'
inst✝¹¹ : Neg K'
inst✝¹⁰ : Sub K'
inst✝⁹ : Inv K'
inst✝⁸ : Div K'
inst✝⁷ : SMul ℕ K'
inst✝⁶ : SMul ℤ K'
inst✝⁵ : SMul ℚ K'
inst✝⁴ : Pow K' ℕ
inst✝³ : Pow K' ℤ
inst✝² : NatCast K'
inst✝¹ : IntCast K'
inst✝ : RatCast K'
f : K' → K
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K'), f (x + y) = f x + f y
mul : ∀ (x y : K'), f (x * y) = f x * f y
neg : ∀ (x : K'), f (-x) = -f x
sub : ∀ (x y : K'), f (x - y) = f x - f y
inv : ∀ (x : K'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K'), f (x / y) = f x / f y
nsmul : ∀ (x : K') (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : K') (n : ℤ), f (n • x) = n • f x
qsmul : ∀ (x : K') (n : ℚ), f (n • x) = n • f x
npow : ∀ (x : K') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K') (n : ℤ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
rat_cast : ∀ (n : ℚ), f ↑n = ↑n
src✝¹ : GroupWithZero K' := Injective.groupWithZero f hf zero one mul inv div npow zpow
src✝ : Ring K' := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ f ↑(Rat.mk' a b) = f (↑a * (↑b)⁻¹)
[PROOFSTEP]
erw [rat_cast, mul, inv, int_cast, nat_cast]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹⁶ : DivisionRing K
K' : Type ?u.52132
inst✝¹⁵ : Zero K'
inst✝¹⁴ : One K'
inst✝¹³ : Add K'
inst✝¹² : Mul K'
inst✝¹¹ : Neg K'
inst✝¹⁰ : Sub K'
inst✝⁹ : Inv K'
inst✝⁸ : Div K'
inst✝⁷ : SMul ℕ K'
inst✝⁶ : SMul ℤ K'
inst✝⁵ : SMul ℚ K'
inst✝⁴ : Pow K' ℕ
inst✝³ : Pow K' ℤ
inst✝² : NatCast K'
inst✝¹ : IntCast K'
inst✝ : RatCast K'
f : K' → K
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K'), f (x + y) = f x + f y
mul : ∀ (x y : K'), f (x * y) = f x * f y
neg : ∀ (x : K'), f (-x) = -f x
sub : ∀ (x y : K'), f (x - y) = f x - f y
inv : ∀ (x : K'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K'), f (x / y) = f x / f y
nsmul : ∀ (x : K') (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : K') (n : ℤ), f (n • x) = n • f x
qsmul : ∀ (x : K') (n : ℚ), f (n • x) = n • f x
npow : ∀ (x : K') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K') (n : ℤ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
rat_cast : ∀ (n : ℚ), f ↑n = ↑n
src✝¹ : GroupWithZero K' := Injective.groupWithZero f hf zero one mul inv div npow zpow
src✝ : Ring K' := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹
[PROOFSTEP]
exact DivisionRing.ratCast_mk a b h1 h2
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹⁶ : DivisionRing K
K' : Type ?u.52132
inst✝¹⁵ : Zero K'
inst✝¹⁴ : One K'
inst✝¹³ : Add K'
inst✝¹² : Mul K'
inst✝¹¹ : Neg K'
inst✝¹⁰ : Sub K'
inst✝⁹ : Inv K'
inst✝⁸ : Div K'
inst✝⁷ : SMul ℕ K'
inst✝⁶ : SMul ℤ K'
inst✝⁵ : SMul ℚ K'
inst✝⁴ : Pow K' ℕ
inst✝³ : Pow K' ℤ
inst✝² : NatCast K'
inst✝¹ : IntCast K'
inst✝ : RatCast K'
f : K' → K
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K'), f (x + y) = f x + f y
mul : ∀ (x y : K'), f (x * y) = f x * f y
neg : ∀ (x : K'), f (-x) = -f x
sub : ∀ (x y : K'), f (x - y) = f x - f y
inv : ∀ (x : K'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K'), f (x / y) = f x / f y
nsmul : ∀ (x : K') (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : K') (n : ℤ), f (n • x) = n • f x
qsmul : ∀ (x : K') (n : ℚ), f (n • x) = n • f x
npow : ∀ (x : K') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K') (n : ℤ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
rat_cast : ∀ (n : ℚ), f ↑n = ↑n
src✝¹ : GroupWithZero K' := Injective.groupWithZero f hf zero one mul inv div npow zpow
src✝ : Ring K' := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a : ℚ
x : K'
⊢ f ((fun x x_1 => x • x_1) a x) = f (↑a * x)
[PROOFSTEP]
erw [qsmul, mul, Rat.smul_def, rat_cast]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹⁶ : Field K
K' : Type ?u.64255
inst✝¹⁵ : Zero K'
inst✝¹⁴ : Mul K'
inst✝¹³ : Add K'
inst✝¹² : Neg K'
inst✝¹¹ : Sub K'
inst✝¹⁰ : One K'
inst✝⁹ : Inv K'
inst✝⁸ : Div K'
inst✝⁷ : SMul ℕ K'
inst✝⁶ : SMul ℤ K'
inst✝⁵ : SMul ℚ K'
inst✝⁴ : Pow K' ℕ
inst✝³ : Pow K' ℤ
inst✝² : NatCast K'
inst✝¹ : IntCast K'
inst✝ : RatCast K'
f : K' → K
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K'), f (x + y) = f x + f y
mul : ∀ (x y : K'), f (x * y) = f x * f y
neg : ∀ (x : K'), f (-x) = -f x
sub : ∀ (x y : K'), f (x - y) = f x - f y
inv : ∀ (x : K'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K'), f (x / y) = f x / f y
nsmul : ∀ (x : K') (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : K') (n : ℤ), f (n • x) = n • f x
qsmul : ∀ (x : K') (n : ℚ), f (n • x) = n • f x
npow : ∀ (x : K') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K') (n : ℤ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
rat_cast : ∀ (n : ℚ), f ↑n = ↑n
src✝¹ : CommGroupWithZero K' := Injective.commGroupWithZero f hf zero one mul inv div npow zpow
src✝ : CommRing K' := Injective.commRing f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ f ↑(Rat.mk' a b) = f (↑a * (↑b)⁻¹)
[PROOFSTEP]
erw [rat_cast, mul, inv, int_cast, nat_cast]
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹⁶ : Field K
K' : Type ?u.64255
inst✝¹⁵ : Zero K'
inst✝¹⁴ : Mul K'
inst✝¹³ : Add K'
inst✝¹² : Neg K'
inst✝¹¹ : Sub K'
inst✝¹⁰ : One K'
inst✝⁹ : Inv K'
inst✝⁸ : Div K'
inst✝⁷ : SMul ℕ K'
inst✝⁶ : SMul ℤ K'
inst✝⁵ : SMul ℚ K'
inst✝⁴ : Pow K' ℕ
inst✝³ : Pow K' ℤ
inst✝² : NatCast K'
inst✝¹ : IntCast K'
inst✝ : RatCast K'
f : K' → K
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K'), f (x + y) = f x + f y
mul : ∀ (x y : K'), f (x * y) = f x * f y
neg : ∀ (x : K'), f (-x) = -f x
sub : ∀ (x y : K'), f (x - y) = f x - f y
inv : ∀ (x : K'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K'), f (x / y) = f x / f y
nsmul : ∀ (x : K') (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : K') (n : ℤ), f (n • x) = n • f x
qsmul : ∀ (x : K') (n : ℚ), f (n • x) = n • f x
npow : ∀ (x : K') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K') (n : ℤ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
rat_cast : ∀ (n : ℚ), f ↑n = ↑n
src✝¹ : CommGroupWithZero K' := Injective.commGroupWithZero f hf zero one mul inv div npow zpow
src✝ : CommRing K' := Injective.commRing f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a : ℤ
b : ℕ
h1 : b ≠ 0
h2 : Nat.coprime (Int.natAbs a) b
⊢ ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹
[PROOFSTEP]
exact DivisionRing.ratCast_mk a b h1 h2
[GOAL]
α : Type u_1
β : Type u_2
K : Type u_3
inst✝¹⁶ : Field K
K' : Type ?u.64255
inst✝¹⁵ : Zero K'
inst✝¹⁴ : Mul K'
inst✝¹³ : Add K'
inst✝¹² : Neg K'
inst✝¹¹ : Sub K'
inst✝¹⁰ : One K'
inst✝⁹ : Inv K'
inst✝⁸ : Div K'
inst✝⁷ : SMul ℕ K'
inst✝⁶ : SMul ℤ K'
inst✝⁵ : SMul ℚ K'
inst✝⁴ : Pow K' ℕ
inst✝³ : Pow K' ℤ
inst✝² : NatCast K'
inst✝¹ : IntCast K'
inst✝ : RatCast K'
f : K' → K
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K'), f (x + y) = f x + f y
mul : ∀ (x y : K'), f (x * y) = f x * f y
neg : ∀ (x : K'), f (-x) = -f x
sub : ∀ (x y : K'), f (x - y) = f x - f y
inv : ∀ (x : K'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K'), f (x / y) = f x / f y
nsmul : ∀ (x : K') (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : K') (n : ℤ), f (n • x) = n • f x
qsmul : ∀ (x : K') (n : ℚ), f (n • x) = n • f x
npow : ∀ (x : K') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K') (n : ℤ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
rat_cast : ∀ (n : ℚ), f ↑n = ↑n
src✝¹ : CommGroupWithZero K' := Injective.commGroupWithZero f hf zero one mul inv div npow zpow
src✝ : CommRing K' := Injective.commRing f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a : ℚ
x : K'
⊢ f ((fun x x_1 => x • x_1) a x) = f (↑a * x)
[PROOFSTEP]
erw [qsmul, mul, Rat.smul_def, rat_cast]
