Theorem: AlmostHom.NonNeg.bddAbove_on_nonpos (RealsQuasiMorphisms/Order.lean)

State before:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ toFun f g ≤ ↑bound' - bound
Tactic:
have : f g - -f (-g) ≤ bound' := by
  apply Int.le_trans (Int.le_natAbs ..); apply Int.ofNat_le.mpr
  rewrite [show f g - -f (-g) = f (-g) - -f g by abel]; exact hₐ g
State after:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
this : toFun f g - -toFun f (-g) ≤ ↑bound'
⊢ toFun f g ≤ ↑bound' - bound

State before:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
this : toFun f g - -toFun f (-g) ≤ ↑bound'
⊢ toFun f g ≤ ↑bound' - bound
Tactic:
linarith [this, h (neg_nonneg_of_nonpos h_g)]
State after:
no goals

State before:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ toFun f g - -toFun f (-g) ≤ ↑bound'
Tactic:
apply Int.le_trans (Int.le_natAbs ..)
State after:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ ↑(|toFun f g - -toFun f (-g)|) ≤ ↑bound'

State before:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ ↑(|toFun f g - -toFun f (-g)|) ≤ ↑bound'
Tactic:
apply Int.ofNat_le.mpr
State after:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ |toFun f g - -toFun f (-g)| ≤ bound'

State before:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ |toFun f g - -toFun f (-g)| ≤ bound'
Tactic:
rewrite [show f g - -f (-g) = f (-g) - -f g by abel]
State after:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ |toFun f (-g) - -toFun f g| ≤ bound'

State before:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ |toFun f (-g) - -toFun f g| ≤ bound'
Tactic:
exact hₐ g
State after:
no goals

State before:
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ toFun f g - -toFun f (-g) = toFun f (-g) - -toFun f g
Tactic:
abel
State after:
no goals