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

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
⊢ ∀ (x y : M F), r x y → x = y
Tactic:
intro x y h₁
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ x = y

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ x = y
Tactic:
apply bisim_lemma (λ x y => x = y ∨ r x y)
State after:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ ∀ (x : M F), x = x ∨ r x x

case h₁
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ ∀ (x y : M F),
    x = y ∨ r x y →
      (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y

case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ x = y ∨ r x y

State before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ ∀ (x : M F), x = x ∨ r x x

case h₁
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ ∀ (x y : M F),
    x = y ∨ r x y →
      (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y

case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ x = y ∨ r x y
Tactic:
. intro _
  left
  rfl
State after:
case h₁
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ ∀ (x y : M F),
    x = y ∨ r x y →
      (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y

case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ x = y ∨ r x y

State before:
case h₁
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ ∀ (x y : M F),
    x = y ∨ r x y →
      (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y

case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ x = y ∨ r x y
Tactic:
. intro 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 [←map_comp, ←map_comp]
    conv =>
      congr <;> rw [←abs_repr z]
    rw [←abs_map]
    rw [←abs_map]
    cases repr z with | mk nz kz =>
    simp only [Container.Map, Function.comp]
    apply congrArg abs
    rw [Container.Obj.snd_equals_iff]
    funext a
    apply Quot.sound
    right
    apply (kz a).2
State after:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ x = y ∨ r x y

State before:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ x = y ∨ r x y
Tactic:
. right; assumption
State after:
no goals

State before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ ∀ (x : M F), x = x ∨ r x x
Tactic:
intro _
State after:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
x✝ : M F
⊢ x✝ = x✝ ∨ r x✝ x✝

State before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
x✝ : M F
⊢ x✝ = x✝ ∨ r x✝ x✝
Tactic:
left
State after:
case h₀.h
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
x✝ : M F
⊢ x✝ = x✝

State before:
case h₀.h
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
x✝ : M F
⊢ x✝ = x✝
Tactic:
rfl
State after:
no goals

State before:
case h₁
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ ∀ (x y : M F),
    x = y ∨ r x y →
      (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y
Tactic:
intro x y h₂
State after:
case h₁
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
h₂ : x = y ∨ r x y
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y

State before:
case h₁
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
h₂ : x = y ∨ r x y
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y
Tactic:
cases h₂
State after:
case h₁.inl
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
h✝ : x = y
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y

case h₁.inr
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
h✝ : r x y
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
h₂ : x = y
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y
Tactic:
case inl h₂ =>
  rw [h₂]
State after:
no goals

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
h₂ : r x y
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y
Tactic:
case inr h₂ =>
  have ⟨z, h₃⟩ := h₀ _ _ h₂
  clear h₂
  rw [←h₃.1, ←h₃.2]
  clear h₃
  rw [←map_comp, ←map_comp]
  conv =>
    congr <;> rw [←abs_repr z]
  rw [←abs_map]
  rw [←abs_map]
  cases repr z with | mk nz kz =>
  simp only [Container.Map, Function.comp]
  apply congrArg abs
  rw [Container.Obj.snd_equals_iff]
  funext a
  apply Quot.sound
  right
  apply (kz a).2
State after:
no goals

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
h₂ : x = y
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y
Tactic:
rw [h₂]
State after:
no goals

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
h₂ : r x y
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y
Tactic:
have ⟨z, h₃⟩ := h₀ _ _ h₂
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
h₂ : r x y
z : F { p // r p.fst p.snd }
h₃ : (fun x => (↑x).fst) <$> z = destruct x ∧ (fun x => (↑x).snd) <$> z = destruct y
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
h₂ : r x y
z : F { p // r p.fst p.snd }
h₃ : (fun x => (↑x).fst) <$> z = destruct x ∧ (fun x => (↑x).snd) <$> z = destruct y
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y
Tactic:
clear h₂
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
h₃ : (fun x => (↑x).fst) <$> z = destruct x ∧ (fun x => (↑x).snd) <$> z = destruct y
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
h₃ : (fun x => (↑x).fst) <$> z = destruct x ∧ (fun x => (↑x).snd) <$> z = destruct y
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> destruct x = (Quot.mk fun x y => x = y ∨ r x y) <$> destruct y
Tactic:
rw [←h₃.1, ←h₃.2]
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
h₃ : (fun x => (↑x).fst) <$> z = destruct x ∧ (fun x => (↑x).snd) <$> z = destruct y
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> (fun x => (↑x).fst) <$> z =
    (Quot.mk fun x y => x = y ∨ r x y) <$> (fun x => (↑x).snd) <$> z

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
h₃ : (fun x => (↑x).fst) <$> z = destruct x ∧ (fun x => (↑x).snd) <$> z = destruct y
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> (fun x => (↑x).fst) <$> z =
    (Quot.mk fun x y => x = y ∨ r x y) <$> (fun x => (↑x).snd) <$> z
Tactic:
clear h₃
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> (fun x => (↑x).fst) <$> z =
    (Quot.mk fun x y => x = y ∨ r x y) <$> (fun x => (↑x).snd) <$> z

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
⊢ (Quot.mk fun x y => x = y ∨ r x y) <$> (fun x => (↑x).fst) <$> z =
    (Quot.mk fun x y => x = y ∨ r x y) <$> (fun x => (↑x).snd) <$> z
Tactic:
rw [←map_comp, ←map_comp]
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
⊢ ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).fst) <$> z =
    ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).snd) <$> z

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
⊢ ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).fst) <$> z =
    ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).snd) <$> z
