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

State before:
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
⊢ map (fun x => b) f = const (ids f) b
Tactic:
ext1 a
State after:
case h
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
⊢ map (fun x => b) f a = const (ids f) b a

State before:
case h
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
⊢ map (fun x => b) f a = const (ids f) b a
Tactic:
simp [const, map_val, ids]
State after:
case h
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
⊢ Option.map (fun x => b) (f a) = if ∃ b, f a = some b then some b else none

State before:
case h
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
⊢ Option.map (fun x => b) (f a) = if ∃ b, f a = some b then some b else none
Tactic:
split <;> simp [Option.map]
State after:
case h.inl
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h✝ : ∃ b, f a = some b
⊢ (match f a with
    | some x => some b
    | none => none) =
    some b

case h.inr
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h✝ : ¬∃ b, f a = some b
⊢ (match f a with
    | some x => some b
    | none => none) =
    none

State before:
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h : ∃ b, f a = some b
⊢ (match f a with
    | some x => some b
    | none => none) =
    some b
Tactic:
case inl h => have ⟨_, h⟩ := h; simp [h]
State after:
no goals

State before:
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h : ¬∃ b, f a = some b
⊢ (match f a with
    | some x => some b
    | none => none) =
    none
Tactic:
case inr h =>
  cases hb : f a <;> simp
  case some b => push_neg at h; have := hb ▸ h b; contradiction
State after:
no goals

State before:
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h : ∃ b, f a = some b
⊢ (match f a with
    | some x => some b
    | none => none) =
    some b
Tactic:
have ⟨_, h⟩ := h
State after:
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h✝ : ∃ b, f a = some b
w✝ : β
h : f a = some w✝
⊢ (match f a with
    | some x => some b
    | none => none) =
    some b

State before:
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h✝ : ∃ b, f a = some b
w✝ : β
h : f a = some w✝
⊢ (match f a with
    | some x => some b
    | none => none) =
    some b
Tactic:
simp [h]
State after:
no goals

State before:
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h : ¬∃ b, f a = some b
⊢ (match f a with
    | some x => some b
    | none => none) =
    none
Tactic:
cases hb : f a <;> simp
State after:
case some
α : Type u_1
β b✝ : Type u_2
f : α ⇀ β
b : b✝
a : α
h : ¬∃ b, f a = some b
val✝ : β
hb : f a = some val✝
⊢ False

State before:
α : Type u_1
β b✝¹ : Type u_2
f : α ⇀ β
b✝ : b✝¹
a : α
h : ¬∃ b, f a = some b
b : β
hb : f a = some b
⊢ False
Tactic:
case some b => push_neg at h; have := hb ▸ h b; contradiction
State after:
no goals

State before:
α : Type u_1
β b✝¹ : Type u_2
f : α ⇀ β
b✝ : b✝¹
a : α
h : ¬∃ b, f a = some b
b : β
hb : f a = some b
⊢ False
Tactic:
push_neg at h
State after:
α : Type u_1
β b✝¹ : Type u_2
f : α ⇀ β
b✝ : b✝¹
a : α
b : β
hb : f a = some b
h : ∀ (b : β), f a ≠ some b
⊢ False

State before:
α : Type u_1
β b✝¹ : Type u_2
f : α ⇀ β
b✝ : b✝¹
a : α
b : β
hb : f a = some b
h : ∀ (b : β), f a ≠ some b
⊢ False
Tactic:
have := hb ▸ h b
State after:
α : Type u_1
β b✝¹ : Type u_2
f : α ⇀ β
b✝ : b✝¹
a : α
b : β
hb : f a = some b
h : ∀ (b : β), f a ≠ some b
this : some b ≠ some b
⊢ False

State before:
α : Type u_1
β b✝¹ : Type u_2
f : α ⇀ β
b✝ : b✝¹
a : α
b : β
hb : f a = some b
h : ∀ (b : β), f a ≠ some b
this : some b ≠ some b
⊢ False
Tactic:
contradiction
State after:
no goals