internlm/Lean-Github huggingface dataset:
Theorem: Hw7.one_is_odd
Proof state before:
⊢ MyOdd 1
Tactic:
dsimp [MyOdd]
Proof state after:
⊢ ∃ k, 2 * k + 1 = 1
Theorem: Hw7.one_is_odd
Proof state before:
⊢ ∃ k, 2 * k + 1 = 1
Tactic:
existsi 0
Proof state after:
⊢ 2 * 0 + 1 = 1
Theorem: Hw7.one_is_odd
Proof state before:
⊢ 2 * 0 + 1 = 1
Tactic:
numbers
Proof state after:
no goals
Theorem: Hw7.zero_isnt_odd
Proof state before:
⊢ ¬MyOdd 0
Tactic:
dsimp [MyOdd]
Proof state after:
⊢ ¬∃ k, 2 * k + 1 = 0
Theorem: Hw7.zero_isnt_odd
Proof state before:
⊢ ¬∃ k, 2 * k + 1 = 0
Tactic:
intro h
Proof state after:
h : ∃ k, 2 * k + 1 = 0
⊢ False
Theorem: Hw7.zero_isnt_odd
Proof state before:
h : ∃ k, 2 * k + 1 = 0
⊢ False
Tactic:
eliminate h with x h
Proof state after:
case intro
x : ℕ
h : 2 * x + 1 = 0
⊢ False
Theorem: Hw7.zero_isnt_odd
Proof state before:
case intro
x : ℕ
h : 2 * x + 1 = 0
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Hw7.one_isnt_even
Proof state before:
⊢ ¬MyEven 1
Tactic:
dsimp [MyEven]
Proof state after:
⊢ ¬∃ k, 2 * k = 1
Theorem: Hw7.one_isnt_even
Proof state before:
⊢ ¬∃ k, 2 * k = 1
Tactic:
intro h
Proof state after:
h : ∃ k, 2 * k = 1
⊢ False
Theorem: Hw7.one_isnt_even
Proof state before:
h : ∃ k, 2 * k = 1
⊢ False
Tactic:
eliminate h with x h
Proof state after:
case intro
x : ℕ
h : 2 * x = 1
⊢ False
Theorem: Hw7.one_isnt_even
Proof state before:
case intro
x : ℕ
h : 2 * x = 1
⊢ False
Tactic:
rewrite [@Nat.mul_eq_one_iff] at h
Proof state after:
case intro
x : ℕ
h : 2 = 1 ∧ x = 1
⊢ False
Theorem: Hw7.one_isnt_even
Proof state before:
case intro
x : ℕ
h : 2 = 1 ∧ x = 1
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Hw7.even_after_odd
Proof state before:
n : ℕ
⊢ MyOdd n → MyEven (n + 1)
Tactic:
dsimp [MyEven, MyOdd]
Proof state after:
n : ℕ
⊢ (∃ k, 2 * k + 1 = n) → ∃ k, 2 * k = n + 1
Theorem: Hw7.even_after_odd
Proof state before:
n : ℕ
⊢ (∃ k, 2 * k + 1 = n) → ∃ k, 2 * k = n + 1
Tactic:
intro h
Proof state after:
n : ℕ
h : ∃ k, 2 * k + 1 = n
⊢ ∃ k, 2 * k = n + 1
Theorem: Hw7.even_after_odd
Proof state before:
n : ℕ
h : ∃ k, 2 * k + 1 = n
⊢ ∃ k, 2 * k = n + 1
Tactic:
eliminate h with x h
Proof state after:
case intro
n x : ℕ
h : 2 * x + 1 = n
⊢ ∃ k, 2 * k = n + 1
Theorem: Hw7.even_after_odd
Proof state before:
case intro
n x : ℕ
h : 2 * x + 1 = n
⊢ ∃ k, 2 * k = n + 1
Tactic:
existsi x + 1
Proof state after:
case intro
n x : ℕ
h : 2 * x + 1 = n
⊢ 2 * (x + 1) = n + 1
Theorem: Hw7.even_after_odd
Proof state before:
case intro
n x : ℕ
h : 2 * x + 1 = n
⊢ 2 * (x + 1) = n + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Hw7.odd_after_even
Proof state before:
n : ℕ
⊢ MyEven n → MyOdd (n + 1)
Tactic:
dsimp [MyEven, MyOdd]
Proof state after:
n : ℕ
⊢ (∃ k, 2 * k = n) → ∃ k, 2 * k + 1 = n + 1
Theorem: Hw7.odd_after_even
Proof state before:
n : ℕ
⊢ (∃ k, 2 * k = n) → ∃ k, 2 * k + 1 = n + 1
Tactic:
intro h
Proof state after:
n : ℕ
h : ∃ k, 2 * k = n
⊢ ∃ k, 2 * k + 1 = n + 1
Theorem: Hw7.odd_after_even
Proof state before:
n : ℕ
h : ∃ k, 2 * k = n
⊢ ∃ k, 2 * k + 1 = n + 1
Tactic:
eliminate h with x h
Proof state after:
case intro
n x : ℕ
h : 2 * x = n
⊢ ∃ k, 2 * k + 1 = n + 1
Theorem: Hw7.odd_after_even
Proof state before:
case intro
n x : ℕ
h : 2 * x = n
⊢ ∃ k, 2 * k + 1 = n + 1
Tactic:
existsi x
Proof state after:
case intro
n x : ℕ
h : 2 * x = n
⊢ 2 * x + 1 = n + 1
Theorem: Hw7.odd_after_even
Proof state before:
case intro
n x : ℕ
h : 2 * x = n
⊢ 2 * x + 1 = n + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Hw7.even_before_odd
Proof state before:
⊢ ∀ (n : ℕ), MyOdd (n + 1) → MyEven n
Tactic:
intro n
Proof state after:
n : ℕ
⊢ MyOdd (n + 1) → MyEven n
Theorem: Hw7.even_before_odd
Proof state before:
n : ℕ
⊢ MyOdd (n + 1) → MyEven n
Tactic:
dsimp [MyEven, MyOdd]
Proof state after:
n : ℕ
⊢ (∃ k, 2 * k + 1 = n + 1) → ∃ k, 2 * k = n
Theorem: Hw7.even_before_odd
Proof state before:
n : ℕ
⊢ (∃ k, 2 * k + 1 = n + 1) → ∃ k, 2 * k = n
Tactic:
intro h
Proof state after:
n : ℕ
h : ∃ k, 2 * k + 1 = n + 1
⊢ ∃ k, 2 * k = n
Theorem: Hw7.even_before_odd
Proof state before:
n : ℕ
h : ∃ k, 2 * k + 1 = n + 1
⊢ ∃ k, 2 * k = n
Tactic:
eliminate h with x hx
Proof state after:
case intro
n x : ℕ
hx : 2 * x + 1 = n + 1
⊢ ∃ k, 2 * k = n
Theorem: Hw7.even_before_odd
Proof state before:
case intro
n x : ℕ
hx : 2 * x + 1 = n + 1
⊢ ∃ k, 2 * k = n
Tactic:
existsi x
Proof state after:
case intro
n x : ℕ
hx : 2 * x + 1 = n + 1
⊢ 2 * x = n
Theorem: Hw7.even_before_odd
Proof state before:
case intro
n x : ℕ
hx : 2 * x + 1 = n + 1
⊢ 2 * x = n
Tactic:
linarith
Proof state after:
no goals
Theorem: Hw7.odd_before_even
Proof state before:
⊢ ∀ (n : ℕ), MyEven (n + 1) → MyOdd n
Tactic:
intro n
Proof state after:
n : ℕ
⊢ MyEven (n + 1) → MyOdd n
Theorem: Hw7.odd_before_even
Proof state before:
n : ℕ
⊢ MyEven (n + 1) → MyOdd n
Tactic:
dsimp [MyEven, MyOdd]
Proof state after:
n : ℕ
⊢ (∃ k, 2 * k = n + 1) → ∃ k, 2 * k + 1 = n
Theorem: Hw7.odd_before_even
Proof state before:
n : ℕ
⊢ (∃ k, 2 * k = n + 1) → ∃ k, 2 * k + 1 = n
Tactic:
intro h
Proof state after:
n : ℕ
h : ∃ k, 2 * k = n + 1
⊢ ∃ k, 2 * k + 1 = n
Theorem: Hw7.odd_before_even
Proof state before:
n : ℕ
h : ∃ k, 2 * k = n + 1
⊢ ∃ k, 2 * k + 1 = n
Tactic:
eliminate h with x hx
Proof state after:
case intro
n x : ℕ
hx : 2 * x = n + 1
⊢ ∃ k, 2 * k + 1 = n
Theorem: Hw7.odd_before_even
Proof state before:
case intro
n x : ℕ
hx : 2 * x = n + 1
⊢ ∃ k, 2 * k + 1 = n
Tactic:
cases x with
| zero => {apply False.elim; simp at hx; linarith}
| succ x => {existsi x; linarith}
Proof state after:
no goals
Theorem: Hw7.odd_before_even
Proof state before:
case intro.zero
n : ℕ
hx : 2 * Nat.zero = n + 1
⊢ ∃ k, 2 * k + 1 = n
Tactic:
apply False.elim
Proof state after:
case intro.zero.h
n : ℕ
hx : 2 * Nat.zero = n + 1
⊢ False
Theorem: Hw7.odd_before_even
Proof state before:
case intro.zero.h
n : ℕ
hx : 2 * Nat.zero = n + 1
⊢ False
Tactic:
simp at hx
Proof state after:
case intro.zero.h
n : ℕ
hx : 0 = n + 1
⊢ False
Theorem: Hw7.odd_before_even
Proof state before:
case intro.zero.h
n : ℕ
hx : 0 = n + 1
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Hw7.odd_before_even
Proof state before:
case intro.succ
n x : ℕ
hx : 2 * Nat.succ x = n + 1
⊢ ∃ k, 2 * k + 1 = n
Tactic:
existsi x
Proof state after:
case intro.succ
n x : ℕ
hx : 2 * Nat.succ x = n + 1
⊢ 2 * x + 1 = n
Theorem: Hw7.odd_before_even
Proof state before:
case intro.succ
n x : ℕ
hx : 2 * Nat.succ x = n + 1
⊢ 2 * x + 1 = n
Tactic:
linarith
Proof state after:
no goals
Theorem: Hw7.even_or_odd
Proof state before:
⊢ ∀ (n : ℕ), MyEven n ∨ MyOdd n
Tactic:
sorry
Proof state after:
no goals
Theorem: Hw7.not_both
Proof state before:
⊢ ∀ (n : ℕ), ¬(MyEven n ∧ MyOdd n)
Tactic:
sorry
Proof state after:
no goals
Theorem: AlmostAdditive.comp
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ (x + y)) - f₁ (f₂ x) - f₁ (f₂ y)| ≤
    |f₁ (f₂ (x + y)) - f₁ (f₂ (x + y) - f₂ x - f₂ y) - f₁ (f₂ x + f₂ y)| + |f₁ (f₂ (x + y) - f₂ x - f₂ y)| +
      |f₁ (f₂ x + f₂ y) - f₁ (f₂ x) - f₁ (f₂ y)|