Tactic:
conv =>
  congr <;> rw [←abs_repr z]
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
⊢ ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).fst) <$> abs (repr z) =
    ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).snd) <$> abs (repr z)

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
⊢ ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).fst) <$> abs (repr z) =
    ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).snd) <$> abs (repr z)
Tactic:
rw [←abs_map]
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
⊢ abs (Container.Map ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).fst) (repr z)) =
    ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).snd) <$> abs (repr z)

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
⊢ abs (Container.Map ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).fst) (repr z)) =
    ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).snd) <$> abs (repr z)
Tactic:
rw [←abs_map]
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
⊢ abs (Container.Map ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).fst) (repr z)) =
    abs (Container.Map ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).snd) (repr z))

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
⊢ abs (Container.Map ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).fst) (repr z)) =
    abs (Container.Map ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).snd) (repr z))
Tactic:
cases repr z with | mk nz kz =>
simp only [Container.Map, Function.comp]
apply congrArg abs
rw [Container.Obj.snd_equals_iff]
funext a
apply Quot.sound
right
apply (kz a).2
State after:
no goals

State before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
⊢ abs (Container.Map ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).fst) { fst := nz, snd := kz }) =
    abs (Container.Map ((Quot.mk fun x y => x = y ∨ r x y) ∘ fun x => (↑x).snd) { fst := nz, snd := kz })
Tactic:
simp only [Container.Map, Function.comp]
State after:
case mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
⊢ abs { fst := nz, snd := fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).fst } =
    abs { fst := nz, snd := fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).snd }

State before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
⊢ abs { fst := nz, snd := fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).fst } =
    abs { fst := nz, snd := fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).snd }
Tactic:
apply congrArg abs
State after:
case mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
⊢ { fst := nz, snd := fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).fst } =
    { fst := nz, snd := fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).snd }

State before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
⊢ { fst := nz, snd := fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).fst } =
    { fst := nz, snd := fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).snd }
Tactic:
rw [Container.Obj.snd_equals_iff]
State after:
case mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
⊢ (fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).fst) = fun x =>
    Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).snd

State before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
⊢ (fun x => Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).fst) = fun x =>
    Quot.mk (fun x y => x = y ∨ r x y) (↑(kz x)).snd
Tactic:
funext a
State after:
case mk.h
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
a : Container.B (C F) nz
⊢ Quot.mk (fun x y => x = y ∨ r x y) (↑(kz a)).fst = Quot.mk (fun x y => x = y ∨ r x y) (↑(kz a)).snd

State before:
case mk.h
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
a : Container.B (C F) nz
⊢ Quot.mk (fun x y => x = y ∨ r x y) (↑(kz a)).fst = Quot.mk (fun x y => x = y ∨ r x y) (↑(kz a)).snd
Tactic:
apply Quot.sound
State after:
case mk.h.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
a : Container.B (C F) nz
⊢ (↑(kz a)).fst = (↑(kz a)).snd ∨ r (↑(kz a)).fst (↑(kz a)).snd

State before:
case mk.h.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
a : Container.B (C F) nz
⊢ (↑(kz a)).fst = (↑(kz a)).snd ∨ r (↑(kz a)).fst (↑(kz a)).snd
Tactic:
right
State after:
case mk.h.a.h
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
a : Container.B (C F) nz
⊢ r (↑(kz a)).fst (↑(kz a)).snd

State before:
case mk.h.a.h
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x✝ y✝ : M F
h₁ : r x✝ y✝
x y : M F
z : F { p // r p.fst p.snd }
nz : (C F).A
kz : Container.B (C F) nz → { p // r p.fst p.snd }
a : Container.B (C F) nz
⊢ r (↑(kz a)).fst (↑(kz a)).snd
Tactic:
apply (kz a).2
State after:
no goals

State before:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ x = y ∨ r x y
Tactic:
right
State after:
case a.h
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ r x y

State before:
case a.h
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x y : M F), r x y → liftr F r (destruct x) (destruct y)
x y : M F
h₁ : r x y
⊢ r x y
Tactic:
assumption
State after:
no goals