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

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), R x y → approx x n = approx y n
Tactic:
intro x y n h₁
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)
x y : M C
n : Nat
h₁ : R x y
⊢ approx x n = approx y n

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
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✝)

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
State after:
no goals

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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)

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
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)

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
State after:
no goals

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
State after:
no goals

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₁
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

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₂
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

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₃
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

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₃
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

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₂
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

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₃
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

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
h₃ : node = nodey
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Tactic:
have h₆ := bisim.lemma0 x n
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
h₆ :
  ∀ (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
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy

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
h₃ : node = nodey
h₆ :
  ∀ (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
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Tactic:
have h₇ := bisim.lemma0 y n
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
h₆ :
  ∀ (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
h₇ :
  ∀ (i : B C (Approx.node (approx y (Nat.succ n)))) (j : B C (destruct y).fst),
    HEq i j → Approx.children (approx y (Nat.succ n)) i = approx (PSigma.snd (destruct y) j) n
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy

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
h₃ : node = nodey
h₆ :
  ∀ (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
h₇ :
  ∀ (i : B C (Approx.node (approx y (Nat.succ n)))) (j : B C (destruct y).fst),
    HEq i j → Approx.children (approx y (Nat.succ n)) i = approx (PSigma.snd (destruct y) j) n
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Tactic:
rw [h₄] at h₆
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
h₆ :
  ∀ (i : B C (Approx.node (Approx.MStep nodex cx))) (j : B C (destruct x).fst),
    HEq i j → Approx.children (Approx.MStep nodex cx) i = approx (PSigma.snd (destruct x) j) n
h₇ :
  ∀ (i : B C (Approx.node (approx y (Nat.succ n)))) (j : B C (destruct y).fst),
    HEq i j → Approx.children (approx y (Nat.succ n)) i = approx (PSigma.snd (destruct y) j) n
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy

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
h₃ : node = nodey
h₆ :
  ∀ (i : B C (Approx.node (Approx.MStep nodex cx))) (j : B C (destruct x).fst),
    HEq i j → Approx.children (Approx.MStep nodex cx) i = approx (PSigma.snd (destruct x) j) n
h₇ :
  ∀ (i : B C (Approx.node (approx y (Nat.succ n)))) (j : B C (destruct y).fst),
    HEq i j → Approx.children (approx y (Nat.succ n)) i = approx (PSigma.snd (destruct y) j) n
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Tactic:
rw [h₅] at h₇
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
h₆ :
  ∀ (i : B C (Approx.node (Approx.MStep nodex cx))) (j : B C (destruct x).fst),
    HEq i j → Approx.children (Approx.MStep nodex cx) i = approx (PSigma.snd (destruct x) j) n
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep nodey cy))) (j : B C (destruct y).fst),
    HEq i j → Approx.children (Approx.MStep nodey cy) i = approx (PSigma.snd (destruct y) j) n
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy

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
h₃ : node = nodey
h₆ :
  ∀ (i : B C (Approx.node (Approx.MStep nodex cx))) (j : B C (destruct x).fst),
    HEq i j → Approx.children (Approx.MStep nodex cx) i = approx (PSigma.snd (destruct x) j) n
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep nodey cy))) (j : B C (destruct y).fst),
    HEq i j → Approx.children (Approx.MStep nodey cy) i = approx (PSigma.snd (destruct y) j) n
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Tactic:
simp only [Approx.children] at h₇ h₆
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
h₆ :
  ∀ (i : B C (Approx.node (Approx.MStep nodex cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep nodey cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy

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
h₃ : node = nodey
h₆ :
  ∀ (i : B C (Approx.node (Approx.MStep nodex cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep nodey cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
⊢ Approx.MStep nodex cx = Approx.MStep nodey cy
Tactic:
induction h₂
State after:
case MStep.MStep.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 : 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₃✝ : nodey = node
h₃ : node = nodey
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep nodey cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
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
⊢ Approx.MStep node cx = Approx.MStep nodey cy

State before:
case MStep.MStep.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 : 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₃✝ : nodey = node
h₃ : node = nodey
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep nodey cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
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
⊢ Approx.MStep node cx = Approx.MStep nodey cy
Tactic:
induction h₃
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
⊢ Approx.MStep node cx = Approx.MStep node cy

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
⊢ Approx.MStep node cx = Approx.MStep node cy
Tactic:
suffices h₈ : ∀ i: C.B node, cx i = cy i by
  have : cx = cy := by
    funext i
    apply h₈
  rw [this]
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), cx i = cy i

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:
intro i
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
⊢ cx i = cy i

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
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

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
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

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₇]
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

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
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)

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
State after:
no goals

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₁
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

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
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

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₂
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

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]
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

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₂
State after:
no goals

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₂
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

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
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

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 : Container.M.node y = node
⊢ Approx.node (Approx.MStep nodey cy) = node
Tactic:
rw [h₅] at h₃
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
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.node (Approx.MStep nodey cy) = Container.M.node y
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

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
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.node (Approx.MStep nodey cy) = Container.M.node y
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
Tactic:
rw [←this]
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
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.node (Approx.MStep nodey cy) = Container.M.node y
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) = Container.M.node y

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
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.node (Approx.MStep nodey cy) = Container.M.node y
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) = Container.M.node y
Tactic:
exact h₃
State after:
no goals

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 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
h₈ : ∀ (i : B C node), cx i = cy i
⊢ Approx.MStep node cx = Approx.MStep node cy
Tactic:
have : cx = cy := by
  funext i
  apply h₈
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 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
h₈ : ∀ (i : B C node), cx i = cy i
this : cx = cy
⊢ Approx.MStep node cx = Approx.MStep node cy

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 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
h₈ : ∀ (i : B C node), cx i = cy i
this : cx = cy
⊢ Approx.MStep node cx = Approx.MStep node cy
Tactic:
rw [this]
State after:
no goals

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 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
h₈ : ∀ (i : B C node), cx i = cy i
⊢ cx = cy
Tactic:
funext i
State after:
case 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
h₈ : ∀ (i : B C node), cx i = cy i
i : B C node
⊢ cx i = cy i