Tactic:
lax_exact Int.natAbs_add_le₃ (f₁ (f₂ (x + y)) - f₁ (f₂ (x + y) - f₂ x - f₂ y) - f₁ (f₂ x + f₂ y))
                             (f₁ (f₂ (x + y) - f₂ x - f₂ y))
                             (f₁ (f₂ x + f₂ y) - f₁ (f₂ x) - f₁ (f₂ y))
Proof state after:
case e_a.e_m
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ f₁ (f₂ (x + y)) - f₁ (f₂ x) - f₁ (f₂ y) =
    f₁ (f₂ (x + y)) - f₁ (f₂ (x + y) - f₂ x - f₂ y) - f₁ (f₂ x + f₂ y) + f₁ (f₂ (x + y) - f₂ x - f₂ y) +
      (f₁ (f₂ x + f₂ y) - f₁ (f₂ x) - f₁ (f₂ y))
Theorem: AlmostAdditive.comp
Proof state before:
case e_a.e_m
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ f₁ (f₂ (x + y)) - f₁ (f₂ x) - f₁ (f₂ y) =
    f₁ (f₂ (x + y)) - f₁ (f₂ (x + y) - f₂ x - f₂ y) - f₁ (f₂ x + f₂ y) + f₁ (f₂ (x + y) - f₂ x - f₂ y) +
      (f₁ (f₂ x + f₂ y) - f₁ (f₂ x) - f₁ (f₂ y))
