internlm/Lean-Github huggingface dataset:
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case right
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
⊢ ∀ (x y : ℝ), f (x + y) = f x * u y + f y
Tactic:
intro x y
Proof state after:
case right
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
x y : ℝ
⊢ f (x + y) = f x * u y + f y
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case right
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
x y : ℝ
⊢ f (x + y) = f x * u y + f y
Tactic:
rw [hk y]
Proof state after:
case right
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
x y : ℝ
⊢ f (x + y) = f x * (k * y).exp + f y
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case right
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
x y : ℝ
⊢ f (x + y) = f x * (k * y).exp + f y
Tactic:
calc Real.exp (k * (x + y)) - 1
         = Real.exp (k * x + k * y) - 1 := by rw [mul_add]
       _ = Real.exp (k * x) * Real.exp (k * y) - 1 := by rw [Real.exp_add]
       _ = (Real.exp (k * x) - 1) * Real.exp (k * y) +
              (Real.exp (k * y) - 1) := by ring
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
⊢ StrictMono f ∨ StrictAnti f
Tactic:
cases' Classical.em (0 < k) with hkp hkn
Proof state after:
case inl
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkp : 0 < k
⊢ StrictMono f ∨ StrictAnti f

case inr
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
⊢ StrictMono f ∨ StrictAnti f
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case inl
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkp : 0 < k
⊢ StrictMono f ∨ StrictAnti f
Tactic:
left
Proof state after:
case inl.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkp : 0 < k
⊢ StrictMono f
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case inl.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkp : 0 < k
⊢ StrictMono f
Tactic:
intro x y hxy
Proof state after:
case inl.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkp : 0 < k
x y : ℝ
hxy : x < y
⊢ f x < f y
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case inl.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkp : 0 < k
x y : ℝ
hxy : x < y
⊢ f x < f y
Tactic:
have := exp_strict_mono' k x y hkp hxy
Proof state after:
case inl.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkp : 0 < k
x y : ℝ
hxy : x < y
this : (k * x).exp < (k * y).exp
⊢ f x < f y
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case inl.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkp : 0 < k
x y : ℝ
hxy : x < y
this : (k * x).exp < (k * y).exp
⊢ f x < f y
Tactic:
exact sub_lt_sub_right this 1
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case inr
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
⊢ StrictMono f ∨ StrictAnti f
Tactic:
right
Proof state after:
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
⊢ StrictAnti f
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
⊢ StrictAnti f
Tactic:
intro x y hxy
Proof state after:
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
x y : ℝ
hxy : x < y
⊢ f y < f x
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
x y : ℝ
hxy : x < y
⊢ f y < f x
Tactic:
have hkn' : k < 0 := by
  simp only [not_lt] at *
  exact Ne.lt_of_le hknz hkn
Proof state after:
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
x y : ℝ
hxy : x < y
hkn' : k < 0
⊢ f y < f x
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
x y : ℝ
hxy : x < y
hkn' : k < 0
⊢ f y < f x
Tactic:
have := exp_strict_anti' k x y hkn' hxy
Proof state after:
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
x y : ℝ
hxy : x < y
hkn' : k < 0
this : (k * y).exp < (k * x).exp
⊢ f y < f x
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
x y : ℝ
hxy : x < y
hkn' : k < 0
this : (k * y).exp < (k * x).exp
⊢ f y < f x
Tactic:
exact sub_lt_sub_right this 1
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
x y : ℝ
hxy : x < y
⊢ k < 0
Tactic:
simp only [not_lt] at *
Proof state after:
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
x y : ℝ
hxy : x < y
hkn : k ≤ 0
⊢ k < 0
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
x y : ℝ
hxy : x < y
hkn : k ≤ 0
⊢ k < 0
Tactic:
exact Ne.lt_of_le hknz hkn
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
x y : ℝ
⊢ (k * (x + y)).exp - 1 = (k * x + k * y).exp - 1
Tactic:
rw [mul_add]
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
x y : ℝ
⊢ (k * x + k * y).exp - 1 = (k * x).exp * (k * y).exp - 1
Tactic:
rw [Real.exp_add]
Proof state after:
no goals
Theorem: Romania1998P12.romania1998_p12_mpr
Proof state before:
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
x y : ℝ
⊢ (k * x).exp * (k * y).exp - 1 = ((k * x).exp - 1) * (k * y).exp + ((k * y).exp - 1)
Tactic:
ring
Proof state after:
no goals
Theorem: Poland1998P4.a_recurrence
Proof state before:
n : ℕ
hn : 2 ≤ n
⊢ a n = a (n - 1) + a (n / 2)
Tactic:
cases' n with n
Proof state after:
case zero
hn : 2 ≤ 0
⊢ a 0 = a (0 - 1) + a (0 / 2)

