Theorem: Imo2022P2.amgm (Compfiles/Imo2022P2.lean)

State before:
a b : ℝ+
⊢ ⟨2, ⋯⟩ ≤ a / b + b / a
Tactic:
change 2 ≤ a.val/b.val + b.val/a.val
State after:
a b : ℝ+
⊢ 2 ≤ ↑a / ↑b + ↑b / ↑a

State before:
a b : ℝ+
⊢ 2 ≤ ↑a / ↑b + ↑b / ↑a
Tactic:
obtain ⟨a, ha⟩ := a
State after:
case mk
b : ℝ+
a : ℝ
ha : 0 < a
⊢ 2 ≤ ↑⟨a, ha⟩ / ↑b + ↑b / ↑⟨a, ha⟩

State before:
case mk
b : ℝ+
a : ℝ
ha : 0 < a
⊢ 2 ≤ ↑⟨a, ha⟩ / ↑b + ↑b / ↑⟨a, ha⟩
Tactic:
obtain ⟨b, hb⟩ := b
State after:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
⊢ 2 ≤ ↑⟨a, ha⟩ / ↑⟨b, hb⟩ + ↑⟨b, hb⟩ / ↑⟨a, ha⟩

State before:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
⊢ 2 ≤ ↑⟨a, ha⟩ / ↑⟨b, hb⟩ + ↑⟨b, hb⟩ / ↑⟨a, ha⟩
Tactic:
dsimp only
State after:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
⊢ 2 ≤ a / b + b / a

State before:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
⊢ 2 ≤ a / b + b / a
Tactic:
field_simp
State after:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
⊢ 2 ≤ (a * a + b * b) / (b * a)

State before:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
⊢ 2 ≤ (a * a + b * b) / (b * a)
Tactic:
have h1 : 0 < b * a := Real.mul_pos hb ha
State after:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 2 ≤ (a * a + b * b) / (b * a)

State before:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 2 ≤ (a * a + b * b) / (b * a)
Tactic:
suffices H : 2 * (b * a) ≤ a * a + b * b by exact (le_div_iff h1).mpr H
State after:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 2 * (b * a) ≤ a * a + b * b

State before:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 2 * (b * a) ≤ a * a + b * b
Tactic:
suffices H : 0 ≤ (a - b)^2 by linarith
State after:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 0 ≤ (a - b) ^ 2

State before:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 0 ≤ (a - b) ^ 2
Tactic:
exact sq_nonneg (a - b)
State after:
no goals

State before:
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
H : 2 * (b * a) ≤ a * a + b * b
⊢ 2 ≤ (a * a + b * b) / (b * a)
Tactic:
exact (le_div_iff h1).mpr H
State after:
no goals

State before:
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
H : 0 ≤ (a - b) ^ 2
⊢ 2 * (b * a) ≤ a * a + b * b
Tactic:
linarith
State after:
no goals