Theorem: IContainer.M.bisim (CoInd/MIdx.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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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, k₁, k₂, h₁, h₂, h₃⟩ := h₀ i ⟨x, wfx⟩ ⟨y, wfy⟩ r
  let ix := (Container.M.destruct x).1.1
  let nx := (Container.M.destruct x).1.2
  let kx := (Container.M.destruct x).2
  let iy := (Container.M.destruct y).1.1
  let ny := (Container.M.destruct y).1.2
  let ky := (Container.M.destruct y).2
  have hix := index_destruct ⟨x, wfx⟩
  have hiy := index_destruct ⟨y, wfy⟩
  have wfx' : ∀ a:B C ix nx, WellFormed (C.N ix nx a) (kx a) := wf_destruct ⟨x, wfx⟩
  have wfy' : ∀ a:B C iy ny, WellFormed (C.N iy ny a) (ky a) := wf_destruct ⟨y, wfy⟩
  simp only at hix hiy wfx wfy
  exists ⟨_, node⟩
  exists λ x => (k₁ x).1
  exists λ x => (k₂ x).1
  constructor
  . cases hix
    have hnx: nx = node := by
      apply congrArg Sigma.fst h₁
    cases hnx
    have h₁ := Sigma.snd_equals _ _ _ h₁
    rw [← h₁]
    rfl
  . constructor
    . cases hiy
      have hny: ny = node := by
        apply congrArg Sigma.fst h₂
      cases hny
      have h₂ := Sigma.snd_equals _ _ _ h₂
      rw [← h₂]
      rfl
    . intro a
      exists C.N i node a
      simp only [toContainer] at a
      exists (by
          cases hix
          have : nx = node := by
            apply congrArg Sigma.fst h₁
          cases this
          have h₁ := Sigma.snd_equals _ _ _ h₁
          have wfx' := wfx' a
          cases h₁
          exact wfx'
        )
      exists (by
          cases hiy
          have : ny = node := by
            apply congrArg Sigma.fst h₂
          cases this
          have h₂ := Sigma.snd_equals _ _ _ h₂
          have wfy' := wfy' a
          cases h₂
          exact 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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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 i node), R (N C i 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, 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node 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:
let ix := (Container.M.destruct x).1.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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
⊢ ∃ 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
⊢ ∃ 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:
let nx := (Container.M.destruct x).1.2
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
⊢ ∃ 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
⊢ ∃ 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:
let kx := (Container.M.destruct x).2
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
⊢ ∃ 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
⊢ ∃ 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:
let iy := (Container.M.destruct y).1.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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
⊢ ∃ 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
⊢ ∃ 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:
let ny := (Container.M.destruct y).1.2
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
⊢ ∃ 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
⊢ ∃ 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:
let ky := (Container.M.destruct y).2
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
⊢ ∃ 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
⊢ ∃ 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 hix := index_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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct ↑{ val := x, property := wfx }).fst.fst
⊢ ∃ 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct ↑{ val := x, property := wfx }).fst.fst
⊢ ∃ 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 hiy := index_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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct ↑{ val := x, property := wfx }).fst.fst
hiy : i = (Container.M.destruct ↑{ val := y, property := wfy }).fst.fst
⊢ ∃ 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct ↑{ val := x, property := wfx }).fst.fst
hiy : i = (Container.M.destruct ↑{ val := y, property := wfy }).fst.fst
⊢ ∃ 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' : ∀ a:B C ix nx, WellFormed (C.N ix nx a) (kx a) := 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct ↑{ val := x, property := wfx }).fst.fst
hiy : i = (Container.M.destruct ↑{ val := y, property := wfy }).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
⊢ ∃ 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct ↑{ val := x, property := wfx }).fst.fst
hiy : i = (Container.M.destruct ↑{ val := y, property := wfy }).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
⊢ ∃ 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' : ∀ a:B C iy ny, WellFormed (C.N iy ny a) (ky a) := 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct ↑{ val := x, property := wfx }).fst.fst
hiy : i = (Container.M.destruct ↑{ val := y, property := wfy }).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ ∃ 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct ↑{ val := x, property := wfx }).fst.fst
hiy : i = (Container.M.destruct ↑{ val := y, property := wfy }).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ ∃ 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:
simp only at hix hiy wfx 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ ∃ 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ ∃ 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ ∃ k₁ k₂,
    Container.M.destruct x = { fst := { fst := i, snd := node }, snd := k₁ } ∧
      Container.M.destruct y = { fst := { fst := i, snd := node }, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) { fst := i, snd := 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ ∃ k₁ k₂,
    Container.M.destruct x = { fst := { fst := i, snd := node }, snd := k₁ } ∧
      Container.M.destruct y = { fst := { fst := i, snd := node }, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) { fst := i, snd := node }),
          ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ ∃ k₂,
    Container.M.destruct x = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₁ x) } ∧
      Container.M.destruct y = { fst := { fst := i, snd := node }, snd := k₂ } ∧
        ∀ (i_1 : Container.B (toContainer C) { fst := i, snd := node }),
          ∃ i_2 wfx wfy, R i_2 { val := (fun x => ↑(k₁ x)) 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ ∃ k₂,
    Container.M.destruct x = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₁ x) } ∧
      Container.M.destruct y = { fst := { fst := i, snd := node }, snd := k₂ } ∧
        ∀ (i_1 : Container.B (toContainer C) { fst := i, snd := node }),
          ∃ i_2 wfx wfy, R i_2 { val := (fun x => ↑(k₁ x)) 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ Container.M.destruct x = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₁ x) } ∧
    Container.M.destruct y = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₂ x) } ∧
      ∀ (i_1 : Container.B (toContainer C) { fst := i, snd := node }),
        ∃ i_2 wfx wfy,
          R i_2 { val := (fun x => ↑(k₁ x)) 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ Container.M.destruct x = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₁ x) } ∧
    Container.M.destruct y = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₂ x) } ∧
      ∀ (i_1 : Container.B (toContainer C) { fst := i, snd := node }),
        ∃ i_2 wfx wfy,
          R i_2 { val := (fun x => ↑(k₁ x)) i_1, property := wfx } { val := (fun x => ↑(k₂ x)) i_1, property := wfy }
