Theorem: Smt.Reconstruct.Arith.arithTransExpZero (Smt/Reconstruct/Arith/TransFns/ArithTransExpZero.lean)

State before:
t : ℝ
⊢ t = 0 ↔ t.exp = 1
Tactic:
apply Iff.intro
State after:
case mp
t : ℝ
⊢ t = 0 → t.exp = 1

case mpr
t : ℝ
⊢ t.exp = 1 → t = 0

State before:
case mp
t : ℝ
⊢ t = 0 → t.exp = 1
Tactic:
intro h
State after:
case mp
t : ℝ
h : t = 0
⊢ t.exp = 1

State before:
case mp
t : ℝ
h : t = 0
⊢ t.exp = 1
Tactic:
rw [h]
State after:
case mp
t : ℝ
h : t = 0
⊢ Real.exp 0 = 1

State before:
case mp
t : ℝ
h : t = 0
⊢ Real.exp 0 = 1
Tactic:
simp
State after:
no goals

State before:
case mpr
t : ℝ
⊢ t.exp = 1 → t = 0
Tactic:
intro h
State after:
case mpr
t : ℝ
h : t.exp = 1
⊢ t = 0

State before:
case mpr
t : ℝ
h : t.exp = 1
⊢ t = 0
Tactic:
simp at h
State after:
case mpr
t : ℝ
h : t = 0
⊢ t = 0

State before:
case mpr
t : ℝ
h : t = 0
⊢ t = 0
Tactic:
assumption
State after:
no goals