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

State before:
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
x : StateT ρ m α
h : SatisfiesM p x
s : ρ
⊢ SatisfiesM (fun x => p x.fst) (x s)
Tactic:
cases h with | intro w hw =>
cases hw
exists Prod.fstToSubtype (p:=p) <$> w s
dsimp [Functor.map, StateT.map]
rw [←comp_map, ←map_eq_pure_bind]
apply map_congr
intro x; rfl
State after:
no goals

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

State before:
case intro.refl
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
s : ρ
w : StateT ρ m { a // p a }
⊢ SatisfiesM (fun x => p x.fst) ((Subtype.val <$> w) s)
Tactic:
exists Prod.fstToSubtype (p:=p) <$> w s
State after:
case intro.refl
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
s : ρ
w : StateT ρ m { a // p a }
⊢ Subtype.val <$> Prod.fstToSubtype <$> w s = (Subtype.val <$> w) s

State before:
case intro.refl
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
s : ρ
w : StateT ρ m { a // p a }
⊢ Subtype.val <$> Prod.fstToSubtype <$> w s = (Subtype.val <$> w) s
Tactic:
dsimp [Functor.map, StateT.map]
State after:
case intro.refl
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
s : ρ
w : StateT ρ m { a // p a }
⊢ Subtype.val <$> Prod.fstToSubtype <$> w s = do
    let __discr ← w s
    pure (__discr.fst.val, __discr.snd)

State before:
case intro.refl
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
s : ρ
w : StateT ρ m { a // p a }
⊢ Subtype.val <$> Prod.fstToSubtype <$> w s = do
    let __discr ← w s
    pure (__discr.fst.val, __discr.snd)
Tactic:
rw [←comp_map, ←map_eq_pure_bind]
State after:
case intro.refl
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
s : ρ
w : StateT ρ m { a // p a }
⊢ (Subtype.val ∘ Prod.fstToSubtype) <$> w s = (fun __discr => (__discr.fst.val, __discr.snd)) <$> w s

State before:
case intro.refl
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
s : ρ
w : StateT ρ m { a // p a }
⊢ (Subtype.val ∘ Prod.fstToSubtype) <$> w s = (fun __discr => (__discr.fst.val, __discr.snd)) <$> w s
Tactic:
apply map_congr
State after:
case intro.refl.h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
s : ρ
w : StateT ρ m { a // p a }
⊢ ∀ (a : Subtype p × ρ), (Subtype.val ∘ Prod.fstToSubtype) a = (a.fst.val, a.snd)

State before:
case intro.refl.h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
s : ρ
w : StateT ρ m { a // p a }
⊢ ∀ (a : Subtype p × ρ), (Subtype.val ∘ Prod.fstToSubtype) a = (a.fst.val, a.snd)
Tactic:
intro x
State after:
case intro.refl.h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
s : ρ
w : StateT ρ m { a // p a }
x : Subtype p × ρ
⊢ (Subtype.val ∘ Prod.fstToSubtype) x = (x.fst.val, x.snd)

State before:
case intro.refl.h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
s : ρ
w : StateT ρ m { a // p a }
x : Subtype p × ρ
⊢ (Subtype.val ∘ Prod.fstToSubtype) x = (x.fst.val, x.snd)
Tactic:
rfl
State after:
no goals

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

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

State before:
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
x : StateT ρ m α
h : ∀ (s : ρ), SatisfiesM (fun x => p x.fst) (x s)
⊢ ∀ (x_1 : ρ),
    (Subtype.val <$> fun s =>
          Prod.fstFromSubtype <$> SubregFunctor.ensureF (x s) (_ : SatisfiesM (fun x => p x.fst) (x s)))
        x_1 =
      x x_1
Tactic:
intro s
State after:
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
x : StateT ρ m α
h : ∀ (s : ρ), SatisfiesM (fun x => p x.fst) (x s)
s : ρ
⊢ (Subtype.val <$> fun s =>
        Prod.fstFromSubtype <$> SubregFunctor.ensureF (x s) (_ : SatisfiesM (fun x => p x.fst) (x s)))
      s =
    x s

State before:
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
x : StateT ρ m α
h : ∀ (s : ρ), SatisfiesM (fun x => p x.fst) (x s)
s : ρ
⊢ (Subtype.val <$> fun s =>
        Prod.fstFromSubtype <$> SubregFunctor.ensureF (x s) (_ : SatisfiesM (fun x => p x.fst) (x s)))
      s =
    x s
Tactic:
dsimp [Functor.map, StateT.map]
State after:
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
x : StateT ρ m α
h : ∀ (s : ρ), SatisfiesM (fun x => p x.fst) (x s)
s : ρ
⊢ (do
      let __discr ← Prod.fstFromSubtype <$> SubregFunctor.ensureF (x s) (_ : SatisfiesM (fun x => p x.fst) (x s))
      pure (__discr.fst.val, __discr.snd)) =
    x s

State before:
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
x : StateT ρ m α
h : ∀ (s : ρ), SatisfiesM (fun x => p x.fst) (x s)
s : ρ
⊢ (do
      let __discr ← Prod.fstFromSubtype <$> SubregFunctor.ensureF (x s) (_ : SatisfiesM (fun x => p x.fst) (x s))
      pure (__discr.fst.val, __discr.snd)) =
    x s
Tactic:
rw [←map_eq_pure_bind, ←comp_map]
State after:
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
x : StateT ρ m α
h : ∀ (s : ρ), SatisfiesM (fun x => p x.fst) (x s)
s : ρ
⊢ ((fun __discr => (__discr.fst.val, __discr.snd)) ∘ Prod.fstFromSubtype) <$>
      SubregFunctor.ensureF (x s) (_ : SatisfiesM (fun x => p x.fst) (x s)) =
    x s

State before:
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
x : StateT ρ m α
h : ∀ (s : ρ), SatisfiesM (fun x => p x.fst) (x s)
s : ρ
⊢ ((fun __discr => (__discr.fst.val, __discr.snd)) ∘ Prod.fstFromSubtype) <$>
      SubregFunctor.ensureF (x s) (_ : SatisfiesM (fun x => p x.fst) (x s)) =
    x s
Tactic:
conv =>
  lhs; lhs; ext as; dsimp [Prod.map]; change as.val
State after:
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
x : StateT ρ m α
h : ∀ (s : ρ), SatisfiesM (fun x => p x.fst) (x s)
s : ρ
⊢ (fun as => as.val) <$> SubregFunctor.ensureF (x s) (_ : SatisfiesM (fun x => p x.fst) (x s)) = x s

State before:
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
x : StateT ρ m α
h : ∀ (s : ρ), SatisfiesM (fun x => p x.fst) (x s)
s : ρ
⊢ (fun as => as.val) <$> SubregFunctor.ensureF (x s) (_ : SatisfiesM (fun x => p x.fst) (x s)) = x s
Tactic:
conv => lhs; lhs; change Subtype.val
State after:
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
α ρ : Type u
p : α → Prop
x : StateT ρ m α
h : ∀ (s : ρ), SatisfiesM (fun x => p x.fst) (x s)
s : ρ
⊢ Subtype.val <$> SubregFunctor.ensureF (x s) (_ : SatisfiesM (fun x => p x.fst) (x s)) = x s

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