Theorem: Cpdt.Chapter7.Computation.bind_fun_computation (Cpdt/Chapter7/DomainTheory.lean)

State before:
α β : Type
m1 : Computation α
m2 : α → Computation β
⊢ ∀ (n : Nat) (v : β), bind_fun m1 m2 n = some v → ∀ (n' : Nat), n' ≥ n → bind_fun m1 m2 n' = some v
Tactic:
intro n v h1 n' h
State after:
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
h1 : bind_fun m1 m2 n = some v
n' : Nat
h : n' ≥ n
⊢ bind_fun m1 m2 n' = some v

State before:
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
h1 : bind_fun m1 m2 n = some v
n' : Nat
h : n' ≥ n
⊢ bind_fun m1 m2 n' = some v
Tactic:
cases h2 : m1.val n with
| none => simp_all[bind_fun]
| some x =>
  simp_all[bind_fun]
  have m1_n'_runs : m1.val n' = some x := m1.property n x h2 n' h
  have m2_n'_runs : (m2 x).val n' = some v := (m2 x).property n v h1 n' h
  simp[m1_n'_runs, m2_n'_runs]
State after:
no goals

State before:
case none
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
h1 : bind_fun m1 m2 n = some v
n' : Nat
h : n' ≥ n
h2 : Subtype.val m1 n = none
⊢ bind_fun m1 m2 n' = some v
Tactic:
simp_all[bind_fun]
State after:
no goals

State before:
case some
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
h1 : bind_fun m1 m2 n = some v
n' : Nat
h : n' ≥ n
x : α
h2 : Subtype.val m1 n = some x
⊢ bind_fun m1 m2 n' = some v
Tactic:
simp_all[bind_fun]
State after:
case some
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
n' : Nat
x : α
h1 : Subtype.val (m2 x) n = some v
h : n' ≥ n
h2 : Subtype.val m1 n = some x
⊢ (match Subtype.val m1 n' with
    | none => none
    | some a => Subtype.val (m2 a) n') =
    some v

State before:
case some
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
n' : Nat
x : α
h1 : Subtype.val (m2 x) n = some v
h : n' ≥ n
h2 : Subtype.val m1 n = some x
⊢ (match Subtype.val m1 n' with
    | none => none
    | some a => Subtype.val (m2 a) n') =
    some v
Tactic:
have m1_n'_runs : m1.val n' = some x := m1.property n x h2 n' h
State after:
case some
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
n' : Nat
x : α
h1 : Subtype.val (m2 x) n = some v
h : n' ≥ n
h2 : Subtype.val m1 n = some x
m1_n'_runs : Subtype.val m1 n' = some x
⊢ (match Subtype.val m1 n' with
    | none => none
    | some a => Subtype.val (m2 a) n') =
    some v

State before:
case some
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
n' : Nat
x : α
h1 : Subtype.val (m2 x) n = some v
h : n' ≥ n
h2 : Subtype.val m1 n = some x
m1_n'_runs : Subtype.val m1 n' = some x
⊢ (match Subtype.val m1 n' with
    | none => none
    | some a => Subtype.val (m2 a) n') =
    some v
Tactic:
have m2_n'_runs : (m2 x).val n' = some v := (m2 x).property n v h1 n' h
State after:
case some
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
n' : Nat
x : α
h1 : Subtype.val (m2 x) n = some v
h : n' ≥ n
h2 : Subtype.val m1 n = some x
m1_n'_runs : Subtype.val m1 n' = some x
m2_n'_runs : Subtype.val (m2 x) n' = some v
⊢ (match Subtype.val m1 n' with
    | none => none
    | some a => Subtype.val (m2 a) n') =
    some v

State before:
case some
α β : Type
m1 : Computation α
m2 : α → Computation β
n : Nat
v : β
n' : Nat
x : α
h1 : Subtype.val (m2 x) n = some v
h : n' ≥ n
h2 : Subtype.val m1 n = some x
m1_n'_runs : Subtype.val m1 n' = some x
m2_n'_runs : Subtype.val (m2 x) n' = some v
⊢ (match Subtype.val m1 n' with
    | none => none
    | some a => Subtype.val (m2 a) n') =
    some v
Tactic:
simp[m1_n'_runs, m2_n'_runs]
State after:
no goals