Tactic:
linarith
Proof state after:
no goals
Theorem: AlmostAdditive.comp
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ (x + y)) - f₁ (f₂ (x + y) - f₂ x - f₂ y) - f₁ (f₂ x + f₂ y)| + |f₁ (f₂ (x + y) - f₂ x - f₂ y)| +
      |f₁ (f₂ x + f₂ y) - f₁ (f₂ x) - f₁ (f₂ y)| ≤
    bound₁ + ((bound₁ + |f₁ 1|) * |f₂ (x + y) - f₂ x - f₂ y| + bound₁) + bound₁
Tactic:
conv in f₁ (f₂ (x + y)) =>
  
  rw [show f₂ (x + y) = (f₂ (x + y) - f₂ x - f₂ y) + (f₂ x + f₂ y)
      by linarith]
Proof state after:
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ (x + y) - f₂ x - f₂ y + (f₂ x + f₂ y)) - f₁ (f₂ (x + y) - f₂ x - f₂ y) - f₁ (f₂ x + f₂ y)| +
        |f₁ (f₂ (x + y) - f₂ x - f₂ y)| +
      |f₁ (f₂ x + f₂ y) - f₁ (f₂ x) - f₁ (f₂ y)| ≤
    bound₁ + ((bound₁ + |f₁ 1|) * |f₂ (x + y) - f₂ x - f₂ y| + bound₁) + bound₁
