Theorem: Partial.attach_map_val (ReactorModel/Extensions.lean)

State before:
α : Sort u_1
β : Type u_2
f : α ⇀ β
⊢ map Subtype.val (attach f) = f
Tactic:
funext a
State after:
case h
α : Sort u_1
β : Type u_2
f : α ⇀ β
a : α
⊢ map Subtype.val (attach f) a = f a

State before:
case h
α : Sort u_1
β : Type u_2
f : α ⇀ β
a : α
⊢ map Subtype.val (attach f) a = f a
Tactic:
simp [map, Option.map, attach]
State after:
case h
α : Sort u_1
β : Type u_2
f : α ⇀ β
a : α
⊢ (match
      match h : f a with
      | none => none
      | some b => some { val := b, property := ⋯ } with
    | some x => some ↑x
    | none => none) =
    f a

State before:
case h
α : Sort u_1
β : Type u_2
f : α ⇀ β
a : α
⊢ (match
      match h : f a with
      | none => none
      | some b => some { val := b, property := ⋯ } with
    | some x => some ↑x
    | none => none) =
    f a
Tactic:
split <;> split at * <;> simp_all
State after:
case h.h_1.h_2
α : Sort u_1
β : Type u_2
f : α ⇀ β
a : α
opt✝ : Option { b // ∃ a, f a = some b }
x✝ : { b // ∃ a, f a = some b }
b✝ : β
heq✝¹ : f a = some b✝
heq✝ : { val := b✝, property := ⋯ } = x✝
⊢ ↑x✝ = b✝

State before:
α : Sort u_1
β : Type u_2
f : α ⇀ β
a : α
opt✝ : Option { b // ∃ a, f a = some b }
x✝ : { b // ∃ a, f a = some b }
b✝ : β
heq✝ : f a = some b✝
h : { val := b✝, property := ⋯ } = x✝
⊢ ↑x✝ = b✝
Tactic:
case _ h => simp [←h]
State after:
no goals

State before:
α : Sort u_1
β : Type u_2
f : α ⇀ β
a : α
opt✝ : Option { b // ∃ a, f a = some b }
x✝ : { b // ∃ a, f a = some b }
b✝ : β
heq✝ : f a = some b✝
h : { val := b✝, property := ⋯ } = x✝
⊢ ↑x✝ = b✝
Tactic:
simp [←h]
State after:
no goals