internlm/Lean-Github huggingface dataset:
Theorem: Free.bind_pure
Proof state before:
case Free
C : _root_.Container
R S : Type u₁
r : R
k✝ : R → Free C S
n : C.A
k : Container.B C n → Free C S
⊢ Map (corec (bind.automaton k✝)) (Map Sum.inr (Functor.Free n k)) = Functor.Free n k
Tactic:
simp only [Map]
Proof state after:
case Free
C : _root_.Container
R S : Type u₁
r : R
k✝ : R → Free C S
n : C.A
k : Container.B C n → Free C S
⊢ Functor.Free n (corec (bind.automaton k✝) ∘ Sum.inr ∘ k) = Functor.Free n k
Theorem: Free.bind_pure
Proof state before:
case Free
C : _root_.Container
R S : Type u₁
r : R
k✝ : R → Free C S
n : C.A
k : Container.B C n → Free C S
⊢ Functor.Free n (corec (bind.automaton k✝) ∘ Sum.inr ∘ k) = Functor.Free n k
Tactic:
conv =>
  lhs
  congr
  simp only [Function.comp]
  intro x
  rw [bind_inr]
Proof state after:
no goals
Theorem: IContainer'.M.wf_destruct
Proof state before:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf : WellFormed i m
⊢ ∀ (x : B C (Container.M.destruct ↑{ val := m, property := wf }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := m, property := wf }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf }) x)
Tactic:
simp only [WellFormed, PWellFormed] at wf
Proof state after:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf : ↑(pgfp (WellFormedF C)) ⊥ i m
⊢ ∀ (x : B C (Container.M.destruct ↑{ val := m, property := wf }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := m, property := wf }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf }) x)
Theorem: IContainer'.M.wf_destruct
Proof state before:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf : ↑(pgfp (WellFormedF C)) ⊥ i m
⊢ ∀ (x : B C (Container.M.destruct ↑{ val := m, property := wf }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := m, property := wf }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf }) x)
Tactic:
rw [←pgfp.unfold] at wf
Proof state after:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (⊥ ⊔ ↑(pgfp (WellFormedF C)) ⊥) i m
⊢ ∀ (x : B C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf✝ }) x)
Theorem: IContainer'.M.wf_destruct
Proof state before:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (⊥ ⊔ ↑(pgfp (WellFormedF C)) ⊥) i m
⊢ ∀ (x : B C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf✝ }) x)
Tactic:
simp only [CompleteLattice.bot_sup] at wf
Proof state after:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (↑(pgfp (WellFormedF C)) ⊥) i m
⊢ ∀ (x : B C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf✝ }) x)
Theorem: IContainer'.M.wf_destruct
Proof state before:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (↑(pgfp (WellFormedF C)) ⊥) i m
⊢ ∀ (x : B C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf✝ }) x)
Tactic:
have ⟨_, y⟩ := wf
Proof state after:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (↑(pgfp (WellFormedF C)) ⊥) i m
left✝ : Idx C (Container.M.destruct m).fst = i
y :
  ∀ (x : B C (Container.M.destruct m).fst),
    ↑(pgfp (WellFormedF C)) ⊥ (Next C (Container.M.destruct m).fst x) (PSigma.snd (Container.M.destruct m) x)
⊢ ∀ (x : B C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf✝ }) x)
Theorem: IContainer'.M.wf_destruct
Proof state before:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (↑(pgfp (WellFormedF C)) ⊥) i m
left✝ : Idx C (Container.M.destruct m).fst = i
y :
  ∀ (x : B C (Container.M.destruct m).fst),
    ↑(pgfp (WellFormedF C)) ⊥ (Next C (Container.M.destruct m).fst x) (PSigma.snd (Container.M.destruct m) x)
⊢ ∀ (x : B C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst),
    WellFormed (Next C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf✝ }) x)
