[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : OrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝¹ : OrderedAddCommMonoid β := orderedAddCommMonoid f hf zero add nsmul
src✝ : Semiring β := Injective.semiring f hf zero one add mul nsmul npow nat_cast
⊢ f 0 ≤ f 1
[PROOFSTEP]
simp only [zero, one, zero_le_one]
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : OrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝¹ : OrderedAddCommMonoid β := orderedAddCommMonoid f hf zero add nsmul
src✝ : Semiring β := Injective.semiring f hf zero one add mul nsmul npow nat_cast
a b c : β
h : a ≤ b
hc : 0 ≤ c
⊢ f (c * a) ≤ f (c * b)
[PROOFSTEP]
rw [mul, mul]
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : OrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝¹ : OrderedAddCommMonoid β := orderedAddCommMonoid f hf zero add nsmul
src✝ : Semiring β := Injective.semiring f hf zero one add mul nsmul npow nat_cast
a b c : β
h : a ≤ b
hc : 0 ≤ c
⊢ f c * f a ≤ f c * f b
[PROOFSTEP]
refine' mul_le_mul_of_nonneg_left h _
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : OrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝¹ : OrderedAddCommMonoid β := orderedAddCommMonoid f hf zero add nsmul
src✝ : Semiring β := Injective.semiring f hf zero one add mul nsmul npow nat_cast
a b c : β
h : a ≤ b
hc : 0 ≤ c
⊢ 0 ≤ f c
[PROOFSTEP]
rwa [← zero]
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : OrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝¹ : OrderedAddCommMonoid β := orderedAddCommMonoid f hf zero add nsmul
src✝ : Semiring β := Injective.semiring f hf zero one add mul nsmul npow nat_cast
a b c : β
h : a ≤ b
hc : 0 ≤ c
⊢ f (a * c) ≤ f (b * c)
[PROOFSTEP]
rw [mul, mul]
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : OrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝¹ : OrderedAddCommMonoid β := orderedAddCommMonoid f hf zero add nsmul
src✝ : Semiring β := Injective.semiring f hf zero one add mul nsmul npow nat_cast
a b c : β
h : a ≤ b
hc : 0 ≤ c
⊢ f a * f c ≤ f b * f c
[PROOFSTEP]
refine' mul_le_mul_of_nonneg_right h _
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : OrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝¹ : OrderedAddCommMonoid β := orderedAddCommMonoid f hf zero add nsmul
src✝ : Semiring β := Injective.semiring f hf zero one add mul nsmul npow nat_cast
a b c : β
h : a ≤ b
hc : 0 ≤ c
⊢ 0 ≤ f c
[PROOFSTEP]
rwa [← zero]
[GOAL]
α : Type u
β : Type u_1
inst✝¹¹ : OrderedRing α
inst✝¹⁰ : Zero β
inst✝⁹ : One β
inst✝⁸ : Add β
inst✝⁷ : Mul β
inst✝⁶ : Neg β
inst✝⁵ : Sub β
inst✝⁴ : SMul ℕ β
inst✝³ : SMul ℤ β
inst✝² : Pow β ℕ
inst✝¹ : NatCast β
inst✝ : IntCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
neg : ∀ (x : β), f (-x) = -f x
sub : ∀ (x y : β), f (x - y) = f x - f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : OrderedSemiring β := Injective.orderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Ring β := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a b : β
ha : 0 ≤ a
hb : 0 ≤ b
⊢ f 0 ≤ f (a * b)
[PROOFSTEP]
rw [zero, mul]
[GOAL]
α : Type u
β : Type u_1
inst✝¹¹ : OrderedRing α
inst✝¹⁰ : Zero β
inst✝⁹ : One β
inst✝⁸ : Add β
inst✝⁷ : Mul β
inst✝⁶ : Neg β
inst✝⁵ : Sub β
inst✝⁴ : SMul ℕ β
inst✝³ : SMul ℤ β
inst✝² : Pow β ℕ
inst✝¹ : NatCast β
inst✝ : IntCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
neg : ∀ (x : β), f (-x) = -f x
sub : ∀ (x y : β), f (x - y) = f x - f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : OrderedSemiring β := Injective.orderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Ring β := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a b : β
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ f a * f b
[PROOFSTEP]
apply mul_nonneg
[GOAL]
case ha
α : Type u
β : Type u_1
inst✝¹¹ : OrderedRing α
inst✝¹⁰ : Zero β
inst✝⁹ : One β
inst✝⁸ : Add β
inst✝⁷ : Mul β
inst✝⁶ : Neg β
inst✝⁵ : Sub β
inst✝⁴ : SMul ℕ β
inst✝³ : SMul ℤ β
inst✝² : Pow β ℕ
inst✝¹ : NatCast β
inst✝ : IntCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
neg : ∀ (x : β), f (-x) = -f x
sub : ∀ (x y : β), f (x - y) = f x - f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : OrderedSemiring β := Injective.orderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Ring β := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a b : β
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ f a
[PROOFSTEP]
rwa [← zero]
[GOAL]
case hb
α : Type u
β : Type u_1
inst✝¹¹ : OrderedRing α
inst✝¹⁰ : Zero β
inst✝⁹ : One β
inst✝⁸ : Add β
inst✝⁷ : Mul β
inst✝⁶ : Neg β
inst✝⁵ : Sub β
inst✝⁴ : SMul ℕ β
inst✝³ : SMul ℤ β
inst✝² : Pow β ℕ
inst✝¹ : NatCast β
inst✝ : IntCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
neg : ∀ (x : β), f (-x) = -f x
sub : ∀ (x y : β), f (x - y) = f x - f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : OrderedSemiring β := Injective.orderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Ring β := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a b : β
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ f b
[PROOFSTEP]
rwa [← zero]
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : StrictOrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝² : OrderedCancelAddCommMonoid β := orderedCancelAddCommMonoid f hf zero add nsmul
src✝¹ : OrderedSemiring β := Injective.orderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Nontrivial β := pullback_nonzero f zero one
a b c : β
h : a < b
hc : 0 < c
⊢ f (c * a) < f (c * b)
[PROOFSTEP]
simpa only [mul, zero] using mul_lt_mul_of_pos_left ‹f a < f b› (by rwa [← zero])
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : StrictOrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝² : OrderedCancelAddCommMonoid β := orderedCancelAddCommMonoid f hf zero add nsmul
src✝¹ : OrderedSemiring β := Injective.orderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Nontrivial β := pullback_nonzero f zero one
a b c : β
h : a < b
hc : 0 < c
⊢ 0 < f c
[PROOFSTEP]
rwa [← zero]
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : StrictOrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝² : OrderedCancelAddCommMonoid β := orderedCancelAddCommMonoid f hf zero add nsmul
src✝¹ : OrderedSemiring β := Injective.orderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Nontrivial β := pullback_nonzero f zero one
a b c : β
h : a < b
hc : 0 < c
⊢ f (a * c) < f (b * c)
[PROOFSTEP]
simpa only [mul, zero] using mul_lt_mul_of_pos_right ‹f a < f b› (by rwa [← zero])
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : StrictOrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝² : OrderedCancelAddCommMonoid β := orderedCancelAddCommMonoid f hf zero add nsmul
src✝¹ : OrderedSemiring β := Injective.orderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Nontrivial β := pullback_nonzero f zero one
a b c : β
h : a < b
hc : 0 < c
⊢ 0 < f c
[PROOFSTEP]
rwa [← zero]
[GOAL]
α : Type u
β : Type u_1
inst✝¹¹ : StrictOrderedRing α
inst✝¹⁰ : Zero β
inst✝⁹ : One β
inst✝⁸ : Add β
inst✝⁷ : Mul β
inst✝⁶ : Neg β
inst✝⁵ : Sub β
inst✝⁴ : SMul ℕ β
inst✝³ : SMul ℤ β
inst✝² : Pow β ℕ
inst✝¹ : NatCast β
inst✝ : IntCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
neg : ∀ (x : β), f (-x) = -f x
sub : ∀ (x y : β), f (x - y) = f x - f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : StrictOrderedSemiring β := Injective.strictOrderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Ring β := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a b : β
a0 : 0 < a
b0 : 0 < b
⊢ f 0 < f (a * b)
[PROOFSTEP]
rw [zero, mul]
[GOAL]
α : Type u
β : Type u_1
inst✝¹¹ : StrictOrderedRing α
inst✝¹⁰ : Zero β
inst✝⁹ : One β
inst✝⁸ : Add β
inst✝⁷ : Mul β
inst✝⁶ : Neg β
inst✝⁵ : Sub β
inst✝⁴ : SMul ℕ β
inst✝³ : SMul ℤ β
inst✝² : Pow β ℕ
inst✝¹ : NatCast β
inst✝ : IntCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
neg : ∀ (x : β), f (-x) = -f x
sub : ∀ (x y : β), f (x - y) = f x - f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : StrictOrderedSemiring β := Injective.strictOrderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Ring β := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a b : β
a0 : 0 < a
b0 : 0 < b
⊢ 0 < f a * f b
[PROOFSTEP]
apply mul_pos
[GOAL]
case ha
α : Type u
β : Type u_1
inst✝¹¹ : StrictOrderedRing α
inst✝¹⁰ : Zero β
inst✝⁹ : One β
inst✝⁸ : Add β
inst✝⁷ : Mul β
inst✝⁶ : Neg β
inst✝⁵ : Sub β
inst✝⁴ : SMul ℕ β
inst✝³ : SMul ℤ β
inst✝² : Pow β ℕ
inst✝¹ : NatCast β
inst✝ : IntCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
neg : ∀ (x : β), f (-x) = -f x
sub : ∀ (x y : β), f (x - y) = f x - f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : StrictOrderedSemiring β := Injective.strictOrderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Ring β := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a b : β
a0 : 0 < a
b0 : 0 < b
⊢ 0 < f a
[PROOFSTEP]
rwa [← zero]
[GOAL]
case hb
α : Type u
β : Type u_1
inst✝¹¹ : StrictOrderedRing α
inst✝¹⁰ : Zero β
inst✝⁹ : One β
inst✝⁸ : Add β
inst✝⁷ : Mul β
inst✝⁶ : Neg β
inst✝⁵ : Sub β
inst✝⁴ : SMul ℕ β
inst✝³ : SMul ℤ β
inst✝² : Pow β ℕ
inst✝¹ : NatCast β
inst✝ : IntCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
neg : ∀ (x : β), f (-x) = -f x
sub : ∀ (x y : β), f (x - y) = f x - f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : StrictOrderedSemiring β := Injective.strictOrderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Ring β := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a b : β
a0 : 0 < a
b0 : 0 < b
⊢ 0 < f b
[PROOFSTEP]
rwa [← zero]
