Theorem: invert_toReal (Ray/Hartogs/FubiniBall.lean)

State before:
x : ENNReal
y : ℝ
yp : y > 0
⊢ x.toReal = y → x = ENNReal.ofReal y
Tactic:
intro h
State after:
x : ENNReal
y : ℝ
yp : y > 0
h : x.toReal = y
⊢ x = ENNReal.ofReal y

State before:
x : ENNReal
y : ℝ
yp : y > 0
h : x.toReal = y
⊢ x = ENNReal.ofReal y
Tactic:
rw [← h]
State after:
x : ENNReal
y : ℝ
yp : y > 0
h : x.toReal = y
⊢ x = ENNReal.ofReal x.toReal

State before:
x : ENNReal
y : ℝ
yp : y > 0
h : x.toReal = y
⊢ x = ENNReal.ofReal x.toReal
Tactic:
refine (ENNReal.ofReal_toReal ?_).symm
State after:
x : ENNReal
y : ℝ
yp : y > 0
h : x.toReal = y
⊢ x ≠ ⊤

State before:
x : ENNReal
y : ℝ
yp : y > 0
h : x.toReal = y
⊢ x ≠ ⊤
Tactic:
contrapose yp
State after:
x : ENNReal
y : ℝ
h : x.toReal = y
yp : ¬x ≠ ⊤
⊢ ¬y > 0

State before:
x : ENNReal
y : ℝ
h : x.toReal = y
yp : ¬x ≠ ⊤
⊢ ¬y > 0
Tactic:
simp only [ne_eq, not_not] at yp
State after:
x : ENNReal
y : ℝ
h : x.toReal = y
yp : x = ⊤
⊢ ¬y > 0

State before:
x : ENNReal
y : ℝ
h : x.toReal = y
yp : x = ⊤
⊢ ¬y > 0
Tactic:
simp only [yp, ENNReal.top_toReal] at h
State after:
x : ENNReal
y : ℝ
yp : x = ⊤
h : 0 = y
⊢ ¬y > 0

State before:
x : ENNReal
y : ℝ
yp : x = ⊤
h : 0 = y
⊢ ¬y > 0
Tactic:
simp only [← h, lt_self_iff_false, not_false_eq_true]
State after:
no goals