Theorem: IContainer'.M.bisim (CoInd/Test.lean)

State before:
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
⊢ ∀ (x y : M C i), R i x y → x = y
Tactic:
intro ⟨x, wfx⟩ ⟨y, wfy⟩ h₁
State after:
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ { val := x, property := wfx } = { val := y, property := wfy }

State before:
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ { val := x, property := wfx } = { val := y, property := wfy }
Tactic:
suffices h: x = y by
  induction h
  rfl
State after:
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ x = y

State before:
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ x = y
Tactic:
apply Container.M.bisim (λ x y => ∃ i, ∃ (wfx: WellFormed i x) (wfy:WellFormed i y), R i ⟨x, wfx⟩ ⟨y, wfy⟩)
State after:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∀ (x y : Container.M (toContainer C)),
    (∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }) →
      ∃ node k₁ k₂,
        Container.M.destruct x = { fst := node, snd := k₁ } ∧
          Container.M.destruct y = { fst := node, snd := k₂ } ∧
            ∀ (i : Container.B (toContainer C) node),
              ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }

case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∀ (x y : Container.M (toContainer C)),
    (∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }) →
      ∃ node k₁ k₂,
        Container.M.destruct x = { fst := node, snd := k₁ } ∧
          Container.M.destruct y = { fst := node, snd := k₂ } ∧
            ∀ (i : Container.B (toContainer C) node),
              ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }

case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }
Tactic:
. intro x y ⟨i, wfx, wfy, r⟩
  have ⟨⟨node, h₄⟩, k₁, k₂, h₁, h₂, h₃⟩ := h₀ i ⟨x, wfx⟩ ⟨y, wfy⟩ r
  have h₁ := lift_destruct_eq _ _ _ _ h₁
  have h₂ := lift_destruct_eq _ _ _ _ h₂
  have wfx' := wf_destruct ⟨x, wfx⟩
  have wfy' := wf_destruct ⟨y, wfy⟩
  exists node
  exists λ a => (k₁ a).1
  exists λ x => (k₂ x).1
  simp only [h₁, h₂, true_and]
  intro a
  exists C.Next node a
  simp only [toContainer] at a
  exists (by
      rw [h₁] at wfx'
      apply wfx'
    )
  exists (by
      rw [h₂] at wfy'
      apply wfy'
    )
  exact h₃ a
State after:
case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }

State before:
case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }
Tactic:
exists i
State after:
case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }

State before:
case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }
Tactic:
exists wfx
State after:
case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ wfy, R i { val := x, property := wfx } { val := y, property := wfy }

State before:
case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ wfy, R i { val := x, property := wfx } { val := y, property := wfy }
Tactic:
exists wfy
State after:
no goals

State before:
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
h : x = y
⊢ { val := x, property := wfx } = { val := y, property := wfy }
Tactic:
induction h
State after:
case refl
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i x
h₁ : R i { val := x, property := wfx } { val := x, property := wfy }
⊢ { val := x, property := wfx } = { val := x, property := wfy }

State before:
case refl
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i x
h₁ : R i { val := x, property := wfx } { val := x, property := wfy }
⊢ { val := x, property := wfx } = { val := x, property := wfy }
Tactic:
rfl
State after:
no goals

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∀ (x y : Container.M (toContainer C)),
    (∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }) →
      ∃ node k₁ k₂,
        Container.M.destruct x = { fst := node, snd := k₁ } ∧
          Container.M.destruct y = { fst := node, snd := k₂ } ∧
            ∀ (i : Container.B (toContainer C) node),
              ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }
Tactic:
intro x y ⟨i, wfx, wfy, r⟩
State after:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ node k₁ k₂,
    Container.M.destruct x = { fst := node, snd := k₁ } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) node),
          ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ node k₁ k₂,
    Container.M.destruct x = { fst := node, snd := k₁ } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) node),
          ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }
Tactic:
have ⟨⟨node, h₄⟩, k₁, k₂, h₁, h₂, h₃⟩ := h₀ i ⟨x, wfx⟩ ⟨y, wfy⟩ r
State after:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
⊢ ∃ node k₁ k₂,
    Container.M.destruct x = { fst := node, snd := k₁ } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) node),
          ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
⊢ ∃ node k₁ k₂,
    Container.M.destruct x = { fst := node, snd := k₁ } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) node),
          ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }
Tactic:
have h₁ := lift_destruct_eq _ _ _ _ h₁
State after:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
⊢ ∃ node k₁ k₂,
    Container.M.destruct x = { fst := node, snd := k₁ } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) node),
          ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
⊢ ∃ node k₁ k₂,
    Container.M.destruct x = { fst := node, snd := k₁ } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) node),
          ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }
Tactic:
have h₂ := lift_destruct_eq _ _ _ _ h₂
State after:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
⊢ ∃ node k₁ k₂,
    Container.M.destruct x = { fst := node, snd := k₁ } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) node),
          ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
⊢ ∃ node k₁ k₂,
    Container.M.destruct x = { fst := node, snd := k₁ } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) node),
          ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }
Tactic:
have wfx' := wf_destruct ⟨x, wfx⟩
State after:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
⊢ ∃ node k₁ k₂,
    Container.M.destruct x = { fst := node, snd := k₁ } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) node),
          ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