Tactic:
constructor
State after:
case h₀.left
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ Container.M.destruct x = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₁ x) }

case h₀.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ Container.M.destruct y = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₂ x) } ∧
    ∀ (i_1 : Container.B (toContainer C) { fst := i, snd := node }),
      ∃ i_2 wfx wfy,
        R i_2 { val := (fun x => ↑(k₁ x)) i_1, property := wfx } { val := (fun x => ↑(k₂ x)) i_1, property := wfy }

State before:
case h₀.left
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ Container.M.destruct x = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₁ x) }

case h₀.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ Container.M.destruct y = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₂ x) } ∧
    ∀ (i_1 : Container.B (toContainer C) { fst := i, snd := node }),
      ∃ i_2 wfx wfy,
        R i_2 { val := (fun x => ↑(k₁ x)) i_1, property := wfx } { val := (fun x => ↑(k₂ x)) i_1, property := wfy }
Tactic:
. cases hix
  have hnx: nx = node := by
    apply congrArg Sigma.fst h₁
  cases hnx
  have h₁ := Sigma.snd_equals _ _ _ h₁
  rw [← h₁]
  rfl
State after:
case h₀.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ Container.M.destruct y = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₂ x) } ∧
    ∀ (i_1 : Container.B (toContainer C) { fst := i, snd := node }),
      ∃ i_2 wfx wfy,
        R i_2 { val := (fun x => ↑(k₁ x)) i_1, property := wfx } { val := (fun x => ↑(k₂ x)) i_1, property := wfy }

State before:
case h₀.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ Container.M.destruct y = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₂ x) } ∧
    ∀ (i_1 : Container.B (toContainer C) { fst := i, snd := node }),
      ∃ i_2 wfx wfy,
        R i_2 { val := (fun x => ↑(k₁ x)) i_1, property := wfx } { val := (fun x => ↑(k₂ x)) i_1, property := wfy }
Tactic:
. constructor
  . cases hiy
    have hny: ny = node := by
      apply congrArg Sigma.fst h₂
    cases hny
    have h₂ := Sigma.snd_equals _ _ _ h₂
    rw [← h₂]
    rfl
  . intro a
    exists C.N i node a
    simp only [toContainer] at a
    exists (by
        cases hix
        have : nx = node := by
          apply congrArg Sigma.fst h₁
        cases this
        have h₁ := Sigma.snd_equals _ _ _ h₁
        have wfx' := wfx' a
        cases h₁
        exact wfx'
      )
    exists (by
        cases hiy
        have : ny = node := by
          apply congrArg Sigma.fst h₂
        cases this
        have h₂ := Sigma.snd_equals _ _ _ h₂
        have wfy' := wfy' a
        cases h₂
        exact wfy'
      )
    exact h₃ a
State after:
no goals

State before:
case h₀.left
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ Container.M.destruct x = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₁ x) }
Tactic:
cases hix
State after:
case h₀.left.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct x).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst node) → M C (N C (Container.M.destruct x).fst.fst node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst node), R (N C (Container.M.destruct x).fst.fst node z) (k₁ z) (k₂ z)
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
⊢ Container.M.destruct x =
    { fst := { fst := (Container.M.destruct x).fst.fst, snd := node }, snd := fun x_1 => ↑(k₁ x_1) }

