internlm/Lean-Github huggingface dataset:
Theorem: Container.M.construct_destruct
Proof state before:
case h₀
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀ : R x y
⊢ ∃ node k₁ k₂,
    destruct x = { fst := node, snd := k₁ } ∧
      destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
Tactic:
have h₀ := congrArg destruct h₀
Proof state after:
case h₀
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
⊢ ∃ node k₁ k₂,
    destruct x = { fst := node, snd := k₁ } ∧
      destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
Theorem: Container.M.construct_destruct
Proof state before:
case h₀
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
⊢ ∃ node k₁ k₂,
    destruct x = { fst := node, snd := k₁ } ∧
      destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
Tactic:
cases h₁:destruct y
Proof state after:
case h₀.mk
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
fst✝ : C.A
snd✝ : B C fst✝ → M C
h₁ : destruct y = { fst := fst✝, snd := snd✝ }
⊢ ∃ node k₁ k₂,
    destruct x = { fst := node, snd := k₁ } ∧
      { fst := fst✝, snd := snd✝ } = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
Theorem: Container.M.construct_destruct
Proof state before:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
node : C.A
k₂ : B C node → M C
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 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)
Tactic:
case mk node k₂ =>
  rw [h₁] at h₀
  simp only [construct, destruct_corec, Map] at h₀
  simp only [construct.automaton, Map] at h₀
  exists node
  exists construct ∘ destruct ∘ k₂
  exists k₂
  constructor
  . exact h₀
  . constructor
    . rfl
    . intro i
      rfl
Proof state after:
no goals
Theorem: Container.M.construct_destruct
Proof state before:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
node : C.A
k₂ : B C node → M C
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 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)
Tactic:
rw [h₁] at h₀
Proof state after:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
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 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)
Theorem: Container.M.construct_destruct
Proof state before:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
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 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)
Tactic:
simp only [construct, destruct_corec, Map] at h₀
Proof state after:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := (construct.automaton { fst := node, snd := k₂ }).fst,
      snd := corec construct.automaton ∘ (construct.automaton { fst := node, snd := k₂ }).snd }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)
Theorem: Container.M.construct_destruct
Proof state before:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ :
  destruct x =
    { fst := (construct.automaton { fst := node, snd := k₂ }).fst,
      snd := corec construct.automaton ∘ (construct.automaton { fst := node, snd := k₂ }).snd }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)
Tactic:
simp only [construct.automaton, Map] at h₀
Proof state after:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)
Theorem: Container.M.construct_destruct
Proof state before:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∃ node_1 k₁ k₂_1,
    destruct x = { fst := node_1, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node_1, snd := k₂_1 } ∧ ∀ (i : B C node_1), R (k₁ i) (k₂_1 i)
Tactic:
exists node
Proof state after:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∃ k₁ k₂_1,
    destruct x = { fst := node, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧ ∀ (i : B C node), R (k₁ i) (k₂_1 i)
Theorem: Container.M.construct_destruct
Proof state before:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∃ k₁ k₂_1,
    destruct x = { fst := node, snd := k₁ } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧ ∀ (i : B C node), R (k₁ i) (k₂_1 i)
Tactic:
exists construct ∘ destruct ∘ k₂
Proof state after:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∃ k₂_1,
    destruct x = { fst := node, snd := construct ∘ destruct ∘ k₂ } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧
        ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂_1 i)
Theorem: Container.M.construct_destruct
Proof state before:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∃ k₂_1,
    destruct x = { fst := node, snd := construct ∘ destruct ∘ k₂ } ∧
      { fst := node, snd := k₂ } = { fst := node, snd := k₂_1 } ∧
        ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂_1 i)
