[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
⊢ StrictMono f
[PROOFSTEP]
refine' StrictMonoOn.Iic_union_Ici (fun x hx y hy hxy => neg_lt_neg_iff.1 _) h₂
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x < y
⊢ -f y < -f x
[PROOFSTEP]
rw [← h₁, ← h₁]
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x < y
⊢ f (-y) < f (-x)
[PROOFSTEP]
exact h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_lt_neg hxy)
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
⊢ Monotone f
[PROOFSTEP]
refine' MonotoneOn.Iic_union_Ici (fun x hx y hy hxy => neg_le_neg_iff.1 _) h₂
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x ≤ y
⊢ -f y ≤ -f x
[PROOFSTEP]
rw [← h₁, ← h₁]
[GOAL]
G : Type u_1
H : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderedAddCommGroup H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
x : G
hx : x ∈ Iic 0
y : G
hy : y ∈ Iic 0
hxy : x ≤ y
⊢ f (-y) ≤ f (-x)
[PROOFSTEP]
exact h₂ (neg_nonneg.2 hy) (neg_nonneg.2 hx) (neg_le_neg hxy)
