Theorem: IQPF.M.bisim (CoInd/QPF/MIdx.lean)

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), r i x y → x = y
Tactic:
intro i x y h₁
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
⊢ x = y

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
⊢ x = y
Tactic:
apply bisim_lemma (λ i x y => x = y ∨ r i x y)
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 : M F i), x = x ∨ r i x x

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)

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

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 : M F i), x = x ∨ r i x x

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)

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:
. intro _ _
  left
  rfl
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),
    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)

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

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)

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:
. intro i x y h₂
  cases h₂
  case inl h₂ =>
    rw [h₂]
  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
State after:
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

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; assumption
State after:
no goals

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 : M F i), x = x ∨ r i x x
Tactic:
intro _ _
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✝ : M F i✝
⊢ x✝ = x✝ ∨ r i✝ x✝ x✝

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✝ : M F i✝
⊢ x✝ = x✝ ∨ r i✝ x✝ x✝
Tactic:
left
State after:
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✝

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
State after:
no goals

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₂
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)

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₂
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)

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₂]
State after:
no goals

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
State after:
no goals

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₂]
State after:
no goals

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₂
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)

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₂
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)

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]
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)

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₃
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)

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]
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

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]
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))

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]
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))

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]
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))

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
State after:
no goals

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]
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 }

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
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 }

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]
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

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]
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
State after:
no goals