internlm/Lean-Github huggingface dataset:
Theorem: Container.M.bisim.lemma1
Proof state before:
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
x y : M C
n : Nat
h₁ : R x y
⊢ approx x n = approx y n
Tactic:
induction n generalizing x y
Proof state after:
case zero
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
x y : M C
h₁ : R x y
⊢ approx x Nat.zero = approx y Nat.zero

case succ
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n✝ : Nat
n_ih✝ : ∀ (x y : M C), R x y → approx x n✝ = approx y n✝
x y : M C
h₁ : R x y
⊢ approx x (Nat.succ n✝) = approx y (Nat.succ n✝)
Theorem: Container.M.bisim.lemma1
Proof state before:
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
x y : M C
h₁ : R x y
⊢ approx x Nat.zero = approx y Nat.zero
Tactic:
case zero =>
  cases x.approx 0
  cases y.approx 0
  rfl
Proof state after:
no goals
Theorem: Container.M.bisim.lemma1
Proof state before:
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
⊢ approx x (Nat.succ n) = approx y (Nat.succ n)
Tactic:
case succ n h =>
  have h₂ := x.node_thm n
  have h₃ := y.node_thm n
  cases h₄: x.approx (.succ n) with
  | MStep nodex cx =>
    cases h₅: y.approx (.succ n) with
    | MStep nodey cy =>
      have ⟨node, k₁, k₂, eq₁, eq₂, kR⟩ := h₀ _ _ h₁
      have h₂ : (Approx.MStep nodex cx).node = node := by
        have := congrArg (λ x => x.1) eq₁
        simp only [destruct] at this
        rw [h₄] at h₂
        rw [←this]
        exact h₂
      have h₃ : (Approx.MStep nodey cy).node = node := by
        have := congrArg (λ x => x.1) eq₂
        simp only [destruct] at this
        rw [h₅] at h₃
        rw [←this]
        exact h₃
      simp [Approx.node] at h₂ h₃
      have h₂ := Eq.symm h₂
      have h₃ := Eq.symm h₃
      have h₆ := bisim.lemma0 x n
      have h₇ := bisim.lemma0 y n
      rw [h₄] at h₆
      rw [h₅] at h₇
      simp only [Approx.children] at h₇ h₆
      induction h₂
      induction h₃
      suffices h₈ : ∀ i: C.B node, cx i = cy i by
        have : cx = cy := by
          funext i
          apply h₈
        rw [this]
      intro i
      have h₆ : ∀ i, cx i = (k₁ i).approx n := by
        have h : ∀ i j, HEq i j → (x.destruct.snd i) = k₁ j := by
          rw [eq₁]
          intro i j heq
          cases heq
          rfl
        intro i
        rw [h₆ i (cast (by simp [congrArg (λ x => x.1) eq₁]) i)]
        . rw [h]
          apply cast_heq
        . apply HEq.symm
          apply cast_heq
      have h₇ : ∀ i, cy i = (k₂ i).approx n := by
        have h : ∀ i j, HEq i j → (y.destruct.snd i) = k₂ j := by
          rw [eq₂]
          intro i j heq
          cases heq
          rfl
        intro i
        rw [h₇ i (cast (by simp [congrArg (λ x => x.1) eq₂]) i)]
        . rw [h]
          apply cast_heq
        . apply HEq.symm
          apply cast_heq
      rw [h₆, h₇]
      apply h
      apply kR