⊢ ∃ node k₁ k₂,
    Container.M.destruct x = { fst := node, snd := k₁ } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) node),
          ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }
Tactic:
have wfy' := wf_destruct ⟨y, wfy⟩
State after:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
⊢ ∃ node k₁ k₂,
    Container.M.destruct x = { fst := node, snd := k₁ } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) node),
          ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
⊢ ∃ node k₁ k₂,
    Container.M.destruct x = { fst := node, snd := k₁ } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) node),
          ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }
Tactic:
exists node
State after:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
⊢ ∃ k₁ k₂,
    Container.M.destruct x = { fst := node, snd := k₁ } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) node),
          ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
⊢ ∃ k₁ k₂,
    Container.M.destruct x = { fst := node, snd := k₁ } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) node),
          ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }
Tactic:
exists λ a => (k₁ a).1
State after:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
⊢ ∃ k₂,
    Container.M.destruct x = { fst := node, snd := fun a => ↑(k₁ a) } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i_1 : Container.B (toContainer C) node),
          ∃ i_2 wfx wfy, R i_2 { val := (fun a => ↑(k₁ a)) i_1, property := wfx } { val := k₂ i_1, property := wfy }

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
⊢ ∃ k₂,
    Container.M.destruct x = { fst := node, snd := fun a => ↑(k₁ a) } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i_1 : Container.B (toContainer C) node),
          ∃ i_2 wfx wfy, R i_2 { val := (fun a => ↑(k₁ a)) i_1, property := wfx } { val := k₂ i_1, property := wfy }
Tactic:
exists λ x => (k₂ x).1
State after:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
⊢ Container.M.destruct x = { fst := node, snd := fun a => ↑(k₁ a) } ∧
    Container.M.destruct y = { fst := node, snd := fun x => ↑(k₂ x) } ∧
      ∀ (i_1 : Container.B (toContainer C) node),
        ∃ i_2 wfx wfy,
          R i_2 { val := (fun a => ↑(k₁ a)) i_1, property := wfx } { val := (fun x => ↑(k₂ x)) i_1, property := wfy }

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
⊢ Container.M.destruct x = { fst := node, snd := fun a => ↑(k₁ a) } ∧
    Container.M.destruct y = { fst := node, snd := fun x => ↑(k₂ x) } ∧
      ∀ (i_1 : Container.B (toContainer C) node),
        ∃ i_2 wfx wfy,
          R i_2 { val := (fun a => ↑(k₁ a)) i_1, property := wfx } { val := (fun x => ↑(k₂ x)) i_1, property := wfy }
Tactic:
simp only [h₁, h₂, true_and]
State after:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
⊢ ∀ (i_1 : Container.B (toContainer C) node),
    ∃ i_2 h h_1,
      R i_2 { val := ↑(k₁ i_1), property := (_ : WellFormed i_2 ((fun a => ↑(k₁ a)) i_1)) }
        { val := ↑(k₂ i_1), property := (_ : WellFormed i_2 ((fun x => ↑(k₂ x)) i_1)) }

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
⊢ ∀ (i_1 : Container.B (toContainer C) node),
    ∃ i_2 h h_1,
      R i_2 { val := ↑(k₁ i_1), property := (_ : WellFormed i_2 ((fun a => ↑(k₁ a)) i_1)) }
        { val := ↑(k₂ i_1), property := (_ : WellFormed i_2 ((fun x => ↑(k₂ x)) i_1)) }
Tactic:
intro a
State after:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
a : Container.B (toContainer C) node
⊢ ∃ i_1 h h_1,
    R i_1 { val := ↑(k₁ a), property := (_ : WellFormed i_1 ((fun a => ↑(k₁ a)) a)) }
      { val := ↑(k₂ a), property := (_ : WellFormed i_1 ((fun x => ↑(k₂ x)) a)) }

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
a : Container.B (toContainer C) node
⊢ ∃ i_1 h h_1,
    R i_1 { val := ↑(k₁ a), property := (_ : WellFormed i_1 ((fun a => ↑(k₁ a)) a)) }
      { val := ↑(k₂ a), property := (_ : WellFormed i_1 ((fun x => ↑(k₂ x)) a)) }
Tactic:
exists C.Next node a
State after:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
a : Container.B (toContainer C) node
⊢ ∃ h h_1,
    R (Next C node a) { val := ↑(k₁ a), property := (_ : WellFormed (Next C node a) ((fun a => ↑(k₁ a)) a)) }
      { val := ↑(k₂ a), property := (_ : WellFormed (Next C node a) ((fun x => ↑(k₂ x)) a)) }

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
a : Container.B (toContainer C) node
⊢ ∃ h h_1,
    R (Next C node a) { val := ↑(k₁ a), property := (_ : WellFormed (Next C node a) ((fun a => ↑(k₁ a)) a)) }
      { val := ↑(k₂ a), property := (_ : WellFormed (Next C node a) ((fun x => ↑(k₂ x)) a)) }