case succ
n : ℕ
hn : 2 ≤ n + 1
⊢ a (n + 1) = a (n + 1 - 1) + a ((n + 1) / 2)
Theorem: Poland1998P4.a_recurrence
Proof state before:
case zero
hn : 2 ≤ 0
⊢ a 0 = a (0 - 1) + a (0 / 2)
Tactic:
exact (Nat.not_succ_le_zero _ hn).elim
Proof state after:
no goals
Theorem: Poland1998P4.a_recurrence
Proof state before:
case succ
n : ℕ
hn : 2 ≤ n + 1
⊢ a (n + 1) = a (n + 1 - 1) + a ((n + 1) / 2)
Tactic:
cases' n
Proof state after:
case succ.zero
hn : 2 ≤ 0 + 1
⊢ a (0 + 1) = a (0 + 1 - 1) + a ((0 + 1) / 2)

case succ.succ
n✝ : ℕ
hn : 2 ≤ n✝ + 1 + 1
⊢ a (n✝ + 1 + 1) = a (n✝ + 1 + 1 - 1) + a ((n✝ + 1 + 1) / 2)
Theorem: Poland1998P4.a_recurrence
Proof state before:
case succ.zero
hn : 2 ≤ 0 + 1
⊢ a (0 + 1) = a (0 + 1 - 1) + a ((0 + 1) / 2)
Tactic:
exact (Nat.not_succ_le_self _ hn).elim
Proof state after:
no goals
Theorem: Poland1998P4.a_recurrence
Proof state before:
case succ.succ
n✝ : ℕ
hn : 2 ≤ n✝ + 1 + 1
⊢ a (n✝ + 1 + 1) = a (n✝ + 1 + 1 - 1) + a ((n✝ + 1 + 1) / 2)
Tactic:
simp only [a, Nat.succ_sub_succ_eq_sub, tsub_zero]
Proof state after:
no goals
Theorem: Poland1998P4.lemma1
Proof state before:
n : ℕ
npos : 0 < n
⊢ 2 * (n - 1) + 1 = 2 * n - 1
Tactic:
cases' n with n
Proof state after:
case zero
npos : 0 < 0
⊢ 2 * (0 - 1) + 1 = 2 * 0 - 1

