Theorem: SubtypeT.deq_of_iff (Dijkstra/Control/Monad/Reify.lean)

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p q : Pred α
hpq : ∀ (a : α), p a ↔ q a
⊢ ∀ (x : SubtypeT m α p), DEq (SubtypeT m α) x (weaken (_ : ∀ (a : α), p a → q a) x)
Tactic:
have : p = q := funext (λ a => propext (hpq a))
State after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p q : Pred α
hpq : ∀ (a : α), p a ↔ q a
this : p = q
⊢ ∀ (x : SubtypeT m α p), DEq (SubtypeT m α) x (weaken (_ : ∀ (a : α), p a → q a) x)

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p q : Pred α
hpq : ∀ (a : α), p a ↔ q a
this : p = q
⊢ ∀ (x : SubtypeT m α p), DEq (SubtypeT m α) x (weaken (_ : ∀ (a : α), p a → q a) x)
Tactic:
cases this
State after:
case refl
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p : Pred α
hpq : ∀ (a : α), p a ↔ p a
⊢ ∀ (x : SubtypeT m α p), DEq (SubtypeT m α) x (weaken (_ : ∀ (a : α), p a → p a) x)

State before:
case refl
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p : Pred α
hpq : ∀ (a : α), p a ↔ p a
⊢ ∀ (x : SubtypeT m α p), DEq (SubtypeT m α) x (weaken (_ : ∀ (a : α), p a → p a) x)
Tactic:
intro x
State after:
case refl
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p : Pred α
hpq : ∀ (a : α), p a ↔ p a
x : SubtypeT m α p
⊢ DEq (SubtypeT m α) x (weaken (_ : ∀ (a : α), p a → p a) x)

State before:
case refl
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p : Pred α
hpq : ∀ (a : α), p a ↔ p a
x : SubtypeT m α p
⊢ DEq (SubtypeT m α) x (weaken (_ : ∀ (a : α), p a → p a) x)
Tactic:
apply DEq.deq_of_eq
State after:
case refl.a
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p : Pred α
hpq : ∀ (a : α), p a ↔ p a
x : SubtypeT m α p
⊢ x = weaken (_ : ∀ (a : α), p a → p a) x

State before:
case refl.a
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p : Pred α
hpq : ∀ (a : α), p a ↔ p a
x : SubtypeT m α p
⊢ x = weaken (_ : ∀ (a : α), p a → p a) x
Tactic:
conv =>
  rhs; dsimp [weaken]; congr
  . skip
  . ext a; change pure a
State after:
case refl.a
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p : Pred α
hpq : ∀ (a : α), p a ↔ p a
x : SubtypeT m α p
⊢ x = do
    let a ← x
    pure a

State before:
case refl.a
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p : Pred α
hpq : ∀ (a : α), p a ↔ p a
x : SubtypeT m α p
⊢ x = do
    let a ← x
    pure a
Tactic:
rw [bind_pure]
State after:
no goals