[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Group α
inst✝² : CommSemigroup β
inst✝¹ : LE β
inst✝ : SubmultiplicativeHomClass F α β
f : F
a b : α
⊢ ↑f a ≤ ↑f b * ↑f (a / b)
[PROOFSTEP]
simpa only [mul_comm, div_mul_cancel'] using map_mul_le_mul f (a / b) b
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Group α
inst✝² : AddCommSemigroup β
inst✝¹ : LE β
inst✝ : MulLEAddHomClass F α β
f : F
a b : α
⊢ ↑f a ≤ ↑f b + ↑f (a / b)
[PROOFSTEP]
simpa only [add_comm, div_mul_cancel'] using map_mul_le_add f (a / b) b
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Group α
inst✝² : CommSemigroup β
inst✝¹ : LE β
inst✝ : SubmultiplicativeHomClass F α β
f : F
a b c : α
⊢ ↑f (a / c) ≤ ↑f (a / b) * ↑f (b / c)
[PROOFSTEP]
simpa only [div_mul_div_cancel'] using map_mul_le_mul f (a / b) (b / c)
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : Group α
inst✝² : AddCommSemigroup β
inst✝¹ : LE β
inst✝ : MulLEAddHomClass F α β
f : F
a b c : α
⊢ ↑f (a / c) ≤ ↑f (a / b) + ↑f (b / c)
[PROOFSTEP]
simpa only [div_mul_div_cancel'] using map_mul_le_add f (a / b) (b / c)
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f (x / y) ≤ ↑f x + ↑f y
[PROOFSTEP]
rw [div_eq_mul_inv, ← map_inv_eq_map f y]
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f (x * y⁻¹) ≤ ↑f x + ↑f y⁻¹
[PROOFSTEP]
exact map_mul_le_add _ _ _
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f (x / y) = ↑f (y / x)
[PROOFSTEP]
rw [← inv_div, map_inv_eq_map]
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f x ≤ ↑f y + ↑f (y / x)
[PROOFSTEP]
simpa only [add_comm, map_div_rev, div_mul_cancel'] using map_mul_le_add f (x / y) y
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : LinearOrderedAddCommGroup β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ |↑f x - ↑f y| ≤ ↑f (x / y)
[PROOFSTEP]
rw [abs_sub_le_iff, sub_le_iff_le_add', sub_le_iff_le_add']
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : LinearOrderedAddCommGroup β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ ↑f x ≤ ↑f y + ↑f (x / y) ∧ ↑f y ≤ ↑f x + ↑f (x / y)
[PROOFSTEP]
exact ⟨le_map_add_map_div _ _ _, le_map_add_map_div' _ _ _⟩
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : LinearOrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
src✝ : GroupSeminormClass F α β := inst✝
f : F
a : α
⊢ 0 ≤ 2 • ↑f a
[PROOFSTEP]
rw [two_nsmul, ← map_one_eq_zero f, ← div_self' a]
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : LinearOrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
src✝ : GroupSeminormClass F α β := inst✝
f : F
a : α
⊢ ↑f (a / a) ≤ ↑f a + ↑f a
[PROOFSTEP]
exact map_div_le_add _ _ _
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupNormClass F α β
f : F
x : α
⊢ x = 1 → ↑f x = 0
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupNormClass F α β
f : F
⊢ ↑f 1 = 0
[PROOFSTEP]
exact map_one_eq_zero _
