Theorem: AlmostHom.comp_almost_comm (RealsQuasiMorphisms/Ring.lean)

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ Bounded (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁)
Tactic:
have succ_le_two_mul (a : ℕ) (ha : a ≠ 0) : a+1 ≤ 2*a := by
  cases a
  case zero => contradiction
  case succ => apply Nat.succ_le.2; linarith [NeZero.pos]
State after:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
⊢ Bounded (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁)

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
⊢ Bounded (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁)
Tactic:
simp only [Bounded, _root_.Bounded]
State after:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
⊢ ∃ bound, ∀ (g : ℤ), |toFun (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁) g| ≤ bound

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
⊢ ∃ bound, ∀ (g : ℤ), |toFun (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁) g| ≤ bound
Tactic:
let ⟨k₁, hf₁⟩ := comp_almost_mul f₁ f₂
State after:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
⊢ ∃ bound, ∀ (g : ℤ), |toFun (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁) g| ≤ bound

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
⊢ ∃ bound, ∀ (g : ℤ), |toFun (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁) g| ≤ bound
Tactic:
let ⟨k₂, hf₂⟩ := comp_almost_mul f₂ f₁
State after:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ∃ bound, ∀ (g : ℤ), |toFun (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁) g| ≤ bound

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ∃ bound, ∀ (g : ℤ), |toFun (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁) g| ≤ bound
Tactic:
exact ⟨_, by
  intro n
  rewrite [show (-f₁.comp f₂ + f₂.comp f₁) n = (-f₁.comp f₂ n + f₂.comp f₁ n) from rfl,
           ←Int.natAbs_neg,
           show -(-f₁.comp f₂ n + f₂.comp f₁ n) = f₁.comp f₂ n - f₂.comp f₁ n by
             rw [neg_add_rev, neg_neg, sub_eq_neg_add]]
  have triag := Int.natAbs_add_le (n * (f₁.comp f₂ n) - f₂ n * f₁ n) (f₂ n * f₁ n - n * (f₂.comp f₁ n))
  simp only [sub_add_sub_cancel, Int.diff_eq] at triag
  if c: n = 0
  then
    simp only [c, zero_mul, zero_sub, Int.natAbs_neg, ge_iff_le] at hf₁ hf₂ |-
    exact self_le_add_right |(f₁.comp f₂ - f₂.comp f₁) 0| (2*(k₁ + k₂))
  else
  have goal_mul_n :=
    calc |n| * |f₁.comp f₂ n - f₂.comp f₁ n|
      = |n*f₁.comp f₂ n - n*f₂.comp f₁ n| := by rw [←Int.natAbs_mul, mul_sub_left_distrib]
    _ ≤ |n*f₁.comp f₂ n - f₂ n * f₁ n| + |f₂ n * f₁ n - n*f₂.comp f₁ n| := triag
    _ ≤ |n*f₁.comp f₂ n - f₂ n * f₁ n| + (|n|+1)*k₂  :=
        by
          rw [mul_comm (f₂ n), ←Int.natAbs_neg (f₁ n * f₂ n - n * f₂.comp f₁ n)]
          apply Nat.add_le_add_left;
          simp only [neg_sub, Int.diff_eq]; exact hf₂ ..
    _ ≤ (|n|+1)*k₁ + (|n|+1)*k₂ := Nat.add_le_add_right (hf₁ ..) ..
    _ = (|n|+1)*(k₁ + k₂) := by ring
    _ ≤ |n| * (2*(k₁ + k₂)) :=
        by
          rw [←mul_assoc, mul_comm |n|]
          exact Nat.mul_le_mul_of_nonneg_right <|
                succ_le_two_mul |n| <|
                Int.natAbs_ne_zero.2 c
  calc |f₁.comp f₂ n - f₂.comp f₁ n|
    ≤ 2*(k₁ + k₂) := le_of_mul_le_mul_left goal_mul_n
      <| Or.resolve_left (Nat.eq_zero_or_pos ..) (Int.natAbs_ne_zero.2 c)
  _ ≤ _ := self_le_add_left  (2*(k₁ + k₂)) |(f₁.comp f₂ - f₂.comp f₁) 0|⟩