Theorem: AlmostAdditive.comp
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ (x + y) - f₂ x - f₂ y + (f₂ x + f₂ y)) - f₁ (f₂ (x + y) - f₂ x - f₂ y) - f₁ (f₂ x + f₂ y)| +
        |f₁ (f₂ (x + y) - f₂ x - f₂ y)| +
      |f₁ (f₂ x + f₂ y) - f₁ (f₂ x) - f₁ (f₂ y)| ≤
    bound₁ + ((bound₁ + |f₁ 1|) * |f₂ (x + y) - f₂ x - f₂ y| + bound₁) + bound₁
Tactic:
refine Nat.add_le_add₃ ?_ ?using_lemma ?_
Proof state after:
case refine_1
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ (x + y) - f₂ x - f₂ y + (f₂ x + f₂ y)) - f₁ (f₂ (x + y) - f₂ x - f₂ y) - f₁ (f₂ x + f₂ y)| ≤ bound₁

case using_lemma
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ (x + y) - f₂ x - f₂ y)| ≤ (bound₁ + |f₁ 1|) * |f₂ (x + y) - f₂ x - f₂ y| + bound₁

case refine_2
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ x + f₂ y) - f₁ (f₂ x) - f₁ (f₂ y)| ≤ bound₁
Theorem: AlmostAdditive.comp
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ (x + y) - f₂ x - f₂ y)| ≤ (bound₁ + |f₁ 1|) * |f₂ (x + y) - f₂ x - f₂ y| + bound₁
Tactic:
case using_lemma => apply h₁.linear_growth_upper_bound_int
Proof state after:
no goals
Theorem: AlmostAdditive.comp
Proof state before:
case refine_1
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ (x + y) - f₂ x - f₂ y + (f₂ x + f₂ y)) - f₁ (f₂ (x + y) - f₂ x - f₂ y) - f₁ (f₂ x + f₂ y)| ≤ bound₁

case refine_2
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ x + f₂ y) - f₁ (f₂ x) - f₁ (f₂ y)| ≤ bound₁
Tactic:
all_goals apply h₁.almost_additive
Proof state after:
no goals
Theorem: AlmostAdditive.comp
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ f₂ (x + y) = f₂ (x + y) - f₂ x - f₂ y + (f₂ x + f₂ y)
Tactic:
linarith
Proof state after:
no goals
Theorem: AlmostAdditive.comp
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ (x + y) - f₂ x - f₂ y)| ≤ (bound₁ + |f₁ 1|) * |f₂ (x + y) - f₂ x - f₂ y| + bound₁
Tactic:
apply h₁.linear_growth_upper_bound_int
Proof state after:
no goals
Theorem: AlmostAdditive.comp
Proof state before:
case refine_2
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |f₁ (f₂ x + f₂ y) - f₁ (f₂ x) - f₁ (f₂ y)| ≤ bound₁
Tactic:
apply h₁.almost_additive
Proof state after:
no goals
Theorem: AlmostAdditive.comp
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f₁ : ℤ → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ bound₁ + ((bound₁ + |f₁ 1|) * |f₂ (x + y) - f₂ x - f₂ y| + bound₁) + bound₁ =
    (bound₁ + |f₁ 1|) * |f₂ (x + y) - f₂ x - f₂ y| + bound₁ * 3
Tactic:
linarith
Proof state after:
no goals
Theorem: AlmostAdditive.comp_sub_bounded_of_sub_bounded
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
bound' : ℕ
h' : Bounded (-f₁ + f₂) bound'
g : G
⊢ -f (f₁ g) + f (f₂ g) = f (f₁ g + (f₂ g - f₁ g)) - f (f₁ g) - f (f₂ g - f₁ g) + f (f₂ g - f₁ g)
Tactic:
rw [Int.add_sub_cancel_right (f₁ g) (f₂ g),
    ←Int.sub_eq_neg_add, Int.sub_add_cancel]
