internlm/Lean-Github huggingface dataset:
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case succ
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
hpi7 : p + 1 < 7
hpi6 : p < 6
hinc : a' (n2 + p + 1) = a' (n2 + p) + a' n1
hadd : n2 + p + 1 = n2 + p.succ
hi6 : p < 7
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Tactic:
have hpp := hp hi6
Proof state after:
case succ
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
hpi7 : p + 1 < 7
hpi6 : p < 6
hinc : a' (n2 + p + 1) = a' (n2 + p) + a' n1
hadd : n2 + p + 1 = n2 + p.succ
hi6 : p < 7
hpp : a' (n2 + p) = a' n2 + a' n1 * ↑p
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case succ
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
hpi7 : p + 1 < 7
hpi6 : p < 6
hinc : a' (n2 + p + 1) = a' (n2 + p) + a' n1
hadd : n2 + p + 1 = n2 + p.succ
hi6 : p < 7
hpp : a' (n2 + p) = a' n2 + a' n1 * ↑p
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Tactic:
have hp1: (p.succ : ZMod 7) = (p : ZMod 7) + 1 := Nat.cast_succ p
Proof state after:
case succ
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
hpi7 : p + 1 < 7
hpi6 : p < 6
hinc : a' (n2 + p + 1) = a' (n2 + p) + a' n1
hadd : n2 + p + 1 = n2 + p.succ
hi6 : p < 7
hpp : a' (n2 + p) = a' n2 + a' n1 * ↑p
hp1 : ↑p.succ = ↑p + 1
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case succ
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
hpi7 : p + 1 < 7
hpi6 : p < 6
hinc : a' (n2 + p + 1) = a' (n2 + p) + a' n1
hadd : n2 + p + 1 = n2 + p.succ
hi6 : p < 7
hpp : a' (n2 + p) = a' n2 + a' n1 * ↑p
hp1 : ↑p.succ = ↑p + 1
⊢ a' (n2 + (p + 1)) = a' n2 + a' n1 * ↑(p + 1)
Tactic:
rw [←hadd, hinc, hpp, hp1]
Proof state after:
case succ
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
hpi7 : p + 1 < 7
hpi6 : p < 6
hinc : a' (n2 + p + 1) = a' (n2 + p) + a' n1
hadd : n2 + p + 1 = n2 + p.succ
hi6 : p < 7
hpp : a' (n2 + p) = a' n2 + a' n1 * ↑p
hp1 : ↑p.succ = ↑p + 1
⊢ a' n2 + a' n1 * ↑p + a' n1 = a' n2 + a' n1 * (↑p + 1)
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case succ
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
p : ℕ
hp : p < 7 → a' (n2 + p) = a' n2 + a' n1 * ↑p
hpi7 : p + 1 < 7
hpi6 : p < 6
hinc : a' (n2 + p + 1) = a' (n2 + p) + a' n1
hadd : n2 + p + 1 = n2 + p.succ
hi6 : p < 7
hpp : a' (n2 + p) = a' n2 + a' n1 * ↑p
hp1 : ↑p.succ = ↑p + 1
⊢ a' n2 + a' n1 * ↑p + a' n1 = a' n2 + a' n1 * (↑p + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inr.inl
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
haez : a' n1 = 0
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
use n1
Proof state after:
case h
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
haez : a' n1 = 0
⊢ n < n1 ∧ a' n1 = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case h
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
haez : a' n1 = 0
⊢ n < n1 ∧ a' n1 = 0
Tactic:
constructor
Proof state after:
case h.left
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
haez : a' n1 = 0
⊢ n < n1

