internlm/Lean-Github huggingface dataset:
Theorem: List.val_zipProof
Proof state before:
α : Type u
p : α → Prop
a : α
as : List α
h_ind : ∀ {h : forAll p as}, Subtype.val <$> zipProof as h = as
h : forAll p (a :: as)
⊢ Subtype.val <$> zipProof (a :: as) h = a :: as
Tactic:
cases h with | intro ha has =>
dsimp [Functor.map, zipProof, List.map] at *
rw [h_ind]
Proof state after:
no goals
Theorem: List.val_zipProof
Proof state before:
case intro
α : Type u
p : α → Prop
a : α
as : List α
h_ind : ∀ {h : forAll p as}, Subtype.val <$> zipProof as h = as
ha : p a
has : forAll p as
⊢ Subtype.val <$> zipProof (a :: as) (_ : p a ∧ forAll p as) = a :: as
Tactic:
dsimp [Functor.map, zipProof, List.map] at *
Proof state after:
case intro
α : Type u
p : α → Prop
a : α
as : List α
h_ind : ∀ {h : forAll p as}, map Subtype.val (zipProof as h) = as
ha : p a
has : forAll p as
⊢ a :: map Subtype.val (zipProof as has) = a :: as
Theorem: List.val_zipProof
Proof state before:
case intro
α : Type u
p : α → Prop
a : α
as : List α
h_ind : ∀ {h : forAll p as}, map Subtype.val (zipProof as h) = as
ha : p a
has : forAll p as
⊢ a :: map Subtype.val (zipProof as has) = a :: as
Tactic:
rw [h_ind]
Proof state after:
no goals
Theorem: List.SatisfiesM_List_eq
Proof state before:
α : Type u
p : α → Prop
as : List α
h : SatisfiesM p as
⊢ forAll p as
Tactic:
cases h with | intro xs hx =>
cases hx
induction xs
case nil => exact True.intro
case cons a as h_ind =>
  exact ⟨a.property, h_ind⟩
