internlm/Lean-Github huggingface dataset:
Theorem: QPF.M.bisim_lemma
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y✝ : Container.M (C F)
h₂✝ : r' x✝ y✝
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x : Container.M (C F)
y : Quot (congr F)
⊢ ∀ (a : Container.M (C F)),
    r (Quot.mk (congr F) x) (Quot.mk (congr F) a) →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) x) =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) a)
Tactic:
clear y
Proof state after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y : Container.M (C F)
h₂✝ : r' x✝ y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x : Container.M (C F)
⊢ ∀ (a : Container.M (C F)),
    r (Quot.mk (congr F) x) (Quot.mk (congr F) a) →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) x) =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) a)
Theorem: QPF.M.bisim_lemma
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y : Container.M (C F)
h₂✝ : r' x✝ y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x : Container.M (C F)
⊢ ∀ (a : Container.M (C F)),
    r (Quot.mk (congr F) x) (Quot.mk (congr F) a) →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) x) =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) a)
Tactic:
intro y h
Proof state after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y✝ : Container.M (C F)
h₂✝ : r' x✝ y✝
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x y : Container.M (C F)
h : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
      (Quot.mk (congr F) x) =
    Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
      (Quot.mk (congr F) y)
Theorem: QPF.M.bisim_lemma
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y✝ : Container.M (C F)
h₂✝ : r' x✝ y✝
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x y : Container.M (C F)
h : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
      (Quot.mk (congr F) x) =
    Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
      (Quot.mk (congr F) y)
Tactic:
apply Quot.sound
Proof state after:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y✝ : Container.M (C F)
h₂✝ : r' x✝ y✝
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x y : Container.M (C F)
h : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ r' x y
Theorem: QPF.M.bisim_lemma
Proof state before:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y✝ : Container.M (C F)
h₂✝ : r' x✝ y✝
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x y : Container.M (C F)
h : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ r' x y
Tactic:
apply h
Proof state after:
no goals
Theorem: QPF.M.bisim_lemma
Proof state before:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ r' x y
Tactic:
apply h₂
Proof state after:
no goals
Theorem: QPF.M.bisim
Proof 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₁
Proof 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
Theorem: QPF.M.bisim
Proof 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)
Proof 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
Theorem: QPF.M.bisim
Proof 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
Proof 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
Theorem: QPF.M.bisim
Proof 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
Proof 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
Theorem: QPF.M.bisim
Proof 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
Proof state after:
no goals
Theorem: QPF.M.bisim
Proof 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 _
Proof 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✝
Theorem: QPF.M.bisim
Proof 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
Proof 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✝
Theorem: QPF.M.bisim
Proof 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
Proof state after:
no goals
Theorem: QPF.M.bisim
Proof 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₂
Proof 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
Theorem: QPF.M.bisim
Proof 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₂
Proof 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
Theorem: QPF.M.bisim
Proof 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₂]
Proof state after:
no goals
Theorem: QPF.M.bisim
Proof 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
Proof state after:
no goals
Theorem: QPF.M.bisim
Proof 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₂]
Proof state after:
no goals
Theorem: QPF.M.bisim
Proof 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₂
Proof 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
Theorem: QPF.M.bisim
Proof 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₂
Proof 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
Theorem: QPF.M.bisim
Proof 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]
Proof 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
Theorem: QPF.M.bisim
Proof 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₃
Proof 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
Theorem: QPF.M.bisim
Proof 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]
Proof 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
Theorem: QPF.M.bisim
Proof 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]
Proof 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)
Theorem: QPF.M.bisim
Proof 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]
Proof 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)
Theorem: QPF.M.bisim
Proof 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]
Proof 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))
Theorem: QPF.M.bisim
Proof 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
Proof state after:
no goals
Theorem: QPF.M.bisim
Proof 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]
Proof 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 }
Theorem: QPF.M.bisim
Proof 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
Proof 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 }