internlm/Lean-Github huggingface dataset:
Theorem: IQPF.M.bisim
Proof state before:
case h₀.h
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i : I
x y : M F i
h₁ : r i x y
i✝ : I
x✝ : M F i✝
⊢ x✝ = x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: IQPF.M.bisim
Proof state before:
case h₁
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i : I
x y : M F i
h₁ : r i x y
⊢ ∀ (i : I) (x y : M F i),
    x = y ∨ r i x y →
      IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct x) =
        IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct y)
Tactic:
intro i x y h₂
Proof state after:
case h₁
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
h₂ : x = y ∨ r i x y
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct x) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct y)
Theorem: IQPF.M.bisim
Proof state before:
case h₁
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
h₂ : x = y ∨ r i x y
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct x) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct y)
Tactic:
cases h₂
Proof state after:
case h₁.inl
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
h✝ : x = y
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct x) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct y)

case h₁.inr
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
h✝ : r i x y
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct x) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct y)
Theorem: IQPF.M.bisim
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
h₂ : x = y
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct x) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct y)
Tactic:
case inl h₂ =>
  rw [h₂]
Proof state after:
no goals
Theorem: IQPF.M.bisim
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
h₂ : r i x y
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct x) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct y)
Tactic:
case inr h₂ =>
  have ⟨z, h₃⟩ := h₀ _ _ _ h₂
  clear h₂
  rw [←h₃.1, ←h₃.2]
  clear h₃
  rw [←imap_spec, ←imap_spec]
  conv =>
    congr <;> rw [←abs_repr z]
  rw [←abs_imap]
  rw [←abs_imap]
  cases repr z with | mk nz kz =>
  simp only [IContainer.Map, Function.comp]
  apply congrArg abs
  rw [Sigma.mk.inj_iff]
  simp only [true_and, heq_eq_eq]
  funext a
  apply Quot.sound
  right
  apply (kz a).2
Proof state after:
no goals
Theorem: IQPF.M.bisim
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
h₂ : x = y
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct x) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct y)
Tactic:
rw [h₂]
Proof state after:
no goals
Theorem: IQPF.M.bisim
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
h₂ : r i x y
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct x) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct y)
Tactic:
have ⟨z, h₃⟩ := h₀ _ _ _ h₂
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
h₂ : r i x y
z : F (fun i => { p // r i p.fst p.snd }) i
h₃ : IFunctor.imap (fun x x_1 => (↑x_1).fst) z = destruct x ∧ IFunctor.imap (fun x x_1 => (↑x_1).snd) z = destruct y
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct x) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct y)
Theorem: IQPF.M.bisim
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
h₂ : r i x y
z : F (fun i => { p // r i p.fst p.snd }) i
h₃ : IFunctor.imap (fun x x_1 => (↑x_1).fst) z = destruct x ∧ IFunctor.imap (fun x x_1 => (↑x_1).snd) z = destruct y
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct x) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct y)
Tactic:
clear h₂
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
h₃ : IFunctor.imap (fun x x_1 => (↑x_1).fst) z = destruct x ∧ IFunctor.imap (fun x x_1 => (↑x_1).snd) z = destruct y
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct x) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct y)
Theorem: IQPF.M.bisim
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
h₃ : IFunctor.imap (fun x x_1 => (↑x_1).fst) z = destruct x ∧ IFunctor.imap (fun x x_1 => (↑x_1).snd) z = destruct y
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct x) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (destruct y)
Tactic:
rw [←h₃.1, ←h₃.2]
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
h₃ : IFunctor.imap (fun x x_1 => (↑x_1).fst) z = destruct x ∧ IFunctor.imap (fun x x_1 => (↑x_1).snd) z = destruct y
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (IFunctor.imap (fun x x_1 => (↑x_1).fst) z) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (IFunctor.imap (fun x x_1 => (↑x_1).snd) z)
Theorem: IQPF.M.bisim
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
h₃ : IFunctor.imap (fun x x_1 => (↑x_1).fst) z = destruct x ∧ IFunctor.imap (fun x x_1 => (↑x_1).snd) z = destruct y
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (IFunctor.imap (fun x x_1 => (↑x_1).fst) z) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (IFunctor.imap (fun x x_1 => (↑x_1).snd) z)
Tactic:
clear h₃
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (IFunctor.imap (fun x x_1 => (↑x_1).fst) z) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (IFunctor.imap (fun x x_1 => (↑x_1).snd) z)
Theorem: IQPF.M.bisim
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
⊢ IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (IFunctor.imap (fun x x_1 => (↑x_1).fst) z) =
    IFunctor.imap (fun i => Quot.mk fun x y => x = y ∨ r i x y) (IFunctor.imap (fun x x_1 => (↑x_1).snd) z)
Tactic:
rw [←imap_spec, ←imap_spec]
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
⊢ IFunctor.imap (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).fst) z =
    IFunctor.imap (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).snd) z
Theorem: IQPF.M.bisim
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
⊢ IFunctor.imap (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).fst) z =
    IFunctor.imap (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).snd) z
Tactic:
conv =>
  congr <;> rw [←abs_repr z]
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
⊢ IFunctor.imap (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).fst) (abs (repr z)) =
    IFunctor.imap (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).snd) (abs (repr z))
Theorem: IQPF.M.bisim
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
⊢ IFunctor.imap (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).fst) (abs (repr z)) =
    IFunctor.imap (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).snd) (abs (repr z))
Tactic:
rw [←abs_imap]
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
⊢ abs (IContainer.Map (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).fst) (repr z)) =
    IFunctor.imap (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).snd) (abs (repr z))
