Theorem: Usa2019P1.lemma_3 (Compfiles/Usa2019P1.lean)

State before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
m : ℕ+
hm3 : Odd ↑m
⊢ f m = m
Tactic:
induction' m using PNat.strongInductionOn with m2 ih
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
⊢ f m2 = m2

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
⊢ f m2 = m2
Tactic:
have h1 := hf m2
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 ^ 2
⊢ f m2 = m2

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
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

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)
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

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
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

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
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

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
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

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]
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

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
State after:
no goals

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)
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

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
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

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
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

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
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

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]
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
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

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
State after:
no goals

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]
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

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
State after:
no goals