Theorem: SatisfiesM_ReaderT_eq' (Dijkstra/Control/Functor/Subreg.lean)

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : SubregFunctor m
ρ α : Type u
p : α → Prop
x : ReaderT ρ m α
h : SatisfiesM p x
s : ρ
⊢ SatisfiesM p (x s)
Tactic:
cases h with | intro x h =>
cases h
exists x s
State after:
no goals

State before:
case intro
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : SubregFunctor m
ρ α : Type u
p : α → Prop
x✝ : ReaderT ρ m α
s : ρ
x : ReaderT ρ m { a // p a }
h : Subtype.val <$> x = x✝
⊢ SatisfiesM p (x✝ s)
Tactic:
cases h
State after:
case intro.refl
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : SubregFunctor m
ρ α : Type u
p : α → Prop
s : ρ
x : ReaderT ρ m { a // p a }
⊢ SatisfiesM p ((Subtype.val <$> x) s)

State before:
case intro.refl
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : SubregFunctor m
ρ α : Type u
p : α → Prop
s : ρ
x : ReaderT ρ m { a // p a }
⊢ SatisfiesM p ((Subtype.val <$> x) s)
Tactic:
exists x s
State after:
no goals

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : SubregFunctor m
ρ α : Type u
p : α → Prop
x : ReaderT ρ m α
h : ∀ (s : ρ), SatisfiesM p (x s)
⊢ SatisfiesM p x
Tactic:
exists λ s => SubregFunctor.ensureF (f:=m) (x s) (h s)
State after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : SubregFunctor m
ρ α : Type u
p : α → Prop
x : ReaderT ρ m α
h : ∀ (s : ρ), SatisfiesM p (x s)
⊢ (Subtype.val <$> fun s => SubregFunctor.ensureF (x s) (_ : SatisfiesM p (x s))) = x

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : SubregFunctor m
ρ α : Type u
p : α → Prop
x : ReaderT ρ m α
h : ∀ (s : ρ), SatisfiesM p (x s)
⊢ (Subtype.val <$> fun s => SubregFunctor.ensureF (x s) (_ : SatisfiesM p (x s))) = x
Tactic:
funext s
State after:
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : SubregFunctor m
ρ α : Type u
p : α → Prop
x : ReaderT ρ m α
h : ∀ (s : ρ), SatisfiesM p (x s)
s : ρ
⊢ (Subtype.val <$> fun s => SubregFunctor.ensureF (x s) (_ : SatisfiesM p (x s))) s = x s

State before:
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : SubregFunctor m
ρ α : Type u
p : α → Prop
x : ReaderT ρ m α
h : ∀ (s : ρ), SatisfiesM p (x s)
s : ρ
⊢ (Subtype.val <$> fun s => SubregFunctor.ensureF (x s) (_ : SatisfiesM p (x s))) s = x s
Tactic:
dsimp [Functor.map]
State after:
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : SubregFunctor m
ρ α : Type u
p : α → Prop
x : ReaderT ρ m α
h : ∀ (s : ρ), SatisfiesM p (x s)
s : ρ
⊢ Subtype.val <$> SubregFunctor.ensureF (x s) (_ : SatisfiesM p (x s)) = x s

State before:
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : SubregFunctor m
ρ α : Type u
p : α → Prop
x : ReaderT ρ m α
h : ∀ (s : ρ), SatisfiesM p (x s)
s : ρ
⊢ Subtype.val <$> SubregFunctor.ensureF (x s) (_ : SatisfiesM p (x s)) = x s
Tactic:
rw [SubregFunctor.val_ensureF]
State after:
no goals