State before:
case 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
h₈ : ∀ (i : B C node), cx i = cy i
i : B C node
⊢ cx i = cy i
Tactic:
apply h₈
State after:
no goals

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 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
⊢ ∀ (i : B C node), cx i = approx (k₁ i) n
Tactic:
have h : ∀ i j, HEq i j → (x.destruct.snd i) = k₁ j := by
  rw [eq₁]
  intro i j heq
  cases heq
  rfl
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 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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
⊢ ∀ (i : B C node), cx i = approx (k₁ i) n

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 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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
⊢ ∀ (i : B C node), cx i = approx (k₁ i) n
Tactic:
intro i
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 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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
i : B C node
⊢ cx i = approx (k₁ i) n

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 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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
i : B C node
⊢ cx i = approx (k₁ i) n
Tactic:
rw [h₆ i (cast (by simp [congrArg (λ x => x.1) eq₁]) i)]
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 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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
i : B C node
⊢ approx (PSigma.snd (destruct x) (cast (_ : B C node = B C (destruct x).fst) i)) n = approx (k₁ i) n

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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
i : B C node
⊢ HEq i (cast (_ : B C node = B C (destruct x).fst) i)

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 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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
i : B C node
⊢ approx (PSigma.snd (destruct x) (cast (_ : B C node = B C (destruct x).fst) i)) n = approx (k₁ i) n

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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
i : B C node
⊢ HEq i (cast (_ : B C node = B C (destruct x).fst) i)
Tactic:
. rw [h]
  apply cast_heq
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 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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
i : B C node
⊢ HEq i (cast (_ : B C node = B C (destruct x).fst) i)

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 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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
i : B C node
⊢ HEq i (cast (_ : B C node = B C (destruct x).fst) i)
Tactic:
. apply HEq.symm
  apply cast_heq