Tactic:
exact y
Proof state after:
no goals
Theorem: IContainer'.M.index_destruct
Proof state before:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf : WellFormed i m
⊢ i = Idx C (Container.M.destruct ↑{ val := m, property := wf }).fst
Tactic:
simp only [WellFormed, PWellFormed] at wf
Proof state after:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf : ↑(pgfp (WellFormedF C)) ⊥ i m
⊢ i = Idx C (Container.M.destruct ↑{ val := m, property := wf }).fst
Theorem: IContainer'.M.index_destruct
Proof state before:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf : ↑(pgfp (WellFormedF C)) ⊥ i m
⊢ i = Idx C (Container.M.destruct ↑{ val := m, property := wf }).fst
Tactic:
rw [←pgfp.unfold] at wf
Proof state after:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (⊥ ⊔ ↑(pgfp (WellFormedF C)) ⊥) i m
⊢ i = Idx C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst
Theorem: IContainer'.M.index_destruct
Proof state before:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (⊥ ⊔ ↑(pgfp (WellFormedF C)) ⊥) i m
⊢ i = Idx C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst
Tactic:
simp only [CompleteLattice.bot_sup] at wf
Proof state after:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (↑(pgfp (WellFormedF C)) ⊥) i m
⊢ i = Idx C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst
Theorem: IContainer'.M.index_destruct
Proof state before:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (↑(pgfp (WellFormedF C)) ⊥) i m
⊢ i = Idx C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst
Tactic:
have ⟨x, _⟩ := wf
Proof state after:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (↑(pgfp (WellFormedF C)) ⊥) i m
x : Idx C (Container.M.destruct m).fst = i
right✝ :
  ∀ (x : B C (Container.M.destruct m).fst),
    ↑(pgfp (WellFormedF C)) ⊥ (Next C (Container.M.destruct m).fst x) (PSigma.snd (Container.M.destruct m) x)
⊢ i = Idx C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst
Theorem: IContainer'.M.index_destruct
Proof state before:
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (↑(pgfp (WellFormedF C)) ⊥) i m
x : Idx C (Container.M.destruct m).fst = i
right✝ :
  ∀ (x : B C (Container.M.destruct m).fst),
    ↑(pgfp (WellFormedF C)) ⊥ (Next C (Container.M.destruct m).fst x) (PSigma.snd (Container.M.destruct m) x)
⊢ i = Idx C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst
Tactic:
apply Eq.symm
Proof state after:
case h
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (↑(pgfp (WellFormedF C)) ⊥) i m
x : Idx C (Container.M.destruct m).fst = i
right✝ :
  ∀ (x : B C (Container.M.destruct m).fst),
    ↑(pgfp (WellFormedF C)) ⊥ (Next C (Container.M.destruct m).fst x) (PSigma.snd (Container.M.destruct m) x)
⊢ Idx C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst = i
Theorem: IContainer'.M.index_destruct
Proof state before:
case h
I : Type u₀
C : IContainer' I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (↑(pgfp (WellFormedF C)) ⊥) i m
x : Idx C (Container.M.destruct m).fst = i
right✝ :
  ∀ (x : B C (Container.M.destruct m).fst),
    ↑(pgfp (WellFormedF C)) ⊥ (Next C (Container.M.destruct m).fst x) (PSigma.snd (Container.M.destruct m) x)
⊢ Idx C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst = i
Tactic:
exact x
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 ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
⊢ ∀ (x y : M C i), R i x y → x = y
Tactic:
intro ⟨x, wfx⟩ ⟨y, wfy⟩ h₁
Proof state after:
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ { val := x, property := wfx } = { val := y, property := wfy }
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 ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ { val := x, property := wfx } = { val := y, property := wfy }
Tactic:
suffices h: x = y by
  induction h
  rfl