Proof state after:
no goals
Theorem: List.SatisfiesM_List_eq
Proof state before:
case intro
α : Type u
p : α → Prop
as : List α
xs : List { a // p a }
hx : Subtype.val <$> xs = as
⊢ forAll p as
Tactic:
cases hx
Proof state after:
case intro.refl
α : Type u
p : α → Prop
xs : List { a // p a }
⊢ forAll p (Subtype.val <$> xs)
Theorem: List.SatisfiesM_List_eq
Proof state before:
case intro.refl
α : Type u
p : α → Prop
xs : List { a // p a }
⊢ forAll p (Subtype.val <$> xs)
Tactic:
induction xs
Proof state after:
case intro.refl.nil
α : Type u
p : α → Prop
⊢ forAll p (Subtype.val <$> [])

case intro.refl.cons
α : Type u
p : α → Prop
head✝ : { a // p a }
tail✝ : List { a // p a }
tail_ih✝ : forAll p (Subtype.val <$> tail✝)
⊢ forAll p (Subtype.val <$> (head✝ :: tail✝))
Theorem: List.SatisfiesM_List_eq
Proof state before:
α : Type u
p : α → Prop
⊢ forAll p (Subtype.val <$> [])
Tactic:
case nil => exact True.intro
Proof state after:
no goals
Theorem: List.SatisfiesM_List_eq
Proof state before:
α : Type u
p : α → Prop
a : { a // p a }
as : List { a // p a }
h_ind : forAll p (Subtype.val <$> as)
⊢ forAll p (Subtype.val <$> (a :: as))
Tactic:
case cons a as h_ind =>
  exact ⟨a.property, h_ind⟩
Proof state after:
no goals
Theorem: List.SatisfiesM_List_eq
Proof state before:
α : Type u
p : α → Prop
⊢ forAll p (Subtype.val <$> [])
Tactic:
exact True.intro
Proof state after:
no goals
Theorem: List.SatisfiesM_List_eq
Proof state before:
α : Type u
p : α → Prop
a : { a // p a }
as : List { a // p a }
h_ind : forAll p (Subtype.val <$> as)
⊢ forAll p (Subtype.val <$> (a :: as))
Tactic:
exact ⟨a.property, h_ind⟩
Proof state after:
no goals
Theorem: List.SatisfiesM_List_eq
Proof state before:
α : Type u
p : α → Prop
as : List α
h : forAll p as
⊢ SatisfiesM p as
Tactic:
exists zipProof as h
Proof state after:
α : Type u
p : α → Prop
as : List α
h : forAll p as
⊢ Subtype.val <$> zipProof as h = as
Theorem: List.SatisfiesM_List_eq
Proof state before:
α : Type u
p : α → Prop
as : List α
h : forAll p as
⊢ Subtype.val <$> zipProof as h = as
Tactic:
exact val_zipProof as
Proof state after:
no goals
Theorem: ExceptT.map_eq_map_errorOrApply
Proof state before:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ f <$> x = errorOrApply f <$> x
Tactic:
rw [Functor.map, Applicative.toFunctor, Monad.toApplicative]
Proof state after:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ instMonadExceptT.1.1.1 f x = errorOrApply f <$> x
Theorem: ExceptT.map_eq_map_errorOrApply
Proof state before:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ instMonadExceptT.1.1.1 f x = errorOrApply f <$> x
Tactic:
unfold instMonadExceptT
Proof state after:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ Monad.mk.1.1.1 f x = errorOrApply f <$> x
Theorem: ExceptT.map_eq_map_errorOrApply
Proof state before:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ Monad.mk.1.1.1 f x = errorOrApply f <$> x
Tactic:
simp
Proof state after:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ ExceptT.map f x = errorOrApply f <$> x
Theorem: ExceptT.map_eq_map_errorOrApply
Proof state before:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ ExceptT.map f x = errorOrApply f <$> x
Tactic:
unfold ExceptT.map
Proof state after:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ (mk do
      let a ← x
      match a with
        | Except.ok a => pure (Except.ok (f a))
        | Except.error e => pure (Except.error e)) =
    errorOrApply f <$> x
Theorem: ExceptT.map_eq_map_errorOrApply
Proof state before:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ (mk do
      let a ← x
      match a with
        | Except.ok a => pure (Except.ok (f a))
        | Except.error e => pure (Except.error e)) =
    errorOrApply f <$> x
Tactic:
rw [map_eq_pure_bind]
Proof state after:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ (mk do
      let a ← x
      match a with
        | Except.ok a => pure (Except.ok (f a))
        | Except.error e => pure (Except.error e)) =
    do
    let a ← x
    pure (errorOrApply f a)
Theorem: ExceptT.map_eq_map_errorOrApply
Proof state before:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ (mk do
      let a ← x
      match a with
        | Except.ok a => pure (Except.ok (f a))
        | Except.error e => pure (Except.error e)) =
    do
    let a ← x
    pure (errorOrApply f a)
Tactic:
apply bind_congr
Proof state after:
case h
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ ∀ (a : Except ε α),
    (match a with
      | Except.ok a => pure (Except.ok (f a))
      | Except.error e => pure (Except.error e)) =
      pure (errorOrApply f a)
Theorem: ExceptT.map_eq_map_errorOrApply
Proof state before:
case h
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ ∀ (a : Except ε α),
    (match a with
      | Except.ok a => pure (Except.ok (f a))
      | Except.error e => pure (Except.error e)) =
      pure (errorOrApply f a)
Tactic:
intro e
Proof state after:
case h
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
e : Except ε α
⊢ (match e with
    | Except.ok a => pure (Except.ok (f a))
    | Except.error e => pure (Except.error e)) =
    pure (errorOrApply f e)
Theorem: ExceptT.map_eq_map_errorOrApply
Proof state before:
case h
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
e : Except ε α
⊢ (match e with
    | Except.ok a => pure (Except.ok (f a))
    | Except.error e => pure (Except.error e)) =
    pure (errorOrApply f e)
Tactic:
cases e <;> rfl
Proof state after:
no goals
Theorem: ExceptT.errorOrApply_val
Proof state before:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
p : α → Prop
⊢ errorOrApply Subtype.val = Subtype.val ∘ toSubtype
Tactic:
funext x
Proof state after:
case h
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
p : α → Prop
x : Except ε (Subtype p)
⊢ errorOrApply Subtype.val x = (Subtype.val ∘ toSubtype) x
Theorem: ExceptT.errorOrApply_val
Proof state before:
case h
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
p : α → Prop
x : Except ε (Subtype p)
⊢ errorOrApply Subtype.val x = (Subtype.val ∘ toSubtype) x
Tactic:
cases x <;> rfl
Proof state after:
no goals
Theorem: ExceptT.from_toSubtype
Proof state before:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
p : α → Prop
⊢ fromSubtype ∘ toSubtype = id
Tactic:
funext x
Proof state after:
case h
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
p : α → Prop
x : Except ε (Subtype p)
⊢ (fromSubtype ∘ toSubtype) x = id x
Theorem: ExceptT.from_toSubtype
Proof state before:
case h
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
p : α → Prop
x : Except ε (Subtype p)
⊢ (fromSubtype ∘ toSubtype) x = id x
Tactic:
cases x <;> rfl
Proof state after:
no goals
Theorem: SatisfiesM_ReaderT_eq'
Proof 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
Proof state after:
no goals
Theorem: SatisfiesM_ReaderT_eq'
Proof 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
Proof 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)
Theorem: SatisfiesM_ReaderT_eq'
Proof 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
Proof state after:
no goals
Theorem: SatisfiesM_ReaderT_eq'
Proof 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)
Proof 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
Theorem: SatisfiesM_ReaderT_eq'
Proof 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
Proof 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
Theorem: SatisfiesM_ReaderT_eq'
Proof 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]
Proof 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
Theorem: SatisfiesM_ReaderT_eq'
Proof 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]
Proof state after:
no goals
Theorem: Prod.fst_from_to_subtype
Proof state before:
α σ : Type u
p : α → Prop
⊢ fstFromSubtype ∘ fstToSubtype = id
Tactic:
funext x
Proof state after:
case h
α σ : Type u
p : α → Prop
x : Subtype p × σ
⊢ (fstFromSubtype ∘ fstToSubtype) x = id x
Theorem: Prod.fst_from_to_subtype
Proof state before:
case h
α σ : Type u
p : α → Prop
x : Subtype p × σ
⊢ (fstFromSubtype ∘ fstToSubtype) x = id x
Tactic:
cases x
Proof state after:
case h.mk
α σ : Type u
p : α → Prop
fst✝ : Subtype p
snd✝ : σ
⊢ (fstFromSubtype ∘ fstToSubtype) (fst✝, snd✝) = id (fst✝, snd✝)
Theorem: Prod.fst_from_to_subtype
Proof state before:
case h.mk
α σ : Type u
p : α → Prop
fst✝ : Subtype p
snd✝ : σ
⊢ (fstFromSubtype ∘ fstToSubtype) (fst✝, snd✝) = id (fst✝, snd✝)
Tactic:
rfl
Proof state after:
no goals
Theorem: Prod.map_val_id
Proof state before:
α σ : Type u
p : α → Prop
⊢ map Subtype.val id = Subtype.val ∘ fstToSubtype
Tactic:
funext x
Proof state after:
case h
α σ : Type u
p : α → Prop
x : Subtype p × σ
⊢ map Subtype.val id x = (Subtype.val ∘ fstToSubtype) x
Theorem: Prod.map_val_id
Proof state before:
case h
α σ : Type u
p : α → Prop
x : Subtype p × σ
⊢ map Subtype.val id x = (Subtype.val ∘ fstToSubtype) x
Tactic:
cases x
Proof state after:
case h.mk
α σ : Type u
p : α → Prop
fst✝ : Subtype p
snd✝ : σ
⊢ map Subtype.val id (fst✝, snd✝) = (Subtype.val ∘ fstToSubtype) (fst✝, snd✝)
Theorem: Prod.map_val_id
Proof state before:
case h.mk
α σ : Type u
p : α → Prop
fst✝ : Subtype p
snd✝ : σ
⊢ map Subtype.val id (fst✝, snd✝) = (Subtype.val ∘ fstToSubtype) (fst✝, snd✝)
Tactic:
rfl
Proof state after:
no goals
Theorem: SatisfiesM_StateT_eq'
Proof 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
Proof state after:
no goals
Theorem: SatisfiesM_StateT_eq'
Proof 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
Proof 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)
Theorem: SatisfiesM_StateT_eq'
Proof 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
Proof 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
Theorem: SatisfiesM_StateT_eq'
Proof 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]
Proof 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)
Theorem: SatisfiesM_StateT_eq'
Proof 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]
Proof 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
Theorem: SatisfiesM_StateT_eq'
Proof 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
Proof 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)
Theorem: SatisfiesM_StateT_eq'
Proof 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
Proof 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)
Theorem: SatisfiesM_StateT_eq'
Proof 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
Proof state after:
no goals
Theorem: SatisfiesM_StateT_eq'
Proof 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)
Proof 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
Theorem: SatisfiesM_StateT_eq'
Proof 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
Proof 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
Theorem: SatisfiesM_StateT_eq'
Proof 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
Proof 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
Theorem: SatisfiesM_StateT_eq'
Proof 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]
Proof 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
Theorem: SatisfiesM_StateT_eq'
Proof 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]
Proof 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
Theorem: SatisfiesM_StateT_eq'
Proof 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
Proof 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
Theorem: SatisfiesM_StateT_eq'
Proof 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
Proof 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
Theorem: SatisfiesM_StateT_eq'
Proof 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)]
Proof state after:
no goals