Theorem: Decidable.prop_eq_of_decide_eq (Table/BuiltinExtensions.lean)

State before:
p q : Prop
ip : Decidable p
iq : Decidable q
h : p = q
⊢ decide p = decide q
Tactic:
cases h
State after:
case refl
p : Prop
ip iq : Decidable p
⊢ decide p = decide p

State before:
case refl
p : Prop
ip iq : Decidable p
⊢ decide p = decide p
Tactic:
apply congr
State after:
case refl.h₁
p : Prop
ip iq : Decidable p
⊢ @decide p = @decide p

case refl.h₂
p : Prop
ip iq : Decidable p
⊢ ip = iq

State before:
case refl.h₁
p : Prop
ip iq : Decidable p
⊢ @decide p = @decide p

case refl.h₂
p : Prop
ip iq : Decidable p
⊢ ip = iq
Tactic:
. simp
State after:
case refl.h₂
p : Prop
ip iq : Decidable p
⊢ ip = iq

State before:
case refl.h₂
p : Prop
ip iq : Decidable p
⊢ ip = iq
Tactic:
. apply eq_of_heq
  apply Subsingleton.helim
  rfl
State after:
no goals

State before:
case refl.h₁
p : Prop
ip iq : Decidable p
⊢ @decide p = @decide p
Tactic:
simp
State after:
no goals

State before:
case refl.h₂
p : Prop
ip iq : Decidable p
⊢ ip = iq
Tactic:
apply eq_of_heq
State after:
case refl.h₂.h
p : Prop
ip iq : Decidable p
⊢ HEq ip iq

State before:
case refl.h₂.h
p : Prop
ip iq : Decidable p
⊢ HEq ip iq
Tactic:
apply Subsingleton.helim
State after:
case refl.h₂.h.h₂
p : Prop
ip iq : Decidable p
⊢ Decidable p = Decidable p

State before:
case refl.h₂.h.h₂
p : Prop
ip iq : Decidable p
⊢ Decidable p = Decidable p
Tactic:
rfl
State after:
no goals