case h.right
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
haez : a' n1 = 0
⊢ a' n1 = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case h.left
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
haez : a' n1 = 0
⊢ n < n1
Tactic:
omega
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case h.right
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
haez : a' n1 = 0
⊢ a' n1 = 0
Tactic:
exact haez
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inr.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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
hanez : ¬a' n1 = 0
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
have := lemma3 n2 (a' n1) hanez hik
Proof state after:
case inr.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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
hanez : ¬a' n1 = 0
this : ∃ i < 7, a' (n2 + i) = 0
⊢ ∃ M, n < M ∧ a' M = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inr.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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
hanez : ¬a' n1 = 0
this : ∃ i < 7, a' (n2 + i) = 0
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
obtain ⟨ii, _, hia'⟩ := this
Proof state after:
case inr.inr.intro.intro
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
hanez : ¬a' n1 = 0
ii : ℕ
left✝ : ii < 7
hia' : a' (n2 + ii) = 0
⊢ ∃ M, n < M ∧ a' M = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case inr.inr.intro.intro
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
hanez : ¬a' n1 = 0
ii : ℕ
left✝ : ii < 7
hia' : a' (n2 + ii) = 0
⊢ ∃ M, n < M ∧ a' M = 0
Tactic:
use (n2 + ii)
Proof state after:
case h
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
hanez : ¬a' n1 = 0
ii : ℕ
left✝ : ii < 7
hia' : a' (n2 + ii) = 0
⊢ n < n2 + ii ∧ a' (n2 + ii) = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case h
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
hanez : ¬a' n1 = 0
ii : ℕ
left✝ : ii < 7
hia' : a' (n2 + ii) = 0
⊢ n < n2 + ii ∧ a' (n2 + ii) = 0
Tactic:
constructor
Proof state after:
case h.left
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
hanez : ¬a' n1 = 0
ii : ℕ
left✝ : ii < 7
hia' : a' (n2 + ii) = 0
⊢ n < n2 + ii

case h.right
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
hanez : ¬a' n1 = 0
ii : ℕ
left✝ : ii < 7
hia' : a' (n2 + ii) = 0
⊢ a' (n2 + ii) = 0
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case h.left
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
hanez : ¬a' n1 = 0
ii : ℕ
left✝ : ii < 7
hia' : a' (n2 + ii) = 0
⊢ n < n2 + ii
Tactic:
linarith
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one_zmod
Proof state before:
case h.right
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) = a' n1
ha2' : a' (n1 + 2) = a' n1
n2 : ℕ := 4 * (n - 1) + 1
hii : ∀ i < 6, a' (n2 + i + 1) = a' (n2 + i) + a' n1
hik : ∀ i < 7, a' (n2 + i) = a' n2 + a' n1 * ↑i
hanez : ¬a' n1 = 0
ii : ℕ
left✝ : ii < 7
hia' : a' (n2 + ii) = 0
⊢ a' (n2 + ii) = 0
Tactic:
assumption
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one
Proof state before:
⊢ ∀ (N : ℕ), 7 ∣ a N → ∃ M, N < M ∧ 7 ∣ Poland1998P4.a M
Tactic:
intro n hn
Proof state after:
n : ℕ
hn : 7 ∣ a n
⊢ ∃ M, n < M ∧ 7 ∣ a M
Theorem: Poland1998P4.can_get_a_later_one
Proof state before:
n : ℕ
hn : 7 ∣ a n
⊢ ∃ M, n < M ∧ 7 ∣ a M
Tactic:
have ha' : a' n = 0 := by
  have : a' n = ⟨a n % 7, Nat.mod_lt _ (Nat.succ_pos _)⟩ := by simp[a']
  rw [this]
  simp only [Nat.mod_eq_zero_of_dvd hn, Fin.mk_zero]
