internlm/Lean-Github huggingface dataset:
Theorem: AlmostHom.comp_almost_mul
Proof state before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin✝ : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hlin : |toFun f₂ n| ≤ a' * |n| + b'
hypcomm : |n * toFun f₁ (toFun f₂ n) - toFun f₂ n * toFun f₁ n| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ b₁ * (|n| * (a' + 1) + (b' + 2)) + b₁ * (a' + 1) ≤
    b₁ * (|n| * (a' + 1) + (b' + 2)) + b₁ * (a' + 1) + b₁ * |n| * (b' + 2)
Tactic:
simp only [le_add_iff_nonneg_right, zero_le]
Proof state after:
no goals
Theorem: AlmostHom.comp_almost_mul
Proof state before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin✝ : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
b₁ : ℕ
hf₁ : AlmostAdditive f₁.toFun b₁
n : ℤ
hlin : |toFun f₂ n| ≤ a' * |n| + b'
hypcomm : |n * toFun f₁ (toFun f₂ n) - toFun f₂ n * toFun f₁ n| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ b₁ * (|n| * (a' + 1) + (b' + 2)) + b₁ * (a' + 1) + b₁ * |n| * (b' + 2) = (|n| + 1) * (b₁ * (a' + 1 + b' + 2))
Tactic:
ring
Proof state after:
no goals
Theorem: AlmostHom.comp_almost_comm
Proof 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]
Proof 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₁)
Theorem: AlmostHom.comp_almost_comm
Proof 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]
Proof 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
Theorem: AlmostHom.comp_almost_comm
Proof 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₂
Proof 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
Theorem: AlmostHom.comp_almost_comm
Proof 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₁
Proof 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
Theorem: AlmostHom.comp_almost_comm
Proof 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|⟩
Proof state after:
no goals
Theorem: AlmostHom.comp_almost_comm
Proof state before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a : ℕ
ha : a ≠ 0
⊢ a + 1 ≤ 2 * a
Tactic:
cases a
Proof 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✝
Theorem: AlmostHom.comp_almost_comm
Proof 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
Proof state after:
no goals
Theorem: AlmostHom.comp_almost_comm
Proof 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]
Proof state after:
no goals
Theorem: AlmostHom.comp_almost_comm
Proof state before:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
ha : Nat.zero ≠ 0
⊢ Nat.zero + 1 ≤ 2 * Nat.zero
Tactic:
contradiction
Proof state after:
no goals
Theorem: AlmostHom.comp_almost_comm
Proof 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
Proof state after:
G : Type ?u.46675
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
n✝ : ℕ
ha : Nat.succ n✝ ≠ 0
⊢ n✝ + 1 < 2 * Nat.succ n✝
Theorem: AlmostHom.comp_almost_comm
Proof 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]
Proof state after:
no goals
Theorem: AlmostHom.comp_almost_comm
Proof 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
Proof 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
Theorem: AlmostHom.comp_almost_comm
Proof 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]]
Proof 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₂
⊢ ℕ
Theorem: AlmostHom.comp_almost_comm
Proof 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|
Proof state after:
no goals
Theorem: AlmostHom.comp_almost_comm
Proof 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]
Proof state after:
no goals
Theorem: AlmostHom.comp_almost_comm
Proof 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₂ |-
Proof 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
Theorem: AlmostHom.comp_almost_comm
Proof 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₂))
Proof state after:
no goals
Theorem: AlmostHom.comp_almost_comm
Proof 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
Proof 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₂)
Theorem: AlmostHom.comp_almost_comm
Proof 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|
Proof state after:
no goals
Theorem: AlmostHom.comp_almost_comm
Proof 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]
Proof state after:
no goals
Theorem: AlmostHom.comp_almost_comm
Proof 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)]
Proof 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₂
Theorem: AlmostHom.comp_almost_comm
Proof 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
Proof 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₂