Tactic:
exists k₂
Proof state after:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ destruct x = { fst := node, snd := construct ∘ destruct ∘ k₂ } ∧
    { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Theorem: Container.M.construct_destruct
Proof state before:
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ destruct x = { fst := node, snd := construct ∘ destruct ∘ k₂ } ∧
    { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Tactic:
constructor
Proof state after:
case left
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ destruct x = { fst := node, snd := construct ∘ destruct ∘ k₂ }

case right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Theorem: Container.M.construct_destruct
Proof state before:
case left
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ destruct x = { fst := node, snd := construct ∘ destruct ∘ k₂ }

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

case right.right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Theorem: Container.M.construct_destruct
Proof state before:
case right.left
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ }

case right.right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Tactic:
. rfl
Proof state after:
case right.right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Theorem: Container.M.construct_destruct
Proof state before:
case right.right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Tactic:
. intro i
  rfl
Proof state after:
no goals
Theorem: Container.M.construct_destruct
Proof state before:
case right.left
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ { fst := node, snd := k₂ } = { fst := node, snd := k₂ }
Tactic:
rfl
Proof state after:
no goals
Theorem: Container.M.construct_destruct
Proof state before:
case right.right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
⊢ ∀ (i : B C node), R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Tactic:
intro i
Proof state after:
case right.right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
i : B C node
⊢ R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Theorem: Container.M.construct_destruct
Proof state before:
case right.right
C : Container
x✝ : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
x y : M C
h₀✝ : R x y
node : C.A
k₂ : B C node → M C
h₁ : destruct y = { fst := node, snd := k₂ }
h₀ : destruct x = { fst := node, snd := (corec fun x => { fst := x.fst, snd := destruct ∘ x.snd }) ∘ destruct ∘ k₂ }
i : B C node
⊢ R ((construct ∘ destruct ∘ k₂) i) (k₂ i)
Tactic:
rfl
Proof state after:
no goals
Theorem: Container.M.construct_destruct
Proof state before:
case a
C : Container
x : M C
R : M C → M C → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
Tactic:
rfl
Proof state after:
no goals
Theorem: IContainer.M.construct_destruct
Proof state before:
I : Type u₀
C : IContainer I
i : I
x : M C i
⊢ construct (destruct x) = x
Tactic:
let R i (x y: M C i) := x = construct (destruct y)
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)
⊢ construct (destruct x) = x
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)
⊢ construct (destruct x) = x
Tactic:
apply bisim R
Proof state after:
case h₀
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),
    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)

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
Theorem: IContainer.M.construct_destruct
Proof state before:
case h₀
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),
    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)

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:
. intro i x y h₀
  have h₀ := congrArg destruct h₀
  cases h₁:destruct y
  case mk node k₂ =>
    rw [h₁] at h₀
    simp only [construct, destruct_corec, Map] at h₀
    simp only [construct.automaton, Map] at h₀
    exists node
    exists λ (x:B C i node) => construct <| destruct <| k₂ x
    exists k₂
    constructor
    . exact h₀
    . constructor
      . rfl
      . intro i
        rfl
Proof state after:
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
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: IContainer.M.construct_destruct
Proof state before:
case h₀
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),
    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)
Tactic:
intro i x y h₀
Proof state after:
case h₀
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 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)
Theorem: IContainer.M.construct_destruct
Proof state before:
case h₀
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 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)
Tactic:
have h₀ := congrArg destruct h₀
Proof state after:
case h₀
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 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)
Theorem: IContainer.M.construct_destruct
Proof state before:
case h₀
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 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)
Tactic:
cases h₁:destruct y
Proof state after:
case h₀.mk
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))
fst✝ : A C i
snd✝ : (y : B C i fst✝) → M C (N C i fst✝ y)
h₁ : destruct y = { fst := fst✝, snd := snd✝ }
⊢ ∃ node k₁ k₂,
    destruct x = { fst := node, snd := k₁ } ∧
      { fst := fst✝, snd := snd✝ } = { fst := node, snd := k₂ } ∧ ∀ (z : B C i node), R (N C i node z) (k₁ 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
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:
case mk node k₂ =>
  rw [h₁] at h₀
  simp only [construct, destruct_corec, Map] at h₀
  simp only [construct.automaton, Map] at h₀
  exists node
  exists λ (x:B C i node) => construct <| destruct <| k₂ x
  exists k₂
  constructor
  . exact h₀
  . constructor
    . rfl
    . intro i
      rfl
Proof state after:
no goals