Proof state after:
no goals
Theorem: AlmostAdditive.comp_sub_bounded_of_sub_bounded
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
bound' : ℕ
h' : Bounded (-f₁ + f₂) bound'
g : G
⊢ bound + ((bound + |f 1|) * bound' + bound) = (bound + |f 1|) * bound' + bound * 2
Tactic:
rw [Nat.add_comm, Nat.add_assoc, Nat.mul_two]
Proof state after:
no goals
Theorem: AlmostAdditive.almost_comp_add
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
g : G
⊢ |HAdd.hAdd (-f ∘ (f₁ + f₂)) (f ∘ f₁ + f ∘ f₂) g| ≤ bound
Tactic:
show |(-f (f₁ g + f₂ g)) + (f (f₁ g) + f (f₂ g))| ≤ bound
Proof state after:
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
g : G
⊢ |-f (f₁ g + f₂ g) + (f (f₁ g) + f (f₂ g))| ≤ bound
Theorem: AlmostAdditive.almost_comp_add
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
g : G
⊢ |-f (f₁ g + f₂ g) + (f (f₁ g) + f (f₂ g))| ≤ bound
Tactic:
rewrite [←Int.natAbs_neg]
Proof state after:
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
g : G
⊢ |-(-f (f₁ g + f₂ g) + (f (f₁ g) + f (f₂ g)))| ≤ bound
Theorem: AlmostAdditive.almost_comp_add
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
g : G
⊢ |-(-f (f₁ g + f₂ g) + (f (f₁ g) + f (f₂ g)))| ≤ bound
Tactic:
lax_exact h.almost_additive (f₁ g) (f₂ g)
Proof state after:
case e_a.e_m
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
g : G
⊢ -(-f (f₁ g + f₂ g) + (f (f₁ g) + f (f₂ g))) = f (f₁ g + f₂ g) - f (f₁ g) - f (f₂ g)
Theorem: AlmostAdditive.almost_comp_add
Proof state before:
case e_a.e_m
G : Type u_1
inst✝ : AddCommGroup G
f : ℤ → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ f₂ : G → ℤ
g : G
⊢ -(-f (f₁ g + f₂ g) + (f (f₁ g) + f (f₂ g))) = f (f₁ g + f₂ g) - f (f₁ g) - f (f₂ g)
Tactic:
linarith
Proof state after:
no goals
Theorem: AlmostHom.add_comp
Proof state before:
G : Type u_1
inst✝ : AddCommGroup G
g : AlmostHom G
f₁ f₂ : AlmostHom ℤ
⊢ AlmostHom.comp (f₁ + f₂) g = AlmostHom.comp f₁ g + AlmostHom.comp f₂ g
Tactic:
ext
Proof state after:
case a.h
G : Type u_1
inst✝ : AddCommGroup G
g : AlmostHom G
f₁ f₂ : AlmostHom ℤ
x✝ : G
⊢ toFun (AlmostHom.comp (f₁ + f₂) g) x✝ = toFun (AlmostHom.comp f₁ g + AlmostHom.comp f₂ g) x✝
Theorem: AlmostHom.add_comp
Proof state before:
case a.h
G : Type u_1
inst✝ : AddCommGroup G
g : AlmostHom G
f₁ f₂ : AlmostHom ℤ
x✝ : G
⊢ toFun (AlmostHom.comp (f₁ + f₂) g) x✝ = toFun (AlmostHom.comp f₁ g + AlmostHom.comp f₂ g) x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: AlmostHom.comp_almost_mul
Proof state before:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
⊢ ∃ k, ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k
Tactic:
let ⟨a', b', hlin⟩ := linear_growth_upper_bound_int f₂
Proof state after:
G : Type ?u.41105
inst✝ : AddCommGroup G
f₁ f₂ : AlmostHom ℤ
a' b' : ℕ
hlin : ∀ (n : ℤ), |toFun f₂ n| ≤ a' * |n| + b'
⊢ ∃ k, ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k
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'
⊢ ∃ k, ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k
Tactic:
let ⟨b₁, hf₁⟩ := f₁.almostAdditive
Proof state after:
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₁
⊢ ∃ k, ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k
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₁
⊢ ∃ k, ∀ (n : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * k
Tactic:
exact ⟨_, by
  intro n
  have hypcomm := AlmostAdditive.almost_smul_interchange (hf₁) (f₂ n) n 1
  specialize hlin n
  simp only [smul_eq_mul, mul_one] at hypcomm
  calc |n * (f₁.comp f₂ n) - f₂ n * f₁ n|
      ≤ b₁*(|f₂ n| + |n| + 2) := hypcomm
    _ ≤ b₁*(a'*|n| + b' + |n| + 2) :=
        by apply mul_le_mul_of_nonneg_left
            (by simp only [add_le_add_iff_right, hlin]) (zero_le _)
    _ = b₁*(|n| * (a' + 1) + (b'+ 2)) := by ring
    _ ≤ b₁*(|n| * (a' + 1) + (b'+ 2)) + b₁*(a'+1) :=
        by simp only [le_add_iff_nonneg_right, zero_le]
    _ ≤ b₁*(|n| * (a' + 1) + (b'+ 2)) + b₁*(a'+1) + b₁*(|n|)*(b'+2) :=
        by simp only [le_add_iff_nonneg_right, zero_le]
    _ = (|n|+1)*(b₁*(a'+1 + b'+2)) := by ring⟩
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 : ℤ), |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850
Tactic:
intro n
Proof state after:
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 : ℤ
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850
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 : ℤ
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850
Tactic:
have hypcomm := AlmostAdditive.almost_smul_interchange (hf₁) (f₂ n) n 1
Proof state after:
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 : ℤ
hypcomm : |n * toFun f₁ (toFun f₂ n • 1) - toFun f₂ n * toFun f₁ (n • 1)| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850
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 : ℤ
hypcomm : |n * toFun f₁ (toFun f₂ n • 1) - toFun f₂ n * toFun f₁ (n • 1)| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850
Tactic:
specialize hlin n
Proof state after:
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 : ℤ
hypcomm : |n * toFun f₁ (toFun f₂ n • 1) - toFun f₂ n * toFun f₁ (n • 1)| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
hlin : |toFun f₂ n| ≤ a' * |n| + b'
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850
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 : ℤ
hypcomm : |n * toFun f₁ (toFun f₂ n • 1) - toFun f₂ n * toFun f₁ (n • 1)| ≤ b₁ * (|toFun f₂ n| + |n| + 2)
hlin : |toFun f₂ n| ≤ a' * |n| + b'
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850
Tactic:
simp only [smul_eq_mul, mul_one] at hypcomm
Proof state after:
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)
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850
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)
⊢ |n * toFun (AlmostHom.comp f₁ f₂) n - toFun f₂ n * toFun f₁ n| ≤ (|n| + 1) * ?m.41850
Tactic:
calc |n * (f₁.comp f₂ n) - f₂ n * f₁ n|
    ≤ b₁*(|f₂ n| + |n| + 2) := hypcomm
  _ ≤ b₁*(a'*|n| + b' + |n| + 2) :=
      by apply mul_le_mul_of_nonneg_left
          (by simp only [add_le_add_iff_right, hlin]) (zero_le _)
  _ = b₁*(|n| * (a' + 1) + (b'+ 2)) := by ring
  _ ≤ b₁*(|n| * (a' + 1) + (b'+ 2)) + b₁*(a'+1) :=
      by simp only [le_add_iff_nonneg_right, zero_le]
  _ ≤ b₁*(|n| * (a' + 1) + (b'+ 2)) + b₁*(a'+1) + b₁*(|n|)*(b'+2) :=
      by simp only [le_add_iff_nonneg_right, zero_le]
  _ = (|n|+1)*(b₁*(a'+1 + b'+2)) := by ring
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₁ * (|toFun f₂ n| + |n| + 2) ≤ b₁ * (a' * |n| + b' + |n| + 2)
Tactic:
apply mul_le_mul_of_nonneg_left
 (by simp only [add_le_add_iff_right, hlin]) (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)
⊢ |toFun f₂ n| + |n| + 2 ≤ a' * |n| + b' + |n| + 2
Tactic:
simp only [add_le_add_iff_right, hlin]
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₁ * (a' * |n| + b' + |n| + 2) = b₁ * (|n| * (a' + 1) + (b' + 2))
Tactic:
ring
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₁ * (|n| * (a' + 1) + (b' + 2)) + b₁ * (a' + 1)
Tactic:
simp only [le_add_iff_nonneg_right, zero_le]
Proof state after:
no goals