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

State before:
α : Type u
a b : α
h : AutoImpl a = AutoImpl b
⊢ val (Eq.mpr h finish) = b
Tactic:
have h' : a = b := by apply AutoImpl.injectivity_axiom; apply h
State after:
α : Type u
a b : α
h : AutoImpl a = AutoImpl b
h' : a = b
⊢ val (Eq.mpr h finish) = b

State before:
α : Type u
a b : α
h : AutoImpl a = AutoImpl b
h' : a = b
⊢ val (Eq.mpr h finish) = b
Tactic:
revert h
State after:
α : Type u
a b : α
h' : a = b
⊢ ∀ (h : AutoImpl a = AutoImpl b), val (Eq.mpr h finish) = b

State before:
α : Type u
a b : α
h' : a = b
⊢ ∀ (h : AutoImpl a = AutoImpl b), val (Eq.mpr h finish) = b
Tactic:
rw[h']
State after:
α : Type u
a b : α
h' : a = b
⊢ ∀ (h : AutoImpl b = AutoImpl b), val (Eq.mpr h finish) = b

State before:
α : Type u
a b : α
h' : a = b
⊢ ∀ (h : AutoImpl b = AutoImpl b), val (Eq.mpr h finish) = b
Tactic:
simp[val,finish,Eq.mpr]
State after:
no goals

State before:
α : Type u
a b : α
h : AutoImpl a = AutoImpl b
⊢ a = b
Tactic:
apply AutoImpl.injectivity_axiom
State after:
case a
α : Type u
a b : α
h : AutoImpl a = AutoImpl b
⊢ AutoImpl a = AutoImpl b

State before:
case a
α : Type u
a b : α
h : AutoImpl a = AutoImpl b
⊢ AutoImpl a = AutoImpl b
Tactic:
apply h
State after:
no goals