case succ
n : ℕ
npos : 0 < n + 1
⊢ 2 * (n + 1 - 1) + 1 = 2 * (n + 1) - 1
Theorem: Poland1998P4.lemma1
Proof state before:
case zero
npos : 0 < 0
⊢ 2 * (0 - 1) + 1 = 2 * 0 - 1
Tactic:
exact (lt_asymm npos npos).elim
Proof state after:
no goals
Theorem: Poland1998P4.lemma1
Proof state before:
case succ
n : ℕ
npos : 0 < n + 1
⊢ 2 * (n + 1 - 1) + 1 = 2 * (n + 1) - 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Poland1998P4.lemma2
Proof state before:
n : ℕ
⊢ (2 * n + 1) / 2 = n
Tactic:
rw [Nat.mul_add_div (Nat.le.step Nat.le.refl) n 1]
Proof state after:
n : ℕ
⊢ n + 1 / (Nat.succ 0).succ = n
Theorem: Poland1998P4.lemma2
Proof state before:
n : ℕ
⊢ n + 1 / (Nat.succ 0).succ = n
Tactic:
simp only [Nat.reduceSucc, Nat.reduceDiv, add_zero]
Proof state after:
no goals
Theorem: Poland1998P4.zmod_ext
Proof state before:
a b : ZMod 7
hz : a.val = b.val
⊢ a = b
Tactic:
have : ((ZMod.val a) : ZMod 7)  = ((ZMod.val b) : ZMod 7) := congrArg Nat.cast hz
Proof state after:
a b : ZMod 7
hz : a.val = b.val
this : ↑a.val = ↑b.val
⊢ a = b
Theorem: Poland1998P4.zmod_ext
Proof state before:
a b : ZMod 7
hz : a.val = b.val
this : ↑a.val = ↑b.val
⊢ a = b
Tactic:
simp only [ZMod.natCast_val, ZMod.cast_id', id_eq] at this
Proof state after:
a b : ZMod 7
hz : a.val = b.val
this : a = b
⊢ a = b
Theorem: Poland1998P4.zmod_ext
Proof state before:
a b : ZMod 7
hz : a.val = b.val
this : a = b
⊢ a = b
Tactic:
exact this
Proof state after:
no goals
Theorem: Poland1998P4.a'_recurrence
Proof state before:
n : ℕ
hn : 2 ≤ n
⊢ a' n = a' (n - 1) + a' (n / 2)
Tactic:
have : (a' n).val = (a' (n - 1) + a' (n / 2)).val := by
  rw [ZMod.val_add]
  simp_rw [a', a_recurrence n hn]
  rw [ZMod.val]
  simp
Proof state after:
n : ℕ
hn : 2 ≤ n
this : (a' n).val = (a' (n - 1) + a' (n / 2)).val
⊢ a' n = a' (n - 1) + a' (n / 2)
Theorem: Poland1998P4.a'_recurrence
Proof state before:
n : ℕ
hn : 2 ≤ n
this : (a' n).val = (a' (n - 1) + a' (n / 2)).val
⊢ a' n = a' (n - 1) + a' (n / 2)
Tactic:
exact zmod_ext _ _ this
Proof state after:
no goals
Theorem: Poland1998P4.a'_recurrence
Proof state before:
n : ℕ
hn : 2 ≤ n
⊢ (a' n).val = (a' (n - 1) + a' (n / 2)).val
Tactic:
rw [ZMod.val_add]
Proof state after:
n : ℕ
hn : 2 ≤ n
⊢ (a' n).val = ((a' (n - 1)).val + (a' (n / 2)).val) % 7
Theorem: Poland1998P4.a'_recurrence
Proof state before:
n : ℕ
hn : 2 ≤ n
⊢ (a' n).val = ((a' (n - 1)).val + (a' (n / 2)).val) % 7
Tactic:
simp_rw [a', a_recurrence n hn]
Proof state after:
n : ℕ
hn : 2 ≤ n
⊢ ZMod.val ⟨(a (n - 1) + a (n / 2)) % 7, ⋯⟩ = (ZMod.val ⟨a (n - 1) % 7, ⋯⟩ + ZMod.val ⟨a (n / 2) % 7, ⋯⟩) % 7
Theorem: Poland1998P4.a'_recurrence
Proof state before:
n : ℕ
hn : 2 ≤ n
⊢ ZMod.val ⟨(a (n - 1) + a (n / 2)) % 7, ⋯⟩ = (ZMod.val ⟨a (n - 1) % 7, ⋯⟩ + ZMod.val ⟨a (n / 2) % 7, ⋯⟩) % 7
Tactic:
rw [ZMod.val]
Proof state after:
n : ℕ
hn : 2 ≤ n
⊢ (match (motive := (x : ℕ) → ZMod x → ℕ) 7 with
      | 0 => Int.natAbs
      | n.succ => Fin.val)
      ⟨(a (n - 1) + a (n / 2)) % 7, ⋯⟩ =
    ((match (motive := (x : ℕ) → ZMod x → ℕ) 7 with
          | 0 => Int.natAbs
          | n.succ => Fin.val)
          ⟨a (n - 1) % 7, ⋯⟩ +
        (match (motive := (x : ℕ) → ZMod x → ℕ) 7 with
          | 0 => Int.natAbs
          | n.succ => Fin.val)
          ⟨a (n / 2) % 7, ⋯⟩) %
      7
Theorem: Poland1998P4.a'_recurrence
Proof state before:
n : ℕ
hn : 2 ≤ n
⊢ (match (motive := (x : ℕ) → ZMod x → ℕ) 7 with
      | 0 => Int.natAbs
      | n.succ => Fin.val)
      ⟨(a (n - 1) + a (n / 2)) % 7, ⋯⟩ =
    ((match (motive := (x : ℕ) → ZMod x → ℕ) 7 with
          | 0 => Int.natAbs
          | n.succ => Fin.val)
          ⟨a (n - 1) % 7, ⋯⟩ +
        (match (motive := (x : ℕ) → ZMod x → ℕ) 7 with
          | 0 => Int.natAbs
          | n.succ => Fin.val)
          ⟨a (n / 2) % 7, ⋯⟩) %
      7
Tactic:
simp
Proof state after:
no goals
Theorem: Poland1998P4.lemma3
Proof state before:
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
⊢ ∃ i < 7, a' (N0 + i) = 0
Tactic:
have hp : Fact (Nat.Prime 7) := ⟨by norm_num⟩
Proof state after:
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
⊢ ∃ i < 7, a' (N0 + i) = 0
Theorem: Poland1998P4.lemma3
Proof state before:
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
⊢ ∃ i < 7, a' (N0 + i) = 0
Tactic:
let ii := - (a' N0) / k
Proof state after:
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
⊢ ∃ i < 7, a' (N0 + i) = 0
Theorem: Poland1998P4.lemma3
Proof state before:
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
⊢ ∃ i < 7, a' (N0 + i) = 0
Tactic:
use ii.val
Proof state after:
case h
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
⊢ ii.val < 7 ∧ a' (N0 + ii.val) = 0
Theorem: Poland1998P4.lemma3
Proof state before:
case h
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
⊢ ii.val < 7 ∧ a' (N0 + ii.val) = 0
Tactic:
constructor
Proof state after:
case h.left
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
⊢ ii.val < 7

case h.right
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
⊢ a' (N0 + ii.val) = 0
Theorem: Poland1998P4.lemma3
Proof state before:
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
⊢ Nat.Prime 7
Tactic:
norm_num
Proof state after:
no goals
Theorem: Poland1998P4.lemma3
Proof state before:
case h.left
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
⊢ ii.val < 7
Tactic:
exact ZMod.val_lt ii
Proof state after:
no goals
Theorem: Poland1998P4.lemma3
Proof state before:
case h.right
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
⊢ a' (N0 + ii.val) = 0
Tactic:
have := hN ii.val (ZMod.val_lt ii)
Proof state after:
case h.right
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
this : a' (N0 + ii.val) = a' N0 + k * ↑ii.val
⊢ a' (N0 + ii.val) = 0
Theorem: Poland1998P4.lemma3
Proof state before:
case h.right
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
this : a' (N0 + ii.val) = a' N0 + k * ↑ii.val
⊢ a' (N0 + ii.val) = 0
Tactic:
rw [this, ZMod.natCast_val, ZMod.cast_id', id_def, mul_div_cancel₀ _ hk]
Proof state after:
case h.right
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
this : a' (N0 + ii.val) = a' N0 + k * ↑ii.val
⊢ a' N0 + -a' N0 = 0
Theorem: Poland1998P4.lemma3
Proof state before:
case h.right
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
this : a' (N0 + ii.val) = a' N0 + k * ↑ii.val
⊢ a' N0 + -a' N0 = 0
Tactic:
exact add_neg_self (a' N0)
Proof state after:
no goals
Theorem: Poland1998P4.lemma6
Proof state before:
n : ℕ
⊢ (4 * (n - 1) + 1 + 3) / 2 = 2 * (n - 1) + 1 + 1
Tactic:
have : (4 * (n - 1) + 1 + 3) = 2 * (2 * (n - 1) + 1 + 1) := by ring
Proof state after:
n : ℕ
this : 4 * (n - 1) + 1 + 3 = 2 * (2 * (n - 1) + 1 + 1)
⊢ (4 * (n - 1) + 1 + 3) / 2 = 2 * (n - 1) + 1 + 1
Theorem: Poland1998P4.lemma6
Proof state before:
n : ℕ
this : 4 * (n - 1) + 1 + 3 = 2 * (2 * (n - 1) + 1 + 1)
⊢ (4 * (n - 1) + 1 + 3) / 2 = 2 * (n - 1) + 1 + 1
Tactic:
rw [this, Nat.mul_div_right]
Proof state after:
case H
n : ℕ
this : 4 * (n - 1) + 1 + 3 = 2 * (2 * (n - 1) + 1 + 1)
⊢ 0 < 2
Theorem: Poland1998P4.lemma6
Proof state before:
case H
n : ℕ
this : 4 * (n - 1) + 1 + 3 = 2 * (2 * (n - 1) + 1 + 1)
⊢ 0 < 2
Tactic:
exact two_pos
Proof state after:
no goals
Theorem: Poland1998P4.lemma6
Proof state before:
n : ℕ
⊢ 4 * (n - 1) + 1 + 3 = 2 * (2 * (n - 1) + 1 + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: Poland1998P4.lemma6'
Proof state before:
n : ℕ
⊢ (4 * (n - 1) + 1 + 4) / 2 = 2 * (n - 1) + 1 + 1
Tactic:
omega
Proof state after:
no goals
Theorem: Poland1998P4.lemma7
Proof state before:
n : ℕ
⊢ (4 * (n - 1) + 1 + 5) / 2 = 2 * (n - 1) + 1 + 2
Tactic:
have h1 : (4 * (n - 1) + 1 + 5) = 2 * (2 * (n - 1) + 1 + 2) := by ring
Proof state after:
n : ℕ
h1 : 4 * (n - 1) + 1 + 5 = 2 * (2 * (n - 1) + 1 + 2)
⊢ (4 * (n - 1) + 1 + 5) / 2 = 2 * (n - 1) + 1 + 2
Theorem: Poland1998P4.lemma7
Proof state before:
n : ℕ
h1 : (4 * (n - 1) + 1 + 5) / 2 = 2 * (2 * (n - 1) + 1 + 2) / 2
⊢ (4 * (n - 1) + 1 + 5) / 2 = 2 * (n - 1) + 1 + 2
Tactic:
rwa[Nat.mul_div_right _ (show 0 < 2 by norm_num)] at h1
Proof state after:
no goals
Theorem: Poland1998P4.lemma7
Proof state before:
n : ℕ
⊢ 4 * (n - 1) + 1 + 5 = 2 * (2 * (n - 1) + 1 + 2)
Tactic:
ring
Proof state after:
no goals
Theorem: Poland1998P4.lemma7
Proof state before:
n : ℕ
h1 : (4 * (n - 1) + 1 + 5) / 2 = 2 * (2 * (n - 1) + 1 + 2) / 2
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Poland1998P4.lemma7'
Proof state before:
n : ℕ
⊢ (4 * (n - 1) + 1 + 6) / 2 = 2 * (n - 1) + 1 + 2
Tactic:
have h1 : (4 * (n - 1) + 1 + 6) = 2 * (2 * (n - 1) + 1 + 2) + 1 := by ring
Proof state after:
n : ℕ
h1 : 4 * (n - 1) + 1 + 6 = 2 * (2 * (n - 1) + 1 + 2) + 1
⊢ (4 * (n - 1) + 1 + 6) / 2 = 2 * (n - 1) + 1 + 2
Theorem: Poland1998P4.lemma7'
Proof state before:
n : ℕ
h1 : 4 * (n - 1) + 1 + 6 = 2 * (2 * (n - 1) + 1 + 2) + 1
⊢ (4 * (n - 1) + 1 + 6) / 2 = 2 * (n - 1) + 1 + 2
Tactic:
rw [h1]
Proof state after:
n : ℕ
h1 : 4 * (n - 1) + 1 + 6 = 2 * (2 * (n - 1) + 1 + 2) + 1
⊢ (2 * (2 * (n - 1) + 1 + 2) + 1) / 2 = 2 * (n - 1) + 1 + 2
Theorem: Poland1998P4.lemma7'
Proof state before:
n : ℕ
h1 : 4 * (n - 1) + 1 + 6 = 2 * (2 * (n - 1) + 1 + 2) + 1
⊢ (2 * (2 * (n - 1) + 1 + 2) + 1) / 2 = 2 * (n - 1) + 1 + 2
Tactic:
exact lemma2 (2 * (n - 1) + 1 + 2)
Proof state after:
no goals
Theorem: Poland1998P4.lemma7'
Proof state before:
n : ℕ
⊢ 4 * (n - 1) + 1 + 6 = 2 * (2 * (n - 1) + 1 + 2) + 1
Tactic:
ring
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
⊢ ∀ (N : ℕ), a' N = 0 → ∃ M, N < M ∧ a' M = 0
Tactic:
intro n hn
Proof state after:
n : ℕ
hn : a' n = 0
⊢ ∃ M, n < M ∧ a' M = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
n : ℕ
hn : a' n = 0
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
obtain (hlt : n < 2) | (hlte : 2 ≤ n) := lt_or_ge n 2
Proof state after:
case inl
n : ℕ
hn : a' n = 0
hlt : n < 2
⊢ ∃ M, n < M ∧ a' M = 0

case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
⊢ ∃ M, n < M ∧ a' M = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
let n1 : ℕ := 2 * (n - 1) + 1
Proof state after:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
⊢ ∃ M, n < M ∧ a' M = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
have npos := calc 0 < 2 := by norm_num
                  _ ≤ n := hlte
Proof state after:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
⊢ ∃ M, n < M ∧ a' M = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
have hn1v : n1 = 2 * n - 1 := lemma1 n npos
Proof state after:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
⊢ ∃ M, n < M ∧ a' M = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
have hn2 : 2 ≤ n1 + 1 := Nat.succ_le_succ le_add_self
Proof state after:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
⊢ ∃ M, n < M ∧ a' M = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
let an1 := a' n1
Proof state after:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
⊢ ∃ M, n < M ∧ a' M = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
have ha1 : a' (n1 + 1) = an1 + a' n := by
  have haa : a' (n1 + 1) = a' n1 + a' (n1.succ / 2) := a'_recurrence (n1 + 1) hn2
  have h2n1 : 2 * n / 2 = n := by norm_num
  have h2n1' : (n1 + 1) / 2 = n := by rw [hn1, h2n1]
  rw [haa, h2n1']
Proof state after:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
⊢ ∃ M, n < M ∧ a' M = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
have ha2 : a' (n1 + 2) = a' (n1 + 1) +  a' n := by
  have haa : a' (n1 + 2) = a' (n1 + 1) + a' (n1.succ.succ / 2) :=
    a'_recurrence (n1 + 2) le_add_self
  have h1 : (2 * n + 1) / 2 = n := lemma2 n
  have hn1v' : 2 * n = n1 + 1 := hn1.symm
  rw [haa]
  congr
  have : n1.succ.succ = (n1 + 1 + 1) := rfl
  rw [this, ←hn1v', h1]
Proof state after:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
ha2 : a' (n1 + 2) = a' (n1 + 1) + a' n
⊢ ∃ M, n < M ∧ a' M = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
ha2 : a' (n1 + 2) = a' (n1 + 1) + a' n
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
have ha1' : a' (n1 + 1) = a' n1 := by
  simp only [hn, add_zero] at ha1
  exact ha1
Proof state after:
case inr
n : ℕ
hn : a' n = 0
hlte : 2 ≤ n
n1 : ℕ := 2 * (n - 1) + 1
npos : 0 < n
hn1v : n1 = 2 * n - 1
hn2 : 2 ≤ n1 + 1
an1 : ZMod 7 := a' n1
hn1 : n1 + 1 = 2 * n
ha1 : a' (n1 + 1) = an1 + a' n
ha2 : a' (n1 + 2) = a' (n1 + 1) + a' n
ha1' : a' (n1 + 1) = a' n1
⊢ ∃ M, n < M ∧ a' M = 0