State after:
no goals

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a : ℕ
ha : a ≠ 0
⊢ a + 1 ≤ 2 * a
Tactic:
cases a
State after:
case zero
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
ha : Nat.zero ≠ 0
⊢ Nat.zero + 1 ≤ 2 * Nat.zero

case succ
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
n✝ : ℕ
ha : Nat.succ n✝ ≠ 0
⊢ Nat.succ n✝ + 1 ≤ 2 * Nat.succ n✝

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
ha : Nat.zero ≠ 0
⊢ Nat.zero + 1 ≤ 2 * Nat.zero
Tactic:
case zero => contradiction
State after:
no goals

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
n✝ : ℕ
ha : Nat.succ n✝ ≠ 0
⊢ Nat.succ n✝ + 1 ≤ 2 * Nat.succ n✝
Tactic:
case succ => apply Nat.succ_le.2; linarith [NeZero.pos]
State after:
no goals

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
ha : Nat.zero ≠ 0
⊢ Nat.zero + 1 ≤ 2 * Nat.zero
Tactic:
contradiction
State after:
no goals

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
n✝ : ℕ
ha : Nat.succ n✝ ≠ 0
⊢ Nat.succ n✝ + 1 ≤ 2 * Nat.succ n✝
Tactic:
apply Nat.succ_le.2
State after:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
n✝ : ℕ
ha : Nat.succ n✝ ≠ 0
⊢ n✝ + 1 < 2 * Nat.succ n✝

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
n✝ : ℕ
ha : Nat.succ n✝ ≠ 0
⊢ n✝ + 1 < 2 * Nat.succ n✝
Tactic:
linarith [NeZero.pos]
State after:
no goals

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ∀ (g : ℤ), |toFun (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁) g| ≤ ?m.49722
Tactic:
intro n
State after:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
⊢ |toFun (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁) n| ≤ ?m.49722

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
⊢ |toFun (-AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁) n| ≤ ?m.49722
Tactic:
rewrite [show (-f₁.comp f₂ + f₂.comp f₁) n = (-f₁.comp f₂ n + f₂.comp f₁ n) from rfl,
         ←Int.natAbs_neg,
         show -(-f₁.comp f₂ n + f₂.comp f₁ n) = f₁.comp f₂ n - f₂.comp f₁ n by
           rw [neg_add_rev, neg_neg, sub_eq_neg_add]]
State after:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
⊢ |toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n| ≤ ?m.49722

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
⊢ |toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n| ≤ ?m.49722

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ
Tactic:
have triag := Int.natAbs_add_le (n * (f₁.comp f₂ n) - f₂ n * f₁ n) (f₂ n * f₁ n - n * (f₂.comp f₁ n))
State after:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n +
        (toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n)| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
⊢ |toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n| ≤ ?m.49722

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n +
        (toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n)| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
⊢ |toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n| ≤ ?m.49722

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ
Tactic:
simp only [sub_add_sub_cancel, Int.diff_eq] at triag
State after:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
⊢ |toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n| ≤ ?m.49722

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
⊢ |toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n| ≤ ?m.49722

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ

G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
⊢ ℕ
Tactic:
if c: n = 0
then
  simp only [c, zero_mul, zero_sub, Int.natAbs_neg, ge_iff_le] at hf₁ hf₂ |-
  exact self_le_add_right |(f₁.comp f₂ - f₂.comp f₁) 0| (2*(k₁ + k₂))
