[GOAL]
α : Type u
a b : Thunk α
eq : Thunk.get a = Thunk.get b
⊢ a = b
[PROOFSTEP]
have ⟨_⟩ := a
[GOAL]
α : Type u
a b : Thunk α
fn✝ : Unit → α
eq : Thunk.get { fn := fn✝ } = Thunk.get b
⊢ { fn := fn✝ } = b
[PROOFSTEP]
have ⟨_⟩ := b
[GOAL]
α : Type u
a b : Thunk α
fn✝¹ fn✝ : Unit → α
eq : Thunk.get { fn := fn✝¹ } = Thunk.get { fn := fn✝ }
⊢ { fn := fn✝¹ } = { fn := fn✝ }
[PROOFSTEP]
congr
[GOAL]
case e_fn
α : Type u
a b : Thunk α
fn✝¹ fn✝ : Unit → α
eq : Thunk.get { fn := fn✝¹ } = Thunk.get { fn := fn✝ }
⊢ fn✝¹ = fn✝
[PROOFSTEP]
exact funext fun _ ↦ eq
[GOAL]
α : Type u
inst✝ : DecidableEq α
⊢ DecidableEq (Thunk α)
[PROOFSTEP]
intro a b
[GOAL]
α : Type u
inst✝ : DecidableEq α
a b : Thunk α
⊢ Decidable (a = b)
[PROOFSTEP]
have : a = b ↔ a.get = b.get := ⟨by intro x; rw [x], by intro; ext; assumption⟩
[GOAL]
α : Type u
inst✝ : DecidableEq α
a b : Thunk α
⊢ a = b → Thunk.get a = Thunk.get b
[PROOFSTEP]
intro x
[GOAL]
α : Type u
inst✝ : DecidableEq α
a b : Thunk α
x : a = b
⊢ Thunk.get a = Thunk.get b
[PROOFSTEP]
rw [x]
[GOAL]
α : Type u
inst✝ : DecidableEq α
a b : Thunk α
⊢ Thunk.get a = Thunk.get b → a = b
[PROOFSTEP]
intro
[GOAL]
α : Type u
inst✝ : DecidableEq α
a b : Thunk α
a✝ : Thunk.get a = Thunk.get b
⊢ a = b
[PROOFSTEP]
ext
[GOAL]
case eq
α : Type u
inst✝ : DecidableEq α
a b : Thunk α
a✝ : Thunk.get a = Thunk.get b
⊢ Thunk.get a = Thunk.get b
[PROOFSTEP]
assumption
[GOAL]
α : Type u
inst✝ : DecidableEq α
a b : Thunk α
this : a = b ↔ Thunk.get a = Thunk.get b
⊢ Decidable (a = b)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u
inst✝ : DecidableEq α
a b : Thunk α
this : a = b ↔ Thunk.get a = Thunk.get b
⊢ Decidable (Thunk.get a = Thunk.get b)
[PROOFSTEP]
infer_instance