State after:
no goals

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 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
⊢ ∀ (i : B C (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
Tactic:
rw [eq₁]
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 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
⊢ ∀ (i : B C { fst := node, snd := k₁ }.fst) (j : B C node), HEq i j → PSigma.snd { fst := node, snd := k₁ } i = k₁ j

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 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
⊢ ∀ (i : B C { fst := node, snd := k₁ }.fst) (j : B C node), HEq i j → PSigma.snd { fst := node, snd := k₁ } i = k₁ j
Tactic:
intro i j heq
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 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
i : B C { fst := node, snd := k₁ }.fst
j : B C node
heq : HEq i j
⊢ PSigma.snd { fst := node, snd := k₁ } i = k₁ j

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 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
i : B C { fst := node, snd := k₁ }.fst
j : B C node
heq : HEq i j
⊢ PSigma.snd { fst := node, snd := k₁ } i = k₁ j
Tactic:
cases heq
State after:
case 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
i : B C { fst := node, snd := k₁ }.fst
⊢ PSigma.snd { fst := node, snd := k₁ } i = k₁ i

State before:
case 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
i : B C { fst := node, snd := k₁ }.fst
⊢ PSigma.snd { fst := node, snd := k₁ } i = k₁ i
Tactic:
rfl
State after:
no goals

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 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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
i : B C node
⊢ B C node = B C (destruct x).fst
Tactic:
simp [congrArg (λ x => x.1) eq₁]
State after:
no goals

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 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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
i : B C node
⊢ approx (PSigma.snd (destruct x) (cast (_ : B C node = B C (destruct x).fst) i)) n = approx (k₁ i) n
Tactic:
rw [h]
State after:
case a
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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
i : B C node
⊢ HEq (cast (_ : B C node = B C (destruct x).fst) i) i

State before:
case a
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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
i : B C node
⊢ HEq (cast (_ : B C node = B C (destruct x).fst) i) i
Tactic:
apply cast_heq
State after:
no goals

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 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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
i : B C node
⊢ HEq i (cast (_ : B C node = B C (destruct x).fst) i)
Tactic:
apply HEq.symm
State after:
case 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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
i : B C node
⊢ HEq (cast (_ : B C node = B C (destruct x).fst) i) i

State before:
case 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 (destruct x).fst) (j : B C node), HEq i j → PSigma.snd (destruct x) i = k₁ j
i : B C node
⊢ HEq (cast (_ : B C node = B C (destruct x).fst) i) i
Tactic:
apply cast_heq
State after:
no goals

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 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
⊢ ∀ (i : B C node), cy i = approx (k₂ i) n
Tactic:
have h : ∀ i j, HEq i j → (y.destruct.snd i) = k₂ j := by
  rw [eq₂]
  intro i j heq
  cases heq
  rfl
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 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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
⊢ ∀ (i : B C node), cy i = approx (k₂ i) n

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 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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
⊢ ∀ (i : B C node), cy i = approx (k₂ i) n
Tactic:
intro i
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 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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ cy i = approx (k₂ i) n

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 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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ cy i = approx (k₂ i) n
Tactic:
rw [h₇ i (cast (by simp [congrArg (λ x => x.1) eq₂]) i)]
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 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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ approx (PSigma.snd (destruct y) (cast (_ : B C node = B C (destruct y).fst) i)) n = approx (k₂ i) n

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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ HEq i (cast (_ : B C node = B C (destruct y).fst) i)

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 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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ approx (PSigma.snd (destruct y) (cast (_ : B C node = B C (destruct y).fst) i)) n = approx (k₂ i) n

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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ HEq i (cast (_ : B C node = B C (destruct y).fst) i)
Tactic:
. rw [h]
  apply cast_heq
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 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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ HEq i (cast (_ : B C node = B C (destruct y).fst) i)

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 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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ HEq i (cast (_ : B C node = B C (destruct y).fst) i)
Tactic:
. apply HEq.symm
  apply cast_heq
State after:
no goals

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 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
⊢ ∀ (i : B C (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
Tactic:
rw [eq₂]
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 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
⊢ ∀ (i : B C { fst := node, snd := k₂ }.fst) (j : B C node), HEq i j → PSigma.snd { fst := node, snd := k₂ } i = k₂ j

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 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
⊢ ∀ (i : B C { fst := node, snd := k₂ }.fst) (j : B C node), HEq i j → PSigma.snd { fst := node, snd := k₂ } i = k₂ j
Tactic:
intro i j heq
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 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
i : B C { fst := node, snd := k₂ }.fst
j : B C node
heq : HEq i j
⊢ PSigma.snd { fst := node, snd := k₂ } i = k₂ j

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 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
i : B C { fst := node, snd := k₂ }.fst
j : B C node
heq : HEq i j
⊢ PSigma.snd { fst := node, snd := k₂ } i = k₂ j
Tactic:
cases heq
State after:
case 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
i : B C { fst := node, snd := k₂ }.fst
⊢ PSigma.snd { fst := node, snd := k₂ } i = k₂ i

State before:
case 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
i : B C { fst := node, snd := k₂ }.fst
⊢ PSigma.snd { fst := node, snd := k₂ } i = k₂ i
Tactic:
rfl
State after:
no goals

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 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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ B C node = B C (destruct y).fst
Tactic:
simp [congrArg (λ x => x.1) eq₂]
State after:
no goals

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 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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ approx (PSigma.snd (destruct y) (cast (_ : B C node = B C (destruct y).fst) i)) n = approx (k₂ i) n
Tactic:
rw [h]
State after:
case a
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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ HEq (cast (_ : B C node = B C (destruct y).fst) i) i

State before:
case a
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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ HEq (cast (_ : B C node = B C (destruct y).fst) i) i
Tactic:
apply cast_heq
State after:
no goals

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 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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ HEq i (cast (_ : B C node = B C (destruct y).fst) i)
Tactic:
apply HEq.symm
State after:
case 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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ HEq (cast (_ : B C node = B C (destruct y).fst) i) i

State before:
case 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 (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ HEq (cast (_ : B C node = B C (destruct y).fst) i) i
Tactic:
apply cast_heq
State after:
no goals