Proof state after:
no goals
Theorem: Container.M.bisim.lemma1
Proof state before:
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
x y : M C
h₁ : R x y
⊢ approx x Nat.zero = approx y Nat.zero
Tactic:
cases x.approx 0
Proof state after:
case MStop
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
x y : M C
h₁ : R x y
⊢ Approx.MStop = approx y Nat.zero
Theorem: Container.M.bisim.lemma1
Proof state before:
case MStop
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
x y : M C
h₁ : R x y
⊢ Approx.MStop = approx y Nat.zero
Tactic:
cases y.approx 0
Proof state after:
case MStop.MStop
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
x y : M C
h₁ : R x y
⊢ Approx.MStop = Approx.MStop
Theorem: Container.M.bisim.lemma1
Proof state before:
case MStop.MStop
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
x y : M C
h₁ : R x y
⊢ Approx.MStop = Approx.MStop
Tactic:
rfl
Proof state after:
no goals
Theorem: Container.M.bisim.lemma1
Proof state before:
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
⊢ approx x (Nat.succ n) = approx y (Nat.succ n)
Tactic:
have h₂ := x.node_thm n
Proof state after:
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂ : Approx.node (approx x (Nat.succ n)) = node x
⊢ approx x (Nat.succ n) = approx y (Nat.succ n)
Theorem: Container.M.bisim.lemma1
Proof state before:
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂ : Approx.node (approx x (Nat.succ n)) = node x
⊢ approx x (Nat.succ n) = approx y (Nat.succ n)
Tactic:
have h₃ := y.node_thm n
Proof state after:
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂ : Approx.node (approx x (Nat.succ n)) = node x
h₃ : Approx.node (approx y (Nat.succ n)) = node y
⊢ approx x (Nat.succ n) = approx y (Nat.succ n)
Theorem: Container.M.bisim.lemma1
Proof state before:
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂ : Approx.node (approx x (Nat.succ n)) = node x
h₃ : Approx.node (approx y (Nat.succ n)) = node y
⊢ approx x (Nat.succ n) = approx y (Nat.succ n)
Tactic:
cases h₄: x.approx (.succ n) with
| MStep nodex cx =>
  cases h₅: y.approx (.succ n) with
  | MStep nodey cy =>
    have ⟨node, k₁, k₂, eq₁, eq₂, kR⟩ := h₀ _ _ h₁
    have h₂ : (Approx.MStep nodex cx).node = node := by
      have := congrArg (λ x => x.1) eq₁
      simp only [destruct] at this
      rw [h₄] at h₂
      rw [←this]
      exact h₂
    have h₃ : (Approx.MStep nodey cy).node = node := by
      have := congrArg (λ x => x.1) eq₂
      simp only [destruct] at this
      rw [h₅] at h₃
      rw [←this]
      exact h₃
    simp [Approx.node] at h₂ h₃
    have h₂ := Eq.symm h₂
    have h₃ := Eq.symm h₃
    have h₆ := bisim.lemma0 x n
    have h₇ := bisim.lemma0 y n
    rw [h₄] at h₆
    rw [h₅] at h₇
    simp only [Approx.children] at h₇ h₆
    induction h₂
    induction h₃
    suffices h₈ : ∀ i: C.B node, cx i = cy i by
      have : cx = cy := by
        funext i
        apply h₈
      rw [this]
    intro i
    have h₆ : ∀ i, cx i = (k₁ i).approx n := by
      have h : ∀ i j, HEq i j → (x.destruct.snd i) = k₁ j := by
        rw [eq₁]
        intro i j heq
        cases heq
        rfl
      intro i
      rw [h₆ i (cast (by simp [congrArg (λ x => x.1) eq₁]) i)]
      . rw [h]
        apply cast_heq
      . apply HEq.symm
        apply cast_heq
    have h₇ : ∀ i, cy i = (k₂ i).approx n := by
      have h : ∀ i j, HEq i j → (y.destruct.snd i) = k₂ j := by
        rw [eq₂]
        intro i j heq
        cases heq
        rfl
      intro i
      rw [h₇ i (cast (by simp [congrArg (λ x => x.1) eq₂]) i)]
      . rw [h]
        apply cast_heq
      . apply HEq.symm
        apply cast_heq
    rw [h₆, h₇]
    apply h
    apply kR
Proof state after:
no goals
Theorem: Container.M.bisim.lemma1
Proof state before:
case MStep
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂ : Approx.node (approx x (Nat.succ n)) = node x
h₃ : Approx.node (approx y (Nat.succ n)) = node y
nodex : C.A
cx : B C nodex → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep nodex cx
⊢ Approx.MStep nodex cx = approx y (Nat.succ n)
Tactic:
cases h₅: y.approx (.succ n) with
| MStep nodey cy =>
  have ⟨node, k₁, k₂, eq₁, eq₂, kR⟩ := h₀ _ _ h₁
  have h₂ : (Approx.MStep nodex cx).node = node := by
    have := congrArg (λ x => x.1) eq₁
    simp only [destruct] at this
    rw [h₄] at h₂
    rw [←this]
    exact h₂
  have h₃ : (Approx.MStep nodey cy).node = node := by
    have := congrArg (λ x => x.1) eq₂
    simp only [destruct] at this
    rw [h₅] at h₃
    rw [←this]
    exact h₃
  simp [Approx.node] at h₂ h₃
  have h₂ := Eq.symm h₂
  have h₃ := Eq.symm h₃
  have h₆ := bisim.lemma0 x n
  have h₇ := bisim.lemma0 y n
  rw [h₄] at h₆
  rw [h₅] at h₇
  simp only [Approx.children] at h₇ h₆
  induction h₂
  induction h₃
  suffices h₈ : ∀ i: C.B node, cx i = cy i by
    have : cx = cy := by
      funext i
      apply h₈
    rw [this]
  intro i
  have h₆ : ∀ i, cx i = (k₁ i).approx n := by
    have h : ∀ i j, HEq i j → (x.destruct.snd i) = k₁ j := by
      rw [eq₁]
      intro i j heq
      cases heq
      rfl
    intro i
    rw [h₆ i (cast (by simp [congrArg (λ x => x.1) eq₁]) i)]
    . rw [h]
      apply cast_heq
    . apply HEq.symm
      apply cast_heq
  have h₇ : ∀ i, cy i = (k₂ i).approx n := by
    have h : ∀ i j, HEq i j → (y.destruct.snd i) = k₂ j := by
      rw [eq₂]
      intro i j heq
      cases heq
      rfl
    intro i
    rw [h₇ i (cast (by simp [congrArg (λ x => x.1) eq₂]) i)]
    . rw [h]
      apply cast_heq
    . apply HEq.symm
      apply cast_heq
  rw [h₆, h₇]
  apply h
  apply kR