State before:
case h₀.left.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct x).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst node) → M C (N C (Container.M.destruct x).fst.fst node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst node), R (N C (Container.M.destruct x).fst.fst node z) (k₁ z) (k₂ z)
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
⊢ Container.M.destruct x =
    { fst := { fst := (Container.M.destruct x).fst.fst, snd := node }, snd := fun x_1 => ↑(k₁ x_1) }
Tactic:
have hnx: nx = node := by
  apply congrArg Sigma.fst h₁
State after:
case h₀.left.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct x).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst node) → M C (N C (Container.M.destruct x).fst.fst node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst node), R (N C (Container.M.destruct x).fst.fst node z) (k₁ z) (k₂ z)
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
hnx : nx = node
⊢ Container.M.destruct x =
    { fst := { fst := (Container.M.destruct x).fst.fst, snd := node }, snd := fun x_1 => ↑(k₁ x_1) }

State before:
case h₀.left.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct x).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst node) → M C (N C (Container.M.destruct x).fst.fst node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst node), R (N C (Container.M.destruct x).fst.fst node z) (k₁ z) (k₂ z)
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
hnx : nx = node
⊢ Container.M.destruct x =
    { fst := { fst := (Container.M.destruct x).fst.fst, snd := node }, snd := fun x_1 => ↑(k₁ x_1) }
Tactic:
cases hnx
State after:
case h₀.left.refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst nx) → M C (N C (Container.M.destruct x).fst.fst nx y)
h₁ : destruct { val := x, property := wfx } = { fst := nx, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := nx, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst nx), R (N C (Container.M.destruct x).fst.fst nx z) (k₁ z) (k₂ z)
⊢ Container.M.destruct x =
    { fst := { fst := (Container.M.destruct x).fst.fst, snd := nx }, snd := fun x_1 => ↑(k₁ x_1) }

State before:
case h₀.left.refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst nx) → M C (N C (Container.M.destruct x).fst.fst nx y)
h₁ : destruct { val := x, property := wfx } = { fst := nx, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := nx, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst nx), R (N C (Container.M.destruct x).fst.fst nx z) (k₁ z) (k₂ z)
⊢ Container.M.destruct x =
    { fst := { fst := (Container.M.destruct x).fst.fst, snd := nx }, snd := fun x_1 => ↑(k₁ x_1) }
Tactic:
have h₁ := Sigma.snd_equals _ _ _ h₁
State after:
case h₀.left.refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst nx) → M C (N C (Container.M.destruct x).fst.fst nx y)
h₁✝ : destruct { val := x, property := wfx } = { fst := nx, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := nx, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst nx), R (N C (Container.M.destruct x).fst.fst nx z) (k₁ z) (k₂ z)
h₁ : (destruct { val := x, property := wfx }).snd = k₁
⊢ Container.M.destruct x =
    { fst := { fst := (Container.M.destruct x).fst.fst, snd := nx }, snd := fun x_1 => ↑(k₁ x_1) }

State before:
case h₀.left.refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst nx) → M C (N C (Container.M.destruct x).fst.fst nx y)
h₁✝ : destruct { val := x, property := wfx } = { fst := nx, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := nx, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst nx), R (N C (Container.M.destruct x).fst.fst nx z) (k₁ z) (k₂ z)
h₁ : (destruct { val := x, property := wfx }).snd = k₁
⊢ Container.M.destruct x =
    { fst := { fst := (Container.M.destruct x).fst.fst, snd := nx }, snd := fun x_1 => ↑(k₁ x_1) }
Tactic:
rw [← h₁]
State after:
case h₀.left.refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst nx) → M C (N C (Container.M.destruct x).fst.fst nx y)
h₁✝ : destruct { val := x, property := wfx } = { fst := nx, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := nx, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst nx), R (N C (Container.M.destruct x).fst.fst nx z) (k₁ z) (k₂ z)
h₁ : (destruct { val := x, property := wfx }).snd = k₁
⊢ Container.M.destruct x =
    { fst := { fst := (Container.M.destruct x).fst.fst, snd := nx },
      snd := fun x_1 => ↑(Sigma.snd (destruct { val := x, property := wfx }) x_1) }

State before:
case h₀.left.refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst nx) → M C (N C (Container.M.destruct x).fst.fst nx y)
h₁✝ : destruct { val := x, property := wfx } = { fst := nx, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := nx, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst nx), R (N C (Container.M.destruct x).fst.fst nx z) (k₁ z) (k₂ z)
h₁ : (destruct { val := x, property := wfx }).snd = k₁
⊢ Container.M.destruct x =
    { fst := { fst := (Container.M.destruct x).fst.fst, snd := nx },
      snd := fun x_1 => ↑(Sigma.snd (destruct { val := x, property := wfx }) x_1) }
