Theorem: IMOSL.IMO2008A3.final_solution_part_2_general (IMOSLLean4/IMO2008/A3/A3.lean)

State before:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p q : Lex (ℕ × β)
h2 : p < q
⊢ (p.1.succ, p.2) < (q.1.succ, q.2)
Tactic:
rwa [prod_lex_lt_iff, Nat.succ_lt_succ_iff, Nat.succ_inj', ← prod_lex_lt_iff]
State after:
no goals

State before:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p q : Lex (ℕ × β)
h2 : p < q
⊢ (p.1, φ^[3 ^ p.1] p.2) < (q.1, φ^[3 ^ q.1] q.2)
Tactic:
rw [prod_lex_lt_iff] at h2 ⊢
State after:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p q : Lex (ℕ × β)
h2 : p.1 < q.1 ∨ p.1 = q.1 ∧ p.2 < q.2
⊢ (p.1, φ^[3 ^ p.1] p.2).1 < (q.1, φ^[3 ^ q.1] q.2).1 ∨
    (p.1, φ^[3 ^ p.1] p.2).1 = (q.1, φ^[3 ^ q.1] q.2).1 ∧ (p.1, φ^[3 ^ p.1] p.2).2 < (q.1, φ^[3 ^ q.1] q.2).2

State before:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p q : Lex (ℕ × β)
h2 : p.1 < q.1 ∨ p.1 = q.1 ∧ p.2 < q.2
⊢ (p.1, φ^[3 ^ p.1] p.2).1 < (q.1, φ^[3 ^ q.1] q.2).1 ∨
    (p.1, φ^[3 ^ p.1] p.2).1 = (q.1, φ^[3 ^ q.1] q.2).1 ∧ (p.1, φ^[3 ^ p.1] p.2).2 < (q.1, φ^[3 ^ q.1] q.2).2
Tactic:
refine h2.imp_right λ h3 ↦ ⟨h3.1, (h.iterate _ h3.2).trans_eq ?_⟩
State after:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p q : Lex (ℕ × β)
h2 : p.1 < q.1 ∨ p.1 = q.1 ∧ p.2 < q.2
h3 : p.1 = q.1 ∧ p.2 < q.2
⊢ φ^[3 ^ p.1] q.2 = (q.1, φ^[3 ^ q.1] q.2).2

State before:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p q : Lex (ℕ × β)
h2 : p.1 < q.1 ∨ p.1 = q.1 ∧ p.2 < q.2
h3 : p.1 = q.1 ∧ p.2 < q.2
⊢ φ^[3 ^ p.1] q.2 = (q.1, φ^[3 ^ q.1] q.2).2
Tactic:
rw [← h3.1]
State after:
no goals

State before:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p : Lex (ℕ × β)
⊢ (((p.1, φ^[3 ^ p.1] p.2).1, φ^[3 ^ (p.1, φ^[3 ^ p.1] p.2).1] (p.1, φ^[3 ^ p.1] p.2).2).1.succ,
      ((p.1, φ^[3 ^ p.1] p.2).1, φ^[3 ^ (p.1, φ^[3 ^ p.1] p.2).1] (p.1, φ^[3 ^ p.1] p.2).2).2) <
    ((p.1.succ, p.2).1, φ^[3 ^ (p.1.succ, p.2).1] (p.1.succ, p.2).2)
Tactic:
refine prod_lex_lt_iff.mpr <| Or.inr <| ⟨rfl, ?_⟩
State after:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p : Lex (ℕ × β)
⊢ (((p.1, φ^[3 ^ p.1] p.2).1, φ^[3 ^ (p.1, φ^[3 ^ p.1] p.2).1] (p.1, φ^[3 ^ p.1] p.2).2).1.succ,
        ((p.1, φ^[3 ^ p.1] p.2).1, φ^[3 ^ (p.1, φ^[3 ^ p.1] p.2).1] (p.1, φ^[3 ^ p.1] p.2).2).2).2 <
    ((p.1.succ, p.2).1, φ^[3 ^ (p.1.succ, p.2).1] (p.1.succ, p.2).2).2

State before:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p : Lex (ℕ × β)
⊢ (((p.1, φ^[3 ^ p.1] p.2).1, φ^[3 ^ (p.1, φ^[3 ^ p.1] p.2).1] (p.1, φ^[3 ^ p.1] p.2).2).1.succ,
        ((p.1, φ^[3 ^ p.1] p.2).1, φ^[3 ^ (p.1, φ^[3 ^ p.1] p.2).1] (p.1, φ^[3 ^ p.1] p.2).2).2).2 <
    ((p.1.succ, p.2).1, φ^[3 ^ (p.1.succ, p.2).1] (p.1.succ, p.2).2).2
Tactic:
rw [← Function.iterate_add_apply, ← two_mul, pow_succ']
State after:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p : Lex (ℕ × β)
⊢ (((p.1, φ^[3 ^ p.1] p.2).1, φ^[2 * 3 ^ (p.1, φ^[3 ^ p.1] p.2).1] p.2).1.succ,
        ((p.1, φ^[3 ^ p.1] p.2).1, φ^[2 * 3 ^ (p.1, φ^[3 ^ p.1] p.2).1] p.2).2).2 <
    ((p.1.succ, p.2).1, φ^[3 * 3 ^ p.1] (p.1.succ, p.2).2).2

State before:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p : Lex (ℕ × β)
⊢ (((p.1, φ^[3 ^ p.1] p.2).1, φ^[2 * 3 ^ (p.1, φ^[3 ^ p.1] p.2).1] p.2).1.succ,
        ((p.1, φ^[3 ^ p.1] p.2).1, φ^[2 * 3 ^ (p.1, φ^[3 ^ p.1] p.2).1] p.2).2).2 <
    ((p.1.succ, p.2).1, φ^[3 * 3 ^ p.1] (p.1.succ, p.2).2).2
Tactic:
exact h.strictMono_iterate_of_lt_map (h0 p.2)
  (Nat.mul_lt_mul_of_pos_right (Nat.lt_succ_self 2)
    (pow_pos (Nat.succ_pos 2) _))
State after:
no goals