Tactic:
simp only [toContainer] at a
State after:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
a : B C node
⊢ ∃ h h_1,
    R (Next C node a) { val := ↑(k₁ a), property := (_ : WellFormed (Next C node a) ((fun a => ↑(k₁ a)) a)) }
      { val := ↑(k₂ a), property := (_ : WellFormed (Next C node a) ((fun x => ↑(k₂ x)) a)) }

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
a : B C node
⊢ ∃ h h_1,
    R (Next C node a) { val := ↑(k₁ a), property := (_ : WellFormed (Next C node a) ((fun a => ↑(k₁ a)) a)) }
      { val := ↑(k₂ a), property := (_ : WellFormed (Next C node a) ((fun x => ↑(k₂ x)) a)) }
Tactic:
exists (by
    rw [h₁] at wfx'
    apply wfx'
  )
State after:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
a : B C node
⊢ ∃ h,
    R (Next C node a) { val := ↑(k₁ a), property := (_ : WellFormed (Next C node a) ((fun a => ↑(k₁ a)) a)) }
      { val := ↑(k₂ a), property := (_ : WellFormed (Next C node a) ((fun x => ↑(k₂ x)) a)) }

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
a : B C node
⊢ ∃ h,
    R (Next C node a) { val := ↑(k₁ a), property := (_ : WellFormed (Next C node a) ((fun a => ↑(k₁ a)) a)) }
      { val := ↑(k₂ a), property := (_ : WellFormed (Next C node a) ((fun x => ↑(k₂ x)) a)) }
Tactic:
exists (by
    rw [h₂] at wfy'
    apply wfy'
  )
State after:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
a : B C node
⊢ R (Next C node a) { val := ↑(k₁ a), property := (_ : WellFormed (Next C node a) ((fun a => ↑(k₁ a)) a)) }
    { val := ↑(k₂ a), property := (_ : WellFormed (Next C node a) ((fun x => ↑(k₂ x)) a)) }

State before:
case h₀
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
a : B C node
⊢ R (Next C node a) { val := ↑(k₁ a), property := (_ : WellFormed (Next C node a) ((fun a => ↑(k₁ a)) a)) }
    { val := ↑(k₂ a), property := (_ : WellFormed (Next C node a) ((fun x => ↑(k₂ x)) a)) }
Tactic:
exact h₃ a
State after:
no goals

State before:
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
a : B C node
⊢ WellFormed (Next C node a) ↑(k₁ a)
Tactic:
rw [h₁] at wfx'
State after:
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀
    (x :
      B C
        { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
            snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }.fst),
    WellFormed
      (Next C
        { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
            snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }.fst
        x)
      (PSigma.snd
        { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
          snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
        x)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
a : B C node
⊢ WellFormed (Next C node a) ↑(k₁ a)

State before:
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀
    (x :
      B C
        { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
            snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }.fst),
    WellFormed
      (Next C
        { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
            snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }.fst
        x)
      (PSigma.snd
        { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
          snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
        x)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
a : B C node
⊢ WellFormed (Next C node a) ↑(k₁ a)
Tactic:
apply wfx'
State after:
no goals

State before:
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀ (x : B C (Container.M.destruct ↑{ val := y, property := wfy }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := y, property := wfy }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := y, property := wfy }) x)
a : B C node
⊢ WellFormed (Next C node a) ↑(k₂ a)
Tactic:
rw [h₂] at wfy'
State after:
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀
    (x :
      B C
        { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
            snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }.fst),
    WellFormed
      (Next C
        { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
            snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }.fst
        x)
      (PSigma.snd
        { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
          snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
        x)
a : B C node
⊢ WellFormed (Next C node a) ↑(k₂ a)

State before:
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁✝¹ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
node : C.A
h₄ : i = Idx C node
k₁ k₂ : (y : B C ↑{ val := node, property := h₄ }) → M C (Next C (↑{ val := node, property := h₄ }) y)
h₁✝ : destruct { val := x, property := wfx } = { fst := { val := node, property := h₄ }, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := { val := node, property := h₄ }, snd := k₂ }
h₃ : ∀ (z : B C ↑{ val := node, property := h₄ }), R (Next C (↑{ val := node, property := h₄ }) z) (k₁ z) (k₂ z)
h₁ :
  Container.M.destruct x =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₁ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₁ } x) }
h₂ :
  Container.M.destruct y =
    { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
      snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
wfx' :
  ∀ (x_1 : B C (Container.M.destruct ↑{ val := x, property := wfx }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := x, property := wfx }).fst x_1)
      (PSigma.snd (Container.M.destruct ↑{ val := x, property := wfx }) x_1)
wfy' :
  ∀
    (x :
      B C
        { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
            snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }.fst),
    WellFormed
      (Next C
        { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
            snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }.fst
        x)
      (PSigma.snd
        { fst := ↑{ fst := { val := node, property := h₄ }, snd := k₂ }.fst,
          snd := fun x => ↑(Sigma.snd { fst := { val := node, property := h₄ }, snd := k₂ } x) }
        x)
a : B C node
⊢ WellFormed (Next C node a) ↑(k₂ a)
Tactic:
apply wfy'
State after:
no goals