Tactic:
rfl
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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct x).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst node) → M C (N C (Container.M.destruct x).fst.fst node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst node), R (N C (Container.M.destruct x).fst.fst node z) (k₁ z) (k₂ z)
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
⊢ nx = node
Tactic:
apply congrArg Sigma.fst h₁
State after:
no goals

State before:
case h₀.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ Container.M.destruct y = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₂ x) } ∧
    ∀ (i_1 : Container.B (toContainer C) { fst := i, snd := node }),
      ∃ i_2 wfx wfy,
        R i_2 { val := (fun x => ↑(k₁ x)) i_1, property := wfx } { val := (fun x => ↑(k₂ x)) i_1, property := wfy }
Tactic:
constructor
State after:
case h₀.right.left
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ Container.M.destruct y = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₂ x) }

case h₀.right.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ ∀ (i_1 : Container.B (toContainer C) { fst := i, snd := node }),
    ∃ i_2 wfx wfy,
      R i_2 { val := (fun x => ↑(k₁ x)) i_1, property := wfx } { val := (fun x => ↑(k₂ x)) i_1, property := wfy }

State before:
case h₀.right.left
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ Container.M.destruct y = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₂ x) }

case h₀.right.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ ∀ (i_1 : Container.B (toContainer C) { fst := i, snd := node }),
    ∃ i_2 wfx wfy,
      R i_2 { val := (fun x => ↑(k₁ x)) i_1, property := wfx } { val := (fun x => ↑(k₂ x)) i_1, property := wfy }
Tactic:
. cases hiy
  have hny: ny = node := by
    apply congrArg Sigma.fst h₂
  cases hny
  have h₂ := Sigma.snd_equals _ _ _ h₂
  rw [← h₂]
  rfl
State after:
case h₀.right.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ ∀ (i_1 : Container.B (toContainer C) { fst := i, snd := node }),
    ∃ i_2 wfx wfy,
      R i_2 { val := (fun x => ↑(k₁ x)) i_1, property := wfx } { val := (fun x => ↑(k₂ x)) i_1, property := wfy }

State before:
case h₀.right.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ ∀ (i_1 : Container.B (toContainer C) { fst := i, snd := node }),
    ∃ i_2 wfx wfy,
      R i_2 { val := (fun x => ↑(k₁ x)) i_1, property := wfx } { val := (fun x => ↑(k₂ x)) i_1, property := wfy }
Tactic:
. intro a
  exists C.N i node a
  simp only [toContainer] at a
  exists (by
      cases hix
      have : nx = node := by
        apply congrArg Sigma.fst h₁
      cases this
      have h₁ := Sigma.snd_equals _ _ _ h₁
      have wfx' := wfx' a
      cases h₁
      exact wfx'
    )
  exists (by
      cases hiy
      have : ny = node := by
        apply congrArg Sigma.fst h₂
      cases this
      have h₂ := Sigma.snd_equals _ _ _ h₂
      have wfy' := wfy' a
      cases h₂
      exact wfy'
    )
  exact h₃ a
State after:
no goals

State before:
case h₀.right.left
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ Container.M.destruct y = { fst := { fst := i, snd := node }, snd := fun x => ↑(k₂ x) }
Tactic:
cases hiy
State after:
case h₀.right.left.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct y).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst node) → M C (N C (Container.M.destruct y).fst.fst node y_1)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst node), R (N C (Container.M.destruct y).fst.fst node z) (k₁ z) (k₂ z)
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
⊢ Container.M.destruct y = { fst := { fst := (Container.M.destruct y).fst.fst, snd := node }, snd := fun x => ↑(k₂ x) }

State before:
case h₀.right.left.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct y).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst node) → M C (N C (Container.M.destruct y).fst.fst node y_1)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst node), R (N C (Container.M.destruct y).fst.fst node z) (k₁ z) (k₂ z)
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
⊢ Container.M.destruct y = { fst := { fst := (Container.M.destruct y).fst.fst, snd := node }, snd := fun x => ↑(k₂ x) }
Tactic:
have hny: ny = node := by
  apply congrArg Sigma.fst h₂
State after:
case h₀.right.left.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct y).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst node) → M C (N C (Container.M.destruct y).fst.fst node y_1)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst node), R (N C (Container.M.destruct y).fst.fst node z) (k₁ z) (k₂ z)
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
hny : ny = node
⊢ Container.M.destruct y = { fst := { fst := (Container.M.destruct y).fst.fst, snd := node }, snd := fun x => ↑(k₂ x) }

