Theorem: Imo2008P4.PosReal.mul_two (Compfiles/Imo2008P4.lean)

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

State before:
case mk
x : ℝ
hx : 0 < x
⊢ ⟨x, hx⟩ * ⟨2, ⋯⟩ = ⟨x, hx⟩ + ⟨x, hx⟩
Tactic:
rw [Subtype.ext_iff]
State after:
case mk
x : ℝ
hx : 0 < x
⊢ ↑(⟨x, hx⟩ * ⟨2, ⋯⟩) = ↑(⟨x, hx⟩ + ⟨x, hx⟩)

State before:
case mk
x : ℝ
hx : 0 < x
⊢ ↑(⟨x, hx⟩ * ⟨2, ⋯⟩) = ↑(⟨x, hx⟩ + ⟨x, hx⟩)
Tactic:
simp [_root_.mul_two]
State after:
no goals