Theorem: Except.bind_eq_ok (FOL/Except.lean)

State before:
ε α β : Type
x : Except ε α
f : α → Except ε β
a : β
⊢ x.bind f = ok a ↔ ∃ b, x = ok b ∧ f b = ok a
Tactic:
cases x
State after:
case error
ε α β : Type
f : α → Except ε β
a : β
a✝ : ε
⊢ (error a✝).bind f = ok a ↔ ∃ b, error a✝ = ok b ∧ f b = ok a

case ok
ε α β : Type
f : α → Except ε β
a : β
a✝ : α
⊢ (ok a✝).bind f = ok a ↔ ∃ b, ok a✝ = ok b ∧ f b = ok a

State before:
ε α β : Type
f : α → Except ε β
a : β
x : ε
⊢ (error x).bind f = ok a ↔ ∃ b, error x = ok b ∧ f b = ok a
Tactic:
case error x =>
  simp only [Except.bind]
  simp
State after:
no goals

State before:
ε α β : Type
f : α → Except ε β
a : β
x : α
⊢ (ok x).bind f = ok a ↔ ∃ b, ok x = ok b ∧ f b = ok a
Tactic:
case ok x =>
  simp only [Except.bind]
  simp
State after:
no goals

State before:
ε α β : Type
f : α → Except ε β
a : β
x : ε
⊢ (error x).bind f = ok a ↔ ∃ b, error x = ok b ∧ f b = ok a
Tactic:
simp only [Except.bind]
State after:
ε α β : Type
f : α → Except ε β
a : β
x : ε
⊢ False ↔ ∃ b, False ∧ f b = ok a

State before:
ε α β : Type
f : α → Except ε β
a : β
x : ε
⊢ False ↔ ∃ b, False ∧ f b = ok a
Tactic:
simp
State after:
no goals

State before:
ε α β : Type
f : α → Except ε β
a : β
x : α
⊢ (ok x).bind f = ok a ↔ ∃ b, ok x = ok b ∧ f b = ok a
Tactic:
simp only [Except.bind]
State after:
ε α β : Type
f : α → Except ε β
a : β
x : α
⊢ f x = ok a ↔ ∃ b, ok x = ok b ∧ f b = ok a

State before:
ε α β : Type
f : α → Except ε β
a : β
x : α
⊢ f x = ok a ↔ ∃ b, ok x = ok b ∧ f b = ok a
Tactic:
simp
State after:
no goals

State before:
ε α β : Type
x : Except ε α
f : α → Except ε β
a : β
⊢ x.bind f = ok a ↔ ∃ b, x = ok b ∧ f b = ok a
Tactic:
cases x
State after:
case error
ε α β : Type
f : α → Except ε β
a : β
a✝ : ε
⊢ (error a✝).bind f = ok a ↔ ∃ b, error a✝ = ok b ∧ f b = ok a

case ok
ε α β : Type
f : α → Except ε β
a : β
a✝ : α
⊢ (ok a✝).bind f = ok a ↔ ∃ b, ok a✝ = ok b ∧ f b = ok a

State before:
ε α β : Type
f : α → Except ε β
a : β
x : ε
⊢ (error x).bind f = ok a ↔ ∃ b, error x = ok b ∧ f b = ok a
Tactic:
case error x =>
  simp only [Except.bind]
  simp
State after:
no goals

State before:
ε α β : Type
f : α → Except ε β
a : β
x : α
⊢ (ok x).bind f = ok a ↔ ∃ b, ok x = ok b ∧ f b = ok a
Tactic:
case ok x =>
  simp only [Except.bind]
  simp
State after:
no goals

State before:
ε α β : Type
f : α → Except ε β
a : β
x : ε
⊢ (error x).bind f = ok a ↔ ∃ b, error x = ok b ∧ f b = ok a
Tactic:
simp only [Except.bind]
State after:
ε α β : Type
f : α → Except ε β
a : β
x : ε
⊢ False ↔ ∃ b, False ∧ f b = ok a

State before:
ε α β : Type
f : α → Except ε β
a : β
x : ε
⊢ False ↔ ∃ b, False ∧ f b = ok a
Tactic:
simp
State after:
no goals

State before:
ε α β : Type
f : α → Except ε β
a : β
x : α
⊢ (ok x).bind f = ok a ↔ ∃ b, ok x = ok b ∧ f b = ok a
Tactic:
simp only [Except.bind]
State after:
ε α β : Type
f : α → Except ε β
a : β
x : α
⊢ f x = ok a ↔ ∃ b, ok x = ok b ∧ f b = ok a

State before:
ε α β : Type
f : α → Except ε β
a : β
x : α
⊢ f x = ok a ↔ ∃ b, ok x = ok b ∧ f b = ok a
Tactic:
simp
State after:
no goals