State before:
case h₀.right.left.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct y).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst node) → M C (N C (Container.M.destruct y).fst.fst node y_1)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst node), R (N C (Container.M.destruct y).fst.fst node z) (k₁ z) (k₂ z)
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
hny : ny = node
⊢ Container.M.destruct y = { fst := { fst := (Container.M.destruct y).fst.fst, snd := node }, snd := fun x => ↑(k₂ x) }
Tactic:
cases hny
State after:
case h₀.right.left.refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst ny) → M C (N C (Container.M.destruct y).fst.fst ny y_1)
h₁ : destruct { val := x, property := wfx } = { fst := ny, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := ny, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst ny), R (N C (Container.M.destruct y).fst.fst ny z) (k₁ z) (k₂ z)
⊢ Container.M.destruct y = { fst := { fst := (Container.M.destruct y).fst.fst, snd := ny }, snd := fun x => ↑(k₂ x) }

State before:
case h₀.right.left.refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst ny) → M C (N C (Container.M.destruct y).fst.fst ny y_1)
h₁ : destruct { val := x, property := wfx } = { fst := ny, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := ny, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst ny), R (N C (Container.M.destruct y).fst.fst ny z) (k₁ z) (k₂ z)
⊢ Container.M.destruct y = { fst := { fst := (Container.M.destruct y).fst.fst, snd := ny }, snd := fun x => ↑(k₂ x) }
Tactic:
have h₂ := Sigma.snd_equals _ _ _ h₂
State after:
case h₀.right.left.refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst ny) → M C (N C (Container.M.destruct y).fst.fst ny y_1)
h₁ : destruct { val := x, property := wfx } = { fst := ny, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := ny, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst ny), R (N C (Container.M.destruct y).fst.fst ny z) (k₁ z) (k₂ z)
h₂ : (destruct { val := y, property := wfy }).snd = k₂
⊢ Container.M.destruct y = { fst := { fst := (Container.M.destruct y).fst.fst, snd := ny }, snd := fun x => ↑(k₂ x) }

State before:
case h₀.right.left.refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst ny) → M C (N C (Container.M.destruct y).fst.fst ny y_1)
h₁ : destruct { val := x, property := wfx } = { fst := ny, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := ny, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst ny), R (N C (Container.M.destruct y).fst.fst ny z) (k₁ z) (k₂ z)
h₂ : (destruct { val := y, property := wfy }).snd = k₂
⊢ Container.M.destruct y = { fst := { fst := (Container.M.destruct y).fst.fst, snd := ny }, snd := fun x => ↑(k₂ x) }
Tactic:
rw [← h₂]
State after:
case h₀.right.left.refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst ny) → M C (N C (Container.M.destruct y).fst.fst ny y_1)
h₁ : destruct { val := x, property := wfx } = { fst := ny, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := ny, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst ny), R (N C (Container.M.destruct y).fst.fst ny z) (k₁ z) (k₂ z)
h₂ : (destruct { val := y, property := wfy }).snd = k₂
⊢ Container.M.destruct y =
    { fst := { fst := (Container.M.destruct y).fst.fst, snd := ny },
      snd := fun x => ↑(Sigma.snd (destruct { val := y, property := wfy }) x) }

State before:
case h₀.right.left.refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst ny) → M C (N C (Container.M.destruct y).fst.fst ny y_1)
h₁ : destruct { val := x, property := wfx } = { fst := ny, snd := k₁ }
h₂✝ : destruct { val := y, property := wfy } = { fst := ny, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst ny), R (N C (Container.M.destruct y).fst.fst ny z) (k₁ z) (k₂ z)
h₂ : (destruct { val := y, property := wfy }).snd = k₂
⊢ Container.M.destruct y =
    { fst := { fst := (Container.M.destruct y).fst.fst, snd := ny },
      snd := fun x => ↑(Sigma.snd (destruct { val := y, property := wfy }) x) }
Tactic:
rfl
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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct y).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst node) → M C (N C (Container.M.destruct y).fst.fst node y_1)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst node), R (N C (Container.M.destruct y).fst.fst node z) (k₁ z) (k₂ z)
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
⊢ ny = node
Tactic:
apply congrArg Sigma.fst h₂
State after:
no goals

State before:
case h₀.right.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
⊢ ∀ (i_1 : Container.B (toContainer C) { fst := i, snd := node }),
    ∃ i_2 wfx wfy,
      R i_2 { val := (fun x => ↑(k₁ x)) i_1, property := wfx } { val := (fun x => ↑(k₂ x)) i_1, property := wfy }
