internlm/Lean-Github huggingface dataset:
Theorem: Usa2019P1.lemma_3
Proof state before:
case a
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 ^ 2
⊢ f m2 = m2
Tactic:
rw [sq] at h1
Proof state after:
case a
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
⊢ f m2 = m2
Theorem: Usa2019P1.lemma_3
Proof state before:
case a
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
⊢ f m2 = m2
Tactic:
obtain h2 | h2 := Classical.em (f^[2] m2 < m2)
Proof state after:
case a.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : f^[2] m2 < m2
⊢ f m2 = m2

case a.inr
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
⊢ f m2 = m2
Theorem: Usa2019P1.lemma_3
Proof state before:
case a.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : f^[2] m2 < m2
⊢ f m2 = m2
Tactic:
let k := f^[2] m2
Proof state after:
case a.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : f^[2] m2 < m2
k : ℕ+ := f^[2] m2
⊢ f m2 = m2
Theorem: Usa2019P1.lemma_3
Proof state before:
case a.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : f^[2] m2 < m2
k : ℕ+ := f^[2] m2
⊢ f m2 = m2
Tactic:
have hkodd : Odd k.val := (pnat_odd_mul h1 hm3).2
Proof state after:
case a.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : f^[2] m2 < m2
k : ℕ+ := f^[2] m2
hkodd : Odd ↑k
⊢ f m2 = m2
Theorem: Usa2019P1.lemma_3
Proof state before:
case a.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : f^[2] m2 < m2
k : ℕ+ := f^[2] m2
hkodd : Odd ↑k
⊢ f m2 = m2
Tactic:
have h3 : f k = k := ih k h2 hkodd
Proof state after:
case a.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : f^[2] m2 < m2
k : ℕ+ := f^[2] m2
hkodd : Odd ↑k
h3 : f k = k
⊢ f m2 = m2
Theorem: Usa2019P1.lemma_3
Proof state before:
case a.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : f^[2] m2 < m2
k : ℕ+ := f^[2] m2
hkodd : Odd ↑k
h3 : f k = k
⊢ f m2 = m2
Tactic:
rw[lemma_1 f hf k m2 2 rfl h3]
Proof state after:
case a.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : f^[2] m2 < m2
k : ℕ+ := f^[2] m2
hkodd : Odd ↑k
h3 : f k = k
⊢ f k = k
Theorem: Usa2019P1.lemma_3
Proof state before:
case a.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : f^[2] m2 < m2
k : ℕ+ := f^[2] m2
hkodd : Odd ↑k
h3 : f k = k
⊢ f k = k
Tactic:
exact h3
Proof state after:
no goals
Theorem: Usa2019P1.lemma_3
Proof state before:
case a.inr
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
⊢ f m2 = m2
Tactic:
obtain h4 | h4 := Classical.em (f^[f m2] m2 < m2)
Proof state after:
case a.inr.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : f^[↑(f m2)] m2 < m2
⊢ f m2 = m2

