Theorem: Container.M.bisim.lemma0 (CoInd/M.lean)

State before:
C : Container
⊢ ∀ (x : M C) (n : Nat) (i : B C (Approx.node (approx x (Nat.succ n)))) (j : B C (destruct x).fst),
    HEq i j → Approx.children (approx x (Nat.succ n)) i = approx (PSigma.snd (destruct x) j) n
Tactic:
intro x n i j heq
State after:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
⊢ Approx.children (approx x (Nat.succ n)) i = approx (PSigma.snd (destruct x) j) n

State before:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
⊢ Approx.children (approx x (Nat.succ n)) i = approx (PSigma.snd (destruct x) j) n
Tactic:
have : i = cast (by rw [node_thm]; simp [destruct]) j := by
  have : C.B x.destruct.fst = C.B (x.approx (.succ n)).node := by rw [node_thm]; simp [destruct]
  rw [Eq_from_Heq j i]
  apply HEq.symm
  assumption
State after:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : i = cast (_ : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))) j
⊢ Approx.children (approx x (Nat.succ n)) i = approx (PSigma.snd (destruct x) j) n

State before:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : i = cast (_ : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))) j
⊢ Approx.children (approx x (Nat.succ n)) i = approx (PSigma.snd (destruct x) j) n
Tactic:
simp only [this, children, Approx.node, destruct]
State after:
no goals

State before:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
⊢ B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))
Tactic:
rw [node_thm]
State after:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
⊢ B C (destruct x).fst = B C (node x)

State before:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
⊢ B C (destruct x).fst = B C (node x)
Tactic:
simp [destruct]
State after:
no goals

State before:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
⊢ i = cast (_ : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))) j
Tactic:
have : C.B x.destruct.fst = C.B (x.approx (.succ n)).node := by rw [node_thm]; simp [destruct]
State after:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))
⊢ i = cast (_ : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))) j

State before:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))
⊢ i = cast (_ : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))) j
Tactic:
rw [Eq_from_Heq j i]
State after:
case h
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))
⊢ HEq j i

State before:
case h
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))
⊢ HEq j i
Tactic:
apply HEq.symm
State after:
case h.h
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))
⊢ HEq i j

State before:
case h.h
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))
⊢ HEq i j
Tactic:
assumption
State after:
no goals