-- Mathlib/.lake/packages/batteries/Batteries/Classes/SatisfiesM.lean
theorem SatisfiesM_EStateM_eq :
    SatisfiesM (m := EStateM ε σ) p x ↔ ∀ s a s', x.run s = .ok a s' → p a

Proof state:
case mpr.refine_2.h
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
w : ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a
s : σ
⊢ (Subtype.val <$> fun s =>
          match q : x.run s with
          | EStateM.Result.ok a s' => EStateM.Result.ok ⟨a, ⋯⟩ s'
          | EStateM.Result.error e s' => EStateM.Result.error e s').run
      s =
    x.run s

Tactic:
rw [EStateM.run_map, EStateM.run]

Result:
case mpr.refine_2.h
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
w : ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a
s : σ
⊢ EStateM.Result.map Subtype.val
      (match q : x.run s with
      | EStateM.Result.ok a s' => EStateM.Result.ok ⟨a, ⋯⟩ s'
      | EStateM.Result.error e s' => EStateM.Result.error e s') =
    x.run s

Proof state:
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ { a // p a }
s : σ
a✝ : α✝
s'✝ : σ
a : { a // p a }
s' : σ
w : x.run s = EStateM.Result.ok a s'
h : ∃ x_1, x.run s = EStateM.Result.ok ⟨a✝, ⋯⟩ s'✝
⊢ p a✝

Tactic:
exact h.1

Result:
no goals

Proof state:
case mpr
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
w : ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a
⊢ SatisfiesM p x

Tactic:
refine ⟨?_, ?_⟩

Result:
case mpr.refine_1
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
w : ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a
⊢ EStateM ε σ { a // p a }

case mpr.refine_2
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
w : ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a
⊢ Subtype.val <$> ?mpr.refine_1 = x

Proof state:
case mp
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
⊢ SatisfiesM p x → ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a

Tactic:
rintro ⟨x, rfl⟩ s a s' h

Result:
case mp.intro
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ { a // p a }
s : σ
a : α✝
s' : σ
h : (Subtype.val <$> x).run s = EStateM.Result.ok a s'
⊢ p a

Proof state:
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ { a // p a }
s : σ
a✝ : α✝
s'✝ : σ
h : (Subtype.val <$> x).run s = EStateM.Result.ok a✝ s'✝
a : { a // p a }
s' : σ
w : x.run s = EStateM.Result.ok a s'
⊢ p a✝

Tactic:
simp at h

Result:
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ { a // p a }
s : σ
a✝ : α✝
s'✝ : σ
a : { a // p a }
s' : σ
w : x.run s = EStateM.Result.ok a s'
h : ∃ x_1, x.run s = EStateM.Result.ok ⟨a✝, ⋯⟩ s'✝
⊢ p a✝

Proof state:
case mp.intro
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ { a // p a }
s : σ
a : α✝
s' : σ
h : (Subtype.val <$> x).run s = EStateM.Result.ok a s'
⊢ p a

Tactic:
match w : x.run s with
| .ok a s' => simp at h; exact h.1
| .error e s' => simp [w] at h

Result:
no goals

Proof state:
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ { a // p a }
s : σ
a : α✝
s'✝ : σ
h : (Subtype.val <$> x).run s = EStateM.Result.ok a s'✝
e : ε
s' : σ
w : x.run s = EStateM.Result.error e s'
⊢ p a

Tactic:
simp [w] at h

Result:
no goals

Proof state:
case mpr.refine_2.h
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
w : ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a
s : σ
⊢ EStateM.Result.map Subtype.val
      (match q : x.run s with
      | EStateM.Result.ok a s' => EStateM.Result.ok ⟨a, ⋯⟩ s'
      | EStateM.Result.error e s' => EStateM.Result.error e s') =
    x.run s

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
⊢ SatisfiesM p x ↔ ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a

Tactic:
constructor

Result:
case mp
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
⊢ SatisfiesM p x → ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a

case mpr
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
⊢ (∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a) → SatisfiesM p x

Proof state:
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
w : ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a
s : σ
a : α✝
s' : σ
q : x.run s = EStateM.Result.ok a s'
⊢ EStateM.Result ε σ { a // p a }

Tactic:
exact .ok ⟨a, w s a s' q⟩ s'

Result:
no goals

Proof state:
case mpr.refine_2
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
w : ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a
⊢ (Subtype.val <$> fun s =>
      match q : x.run s with
      | EStateM.Result.ok a s' => EStateM.Result.ok ⟨a, ⋯⟩ s'
      | EStateM.Result.error e s' => EStateM.Result.error e s') =
    x

Tactic:
ext s

Result:
case mpr.refine_2.h
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
w : ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a
s : σ
⊢ (Subtype.val <$> fun s =>
          match q : x.run s with
          | EStateM.Result.ok a s' => EStateM.Result.ok ⟨a, ⋯⟩ s'
          | EStateM.Result.error e s' => EStateM.Result.error e s').run
      s =
    x.run s

Proof state:
case mpr
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
⊢ (∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a) → SatisfiesM p x

Tactic:
intro w

Result:
case mpr
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
w : ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a
⊢ SatisfiesM p x

Proof state:
case mpr.refine_1
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
w : ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a
s : σ
⊢ EStateM.Result ε σ { a // p a }

Tactic:
match q : x.run s with
| .ok a s' => exact .ok ⟨a, w s a s' q⟩ s'
| .error e s' => exact .error e s'

Result:
no goals

Proof state:
case mpr.refine_1
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
w : ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a
⊢ EStateM ε σ { a // p a }

Tactic:
intro s

Result:
case mpr.refine_1
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
w : ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a
s : σ
⊢ EStateM.Result ε σ { a // p a }

Proof state:
ε σ α✝ : Type u_1
p : α✝ → Prop
x : EStateM ε σ α✝
w : ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a
s : σ
e : ε
s' : σ
q : x.run s = EStateM.Result.error e s'
⊢ EStateM.Result ε σ { a // p a }

Tactic:
exact .error e s'

Result:
no goals