Tactic:
intro a
State after:
case h₀.right.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
a : Container.B (toContainer C) { fst := i, snd := node }
⊢ ∃ i_1 wfx wfy, R i_1 { val := (fun x => ↑(k₁ x)) a, property := wfx } { val := (fun x => ↑(k₂ x)) a, property := wfy }

State before:
case h₀.right.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
a : Container.B (toContainer C) { fst := i, snd := node }
⊢ ∃ i_1 wfx wfy, R i_1 { val := (fun x => ↑(k₁ x)) a, property := wfx } { val := (fun x => ↑(k₂ x)) a, property := wfy }
Tactic:
exists C.N i node a
State after:
case h₀.right.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
a : Container.B (toContainer C) { fst := i, snd := node }
⊢ ∃ wfx wfy,
    R (N C i node a) { val := (fun x => ↑(k₁ x)) a, property := wfx } { val := (fun x => ↑(k₂ x)) a, property := wfy }

State before:
case h₀.right.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
a : Container.B (toContainer C) { fst := i, snd := node }
⊢ ∃ wfx wfy,
    R (N C i node a) { val := (fun x => ↑(k₁ x)) a, property := wfx } { val := (fun x => ↑(k₂ x)) a, property := wfy }
Tactic:
simp only [toContainer] at a
State after:
case h₀.right.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
a : B C i node
⊢ ∃ wfx wfy,
    R (N C i node a) { val := (fun x => ↑(k₁ x)) a, property := wfx } { val := (fun x => ↑(k₂ x)) a, property := wfy }

State before:
case h₀.right.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
a : B C i node
⊢ ∃ wfx wfy,
    R (N C i node a) { val := (fun x => ↑(k₁ x)) a, property := wfx } { val := (fun x => ↑(k₂ x)) a, property := wfy }
Tactic:
exists (by
    cases hix
    have : nx = node := by
      apply congrArg Sigma.fst h₁
    cases this
    have h₁ := Sigma.snd_equals _ _ _ h₁
    have wfx' := wfx' a
    cases h₁
    exact wfx'
  )
State after:
case h₀.right.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
a : B C i node
⊢ ∃ wfy_1,
    R (N C i node a) { val := (fun x => ↑(k₁ x)) a, property := (_ : WellFormed (N C i node a) ((fun x => ↑(k₁ x)) a)) }
      { val := (fun x => ↑(k₂ x)) a, property := wfy_1 }

State before:
case h₀.right.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
a : B C i node
⊢ ∃ wfy_1,
    R (N C i node a) { val := (fun x => ↑(k₁ x)) a, property := (_ : WellFormed (N C i node a) ((fun x => ↑(k₁ x)) a)) }
      { val := (fun x => ↑(k₂ x)) a, property := wfy_1 }
Tactic:
exists (by
    cases hiy
    have : ny = node := by
      apply congrArg Sigma.fst h₂
    cases this
    have h₂ := Sigma.snd_equals _ _ _ h₂
    have wfy' := wfy' a
    cases h₂
    exact wfy'
  )
State after:
case h₀.right.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
a : B C i node
⊢ R (N C i node a) { val := (fun x => ↑(k₁ x)) a, property := (_ : WellFormed (N C i node a) ((fun x => ↑(k₁ x)) a)) }
    { val := (fun x => ↑(k₂ x)) a, property := (_ : WellFormed (N C i node a) ((fun x => ↑(k₂ x)) a)) }

State before:
case h₀.right.right
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
a : B C i node
⊢ R (N C i node a) { val := (fun x => ↑(k₁ x)) a, property := (_ : WellFormed (N C i node a) ((fun x => ↑(k₁ x)) a)) }
    { val := (fun x => ↑(k₂ x)) a, property := (_ : WellFormed (N C i 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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
a : B C i node
⊢ WellFormed (N C i node a) ((fun x => ↑(k₁ x)) a)
Tactic:
cases hix
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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct x).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst node) → M C (N C (Container.M.destruct x).fst.fst node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst node), R (N C (Container.M.destruct x).fst.fst node z) (k₁ z) (k₂ z)
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
a : B C (Container.M.destruct x).fst.fst node
⊢ WellFormed (N C (Container.M.destruct x).fst.fst node a) ((fun x_1 => ↑(k₁ x_1)) a)

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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct x).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst node) → M C (N C (Container.M.destruct x).fst.fst node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst node), R (N C (Container.M.destruct x).fst.fst node z) (k₁ z) (k₂ z)
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
a : B C (Container.M.destruct x).fst.fst node
⊢ WellFormed (N C (Container.M.destruct x).fst.fst node a) ((fun x_1 => ↑(k₁ x_1)) a)
Tactic:
have : nx = node := by
  apply congrArg Sigma.fst 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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct x).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst node) → M C (N C (Container.M.destruct x).fst.fst node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst node), R (N C (Container.M.destruct x).fst.fst node z) (k₁ z) (k₂ z)
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
a : B C (Container.M.destruct x).fst.fst node
this : nx = node
⊢ WellFormed (N C (Container.M.destruct x).fst.fst node a) ((fun x_1 => ↑(k₁ x_1)) a)

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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct x).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst node) → M C (N C (Container.M.destruct x).fst.fst node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst node), R (N C (Container.M.destruct x).fst.fst node z) (k₁ z) (k₂ z)
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
a : B C (Container.M.destruct x).fst.fst node
this : nx = node
⊢ WellFormed (N C (Container.M.destruct x).fst.fst node a) ((fun x_1 => ↑(k₁ x_1)) a)
Tactic:
cases this
State after:
case refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst nx) → M C (N C (Container.M.destruct x).fst.fst nx y)
h₁ : destruct { val := x, property := wfx } = { fst := nx, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := nx, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst nx), R (N C (Container.M.destruct x).fst.fst nx z) (k₁ z) (k₂ z)
a : B C (Container.M.destruct x).fst.fst nx
⊢ WellFormed (N C (Container.M.destruct x).fst.fst nx a) ((fun x_1 => ↑(k₁ x_1)) a)

