internlm/Lean-Github huggingface dataset:
Theorem: IContainer.M.construct_destruct
Proof state before:
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
h₀ : destruct x = destruct (construct (destruct y))
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)
Tactic:
rw [h₁] at h₀
Proof state after:
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₀ : destruct x = destruct (construct { fst := node, snd := k₂ })
h₁ : destruct y = { fst := node, snd := k₂ }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)
Theorem: IContainer.M.construct_destruct
Proof state before:
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₀ : destruct x = destruct (construct { fst := node, snd := k₂ })
h₁ : destruct y = { fst := node, snd := k₂ }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)
Tactic:
simp only [construct, destruct_corec, Map] at h₀
Proof state after:
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    match construct.automaton i { fst := node, snd := k₂ } with
    | { fst := x, snd := k } => { fst := x, snd := fun y => corec construct.automaton (k y) }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)
Theorem: IContainer.M.construct_destruct
Proof state before:
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    match construct.automaton i { fst := node, snd := k₂ } with
    | { fst := x, snd := k } => { fst := x, snd := fun y => corec construct.automaton (k y) }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)
Tactic:
simp only [construct.automaton, Map] at h₀
Proof state after:
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)
Theorem: IContainer.M.construct_destruct
Proof state before:
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧
        ∀ (z : B C i node_1), R (N C i node_1 z) (k₁ z) (k₂_1 z)
Tactic:
exists node
Proof state after:
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ ∃ k₁ k₂_1,
    destruct x = { fst := node, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧ ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂_1 z)
Theorem: IContainer.M.construct_destruct
Proof state before:
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ ∃ k₁ k₂_1,
    destruct x = { fst := node, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧ ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂_1 z)
Tactic:
exists λ (x:B C i node) => construct <| destruct <| k₂ x
Proof state after:
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ ∃ k₂_1,
    destruct x = { fst := node, snd := fun x => construct (destruct (k₂ x)) } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧
        ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂_1 z)
Theorem: IContainer.M.construct_destruct
Proof state before:
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ ∃ k₂_1,
    destruct x = { fst := node, snd := fun x => construct (destruct (k₂ x)) } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧
        ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂_1 z)
Tactic:
exists k₂
Proof state after:
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ destruct x = { fst := node, snd := fun x => construct (destruct (k₂ x)) } ∧
    { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧
      ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
Theorem: IContainer.M.construct_destruct
Proof state before:
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ destruct x = { fst := node, snd := fun x => construct (destruct (k₂ x)) } ∧
    { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧
      ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
Tactic:
constructor
Proof state after:
case left
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ destruct x = { fst := node, snd := fun x => construct (destruct (k₂ x)) }

case right
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧
    ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
Theorem: IContainer.M.construct_destruct
Proof state before:
case left
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ destruct x = { fst := node, snd := fun x => construct (destruct (k₂ x)) }

case right
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧
    ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
Tactic:
. exact h₀
Proof state after:
case right
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧
    ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
Theorem: IContainer.M.construct_destruct
Proof state before:
case right
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧
    ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
Tactic:
. constructor
  . rfl
  . intro i
    rfl
Proof state after:
no goals
Theorem: IContainer.M.construct_destruct
Proof state before:
case left
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ destruct x = { fst := node, snd := fun x => construct (destruct (k₂ x)) }
Tactic:
exact h₀
Proof state after:
no goals
Theorem: IContainer.M.construct_destruct
Proof state before:
case right
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧
    ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
Tactic:
constructor
Proof state after:
case right.left
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ }

case right.right
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
Theorem: IContainer.M.construct_destruct
Proof state before:
case right.left
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ }

case right.right
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
Tactic:
. rfl
Proof state after:
case right.right
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
Theorem: IContainer.M.construct_destruct
Proof state before:
case right.right
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
Tactic:
. intro i
  rfl
Proof state after:
no goals
Theorem: IContainer.M.construct_destruct
Proof state before:
case right.left
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ }
Tactic:
rfl
Proof state after:
no goals
Theorem: IContainer.M.construct_destruct
Proof state before:
case right.right
I : Type u₀
C : IContainer I
i✝ : I
x✝ : M C i✝
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i : I
x y : M C i
h₀✝ : R i x y
node : A C i
k₂ : (y : B C i node) → M C (N C i node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
⊢ ∀ (z : B C i node), R (N C i node z) ((fun x => construct (destruct (k₂ x))) z) (k₂ z)
Tactic:
intro i
Proof state after:
case right.right
I : Type u₀
C : IContainer I
i✝¹ : I
x✝ : M C i✝¹
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i✝ : I
x y : M C i✝
h₀✝ : R i✝ x y
node : A C i✝
k₂ : (y : B C i✝ node) → M C (N C i✝ node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
i : B C i✝ node
⊢ R (N C i✝ node i) ((fun x => construct (destruct (k₂ x))) i) (k₂ i)
Theorem: IContainer.M.construct_destruct
Proof state before:
case right.right
I : Type u₀
C : IContainer I
i✝¹ : I
x✝ : M C i✝¹
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
i✝ : I
x y : M C i✝
h₀✝ : R i✝ x y
node : A C i✝
k₂ : (y : B C i✝ node) → M C (N C i✝ node y)
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := node,
      snd := fun y =>
        corec
          (fun i x =>
            match x with
            | { fst := x, snd := k } => { fst := x, snd := fun y => destruct (k y) })
          (destruct (k₂ y)) }
i : B C i✝ node
⊢ R (N C i✝ node i) ((fun x => construct (destruct (k₂ x))) i) (k₂ i)
Tactic:
rfl
Proof state after:
no goals
Theorem: IContainer.M.construct_destruct
Proof state before:
case a
I : Type u₀
C : IContainer I
i : I
x : M C i
R : (i : I) → M C i → M C i → Prop := fun i x y => x = construct (destruct y)
⊢ R i (construct (destruct x)) x
Tactic:
rfl
Proof state after:
no goals
Theorem: QPF.M.construct_destruct
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
x : M F
⊢ construct (destruct x) = x
Tactic:
let R (x y: M F) := x = construct (destruct y)
Proof state after:
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ construct (destruct x) = x
Theorem: QPF.M.construct_destruct
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ construct (destruct x) = x
Tactic:
apply bisim R
Proof state after:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ ∀ (x y : M F), R x y → liftr F R (destruct x) (destruct y)

case a
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
Theorem: QPF.M.construct_destruct
Proof state before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ ∀ (x y : M F), R x y → liftr F R (destruct x) (destruct y)

case a
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
Tactic:
. intro x y h₀
  have h₀ := congrArg destruct h₀
  simp [liftr]
  simp only [construct, destruct_corec, construct.automaton] at h₀
  exists Functor.map (λ a => ⟨⟨construct <| destruct a, a⟩, by simp⟩) (destruct y)
  rw [h₀]
  constructor
  . simp only [←QPF.map_comp]
    rfl
  . rw [←QPF.M.map_comp]
    have : inst.map id (destruct y) = destruct y := by rw [QPF.map_id]
    apply Eq.trans _ this
    apply congrFun
    funext _
    rfl
Proof state after:
case a
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
Theorem: QPF.M.construct_destruct
Proof state before:
case a
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
Tactic:
. rfl
Proof state after:
no goals
Theorem: QPF.M.construct_destruct
Proof state before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ ∀ (x y : M F), R x y → liftr F R (destruct x) (destruct y)
Tactic:
intro x y h₀
Proof state after:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀ : R x y
⊢ liftr F R (destruct x) (destruct y)