case a.inr.inr
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : ¬f^[↑(f m2)] m2 < m2
⊢ f m2 = m2
Theorem: Usa2019P1.lemma_3
Proof state before:
case a.inr.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : f^[↑(f m2)] m2 < m2
⊢ f m2 = m2
Tactic:
let k := f^[f m2] m2
Proof state after:
case a.inr.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : f^[↑(f m2)] m2 < m2
k : ℕ+ := f^[↑(f m2)] m2
⊢ f m2 = m2
Theorem: Usa2019P1.lemma_3
Proof state before:
case a.inr.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : f^[↑(f m2)] m2 < m2
k : ℕ+ := f^[↑(f m2)] m2
⊢ f m2 = m2
Tactic:
have hkodd : Odd k.val := (pnat_odd_mul h1 hm3).1
Proof state after:
case a.inr.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : f^[↑(f m2)] m2 < m2
k : ℕ+ := f^[↑(f m2)] m2
hkodd : Odd ↑k
⊢ f m2 = m2
Theorem: Usa2019P1.lemma_3
Proof state before:
case a.inr.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : f^[↑(f m2)] m2 < m2
k : ℕ+ := f^[↑(f m2)] m2
hkodd : Odd ↑k
⊢ f m2 = m2
Tactic:
have h3 : f k = k := ih k h4 hkodd
Proof state after:
case a.inr.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : f^[↑(f m2)] m2 < m2
k : ℕ+ := f^[↑(f m2)] m2
hkodd : Odd ↑k
h3 : f k = k
⊢ f m2 = m2
Theorem: Usa2019P1.lemma_3
Proof state before:
case a.inr.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : f^[↑(f m2)] m2 < m2
k : ℕ+ := f^[↑(f m2)] m2
hkodd : Odd ↑k
h3 : f k = k
⊢ f m2 = m2
Tactic:
rw[lemma_1 f hf k m2 _ rfl h3]
Proof state after:
case a.inr.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : f^[↑(f m2)] m2 < m2
k : ℕ+ := f^[↑(f m2)] m2
hkodd : Odd ↑k
h3 : f k = k
⊢ f k = k
Theorem: Usa2019P1.lemma_3
Proof state before:
case a.inr.inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : f^[↑(f m2)] m2 < m2
k : ℕ+ := f^[↑(f m2)] m2
hkodd : Odd ↑k
h3 : f k = k
⊢ f k = k
Tactic:
exact h3
Proof state after:
no goals
Theorem: Usa2019P1.lemma_3
Proof state before:
case a.inr.inr
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : ¬f^[↑(f m2)] m2 < m2
h5 : f^[2] m2 = m2 ∧ f^[↑(f m2)] m2 = m2
⊢ f m2 = m2
Tactic:
obtain ⟨h6, h7⟩ := h5
Proof state after:
case a.inr.inr.intro
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : ¬f^[↑(f m2)] m2 < m2
h6 : f^[2] m2 = m2
h7 : f^[↑(f m2)] m2 = m2
⊢ f m2 = m2
Theorem: Usa2019P1.lemma_3
Proof state before:
case a.inr.inr.intro
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : ¬f^[↑(f m2)] m2 < m2
h6 : f^[2] m2 = m2
h7 : f^[↑(f m2)] m2 = m2
⊢ f m2 = m2
Tactic:
have h8 : f^[2] m2 = f^[↑(f m2)] m2 := by rw[h7]; exact h6
Proof state after:
case a.inr.inr.intro
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : ¬f^[↑(f m2)] m2 < m2
h6 : f^[2] m2 = m2
h7 : f^[↑(f m2)] m2 = m2
h8 : f^[2] m2 = f^[↑(f m2)] m2
⊢ f m2 = m2
Theorem: Usa2019P1.lemma_3
Proof state before:
case a.inr.inr.intro
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : ¬f^[↑(f m2)] m2 < m2
h6 : f^[2] m2 = m2
h7 : f^[↑(f m2)] m2 = m2
h8 : f^[2] m2 = f^[↑(f m2)] m2
⊢ f m2 = m2
Tactic:
exact lemma_2 f hf _ h8 h7 hm3
Proof state after:
no goals
Theorem: Usa2019P1.lemma_3
Proof state before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : ¬f^[↑(f m2)] m2 < m2
⊢ f^[2] m2 = m2 ∧ f^[↑(f m2)] m2 = m2
Tactic:
simp at h2 h4
Proof state after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h4 : m2 ≤ f^[↑(f m2)] m2
⊢ f^[2] m2 = m2 ∧ f^[↑(f m2)] m2 = m2
Theorem: Usa2019P1.lemma_3
Proof state before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h4 : m2 ≤ f^[↑(f m2)] m2
⊢ f^[2] m2 = m2 ∧ f^[↑(f m2)] m2 = m2
Tactic:
by_contra H
Proof state after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h4 : m2 ≤ f^[↑(f m2)] m2
H : ¬(f^[2] m2 = m2 ∧ f^[↑(f m2)] m2 = m2)
⊢ False
Theorem: Usa2019P1.lemma_3
Proof state before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h4 : m2 ≤ f^[↑(f m2)] m2
H : ¬(f^[2] m2 = m2 ∧ f^[↑(f m2)] m2 = m2)
⊢ False
Tactic:
rw [not_and_or] at H
Proof state after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h4 : m2 ≤ f^[↑(f m2)] m2
H : ¬f^[2] m2 = m2 ∨ ¬f^[↑(f m2)] m2 = m2
⊢ False
Theorem: Usa2019P1.lemma_3
Proof state before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h4 : m2 ≤ f^[↑(f m2)] m2
H : ¬f^[2] m2 = m2 ∨ ¬f^[↑(f m2)] m2 = m2
⊢ False
Tactic:
obtain h9 | h9 := H
Proof state after:
case inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h4 : m2 ≤ f^[↑(f m2)] m2
h9 : ¬f^[2] m2 = m2
⊢ False