Proof state after:
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
⊢ ∃ M, n < M ∧ 7 ∣ a M
Theorem: Poland1998P4.can_get_a_later_one
Proof state before:
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
⊢ ∃ M, n < M ∧ 7 ∣ a M
Tactic:
obtain ⟨m, hmgt, hm7⟩ := can_get_a_later_one_zmod n ha'
Proof state after:
case intro.intro
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
m : ℕ
hmgt : n < m
hm7 : a' m = 0
⊢ ∃ M, n < M ∧ 7 ∣ a M
Theorem: Poland1998P4.can_get_a_later_one
Proof state before:
case intro.intro
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
m : ℕ
hmgt : n < m
hm7 : a' m = 0
⊢ ∃ M, n < M ∧ 7 ∣ a M
Tactic:
use m
Proof state after:
case h
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
m : ℕ
hmgt : n < m
hm7 : a' m = 0
⊢ n < m ∧ 7 ∣ a m
Theorem: Poland1998P4.can_get_a_later_one
Proof state before:
case h
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
m : ℕ
hmgt : n < m
hm7 : a' m = 0
⊢ n < m ∧ 7 ∣ a m
Tactic:
use hmgt
Proof state after:
case right
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
m : ℕ
hmgt : n < m
hm7 : a' m = 0
⊢ 7 ∣ a m
Theorem: Poland1998P4.can_get_a_later_one
Proof state before:
case right
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
m : ℕ
hmgt : n < m
hm7 : a' m = 0
⊢ 7 ∣ a m
Tactic:
exact Fin.natCast_eq_zero.mp hm7
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one
Proof state before:
n : ℕ
hn : 7 ∣ a n
⊢ a' n = 0
Tactic:
have : a' n = ⟨a n % 7, Nat.mod_lt _ (Nat.succ_pos _)⟩ := by simp[a']
Proof state after:
n : ℕ
hn : 7 ∣ a n
this : a' n = ⟨a n % 7, ⋯⟩
⊢ a' n = 0
Theorem: Poland1998P4.can_get_a_later_one
Proof state before:
n : ℕ
hn : 7 ∣ a n
this : a' n = ⟨a n % 7, ⋯⟩
⊢ a' n = 0
Tactic:
rw [this]
Proof state after:
n : ℕ
hn : 7 ∣ a n
this : a' n = ⟨a n % 7, ⋯⟩
⊢ ⟨a n % 7, ⋯⟩ = 0
Theorem: Poland1998P4.can_get_a_later_one
Proof state before:
n : ℕ
hn : 7 ∣ a n
this : a' n = ⟨a n % 7, ⋯⟩
⊢ ⟨a n % 7, ⋯⟩ = 0
Tactic:
simp only [Nat.mod_eq_zero_of_dvd hn, Fin.mk_zero]
Proof state after:
no goals
Theorem: Poland1998P4.can_get_a_later_one
Proof state before:
n : ℕ
hn : 7 ∣ a n
⊢ a' n = ⟨a n % 7, ⋯⟩
Tactic:
simp[a']
Proof state after:
no goals
Theorem: Poland1998P4.strengthen
Proof state before:
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
he : ∃ N, P N
⊢ ∀ (N : ℕ), ∃ M, N < M ∧ P M
Tactic:
obtain ⟨N0, hn0⟩ := he
Proof state after:
case intro
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
⊢ ∀ (N : ℕ), ∃ M, N < M ∧ P M
Theorem: Poland1998P4.strengthen
Proof state before:
case intro
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
⊢ ∀ (N : ℕ), ∃ M, N < M ∧ P M
Tactic:
intro N
Proof state after:
case intro
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
N : ℕ
⊢ ∃ M, N < M ∧ P M
Theorem: Poland1998P4.strengthen
Proof state before:
case intro
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
N : ℕ
⊢ ∃ M, N < M ∧ P M
Tactic:
induction' N with pn hpn
Proof state after:
case intro.zero
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
⊢ ∃ M, 0 < M ∧ P M

case intro.succ
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn : ℕ
hpn : ∃ M, pn < M ∧ P M
⊢ ∃ M, pn + 1 < M ∧ P M
Theorem: Poland1998P4.strengthen
Proof state before:
case intro.zero
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
⊢ ∃ M, 0 < M ∧ P M
Tactic:
obtain (hlt : 0 < N0) | (hlte : N0 ≤ 0) := lt_or_ge 0 N0
Proof state after:
case intro.zero.inl
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
hlt : 0 < N0
⊢ ∃ M, 0 < M ∧ P M

case intro.zero.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
hlte : N0 ≤ 0
⊢ ∃ M, 0 < M ∧ P M
Theorem: Poland1998P4.strengthen
Proof state before:
case intro.zero.inl
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
hlt : 0 < N0
⊢ ∃ M, 0 < M ∧ P M
Tactic:
exact ⟨N0, hlt, hn0⟩
Proof state after:
no goals
Theorem: Poland1998P4.strengthen
Proof state before:
case intro.zero.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
hlte : N0 ≤ 0
⊢ ∃ M, 0 < M ∧ P M
Tactic:
have heq : N0 = 0 := eq_bot_iff.mpr hlte
Proof state after:
case intro.zero.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
hlte : N0 ≤ 0
heq : N0 = 0
⊢ ∃ M, 0 < M ∧ P M
Theorem: Poland1998P4.strengthen
Proof state before:
case intro.zero.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
hlte : N0 ≤ 0
heq : N0 = 0
⊢ ∃ M, 0 < M ∧ P M
Tactic:
rw [heq] at hn0
Proof state after:
case intro.zero.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P 0
hlte : N0 ≤ 0
heq : N0 = 0
⊢ ∃ M, 0 < M ∧ P M
Theorem: Poland1998P4.strengthen
Proof state before:
case intro.zero.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P 0
hlte : N0 ≤ 0
heq : N0 = 0
⊢ ∃ M, 0 < M ∧ P M
Tactic:
exact h 0 hn0
Proof state after:
no goals
Theorem: Poland1998P4.strengthen
Proof state before:
case intro.succ
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn : ℕ
hpn : ∃ M, pn < M ∧ P M
⊢ ∃ M, pn + 1 < M ∧ P M
Tactic:
obtain ⟨m, hm, hmp⟩ := hpn
Proof state after:
case intro.succ.intro.intro
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
⊢ ∃ M, pn + 1 < M ∧ P M
Theorem: Poland1998P4.strengthen
Proof state before:
case intro.succ.intro.intro
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
⊢ ∃ M, pn + 1 < M ∧ P M
Tactic:
obtain (hlt : pn + 1 < m) |  (hlte : m ≤ pn + 1) := lt_or_ge (pn + 1) m
Proof state after:
case intro.succ.intro.intro.inl
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
hlt : pn + 1 < m
⊢ ∃ M, pn + 1 < M ∧ P M

case intro.succ.intro.intro.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
hlte : m ≤ pn + 1
⊢ ∃ M, pn + 1 < M ∧ P M
Theorem: Poland1998P4.strengthen
Proof state before:
case intro.succ.intro.intro.inl
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
hlt : pn + 1 < m
⊢ ∃ M, pn + 1 < M ∧ P M
Tactic:
exact ⟨m, hlt, hmp⟩
Proof state after:
no goals
Theorem: Poland1998P4.strengthen
Proof state before:
case intro.succ.intro.intro.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
hlte : m ≤ pn + 1
⊢ ∃ M, pn + 1 < M ∧ P M
Tactic:
have heq : m = pn + 1 := le_antisymm hlte hm
Proof state after:
case intro.succ.intro.intro.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
hlte : m ≤ pn + 1
heq : m = pn + 1
⊢ ∃ M, pn + 1 < M ∧ P M
Theorem: Poland1998P4.strengthen
Proof state before:
case intro.succ.intro.intro.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
hlte : m ≤ pn + 1
heq : m = pn + 1
⊢ ∃ M, pn + 1 < M ∧ P M
Tactic:
rw [heq] at hmp
Proof state after:
case intro.succ.intro.intro.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P (pn + 1)
hlte : m ≤ pn + 1
heq : m = pn + 1
⊢ ∃ M, pn + 1 < M ∧ P M
Theorem: Poland1998P4.strengthen
Proof state before:
case intro.succ.intro.intro.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P (pn + 1)
hlte : m ≤ pn + 1
heq : m = pn + 1
⊢ ∃ M, pn + 1 < M ∧ P M
Tactic:
exact h (pn.succ) hmp
Proof state after:
no goals
Theorem: Poland1998P4.poland1998_p4'
Proof state before:
⊢ ∀ (N : ℕ), ∃ M, N < M ∧ 7 ∣ a M
Tactic:
have he : 7 ∣ a 5 := by simp [a', a]
Proof state after:
he : 7 ∣ a 5
⊢ ∀ (N : ℕ), ∃ M, N < M ∧ 7 ∣ a M
Theorem: Poland1998P4.poland1998_p4'
Proof state before:
he : 7 ∣ a 5
⊢ ∀ (N : ℕ), ∃ M, N < M ∧ 7 ∣ a M
Tactic:
exact strengthen can_get_a_later_one ⟨5, he⟩
Proof state after:
no goals
Theorem: Poland1998P4.poland1998_p4'
Proof state before:
⊢ 7 ∣ a 5
Tactic:
simp [a', a]
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.A_ne_B
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ 0 ≠ 1
Tactic:
decide
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.A_ne_C
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ 0 ≠ 2
Tactic:
decide
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.B_ne_C
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ 1 ≠ 2
Tactic:
decide
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.symm_triangleABC
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ cfg.symm.triangleABC = reindex cfg.triangleABC (Equiv.swap 0 1)
Tactic:
ext i
Proof state after:
case h
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
i : Fin (2 + 1)
⊢ cfg.symm.triangleABC.points i = (reindex cfg.triangleABC (Equiv.swap 0 1)).points i
Theorem: Imo2019P2.Imo2019q2Cfg.symm_triangleABC
Proof state before:
case h
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
i : Fin (2 + 1)
⊢ cfg.symm.triangleABC.points i = (reindex cfg.triangleABC (Equiv.swap 0 1)).points i
Tactic:
fin_cases i <;> rfl
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.symm_triangleABC_circumsphere
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ circumsphere cfg.symm.triangleABC = circumsphere cfg.triangleABC
Tactic:
rw [symm_triangleABC, Affine.Simplex.circumsphere_reindex]
Proof state after:
no goals
Theorem: Imo2019P2.Imo2019q2Cfg.symm_A₂
Proof state before:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ cfg.symm.A₂ = cfg.B₂
Tactic:
simp_rw [A₂, B₂, symm_triangleABC_circumsphere]
Proof state after:
V : Type u_1
Pt : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace Pt
inst✝ : NormedAddTorsor V Pt
hd2 : Fact (finrank ℝ V = 2)
cfg : Imo2019q2Cfg V Pt
⊢ (circumsphere cfg.triangleABC).secondInter cfg.symm.A (cfg.symm.A₁ -ᵥ cfg.symm.A) =
    (circumsphere cfg.triangleABC).secondInter cfg.B (cfg.B₁ -ᵥ cfg.B)