Theorem: SciLean.AutoImpl.impl_eq_spec (SciLean/Core/old/Meta/RewriteBy.lean)

State before:
α✝ : Type u_1
a : α✝
x : AutoImpl a
⊢ a = val x
Tactic:
cases x
State after:
case exact
α✝ : Type u_1
a a✝ : α✝
h✝ : a✝ = a
⊢ a = val (AutoExactSolution.exact a✝ h✝)

State before:
case exact
α✝ : Type u_1
a a✝ : α✝
h✝ : a✝ = a
⊢ a = val (AutoExactSolution.exact a✝ h✝)
Tactic:
rename_i a' h
State after:
case exact
α✝ : Type u_1
a a' : α✝
h : a' = a
⊢ a = val (AutoExactSolution.exact a' h)

State before:
case exact
α✝ : Type u_1
a a' : α✝
h : a' = a
⊢ a = val (AutoExactSolution.exact a' h)
Tactic:
simp[AutoImpl.val, val, h]
State after:
no goals