internlm/Lean-Github huggingface dataset:
Theorem: IContainer.M.bisim
Proof 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
Proof 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 }
Theorem: IContainer.M.bisim
Proof 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
Proof state after:
no goals
Theorem: IContainer.M.bisim
Proof 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
Proof state after:
no goals
Theorem: IContainer.M.bisim
Proof 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₁
Proof state after:
no goals
Theorem: IContainer.M.bisim
Proof 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
Proof state after:
no goals
Theorem: IContainer.M.bisim
Proof 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
Proof state after:
no goals
Theorem: IContainer.M.bisim
Proof 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₂
Proof state after:
no goals
Theorem: IContainer.M.bisim
Proof 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
Proof state after:
no goals
Theorem: IContainer.M.bisim
Proof 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'
Proof state after:
no goals
Theorem: IContainer.M.bisim
Proof 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₁
Proof state after:
no goals