State before:
case refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst nx) → M C (N C (Container.M.destruct x).fst.fst nx y)
h₁ : destruct { val := x, property := wfx } = { fst := nx, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := nx, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst nx), R (N C (Container.M.destruct x).fst.fst nx z) (k₁ z) (k₂ z)
a : B C (Container.M.destruct x).fst.fst nx
⊢ WellFormed (N C (Container.M.destruct x).fst.fst nx a) ((fun x_1 => ↑(k₁ x_1)) a)
Tactic:
have h₁ := Sigma.snd_equals _ _ _ h₁
State after:
case refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst nx) → M C (N C (Container.M.destruct x).fst.fst nx y)
h₁✝ : destruct { val := x, property := wfx } = { fst := nx, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := nx, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst nx), R (N C (Container.M.destruct x).fst.fst nx z) (k₁ z) (k₂ z)
a : B C (Container.M.destruct x).fst.fst nx
h₁ : (destruct { val := x, property := wfx }).snd = k₁
⊢ WellFormed (N C (Container.M.destruct x).fst.fst nx a) ((fun x_1 => ↑(k₁ x_1)) a)

State before:
case refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst nx) → M C (N C (Container.M.destruct x).fst.fst nx y)
h₁✝ : destruct { val := x, property := wfx } = { fst := nx, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := nx, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst nx), R (N C (Container.M.destruct x).fst.fst nx z) (k₁ z) (k₂ z)
a : B C (Container.M.destruct x).fst.fst nx
h₁ : (destruct { val := x, property := wfx }).snd = k₁
⊢ WellFormed (N C (Container.M.destruct x).fst.fst nx a) ((fun x_1 => ↑(k₁ x_1)) a)
Tactic:
have wfx' := wfx' a
State after:
case refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx'✝ : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst nx) → M C (N C (Container.M.destruct x).fst.fst nx y)
h₁✝ : destruct { val := x, property := wfx } = { fst := nx, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := nx, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst nx), R (N C (Container.M.destruct x).fst.fst nx z) (k₁ z) (k₂ z)
a : B C (Container.M.destruct x).fst.fst nx
h₁ : (destruct { val := x, property := wfx }).snd = k₁
wfx' : WellFormed (N C ix nx a) (kx a)
⊢ WellFormed (N C (Container.M.destruct x).fst.fst nx a) ((fun x_1 => ↑(k₁ x_1)) a)

State before:
case refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx'✝ : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst nx) → M C (N C (Container.M.destruct x).fst.fst nx y)
h₁✝ : destruct { val := x, property := wfx } = { fst := nx, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := nx, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst nx), R (N C (Container.M.destruct x).fst.fst nx z) (k₁ z) (k₂ z)
a : B C (Container.M.destruct x).fst.fst nx
h₁ : (destruct { val := x, property := wfx }).snd = k₁
wfx' : WellFormed (N C ix nx a) (kx a)
⊢ WellFormed (N C (Container.M.destruct x).fst.fst nx a) ((fun x_1 => ↑(k₁ x_1)) a)
Tactic:
cases h₁
State after:
case refl.refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx'✝ : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
k₂ : (y : B C (Container.M.destruct x).fst.fst nx) → M C (N C (Container.M.destruct x).fst.fst nx y)
h₂ : destruct { val := y, property := wfy } = { fst := nx, snd := k₂ }
a : B C (Container.M.destruct x).fst.fst nx
wfx' : WellFormed (N C ix nx a) (kx a)
h₁ : destruct { val := x, property := wfx } = { fst := nx, snd := (destruct { val := x, property := wfx }).snd }
h₃ :
  ∀ (z : B C (Container.M.destruct x).fst.fst nx),
    R (N C (Container.M.destruct x).fst.fst nx z) (Sigma.snd (destruct { val := x, property := wfx }) z) (k₂ z)