case inr
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h4 : m2 ≤ f^[↑(f m2)] m2
h9 : ¬f^[↑(f m2)] m2 = m2
⊢ False
Theorem: Usa2019P1.lemma_3
Proof state before:
case inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h4 : m2 ≤ f^[↑(f m2)] m2
h9 : ¬f^[2] m2 = m2
⊢ False
Tactic:
replace h2 : m2 < f (f m2) := Ne.lt_of_le' h9 h2
Proof state after:
case inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h4 : m2 ≤ f^[↑(f m2)] m2
h9 : ¬f^[2] m2 = m2
h2 : m2 < f (f m2)
⊢ False
Theorem: Usa2019P1.lemma_3
Proof state before:
case inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h4 : m2 ≤ f^[↑(f m2)] m2
h9 : ¬f^[2] m2 = m2
h2 : m2 < f (f m2)
⊢ False
Tactic:
have h10 : m2 * m2 < f^[↑(f m2)] m2 * f (f m2) := mul_lt_mul_of_le_of_lt h4 h2
Proof state after:
case inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h4 : m2 ≤ f^[↑(f m2)] m2
h9 : ¬f^[2] m2 = m2
h2 : m2 < f (f m2)
h10 : m2 * m2 < f^[↑(f m2)] m2 * f (f m2)
⊢ False
Theorem: Usa2019P1.lemma_3
Proof state before:
case inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h4 : m2 ≤ f^[↑(f m2)] m2
h9 : ¬f^[2] m2 = m2
h2 : m2 < f (f m2)
h10 : m2 * m2 < f^[↑(f m2)] m2 * f (f m2)
⊢ False
Tactic:
rw [←h1] at h10
Proof state after:
case inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h4 : m2 ≤ f^[↑(f m2)] m2
h9 : ¬f^[2] m2 = m2
h2 : m2 < f (f m2)
h10 : f^[↑(f m2)] m2 * f (f m2) < f^[↑(f m2)] m2 * f (f m2)
⊢ False
Theorem: Usa2019P1.lemma_3
Proof state before:
case inl
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h4 : m2 ≤ f^[↑(f m2)] m2
h9 : ¬f^[2] m2 = m2
h2 : m2 < f (f m2)
h10 : f^[↑(f m2)] m2 * f (f m2) < f^[↑(f m2)] m2 * f (f m2)
⊢ False
Tactic:
exact LT.lt.false h10
Proof state after:
no goals
Theorem: Usa2019P1.lemma_3
Proof state before:
case inr
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h4 : m2 ≤ f^[↑(f m2)] m2
h9 : ¬f^[↑(f m2)] m2 = m2
⊢ False
Tactic:
replace h4 : m2 < f^[f m2] m2 := Ne.lt_of_le' h9 h4
Proof state after:
case inr
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h9 : ¬f^[↑(f m2)] m2 = m2
h4 : m2 < f^[↑(f m2)] m2
⊢ False
Theorem: Usa2019P1.lemma_3
Proof state before:
case inr
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h9 : ¬f^[↑(f m2)] m2 = m2
h4 : m2 < f^[↑(f m2)] m2
⊢ False
Tactic:
have h10 : m2 * m2 < f^[↑(f m2)] m2 * f (f m2) := mul_lt_mul_of_lt_of_le h4 h2
Proof state after:
case inr
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h9 : ¬f^[↑(f m2)] m2 = m2
h4 : m2 < f^[↑(f m2)] m2
h10 : m2 * m2 < f^[↑(f m2)] m2 * f (f m2)
⊢ False
Theorem: Usa2019P1.lemma_3
Proof state before:
case inr
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h9 : ¬f^[↑(f m2)] m2 = m2
h4 : m2 < f^[↑(f m2)] m2
h10 : m2 * m2 < f^[↑(f m2)] m2 * f (f m2)
⊢ False
Tactic:
rw [←h1] at h10
Proof state after:
case inr
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h9 : ¬f^[↑(f m2)] m2 = m2
h4 : m2 < f^[↑(f m2)] m2
h10 : f^[↑(f m2)] m2 * f (f m2) < f^[↑(f m2)] m2 * f (f m2)
⊢ False
Theorem: Usa2019P1.lemma_3
Proof state before:
case inr
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : m2 ≤ f (f m2)
h9 : ¬f^[↑(f m2)] m2 = m2
h4 : m2 < f^[↑(f m2)] m2
h10 : f^[↑(f m2)] m2 * f (f m2) < f^[↑(f m2)] m2 * f (f m2)
⊢ False
Tactic:
exact LT.lt.false h10
Proof state after:
no goals
Theorem: Usa2019P1.lemma_3
Proof state before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : ¬f^[↑(f m2)] m2 < m2
h6 : f^[2] m2 = m2
h7 : f^[↑(f m2)] m2 = m2
⊢ f^[2] m2 = f^[↑(f m2)] m2
Tactic:
rw[h7]
Proof state after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : ¬f^[↑(f m2)] m2 < m2
h6 : f^[2] m2 = m2
h7 : f^[↑(f m2)] m2 = m2
⊢ f^[2] m2 = m2
Theorem: Usa2019P1.lemma_3
Proof state before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m2 : ℕ+
ih : ∀ m < m2, Odd ↑m → f m = m
hm3 : Odd ↑m2
h1 : f^[↑(f m2)] m2 * f (f m2) = m2 * m2
h2 : ¬f^[2] m2 < m2
h4 : ¬f^[↑(f m2)] m2 < m2
h6 : f^[2] m2 = m2
h7 : f^[↑(f m2)] m2 = m2
⊢ f^[2] m2 = m2
Tactic:
exact h6
Proof state after:
no goals
Theorem: Usa2005P2.lemma1
Proof state before:
x : ZMod 13
⊢ x ^ 3 = 0 ∨ x ^ 3 = 1 ∨ x ^ 3 = -1 ∨ x ^ 3 = 5 ∨ x ^ 3 = -5
Tactic:
reduce_mod_char
Proof state after:
x : ZMod 13
⊢ x ^ 3 = 0 ∨ x ^ 3 = 1 ∨ x ^ 3 = 12 ∨ x ^ 3 = 5 ∨ x ^ 3 = 8
Theorem: Usa2005P2.lemma1
Proof state before:
x : ZMod 13
⊢ x ^ 3 = 0 ∨ x ^ 3 = 1 ∨ x ^ 3 = 12 ∨ x ^ 3 = 5 ∨ x ^ 3 = 8
Tactic:
fin_cases x <;> decide
Proof state after:
no goals
Theorem: Usa2001P3.usa2001_p3_lemma
Proof state before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
⊢ a * b + b * c + c * a - a * b * c ≤ 2
Tactic:
have eq1 := calc
  (2 + a) * (2 - a) = 4 - a ^ 2 := by ring_nf
  _ = a ^ 2 + b ^ 2 + c ^ 2 + a * b * c - a ^ 2 := by rw [h]
  _ = (b ^ 2 + c ^ 2) + a * b * c := by ring_nf
  _ ≥ 2 * b * c + a * b * c := by rel [two_mul_le_add_sq b c]
  _ = (2 + a) * (b * c) := by ring_nf