else
have goal_mul_n :=
  calc |n| * |f₁.comp f₂ n - f₂.comp f₁ n|
    = |n*f₁.comp f₂ n - n*f₂.comp f₁ n| := by rw [←Int.natAbs_mul, mul_sub_left_distrib]
  _ ≤ |n*f₁.comp f₂ n - f₂ n * f₁ n| + |f₂ n * f₁ n - n*f₂.comp f₁ n| := triag
  _ ≤ |n*f₁.comp f₂ n - f₂ n * f₁ n| + (|n|+1)*k₂  :=
      by
        rw [mul_comm (f₂ n), ←Int.natAbs_neg (f₁ n * f₂ n - n * f₂.comp f₁ n)]
        apply Nat.add_le_add_left;
        simp only [neg_sub, Int.diff_eq]; exact hf₂ ..
  _ ≤ (|n|+1)*k₁ + (|n|+1)*k₂ := Nat.add_le_add_right (hf₁ ..) ..
  _ = (|n|+1)*(k₁ + k₂) := by ring
  _ ≤ |n| * (2*(k₁ + k₂)) :=
      by
        rw [←mul_assoc, mul_comm |n|]
        exact Nat.mul_le_mul_of_nonneg_right <|
              succ_le_two_mul |n| <|
              Int.natAbs_ne_zero.2 c
calc |f₁.comp f₂ n - f₂.comp f₁ n|
  ≤ 2*(k₁ + k₂) := le_of_mul_le_mul_left goal_mul_n
    <| Or.resolve_left (Nat.eq_zero_or_pos ..) (Int.natAbs_ne_zero.2 c)
_ ≤ _ := self_le_add_left  (2*(k₁ + k₂)) |(f₁.comp f₂ - f₂.comp f₁) 0|
State after:
no goals

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
⊢ -(-toFun (AlmostHom.comp f₁ f₂) n + toFun (AlmostHom.comp f₂ f₁) n) =
    toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n
Tactic:
rw [neg_add_rev, neg_neg, sub_eq_neg_add]
State after:
no goals

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : n = 0
⊢ |toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n| ≤ ?m.49722
Tactic:
simp only [c, zero_mul, zero_sub, Int.natAbs_neg, ge_iff_le] at hf₁ hf₂ |-
State after:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : n = 0
⊢ |toFun (AlmostHom.comp f₁ f₂) 0 - toFun (AlmostHom.comp f₂ f₁) 0| ≤ ?m.49722

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : n = 0
⊢ |toFun (AlmostHom.comp f₁ f₂) 0 - toFun (AlmostHom.comp f₂ f₁) 0| ≤ ?m.49722
Tactic:
exact self_le_add_right |(f₁.comp f₂ - f₂.comp f₁) 0| (2*(k₁ + k₂))
State after:
no goals

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
⊢ |toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n| ≤
    |toFun (AlmostHom.comp f₁ f₂ - AlmostHom.comp f₂ f₁) 0| + 2 * (k₁ + k₂)
Tactic:
have goal_mul_n :=
  calc |n| * |f₁.comp f₂ n - f₂.comp f₁ n|
    = |n*f₁.comp f₂ n - n*f₂.comp f₁ n| := by rw [←Int.natAbs_mul, mul_sub_left_distrib]
  _ ≤ |n*f₁.comp f₂ n - f₂ n * f₁ n| + |f₂ n * f₁ n - n*f₂.comp f₁ n| := triag
  _ ≤ |n*f₁.comp f₂ n - f₂ n * f₁ n| + (|n|+1)*k₂  :=
      by
        rw [mul_comm (f₂ n), ←Int.natAbs_neg (f₁ n * f₂ n - n * f₂.comp f₁ n)]
        apply Nat.add_le_add_left;
        simp only [neg_sub, Int.diff_eq]; exact hf₂ ..
  _ ≤ (|n|+1)*k₁ + (|n|+1)*k₂ := Nat.add_le_add_right (hf₁ ..) ..
  _ = (|n|+1)*(k₁ + k₂) := by ring
  _ ≤ |n| * (2*(k₁ + k₂)) :=
      by
        rw [←mul_assoc, mul_comm |n|]
        exact Nat.mul_le_mul_of_nonneg_right <|
              succ_le_two_mul |n| <|
              Int.natAbs_ne_zero.2 c
