Theorem: IQPF.M.bisim_lemma
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 : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i✝¹ : I
x✝ y✝ : IContainer.M (C F) i✝¹
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
i✝ : I
x y : IContainer.M (C F) i✝
h₂✝ : r' i✝ x y
nx : IContainer.A (C F) i✝
kx : (y : IContainer.B (C F) i✝ nx) → IContainer.M (C F) (IContainer.N (C F) i✝ nx y)
ny : IContainer.A (C F) i✝
ky : (y : IContainer.B (C F) i✝ ny) → IContainer.M (C F) (IContainer.N (C F) i✝ ny y)
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := nx, snd := kx })) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := ny, snd := ky }))
i : I
⊢ ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b

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 : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i✝¹ : I
x✝ y✝ : IContainer.M (C F) i✝¹
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
i✝ : I
x y : IContainer.M (C F) i✝
h₂✝ : r' i✝ x y
nx : IContainer.A (C F) i✝
kx : (y : IContainer.B (C F) i✝ nx) → IContainer.M (C F) (IContainer.N (C F) i✝ nx y)
ny : IContainer.A (C F) i✝
ky : (y : IContainer.B (C F) i✝ ny) → IContainer.M (C F) (IContainer.N (C F) i✝ ny y)
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := nx, snd := kx })) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := ny, snd := ky }))
i : I
⊢ ∀ (a b : Quot (congr F i)), r i a b → Quot.lift (Quot.mk (r' i)) ?m.25601 a = Quot.lift (Quot.mk (r' i)) ?m.25601 b
Tactic:
. intro a b h₃
  apply Quot.sound
  simp only
  rw [Quot.sound h₃]
  apply 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 : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i✝¹ : I
x✝ y✝ : IContainer.M (C F) i✝¹
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
i✝ : I
x y : IContainer.M (C F) i✝
h₂✝ : r' i✝ x y
nx : IContainer.A (C F) i✝
kx : (y : IContainer.B (C F) i✝ nx) → IContainer.M (C F) (IContainer.N (C F) i✝ nx y)
ny : IContainer.A (C F) i✝
ky : (y : IContainer.B (C F) i✝ ny) → IContainer.M (C F) (IContainer.N (C F) i✝ ny y)
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := nx, snd := kx })) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := ny, snd := ky }))
i : I
⊢ ∀ (a b : Quot (congr F i)),
    r i a b →
      Quot.lift (Quot.mk (r' i))
          (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b) a =
        Quot.lift (Quot.mk (r' i))
          (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b) b