Proof state after:
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ x = y
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 ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ x = y
Tactic:
apply Container.M.bisim (λ x y => ∃ i, ∃ (wfx: WellFormed i x) (wfy:WellFormed i y), R i ⟨x, wfx⟩ ⟨y, wfy⟩)
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 ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∀ (x y : Container.M (toContainer C)),
    (∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }) →
      ∃ node k₁ k₂,
        Container.M.destruct x = { fst := node, snd := k₁ } ∧
          Container.M.destruct y = { fst := node, snd := k₂ } ∧
            ∀ (i : Container.B (toContainer C) node),
              ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }

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

case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }
Tactic:
. intro x y ⟨i, wfx, wfy, r⟩
  have ⟨⟨node, h₄⟩, k₁, k₂, h₁, h₂, h₃⟩ := h₀ i ⟨x, wfx⟩ ⟨y, wfy⟩ r
  have h₁ := lift_destruct_eq _ _ _ _ h₁
  have h₂ := lift_destruct_eq _ _ _ _ h₂
  have wfx' := wf_destruct ⟨x, wfx⟩
  have wfy' := wf_destruct ⟨y, wfy⟩
  exists node
  exists λ a => (k₁ a).1
  exists λ x => (k₂ x).1
  simp only [h₁, h₂, true_and]
  intro a
  exists C.Next node a
  simp only [toContainer] at a
  exists (by
      rw [h₁] at wfx'
      apply wfx'
    )
  exists (by
      rw [h₂] at wfy'
      apply wfy'
    )
  exact h₃ a
Proof state after:
case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }
Theorem: IContainer'.M.bisim
Proof state before:
case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }
Tactic:
exists i
Proof state after:
case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }
Theorem: IContainer'.M.bisim
Proof state before:
case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }
Tactic:
exists wfx
Proof state after:
case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ wfy, R i { val := x, property := wfx } { val := y, property := wfy }
Theorem: IContainer'.M.bisim
Proof state before:
case a
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ wfy, R i { val := x, property := wfx } { val := y, property := wfy }
Tactic:
exists wfy
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 ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
h : x = y
⊢ { val := x, property := wfx } = { val := y, property := wfy }
Tactic:
induction h
Proof state after:
case refl
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i x
h₁ : R i { val := x, property := wfx } { val := x, property := wfy }
⊢ { val := x, property := wfx } = { val := x, property := wfy }
Theorem: IContainer'.M.bisim
Proof state before:
case refl
I : Type u₀
C : IContainer' I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i x
h₁ : R i { val := x, property := wfx } { val := x, property := wfy }
⊢ { val := x, property := wfx } = { val := x, property := wfy }
Tactic:
rfl
Proof state after:
no goals
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 ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i : I
x : Container.M (toContainer C)
wfx : WellFormed i x
y : Container.M (toContainer C)
wfy : WellFormed i y
h₁ : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∀ (x y : Container.M (toContainer C)),
    (∃ i wfx wfy, R i { val := x, property := wfx } { val := y, property := wfy }) →
      ∃ node k₁ k₂,
        Container.M.destruct x = { fst := node, snd := k₁ } ∧
          Container.M.destruct y = { fst := node, snd := k₂ } ∧
            ∀ (i : Container.B (toContainer C) node),
              ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }
Tactic:
intro x y ⟨i, wfx, wfy, r⟩
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 ↑node), R (Next C (↑node) z) (k₁ z) (k₂ z)
i✝ : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i✝ x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i✝ y✝
h₁ : R i✝ { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
i : I
wfx : WellFormed i x
wfy : WellFormed i y
r : R i { val := x, property := wfx } { val := y, property := wfy }
⊢ ∃ node k₁ k₂,
    Container.M.destruct x = { fst := node, snd := k₁ } ∧
      Container.M.destruct y = { fst := node, snd := k₂ } ∧
        ∀ (i : Container.B (toContainer C) node),
          ∃ i_1 wfx wfy, R i_1 { val := k₁ i, property := wfx } { val := k₂ i, property := wfy }