internlm/Lean-Github huggingface dataset:
Theorem: AlmostHom.comp_almost_comm
Proof 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]
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
⊢ |n * toFun (AlmostHom.comp f₂ f₁) n - toFun f₁ n * toFun f₂ n| ≤ (|n| + 1) * k₂
Theorem: AlmostHom.comp_almost_comm
Proof 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₂ ..
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| + 1) * k₁ + (|n| + 1) * k₂ = (|n| + 1) * (k₁ + k₂)
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 ℤ
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|]
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| + 1) * (k₁ + k₂) ≤ 2 * |n| * (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
⊢ (|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
Proof state after:
no goals
Theorem: EudoxusReal.mul_comm
Proof state before:
G : Type ?u.57147
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ AlmostHom.comp f₁ f₂ ≈ AlmostHom.comp f₂ f₁
Tactic:
show (QuotientAddGroup.leftRel ..).r ..
Proof state after:
G : Type ?u.57147
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ Setoid.r (AlmostHom.comp f₁ f₂) (AlmostHom.comp f₂ f₁)
Theorem: EudoxusReal.mul_comm
Proof state before:
G : Type ?u.57147
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ Setoid.r (AlmostHom.comp f₁ f₂) (AlmostHom.comp f₂ f₁)
Tactic:
rewrite [QuotientAddGroup.leftRel_apply]
Proof state after:
G : Type ?u.57147
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ -AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁ ∈ boundedAlmostHoms ℤ
Theorem: EudoxusReal.mul_comm
Proof state before:
G : Type ?u.57147
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ -AlmostHom.comp f₁ f₂ + AlmostHom.comp f₂ f₁ ∈ boundedAlmostHoms ℤ
Tactic:
exact AlmostHom.comp_almost_comm f₁ f₂
Proof state after:
no goals
Theorem: int_wf_of_lower_bound
Proof state before:
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
⊢ (fun x y => ↑x < ↑y) = Measure fun x => Int.natAbs (↑x - a)
Tactic:
ext x y
Proof state after:
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ Measure (fun x => Int.natAbs (↑x - a)) x y
Theorem: int_wf_of_lower_bound
Proof state before:
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ Measure (fun x => Int.natAbs (↑x - a)) x y
Tactic:
unfold Measure InvImage
Proof state after:
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ (fun a b => a < b) ((fun x => Int.natAbs (↑x - a)) x) ((fun x => Int.natAbs (↑x - a)) y)
Theorem: int_wf_of_lower_bound
Proof state before:
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ (fun a b => a < b) ((fun x => Int.natAbs (↑x - a)) x) ((fun x => Int.natAbs (↑x - a)) y)
Tactic:
dsimp
Proof state after:
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ Int.natAbs (↑x - a) < Int.natAbs (↑y - a)
Theorem: int_wf_of_lower_bound
Proof state before:
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ Int.natAbs (↑x - a) < Int.natAbs (↑y - a)
Tactic:
rewrite [←Int.ofNat_lt, this, this]
Proof state after:
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ ↑x - a < ↑y - a
Theorem: int_wf_of_lower_bound
Proof state before:
case h.h.a
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y ↔ ↑x - a < ↑y - a
Tactic:
apply Iff.intro
Proof state after:
case h.h.a.mp
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x < ↑y → ↑x - a < ↑y - a

case h.h.a.mpr
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
x y : ↑s
⊢ ↑x - a < ↑y - a → ↑x < ↑y
Theorem: int_wf_of_lower_bound
Proof state before:
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this✝ : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
this : (fun x y => ↑x < ↑y) = Measure fun x => Int.natAbs (↑x - a)
⊢ Set.IsWf s
Tactic:
unfold Set.IsWf Set.WellFoundedOn
Proof state after:
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this✝ : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
this : (fun x y => ↑x < ↑y) = Measure fun x => Int.natAbs (↑x - a)
⊢ WellFounded fun a b => (fun x x_1 => x < x_1) ↑a ↑b
Theorem: int_wf_of_lower_bound
Proof state before:
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this✝ : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
this : (fun x y => ↑x < ↑y) = Measure fun x => Int.natAbs (↑x - a)
⊢ WellFounded fun a b => (fun x x_1 => x < x_1) ↑a ↑b
Tactic:
rewrite [this]
Proof state after:
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this✝ : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
this : (fun x y => ↑x < ↑y) = Measure fun x => Int.natAbs (↑x - a)
⊢ WellFounded (Measure fun x => Int.natAbs (↑x - a))
Theorem: int_wf_of_lower_bound
Proof state before:
s : Set ℤ
a : ℤ
h : a ∈ lowerBounds s
this✝ : ∀ (x : ↑s), ↑(Int.natAbs (↑x - a)) = ↑x - a
this : (fun x y => ↑x < ↑y) = Measure fun x => Int.natAbs (↑x - a)
⊢ WellFounded (Measure fun x => Int.natAbs (↑x - a))
Tactic:
apply IsWellFounded.wf
Proof state after:
no goals
Theorem: Int.subNatNat_le_sub
Proof state before:
a b : ℕ
⊢ subNatNat a b ≤ ↑(a - b)
Tactic:
unfold subNatNat
Proof state after:
a b : ℕ
⊢ (match b - a with
    | 0 => ofNat (a - b)
    | Nat.succ k => -[k+1]) ≤
    ↑(a - b)
Theorem: Int.subNatNat_le_sub
Proof state before:
a b : ℕ
⊢ (match b - a with
    | 0 => ofNat (a - b)
    | Nat.succ k => -[k+1]) ≤
    ↑(a - b)
Tactic:
split
Proof state after:
case h_1
a b x✝ : ℕ
heq✝ : b - a = 0
⊢ ofNat (a - b) ≤ ↑(a - b)

case h_2
a b x✝ m✝ : ℕ
heq✝ : b - a = Nat.succ m✝
⊢ -[m✝+1] ≤ ↑(a - b)
Theorem: Int.add_sub_cancel_right
Proof state before:
a✝ b✝ : ℕ
a b c : ℤ
⊢ a + (b - a) = b
Tactic:
rewrite [Int.add_comm]
Proof state after:
a✝ b✝ : ℕ
a b c : ℤ
⊢ b - a + a = b
Theorem: Int.add_sub_cancel_right
Proof state before:
a✝ b✝ : ℕ
a b c : ℤ
⊢ b - a + a = b
Tactic:
apply Int.sub_add_cancel
Proof state after:
no goals
Theorem: Int.natAbs_eq'
Proof state before:
a b c d : ℤ
⊢ ↑(|a|) = a ∨ ↑(|a|) = -a
Tactic:
conv => lhs; rewrite [eq_comm]
Proof state after:
a b c d : ℤ
⊢ a = ↑(|a|) ∨ ↑(|a|) = -a
Theorem: Int.natAbs_eq'
Proof state before:
a b c d : ℤ
⊢ a = ↑(|a|) ∨ ↑(|a|) = -a
Tactic:
conv => rhs; rewrite [eq_comm, Int.neg_eq_comm, eq_comm]
Proof state after:
a b c d : ℤ
⊢ a = ↑(|a|) ∨ a = -↑(|a|)
Theorem: Int.natAbs_eq'
Proof state before:
a b c d : ℤ
⊢ a = ↑(|a|) ∨ a = -↑(|a|)
Tactic:
exact natAbs_eq a
Proof state after:
no goals
Theorem: Int.sub_le_natAbs_sub
Proof state before:
a b c d : ℤ
⊢ ↑(|a|) - ↑(|b|) ≤ ↑(|a - b|)
Tactic:
repeat rw [Int.coe_natAbs]
Proof state after:
a b c d : ℤ
⊢ abs a - abs b ≤ abs (a - b)
Theorem: Int.sub_le_natAbs_sub
Proof state before:
a b c d : ℤ
⊢ abs a - abs b ≤ abs (a - b)
Tactic:
exact abs_sub_abs_le_abs_sub a b
Proof state after:
no goals
Theorem: Int.sub_le_natAbs_sub
Proof state before:
a b c d : ℤ
⊢ abs a - abs b ≤ ↑(|a - b|)
Tactic:
rw [Int.coe_natAbs]
Proof state after:
a b c d : ℤ
⊢ abs a - abs b ≤ abs (a - b)
Theorem: Int.neg_natAbs_le
Proof state before:
a b c d : ℤ
⊢ -↑(|a|) ≤ a
Tactic:
conv => rhs; rewrite [←a.neg_neg]
Proof state after:
a b c d : ℤ
⊢ -↑(|a|) ≤ - -a
Theorem: Int.neg_natAbs_le
Proof state before:
a b c d : ℤ
⊢ -↑(|a|) ≤ - -a
Tactic:
exact Int.neg_le_neg a.neg_le_natAbs
Proof state after:
no goals
Theorem: Int.natAbs_le'
Proof state before:
a✝ b✝ c d a b : ℤ
h₁ : a ≤ b
h₂ : -a ≤ b
⊢ ↑(|a|) ≤ b
Tactic:
apply Int.natAbs_eq' a |>.elim <;> (intro h; rwa [h])
Proof state after:
no goals
Theorem: Int.natAbs_le'
Proof state before:
case right
a✝ b✝ c d a b : ℤ
h₁ : a ≤ b
h₂ : -a ≤ b
⊢ ↑(|a|) = -a → ↑(|a|) ≤ b
Tactic:
intro h
Proof state after:
case right
a✝ b✝ c d a b : ℤ
h₁ : a ≤ b
h₂ : -a ≤ b
h : ↑(|a|) = -a
⊢ ↑(|a|) ≤ b
Theorem: Int.natAbs_le'
Proof state before:
case right
a✝ b✝ c d a b : ℤ
h₁ : a ≤ b
h₂ : -a ≤ b
h : ↑(|a|) = -a
⊢ ↑(|a|) ≤ b
Tactic:
rwa [h]
Proof state after:
no goals
Theorem: Int.natAbs_le
Proof state before:
a✝ b✝ c d a : ℤ
b : ℕ
⊢ a ≤ ↑b → -a ≤ ↑b → |a| ≤ b
Tactic:
exact_mod_cast @natAbs_le' a b
Proof state after:
no goals
Theorem: Int.natAbs_le_iff
Proof state before:
a b✝ c d : ℤ
b : ℕ
⊢ |a| ≤ b ↔ a ≤ ↑b ∧ -a ≤ ↑b
Tactic:
exact_mod_cast natAbs_le_iff' a b
Proof state after:
no goals
Theorem: Int.diff_self_eq_zero
Proof state before:
a b c d : ℤ
⊢ diff a a = 0
Tactic:
unfold diff natAbs
Proof state after:
a b c d : ℤ
⊢ (match a - a with
    | ofNat m => m
    | -[m+1] => Nat.succ m) =
    0
Theorem: Int.diff_self_eq_zero
Proof state before:
a b c d : ℤ
⊢ (match a - a with
    | ofNat m => m
    | -[m+1] => Nat.succ m) =
    0
Tactic:
rw [Int.sub_self a]
Proof state after:
no goals
Theorem: Int.diff_comm
Proof state before:
a b c d : ℤ
⊢ diff a b = diff b a
Tactic:
unfold diff
Proof state after:
a b c d : ℤ
⊢ |a - b| = |b - a|
Theorem: Int.diff_comm
Proof state before:
a b c d : ℤ
⊢ |a - b| = |b - a|
Tactic:
rw [←Int.natAbs_neg, Int.neg_sub]
Proof state after:
no goals
Theorem: Int.triangle_ineq
Proof state before:
a b c d : ℤ
⊢ diff a c ≤ diff a b + diff b c
Tactic:
unfold diff
Proof state after:
a b c d : ℤ
⊢ |a - c| ≤ |a - b| + |b - c|
Theorem: Int.triangle_ineq
Proof state before:
a b c d : ℤ
⊢ |a - c| ≤ |a - b| + |b - c|
Tactic:
rewrite [show a - c = (a - b) + (b - c)
         by rw [←Int.add_sub_assoc, Int.sub_add_cancel]]
Proof state after:
a b c d : ℤ
⊢ |a - b + (b - c)| ≤ |a - b| + |b - c|
Theorem: Int.triangle_ineq
Proof state before:
a b c d : ℤ
⊢ |a - b + (b - c)| ≤ |a - b| + |b - c|
Tactic:
apply Int.natAbs_add_le
Proof state after:
no goals
Theorem: Int.triangle_ineq
Proof state before:
a b c d : ℤ
⊢ a - c = a - b + (b - c)
Tactic:
rw [←Int.add_sub_assoc, Int.sub_add_cancel]
Proof state after:
no goals
Theorem: AlmostAdditive.almost_zero
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f 0| = |f (0 + 0) - f 0 - f 0|
Tactic:
rw [←Int.natAbs_neg, add_zero,
    sub_self, zero_sub]
Proof state after:
no goals
Theorem: AlmostAdditive.almost_neg
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (-g) - -f g| ≤ |f (-g) + f g - f 0| + |f 0|
Tactic:
lax_exact Int.natAbs_add_le (f (-g) + f g - f 0) (f 0)
Proof state after:
case e_a.e_m
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ f (-g) - -f g = f (-g) + f g - f 0 + f 0
Theorem: AlmostAdditive.almost_neg
Proof state before:
case e_a.e_m
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ f (-g) - -f g = f (-g) + f g - f 0 + f 0
Tactic:
linarith
Proof state after:
no goals
Theorem: AlmostAdditive.almost_neg
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (-g) + f g - f 0| + |f 0| = |f (-g + g) - f (-g) - f g| + |f 0|
Tactic:
congr 1
Proof state after:
case e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (-g) + f g - f 0| = |f (-g + g) - f (-g) - f g|
Theorem: AlmostAdditive.almost_neg
Proof state before:
case e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (-g) + f g - f 0| = |f (-g + g) - f (-g) - f g|
Tactic:
rewrite [←Int.natAbs_neg, ←add_left_neg g]
Proof state after:
case e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |-(f (-g) + f g - f (-g + g))| = |f (-g + g) - f (-g) - f g|
Theorem: AlmostAdditive.almost_neg
Proof state before:
case e_a
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |-(f (-g) + f g - f (-g + g))| = |f (-g + g) - f (-g) - f g|
Tactic:
congr
Proof state after:
case e_a.e_m
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ -(f (-g) + f g - f (-g + g)) = f (-g + g) - f (-g) - f g
Theorem: AlmostAdditive.almost_neg
Proof state before:
case e_a.e_m
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ -(f (-g) + f g - f (-g + g)) = f (-g + g) - f (-g) - f g
Tactic:
linarith
Proof state after:
no goals
Theorem: AlmostAdditive.almost_neg
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (-g + g) - f (-g) - f g| + |f 0| ≤ bound * 2
Tactic:
linarith [h.almost_additive (-g) g, h.almost_zero]
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
m n : ℤ
g : G
⊢ |f (m • g) - m * f g| ≤ bound * (|m| + 1)
Tactic:
cases m <;> (rename_i m; induction m)
Proof state after:
case ofNat.zero
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (Int.ofNat Nat.zero • g) - Int.ofNat Nat.zero * f g| ≤ bound * (|Int.ofNat Nat.zero| + 1)

case ofNat.succ
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
n✝ : ℕ
n_ih✝ : |f (Int.ofNat n✝ • g) - Int.ofNat n✝ * f g| ≤ bound * (|Int.ofNat n✝| + 1)
⊢ |f (Int.ofNat (Nat.succ n✝) • g) - Int.ofNat (Nat.succ n✝) * f g| ≤ bound * (|Int.ofNat (Nat.succ n✝)| + 1)

case negSucc.zero
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (Int.negSucc Nat.zero • g) - Int.negSucc Nat.zero * f g| ≤ bound * (|Int.negSucc Nat.zero| + 1)

case negSucc.succ
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
n✝ : ℕ
n_ih✝ : |f (Int.negSucc n✝ • g) - Int.negSucc n✝ * f g| ≤ bound * (|Int.negSucc n✝| + 1)
⊢ |f (Int.negSucc (Nat.succ n✝) • g) - Int.negSucc (Nat.succ n✝) * f g| ≤ bound * (|Int.negSucc (Nat.succ n✝)| + 1)
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (Int.ofNat Nat.zero • g) - Int.ofNat Nat.zero * f g| ≤ bound * (|Int.ofNat Nat.zero| + 1)
Tactic:
case ofNat.zero => simp; exact h.almost_zero
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.ofNat m • g) - Int.ofNat m * f g| ≤ bound * (|Int.ofNat m| + 1)
⊢ |f (Int.ofNat (Nat.succ m) • g) - Int.ofNat (Nat.succ m) * f g| ≤ bound * (|Int.ofNat (Nat.succ m)| + 1)
Tactic:
case ofNat.succ m hᵢ =>
  rewrite [Int.ofNat_eq_coe, ofNat_zsmul] at hᵢ ⊢
  
  rewrite [show m.succ • g = g + m • g from AddMonoid.nsmul_succ ..,
           show ↑(m.succ) * f g = f g + m * f g
             by rewrite [Nat.succ_eq_add_one, Nat.cast_succ]; linarith]
  calc |f (g + m • g) - (f g + m * f g)|
      = |(f (g + m • g) - f g - f (m • g)) + (f (m • g) - m * f g)|
          := congrArg Int.natAbs <| by linarith
    _ ≤ |f (g + m • g) - f g - f (m • g)| + |f (m • g) - m * f g|
          := Int.natAbs_add_le ..
    _ ≤ bound + bound * (m + 1)
          := Nat.add_le_add (h.almost_additive ..) hᵢ
    _ = bound * (m.succ + 1)
          := by linarith
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (Int.negSucc Nat.zero • g) - Int.negSucc Nat.zero * f g| ≤ bound * (|Int.negSucc Nat.zero| + 1)
Tactic:
case negSucc.zero =>
  rewrite [show Int.negSucc Nat.zero = -1 by rfl]; simpa using h.almost_neg g
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
⊢ |f (Int.negSucc (Nat.succ m) • g) - Int.negSucc (Nat.succ m) * f g| ≤ bound * (|Int.negSucc (Nat.succ m)| + 1)
Tactic:
case negSucc.succ m hᵢ =>
  conv => lhs; rewrite [←Int.negSucc_sub_one]
  rewrite [sub_zsmul, one_zsmul, sub_mul, one_mul]
  calc |f (Int.negSucc m • g + -g) - (Int.negSucc m * f g - f g)|
      = |(-(f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g))
         + (f (Int.negSucc m • g) - Int.negSucc m * f g)|
          := congrArg Int.natAbs <| by linarith
    _ ≤ |f (Int.negSucc m • g) - f (Int.negSucc m • g + -g) - f g|
        + |f (Int.negSucc m • g) - Int.negSucc m * f g|
          := by conv => rhs; arg 1; rewrite [←Int.natAbs_neg]
                apply Int.natAbs_add_le
    _ ≤ bound + bound * (|Int.negSucc m| + 1)
          := Nat.add_le_add (by rewrite [←congrArg f <| neg_add_cancel_right ..]
                                apply h.almost_additive _ g)
                            hᵢ
    _ = bound * (|Int.negSucc m.succ| + 1)
          := by simp only [Int.natAbs_negSucc]; linarith
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul
Proof state before:
case negSucc
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
a✝ : ℕ
⊢ |f (Int.negSucc a✝ • g) - Int.negSucc a✝ * f g| ≤ bound * (|Int.negSucc a✝| + 1)
Tactic:
rename_i m
Proof state after:
case negSucc
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
⊢ |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
Theorem: AlmostAdditive.almost_smul
Proof state before:
case negSucc
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
⊢ |f (Int.negSucc m • g) - Int.negSucc m * f g| ≤ bound * (|Int.negSucc m| + 1)
Tactic:
induction m
Proof state after:
case negSucc.zero
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (Int.negSucc Nat.zero • g) - Int.negSucc Nat.zero * f g| ≤ bound * (|Int.negSucc Nat.zero| + 1)

case negSucc.succ
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
n✝ : ℕ
n_ih✝ : |f (Int.negSucc n✝ • g) - Int.negSucc n✝ * f g| ≤ bound * (|Int.negSucc n✝| + 1)
⊢ |f (Int.negSucc (Nat.succ n✝) • g) - Int.negSucc (Nat.succ n✝) * f g| ≤ bound * (|Int.negSucc (Nat.succ n✝)| + 1)
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f (Int.ofNat Nat.zero • g) - Int.ofNat Nat.zero * f g| ≤ bound * (|Int.ofNat Nat.zero| + 1)
Tactic:
simp
Proof state after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f 0| ≤ bound
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
⊢ |f 0| ≤ bound
Tactic:
exact h.almost_zero
Proof state after:
no goals
Theorem: AlmostAdditive.almost_smul
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (Int.ofNat m • g) - Int.ofNat m * f g| ≤ bound * (|Int.ofNat m| + 1)
⊢ |f (Int.ofNat (Nat.succ m) • g) - Int.ofNat (Nat.succ m) * f g| ≤ bound * (|Int.ofNat (Nat.succ m)| + 1)
Tactic:
rewrite [Int.ofNat_eq_coe, ofNat_zsmul] at hᵢ ⊢
Proof state after:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
n : ℤ
g : G
m : ℕ
hᵢ : |f (m • g) - ↑m * f g| ≤ bound * (|↑m| + 1)
⊢ |f (Nat.succ m • g) - ↑(Nat.succ m) * f g| ≤ bound * (|↑(Nat.succ m)| + 1)