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 }
⊢ Quot r → Quot r'
Tactic:
apply Quot.lift (Quot.lift (Quot.mk r') _) _
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 }
⊢ ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b

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 }
⊢ ∀ (a b : Quot (congr F)), r a b → Quot.lift (Quot.mk r') ?m.11689 a = Quot.lift (Quot.mk r') ?m.11689 b
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 }
⊢ ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b

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 }
⊢ ∀ (a b : Quot (congr F)), r a b → Quot.lift (Quot.mk r') ?m.11689 a = Quot.lift (Quot.mk r') ?m.11689 b
Tactic:
. intro a b h₃
  apply Quot.sound
  simp only
  rw [Quot.sound h₃]
  apply 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 }
⊢ ∀ (a b : Quot (congr F)),
    r a b →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) a =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b
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 }
⊢ ∀ (a b : Quot (congr F)),
    r a b →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) a =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b
Tactic:
. intro x; apply Quot.inductionOn (motive := _) x; clear x
  intro x y; apply Quot.inductionOn (motive := _) y; clear y
  intro y h
  apply Quot.sound
  apply h
Proof state after:
no goals
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 }
⊢ ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b
Tactic:
intro a b 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 }
a b : Container.M (C F)
h₃ : congr F a b
⊢ Quot.mk r' a = Quot.mk r' b
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 }
a b : Container.M (C F)
h₃ : congr F a b
⊢ Quot.mk r' a = Quot.mk r' b
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 }
a b : Container.M (C F)
h₃ : congr F a b
⊢ r' a b
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 }
a b : Container.M (C F)
h₃ : congr F a b
⊢ r' a b
Tactic:
simp only
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 }
a b : Container.M (C F)
h₃ : congr F a b
⊢ r (Quot.mk (congr F) a) (Quot.mk (congr F) b)
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 }
a b : Container.M (C F)
h₃ : congr F a b
⊢ r (Quot.mk (congr F) a) (Quot.mk (congr F) b)
Tactic:
rw [Quot.sound h₃]
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 }
a b : Container.M (C F)
h₃ : congr F a b
⊢ r (Quot.mk (congr F) b) (Quot.mk (congr F) b)
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 }
a b : Container.M (C F)
h₃ : congr F a b
⊢ r (Quot.mk (congr F) b) (Quot.mk (congr F) b)
Tactic:
apply h₀
Proof state after:
no goals
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 }
⊢ ∀ (a b : Quot (congr F)),
    r a b →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) a =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b
Tactic:
intro x
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 : Quot (congr F)
⊢ ∀ (b : Quot (congr F)),
    r x b →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) x =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b
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 : Quot (congr F)
⊢ ∀ (b : Quot (congr F)),
    r x b →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) x =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b
Tactic:
apply Quot.inductionOn (motive := _) x
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 : Quot (congr F)
⊢ ∀ (a : Container.M (C F)) (b : Quot (congr F)),
    r (Quot.mk (congr F) a) b →
      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) =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b
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 : Quot (congr F)
⊢ ∀ (a : Container.M (C F)) (b : Quot (congr F)),
    r (Quot.mk (congr F) a) b →
      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) =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b
Tactic:
clear x
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 }
⊢ ∀ (a : Container.M (C F)) (b : Quot (congr F)),
    r (Quot.mk (congr F) a) b →
      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) =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b
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 }
⊢ ∀ (a : Container.M (C F)) (b : Quot (congr F)),
    r (Quot.mk (congr F) a) b →
      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) =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b
Tactic:
intro x 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)
y : Quot (congr F)
⊢ r (Quot.mk (congr F) x) 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) 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 : Container.M (C F)
y : Quot (congr F)
⊢ r (Quot.mk (congr F) x) 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) y
Tactic:
apply Quot.inductionOn (motive := _) 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)
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)