Theorem: EStateM.SatisfiesM_EStateM_eq (Dijkstra/Control/Functor/Subreg.lean)

State before:
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
hx : SatisfiesM p x
s : σ
a : α
x✝ : σ
⊢ x s = Result.ok a x✝ → p a
Tactic:
cases hx with | intro w hw =>
cases hw
dsimp [Functor.map, EStateM.map]
cases w s <;> intro h
case ok a s' => exact (Result.ok.inj h).left ▸ a.property
case error e s' => cases h
State after:
no goals

State before:
case intro
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
hw : Subtype.val <$> w = x
⊢ x s = Result.ok a x✝ → p a
Tactic:
cases hw
State after:
case intro.refl
ε σ α : Type u
p : α → Prop
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
⊢ (Subtype.val <$> w) s = Result.ok a x✝ → p a

State before:
case intro.refl
ε σ α : Type u
p : α → Prop
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
⊢ (Subtype.val <$> w) s = Result.ok a x✝ → p a
Tactic:
dsimp [Functor.map, EStateM.map]
State after:
case intro.refl
ε σ α : Type u
p : α → Prop
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
⊢ (match w s with
      | Result.ok a s => Result.ok a.val s
      | Result.error e s => Result.error e s) =
      Result.ok a x✝ →
    p a

State before:
case intro.refl
ε σ α : Type u
p : α → Prop
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
⊢ (match w s with
      | Result.ok a s => Result.ok a.val s
      | Result.error e s => Result.error e s) =
      Result.ok a x✝ →
    p a
Tactic:
cases w s <;> intro h
State after:
case intro.refl.ok
ε σ α : Type u
p : α → Prop
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
a✝¹ : { a // p a }
a✝ : σ
h :
  (match Result.ok a✝¹ a✝ with
    | Result.ok a s => Result.ok a.val s
    | Result.error e s => Result.error e s) =
    Result.ok a x✝
⊢ p a

case intro.refl.error
ε σ α : Type u
p : α → Prop
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
a✝¹ : ε
a✝ : σ
h :
  (match Result.error a✝¹ a✝ with
    | Result.ok a s => Result.ok a.val s
    | Result.error e s => Result.error e s) =
    Result.ok a x✝
⊢ p a

State before:
ε σ α : Type u
p : α → Prop
s : σ
a✝ : α
x✝ : σ
w : EStateM ε σ { a // p a }
a : { a // p a }
s' : σ
h :
  (match Result.ok a s' with
    | Result.ok a s => Result.ok a.val s
    | Result.error e s => Result.error e s) =
    Result.ok a✝ x✝
⊢ p a✝
Tactic:
case ok a s' => exact (Result.ok.inj h).left ▸ a.property
State after:
no goals

State before:
ε σ α : Type u
p : α → Prop
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
e : ε
s' : σ
h :
  (match Result.error e s' with
    | Result.ok a s => Result.ok a.val s
    | Result.error e s => Result.error e s) =
    Result.ok a x✝
⊢ p a
Tactic:
case error e s' => cases h
State after:
no goals

State before:
ε σ α : Type u
p : α → Prop
s : σ
a✝ : α
x✝ : σ
w : EStateM ε σ { a // p a }
a : { a // p a }
s' : σ
h :
  (match Result.ok a s' with
    | Result.ok a s => Result.ok a.val s
    | Result.error e s => Result.error e s) =
    Result.ok a✝ x✝
⊢ p a✝
Tactic:
exact (Result.ok.inj h).left ▸ a.property
State after:
no goals

State before:
ε σ α : Type u
p : α → Prop
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
e : ε
s' : σ
h :
  (match Result.error e s' with
    | Result.ok a s => Result.ok a.val s
    | Result.error e s => Result.error e s) =
    Result.ok a x✝
⊢ p a
Tactic:
cases h
State after:
no goals

State before:
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
h : ∀ (s : σ) (a : α) (s' : σ), x s = Result.ok a s' → p a
⊢ SatisfiesM p x
Tactic:
exists λ s => (x s).zipProof (h s)
State after:
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
h : ∀ (s : σ) (a : α) (s' : σ), x s = Result.ok a s' → p a
⊢ (Subtype.val <$> fun s => Result.zipProof (x s) (_ : ∀ (a : α) (s' : σ), x s = Result.ok a s' → p a)) = x

State before:
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
h : ∀ (s : σ) (a : α) (s' : σ), x s = Result.ok a s' → p a
⊢ (Subtype.val <$> fun s => Result.zipProof (x s) (_ : ∀ (a : α) (s' : σ), x s = Result.ok a s' → p a)) = x
Tactic:
funext s
State after:
case h
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
h : ∀ (s : σ) (a : α) (s' : σ), x s = Result.ok a s' → p a
s : σ
⊢ (Subtype.val <$> fun s => Result.zipProof (x s) (_ : ∀ (a : α) (s' : σ), x s = Result.ok a s' → p a)) s = x s

State before:
case h
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
h : ∀ (s : σ) (a : α) (s' : σ), x s = Result.ok a s' → p a
s : σ
⊢ (Subtype.val <$> fun s => Result.zipProof (x s) (_ : ∀ (a : α) (s' : σ), x s = Result.ok a s' → p a)) s = x s
Tactic:
dsimp [Functor.map, EStateM.map]
State after:
case h
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
h : ∀ (s : σ) (a : α) (s' : σ), x s = Result.ok a s' → p a
s : σ
⊢ (match Result.zipProof (x s) (_ : ∀ (a : α) (s' : σ), x s = Result.ok a s' → p a) with
    | Result.ok a s => Result.ok a.val s
    | Result.error e s => Result.error e s) =
    x s

State before:
case h
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
h : ∀ (s : σ) (a : α) (s' : σ), x s = Result.ok a s' → p a
s : σ
⊢ (match Result.zipProof (x s) (_ : ∀ (a : α) (s' : σ), x s = Result.ok a s' → p a) with
    | Result.ok a s => Result.ok a.val s
    | Result.error e s => Result.error e s) =
    x s
Tactic:
conv =>
  lhs; change Result.map (Subtype.val (p:=p)) ((x s).zipProof (h s))
  rw [Result.map_val_zipProof]
State after:
no goals