Theorem: IQPF.M.bisim
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
⊢ abs (IContainer.Map (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).fst) (repr z)) =
    IFunctor.imap (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).snd) (abs (repr z))
Tactic:
rw [←abs_imap]
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
⊢ abs (IContainer.Map (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).fst) (repr z)) =
    abs (IContainer.Map (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).snd) (repr z))
Theorem: IQPF.M.bisim
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
⊢ abs (IContainer.Map (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).fst) (repr z)) =
    abs (IContainer.Map (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).snd) (repr z))
Tactic:
cases repr z with | mk nz kz =>
simp only [IContainer.Map, Function.comp]
apply congrArg abs
rw [Sigma.mk.inj_iff]
simp only [true_and, heq_eq_eq]
funext a
apply Quot.sound
right
apply (kz a).2
Proof state after:
no goals
Theorem: IQPF.M.bisim
Proof state before:
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
⊢ abs (IContainer.Map (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).fst) { fst := nz, snd := kz }) =
    abs (IContainer.Map (fun i => (Quot.mk fun x y => x = y ∨ r i x y) ∘ fun x => (↑x).snd) { fst := nz, snd := kz })
Tactic:
simp only [IContainer.Map, Function.comp]
Proof state after:
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
⊢ abs
      { fst := nz,
        snd := fun y => Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).fst } =
    abs
      { fst := nz, snd := fun y => Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).snd }
Theorem: IQPF.M.bisim
Proof state before:
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
⊢ abs
      { fst := nz,
        snd := fun y => Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).fst } =
    abs
      { fst := nz, snd := fun y => Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).snd }
Tactic:
apply congrArg abs
Proof state after:
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
⊢ { fst := nz, snd := fun y => Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).fst } =
    { fst := nz, snd := fun y => Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).snd }
Theorem: IQPF.M.bisim
Proof state before:
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
⊢ { fst := nz, snd := fun y => Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).fst } =
    { fst := nz, snd := fun y => Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).snd }
Tactic:
rw [Sigma.mk.inj_iff]
Proof state after:
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
⊢ nz = nz ∧
    HEq (fun y => Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).fst) fun y =>
      Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).snd
Theorem: IQPF.M.bisim
Proof state before:
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
⊢ nz = nz ∧
    HEq (fun y => Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).fst) fun y =>
      Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).snd
Tactic:
simp only [true_and, heq_eq_eq]
Proof state after:
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
⊢ (fun y => Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).fst) = fun y =>
    Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).snd
Theorem: IQPF.M.bisim
Proof state before:
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
⊢ (fun y => Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).fst) = fun y =>
    Quot.mk (fun x y_1 => x = y_1 ∨ r (IContainer.N (C F) i nz y) x y_1) (↑(kz y)).snd
Tactic:
funext a
Proof state after:
case mk.h
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
a : IContainer.B (C F) i nz
⊢ Quot.mk (fun x y => x = y ∨ r (IContainer.N (C F) i nz a) x y) (↑(kz a)).fst =
    Quot.mk (fun x y => x = y ∨ r (IContainer.N (C F) i nz a) x y) (↑(kz a)).snd
Theorem: IQPF.M.bisim
Proof state before:
case mk.h
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
a : IContainer.B (C F) i nz
⊢ Quot.mk (fun x y => x = y ∨ r (IContainer.N (C F) i nz a) x y) (↑(kz a)).fst =
    Quot.mk (fun x y => x = y ∨ r (IContainer.N (C F) i nz a) x y) (↑(kz a)).snd
Tactic:
apply Quot.sound
Proof state after:
case mk.h.a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
a : IContainer.B (C F) i nz
⊢ (↑(kz a)).fst = (↑(kz a)).snd ∨ r (IContainer.N (C F) i nz a) (↑(kz a)).fst (↑(kz a)).snd
Theorem: IQPF.M.bisim
Proof state before:
case mk.h.a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
a : IContainer.B (C F) i nz
⊢ (↑(kz a)).fst = (↑(kz a)).snd ∨ r (IContainer.N (C F) i nz a) (↑(kz a)).fst (↑(kz a)).snd
Tactic:
right
Proof state after:
case mk.h.a.h
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
a : IContainer.B (C F) i nz
⊢ r (IContainer.N (C F) i nz a) (↑(kz a)).fst (↑(kz a)).snd
Theorem: IQPF.M.bisim
Proof state before:
case mk.h.a.h
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i✝ : I
x✝ y✝ : M F i✝
h₁ : r i✝ x✝ y✝
i : I
x y : M F i
z : F (fun i => { p // r i p.fst p.snd }) i
nz : IContainer.A (C F) i
kz : (y : IContainer.B (C F) i nz) → (fun i => { p // r i p.fst p.snd }) (IContainer.N (C F) i nz y)
a : IContainer.B (C F) i nz
⊢ r (IContainer.N (C F) i nz a) (↑(kz a)).fst (↑(kz a)).snd
Tactic:
apply (kz a).2
Proof state after:
no goals
Theorem: IQPF.M.bisim
Proof state before:
case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i : I
x y : M F i
h₁ : r i x y
⊢ x = y ∨ r i x y
Tactic:
right
Proof state after:
case a.h
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i : I
x y : M F i
h₁ : r i x y
⊢ r i x y
Theorem: IQPF.M.bisim
Proof state before:
case a.h
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x y : M F i), r i x y → liftr F r i (destruct x) (destruct y)
i : I
x y : M F i
h₁ : r i x y
⊢ r i x y
Tactic:
assumption
Proof state after:
no goals