⊢ WellFormed (N C (Container.M.destruct x).fst.fst nx a)
    ((fun x_1 => ↑(Sigma.snd (destruct { val := x, property := wfx }) x_1)) a)

State before:
case refl.refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx'✝ : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
k₂ : (y : B C (Container.M.destruct x).fst.fst nx) → M C (N C (Container.M.destruct x).fst.fst nx y)
h₂ : destruct { val := y, property := wfy } = { fst := nx, snd := k₂ }
a : B C (Container.M.destruct x).fst.fst nx
wfx' : WellFormed (N C ix nx a) (kx a)
h₁ : destruct { val := x, property := wfx } = { fst := nx, snd := (destruct { val := x, property := wfx }).snd }
h₃ :
  ∀ (z : B C (Container.M.destruct x).fst.fst nx),
    R (N C (Container.M.destruct x).fst.fst nx z) (Sigma.snd (destruct { val := x, property := wfx }) z) (k₂ z)
⊢ WellFormed (N C (Container.M.destruct x).fst.fst nx a)
    ((fun x_1 => ↑(Sigma.snd (destruct { val := x, property := wfx }) x_1)) a)
Tactic:
exact 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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct x).fst.fst x
wfy : WellFormed (Container.M.destruct x).fst.fst y
r : R (Container.M.destruct x).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct x).fst.fst
k₁ k₂ : (y : B C (Container.M.destruct x).fst.fst node) → M C (N C (Container.M.destruct x).fst.fst node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct x).fst.fst node), R (N C (Container.M.destruct x).fst.fst node z) (k₁ z) (k₂ z)
hiy : (Container.M.destruct x).fst.fst = (Container.M.destruct y).fst.fst
a : B C (Container.M.destruct x).fst.fst node
⊢ nx = node
Tactic:
apply congrArg Sigma.fst h₁
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 i node), R (N C i 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 : A C i
k₁ k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
hix : i = (Container.M.destruct x).fst.fst
hiy : i = (Container.M.destruct y).fst.fst
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
a : B C i node
⊢ WellFormed (N C i node a) ((fun x => ↑(k₂ x)) a)
Tactic:
cases hiy
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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct y).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst node) → M C (N C (Container.M.destruct y).fst.fst node y_1)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst node), R (N C (Container.M.destruct y).fst.fst node z) (k₁ z) (k₂ z)
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
a : B C (Container.M.destruct y).fst.fst node
⊢ WellFormed (N C (Container.M.destruct y).fst.fst node a) ((fun x => ↑(k₂ x)) a)

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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct y).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst node) → M C (N C (Container.M.destruct y).fst.fst node y_1)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst node), R (N C (Container.M.destruct y).fst.fst node z) (k₁ z) (k₂ z)
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
a : B C (Container.M.destruct y).fst.fst node
⊢ WellFormed (N C (Container.M.destruct y).fst.fst node a) ((fun x => ↑(k₂ x)) a)
Tactic:
have : ny = node := by
  apply congrArg Sigma.fst 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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct y).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst node) → M C (N C (Container.M.destruct y).fst.fst node y_1)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst node), R (N C (Container.M.destruct y).fst.fst node z) (k₁ z) (k₂ z)
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
a : B C (Container.M.destruct y).fst.fst node
this : ny = node
⊢ WellFormed (N C (Container.M.destruct y).fst.fst node a) ((fun x => ↑(k₂ x)) a)

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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct y).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst node) → M C (N C (Container.M.destruct y).fst.fst node y_1)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst node), R (N C (Container.M.destruct y).fst.fst node z) (k₁ z) (k₂ z)
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
a : B C (Container.M.destruct y).fst.fst node
this : ny = node
⊢ WellFormed (N C (Container.M.destruct y).fst.fst node a) ((fun x => ↑(k₂ x)) a)
Tactic:
cases this
State after:
case refl.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 i node), R (N C i 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)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst ny) → M C (N C (Container.M.destruct y).fst.fst ny y_1)
h₁ : destruct { val := x, property := wfx } = { fst := ny, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := ny, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst ny), R (N C (Container.M.destruct y).fst.fst ny z) (k₁ z) (k₂ z)
a : B C (Container.M.destruct y).fst.fst ny
⊢ WellFormed (N C (Container.M.destruct y).fst.fst ny a) ((fun x => ↑(k₂ x)) a)