internlm/Lean-Github huggingface dataset:
Theorem: Container.M.bisim.lemma1
Proof state before:
case MStep.MStep.refl.refl
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 nodey 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)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i : B C node
⊢ cx i = cy i
Tactic:
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
Proof state after:
case MStep.MStep.refl.refl
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 nodey 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)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
⊢ cx i = cy i
Theorem: Container.M.bisim.lemma1
Proof state before:
case MStep.MStep.refl.refl
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 nodey 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)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
⊢ cx i = cy i
Tactic:
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
Proof state after:
case MStep.MStep.refl.refl
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 nodey 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)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
h₇ : ∀ (i : B C node), cy i = approx (k₂ i) n
⊢ cx i = cy i
Theorem: Container.M.bisim.lemma1
Proof state before:
case MStep.MStep.refl.refl
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 nodey 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)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
h₇ : ∀ (i : B C node), cy i = approx (k₂ i) n
⊢ cx i = cy i
Tactic:
rw [h₆, h₇]
Proof state after:
case MStep.MStep.refl.refl
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 nodey 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)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
h₇ : ∀ (i : B C node), cy i = approx (k₂ i) n
⊢ approx (k₁ i) n = approx (k₂ i) n
Theorem: Container.M.bisim.lemma1
Proof state before:
case MStep.MStep.refl.refl
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 nodey 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)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
h₇ : ∀ (i : B C node), cy i = approx (k₂ i) n
⊢ approx (k₁ i) n = approx (k₂ i) n
Tactic:
apply h
Proof state after:
case MStep.MStep.refl.refl.h₁
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 nodey 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)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
h₇ : ∀ (i : B C node), cy i = approx (k₂ i) n
⊢ R (k₁ i) (k₂ i)
Theorem: Container.M.bisim.lemma1
Proof state before:
case MStep.MStep.refl.refl.h₁
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 nodey 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)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
h₇ : ∀ (i : B C node), cy i = approx (k₂ i) n
⊢ R (k₁ i) (k₂ i)
Tactic:
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)
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.node (Approx.MStep nodex cx) = node
Tactic:
have := congrArg (λ x => x.1) eq₁
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)) = 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)
this : (fun x => x.fst) (destruct x) = (fun x => x.fst) { fst := node, snd := k₁ }
⊢ Approx.node (Approx.MStep nodex cx) = node
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)) = 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)
this : (fun x => x.fst) (destruct x) = (fun x => x.fst) { fst := node, snd := k₁ }
⊢ Approx.node (Approx.MStep nodex cx) = node
Tactic:
simp only [destruct] at this
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)) = 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)
this : Container.M.node x = node
⊢ Approx.node (Approx.MStep nodex cx) = node
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)) = 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)
this : Container.M.node x = node
⊢ Approx.node (Approx.MStep nodex cx) = node
Tactic:
rw [h₄] at h₂
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 y (Nat.succ n)) = Container.M.node y
nodex : C.A
cx : B C nodex → Approx C n
h₂ : Approx.node (Approx.MStep nodex cx) = Container.M.node x
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)
this : Container.M.node x = node
⊢ Approx.node (Approx.MStep nodex cx) = node
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 y (Nat.succ n)) = Container.M.node y
nodex : C.A
cx : B C nodex → Approx C n
h₂ : Approx.node (Approx.MStep nodex cx) = Container.M.node x
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)
this : Container.M.node x = node
⊢ Approx.node (Approx.MStep nodex cx) = node
Tactic:
rw [←this]
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 y (Nat.succ n)) = Container.M.node y
nodex : C.A
cx : B C nodex → Approx C n
h₂ : Approx.node (Approx.MStep nodex cx) = Container.M.node x
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)
this : Container.M.node x = node
⊢ Approx.node (Approx.MStep nodex cx) = Container.M.node x
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 y (Nat.succ n)) = Container.M.node y
nodex : C.A
cx : B C nodex → Approx C n
h₂ : Approx.node (Approx.MStep nodex cx) = Container.M.node x
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)
this : Container.M.node x = node
⊢ Approx.node (Approx.MStep nodex cx) = Container.M.node x
Tactic:
exact h₂
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
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.node (Approx.MStep nodey cy) = node
Tactic:
have := congrArg (λ x => x.1) eq₂
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)) = 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
this : (fun x => x.fst) (destruct y) = (fun x => x.fst) { fst := node, snd := k₂ }
⊢ Approx.node (Approx.MStep nodey cy) = node
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)) = 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
this : (fun x => x.fst) (destruct y) = (fun x => x.fst) { fst := node, snd := k₂ }
⊢ Approx.node (Approx.MStep nodey cy) = node
Tactic:
simp only [destruct] at this
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)) = 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
this : Container.M.node y = node
⊢ Approx.node (Approx.MStep nodey cy) = node