Proof state after:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
⊢ a * b + b * c + c * a - a * b * c ≤ 2
Theorem: Usa2001P3.usa2001_p3_lemma
Proof state before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
⊢ a * b + b * c + c * a - a * b * c ≤ 2
Tactic:
have a2gt0 : 2 + a > 0 := by linarith
Proof state after:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
⊢ a * b + b * c + c * a - a * b * c ≤ 2
Theorem: Usa2001P3.usa2001_p3_lemma
Proof state before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
⊢ a * b + b * c + c * a - a * b * c ≤ 2
Tactic:
have bc := (mul_le_mul_left a2gt0).mp eq1
Proof state after:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ a * b + b * c + c * a - a * b * c ≤ 2
Theorem: Usa2001P3.usa2001_p3_lemma
Proof state before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ a * b + b * c + c * a - a * b * c ≤ 2
Tactic:
calc
  a * b + b * c + c * a - a * b * c = a * b + b * c + a * c * (1 - b) := by ring_nf
  _ ≤ a * b + (2 - a) + a * c * (1 - b) := by gcongr
  _ = 2 - a * ((b - 1) * (c - 1)) := by ring_nf
  _ ≤ 2 - 0 := by gcongr; positivity
  _ = 2 := by norm_num
Proof state after:
no goals
Theorem: Usa2001P3.usa2001_p3_lemma
Proof state before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
⊢ (2 + a) * (2 - a) = 4 - a ^ 2
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Usa2001P3.usa2001_p3_lemma
Proof state before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
⊢ 4 - a ^ 2 = a ^ 2 + b ^ 2 + c ^ 2 + a * b * c - a ^ 2
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Usa2001P3.usa2001_p3_lemma
Proof state before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
⊢ a ^ 2 + b ^ 2 + c ^ 2 + a * b * c - a ^ 2 = b ^ 2 + c ^ 2 + a * b * c
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Usa2001P3.usa2001_p3_lemma
Proof state before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
⊢ b ^ 2 + c ^ 2 + a * b * c ≥ 2 * b * c + a * b * c
Tactic:
rel [two_mul_le_add_sq b c]
Proof state after:
no goals
Theorem: Usa2001P3.usa2001_p3_lemma
Proof state before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
⊢ 2 * b * c + a * b * c = (2 + a) * (b * c)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Usa2001P3.usa2001_p3_lemma
Proof state before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
⊢ 2 + a > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Usa2001P3.usa2001_p3_lemma
Proof state before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ a * b + b * c + c * a - a * b * c = a * b + b * c + a * c * (1 - b)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Usa2001P3.usa2001_p3_lemma
Proof state before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ a * b + b * c + a * c * (1 - b) ≤ a * b + (2 - a) + a * c * (1 - b)
Tactic:
gcongr
Proof state after:
no goals
Theorem: Usa2001P3.usa2001_p3_lemma
Proof state before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ a * b + (2 - a) + a * c * (1 - b) = 2 - a * ((b - 1) * (c - 1))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Usa2001P3.usa2001_p3_lemma
Proof state before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ 2 - a * ((b - 1) * (c - 1)) ≤ 2 - 0
Tactic:
gcongr
Proof state after:
case h
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ 0 ≤ a * ((b - 1) * (c - 1))
Theorem: Usa2001P3.usa2001_p3_lemma
Proof state before:
case h
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ 0 ≤ a * ((b - 1) * (c - 1))
Tactic:
positivity
Proof state after:
no goals
Theorem: Usa2001P3.usa2001_p3_lemma
Proof state before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ 2 - 0 = 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Imo1962P1.without_digits
Proof state before:
n : ℕ
h1 : ProblemPredicate n
⊢ ∃ c, ProblemPredicate' c n
Tactic:
use n / 10
Proof state after:
case h
n : ℕ
h1 : ProblemPredicate n
⊢ ProblemPredicate' (n / 10) n