State after:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
goal_mul_n : |n| * |toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n| ≤ |n| * (2 * (k₁ + k₂))
⊢ |toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n| ≤
    |toFun (AlmostHom.comp f₁ f₂ - AlmostHom.comp f₂ f₁) 0| + 2 * (k₁ + k₂)

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
goal_mul_n : |n| * |toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n| ≤ |n| * (2 * (k₁ + k₂))
⊢ |toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n| ≤
    |toFun (AlmostHom.comp f₁ f₂ - AlmostHom.comp f₂ f₁) 0| + 2 * (k₁ + k₂)
Tactic:
calc |f₁.comp f₂ n - f₂.comp f₁ n|
  ≤ 2*(k₁ + k₂) := le_of_mul_le_mul_left goal_mul_n
    <| Or.resolve_left (Nat.eq_zero_or_pos ..) (Int.natAbs_ne_zero.2 c)
_ ≤ _ := self_le_add_left  (2*(k₁ + k₂)) |(f₁.comp f₂ - f₂.comp f₁) 0|
State after:
no goals

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
⊢ |n| * |toFun (AlmostHom.comp f₁ f₂) n - toFun (AlmostHom.comp f₂ f₁) n| =
    |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n|
Tactic:
rw [←Int.natAbs_mul, mul_sub_left_distrib]
State after:
no goals

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| + (|n| + 1) * k₂
Tactic:
rw [mul_comm (f₂ n), ←Int.natAbs_neg (f₁ n * f₂ n - n * f₂.comp f₁ n)]
State after:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₁ n * toFun f₂ n| +
      |-(toFun f₁ n * toFun f₂ n - n * toFun (AlmostHom.comp f₂ f₁) n)| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₁ n * toFun f₂ n| + (|n| + 1) * k₂

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₁ n * toFun f₂ n| +
      |-(toFun f₁ n * toFun f₂ n - n * toFun (AlmostHom.comp f₂ f₁) n)| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₁ n * toFun f₂ n| + (|n| + 1) * k₂
Tactic:
apply Nat.add_le_add_left
State after:
case h
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
⊢ |-(toFun f₁ n * toFun f₂ n - n * toFun (AlmostHom.comp f₂ f₁) n)| ≤ (|n| + 1) * k₂

State before:
case h
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
⊢ |-(toFun f₁ n * toFun f₂ n - n * toFun (AlmostHom.comp f₂ f₁) n)| ≤ (|n| + 1) * k₂
Tactic:
simp only [neg_sub, Int.diff_eq]
State after:
case h
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
⊢ |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂

State before:
case h
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
⊢ |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
Tactic:
exact hf₂ ..
State after:
no goals

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
⊢ (|n| + 1) * k₁ + (|n| + 1) * k₂ = (|n| + 1) * (k₁ + k₂)
Tactic:
ring
State after:
no goals

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
⊢ (|n| + 1) * (k₁ + k₂) ≤ |n| * (2 * (k₁ + k₂))
Tactic:
rw [←mul_assoc, mul_comm |n|]
State after:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
⊢ (|n| + 1) * (k₁ + k₂) ≤ 2 * |n| * (k₁ + k₂)

State before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
succ_le_two_mul : ∀ (a : ℕ), a ≠ 0 → a + 1 ≤ 2 * a
k₁ : ℕ
hf₁ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k₁
k₂ : ℕ
hf₂ : ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
n : ℤ
triag :
  |n * toFun (AlmostHom.comp f₁ f₂) n - n * toFun (AlmostHom.comp f₂ f₁) n| ≤
    |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| +
      |toFun f₂ n * toFun f₁ n - n * toFun (AlmostHom.comp f₂ f₁) n|
c : ¬n = 0
⊢ (|n| + 1) * (k₁ + k₂) ≤ 2 * |n| * (k₁ + k₂)
Tactic:
exact Nat.mul_le_mul_of_nonneg_right <|
      succ_le_two_mul |n| <|
      Int.natAbs_ne_zero.2 c
State after:
no goals