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

State before:
a : ℝ+
⊢ a + a = ⟨2, ⋯⟩ * a
Tactic:
obtain ⟨a, ha⟩ := a
State after:
case mk
a : ℝ
ha : 0 < a
⊢ ⟨a, ha⟩ + ⟨a, ha⟩ = ⟨2, ⋯⟩ * ⟨a, ha⟩

State before:
case mk
a : ℝ
ha : 0 < a
⊢ ⟨a, ha⟩ + ⟨a, ha⟩ = ⟨2, ⋯⟩ * ⟨a, ha⟩
Tactic:
apply Subtype.val_injective
State after:
case mk.a
a : ℝ
ha : 0 < a
⊢ ↑(⟨a, ha⟩ + ⟨a, ha⟩) = ↑(⟨2, ⋯⟩ * ⟨a, ha⟩)

State before:
case mk.a
a : ℝ
ha : 0 < a
⊢ ↑(⟨a, ha⟩ + ⟨a, ha⟩) = ↑(⟨2, ⋯⟩ * ⟨a, ha⟩)
Tactic:
dsimp
State after:
case mk.a
a : ℝ
ha : 0 < a
⊢ a + a = 2 * a

State before:
case mk.a
a : ℝ
ha : 0 < a
⊢ a + a = 2 * a
Tactic:
exact (two_mul a).symm
State after:
no goals