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

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

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

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