Proof state after:
no goals
Theorem: Container.M.bisim.lemma1
Proof state before:
case MStep.MStep
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂ : Approx.node (approx x (Nat.succ n)) = node x
h₃ : Approx.node (approx y (Nat.succ n)) = node y
nodex : C.A
cx : B C nodex → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep nodex cx
nodey : C.A
cy : B C nodey → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep nodey cy
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Tactic:
have ⟨node, k₁, k₂, eq₁, eq₂, kR⟩ := h₀ _ _ h₁
Proof state after:
case MStep.MStep
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex : C.A
cx : B C nodex → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep nodex cx
nodey : C.A
cy : B C nodey → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep nodey cy
node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Theorem: Container.M.bisim.lemma1
Proof state before:
case MStep.MStep
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex : C.A
cx : B C nodex → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep nodex cx
nodey : C.A
cy : B C nodey → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep nodey cy
node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Tactic:
have h₂ : (Approx.MStep nodex cx).node = node := by
  have := congrArg (λ x => x.1) eq₁
  simp only [destruct] at this
  rw [h₄] at h₂
  rw [←this]
  exact h₂
Proof state after:
case MStep.MStep
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex : C.A
cx : B C nodex → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep nodex cx
nodey : C.A
cy : B C nodey → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep nodey cy
node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
h₂ : Approx.node (Approx.MStep nodex cx) = node
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Theorem: Container.M.bisim.lemma1
Proof state before:
case MStep.MStep
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex : C.A
cx : B C nodex → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep nodex cx
nodey : C.A
cy : B C nodey → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep nodey cy
node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
h₂ : Approx.node (Approx.MStep nodex cx) = node
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Tactic:
have h₃ : (Approx.MStep nodey cy).node = node := by
  have := congrArg (λ x => x.1) eq₂
  simp only [destruct] at this
  rw [h₅] at h₃
  rw [←this]
  exact h₃
Proof state after:
case MStep.MStep
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex : C.A
cx : B C nodex → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep nodex cx
nodey : C.A
cy : B C nodey → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep nodey cy
node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
h₂ : Approx.node (Approx.MStep nodex cx) = node
h₃ : Approx.node (Approx.MStep nodey cy) = node
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Theorem: Container.M.bisim.lemma1
Proof state before:
case MStep.MStep
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex : C.A
cx : B C nodex → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep nodex cx
nodey : C.A
cy : B C nodey → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep nodey cy
node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
h₂ : Approx.node (Approx.MStep nodex cx) = node
h₃ : Approx.node (Approx.MStep nodey cy) = node
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Tactic:
simp [Approx.node] at h₂ h₃
Proof state after:
case MStep.MStep
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex : C.A
cx : B C nodex → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep nodex cx
nodey : C.A
cy : B C nodey → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep nodey cy
node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
h₂ : nodex = node
h₃ : nodey = node
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Theorem: Container.M.bisim.lemma1
Proof state before:
case MStep.MStep
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex : C.A
cx : B C nodex → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep nodex cx
nodey : C.A
cy : B C nodey → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep nodey cy
node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
h₂ : nodex = node
h₃ : nodey = node
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Tactic:
have h₂ := Eq.symm h₂
Proof state after:
case MStep.MStep
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝¹ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex : C.A
cx : B C nodex → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep nodex cx
nodey : C.A
cy : B C nodey → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep nodey cy
node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
h₂✝ : nodex = node
h₃ : nodey = node
h₂ : node = nodex
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Theorem: Container.M.bisim.lemma1
Proof state before:
case MStep.MStep
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝¹ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex : C.A
cx : B C nodex → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep nodex cx
nodey : C.A
cy : B C nodey → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep nodey cy
node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
h₂✝ : nodex = node
h₃ : nodey = node
h₂ : node = nodex
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Tactic:
have h₃ := Eq.symm h₃
Proof state after:
case MStep.MStep
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝¹ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝¹ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex : C.A
cx : B C nodex → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep nodex cx
nodey : C.A
cy : B C nodey → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep nodey cy
node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
h₂✝ : nodex = node
h₃✝ : nodey = node
h₂ : node = nodex
h₃ : node = nodey
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy