internlm/Lean-Github huggingface dataset:
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)
⊢ ∀ (x y : Container.M (C F)), r' x y → ↑(precongr F) r' x y
Tactic:
clear h₂
Proof state after:
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)
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)), r' x y → ↑(precongr F) r' x y
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)
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)), r' x y → ↑(precongr F) r' x y
Tactic:
intro x y h₂
Proof state after:
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)
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
⊢ ↑(precongr F) r' x y
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)
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
⊢ ↑(precongr F) r' x y
Tactic:
simp only [precongr, map_quot]
Proof state after:
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)
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
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct x)) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))
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)
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
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct x)) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))
Tactic:
have h₂ := h₁ _ _ h₂
Proof state after:
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)
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
h₂ : Quot.mk r <$> destruct (Quot.mk (congr F) x) = Quot.mk r <$> destruct (Quot.mk (congr F) y)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct x)) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))
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)
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
h₂ : Quot.mk r <$> destruct (Quot.mk (congr F) x) = Quot.mk r <$> destruct (Quot.mk (congr F) y)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct x)) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))
Tactic:
simp only [destruct, destruct.f] at h₂
Proof state after:
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)
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
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs (Container.M.destruct x) =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs (Container.M.destruct y)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct x)) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))
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)
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
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs (Container.M.destruct x) =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs (Container.M.destruct y)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct x)) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))
Tactic:
generalize Container.M.destruct x = x at *
Proof state after:
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)
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
x : Container.Obj (C F) (Container.M (C F))
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs x =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs (Container.M.destruct y)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) x) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))
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)
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
x : Container.Obj (C F) (Container.M (C F))
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs x =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs (Container.M.destruct y)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) x) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))
Tactic:
generalize Container.M.destruct y = y at *
Proof state after:
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)
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✝
x y : Container.Obj (C F) (Container.M (C F))
h₂ : Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs x = Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs y
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) x) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) y)
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)
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✝
x y : Container.Obj (C F) (Container.M (C F))
h₂ : Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs x = Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs y
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) x) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) y)
Tactic:
cases x with | mk nx kx =>
cases y with | mk ny ky =>
let f : Quot r → Quot r' :=
  by
    apply Quot.lift (Quot.lift (Quot.mk r') _) _
    . intro a b h₃
      apply Quot.sound
      simp only
      rw [Quot.sound h₃]
      apply h₀
    . 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
have : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r' := rfl
conv =>
  congr
  . rhs
    lhs
    intro i
    rw [←this]
    rfl
  . rhs
    lhs
    intro i
    rw [←this]
rw [Container.Map_spec, Container.Map_spec, Container.Map_spec, Container.Map_spec]
rw [inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, h₂]
Proof state after:
no goals
Theorem: QPF.M.bisim_lemma
Proof state before:
case a.a.mk
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✝
y : Container.Obj (C F) (Container.M (C F))
nx : (C F).A
kx : Container.B (C F) nx → 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 y
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := nx, snd := kx }) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) y)
Tactic:
cases y with | mk ny ky =>
let f : Quot r → Quot r' :=
  by
    apply Quot.lift (Quot.lift (Quot.mk r') _) _
    . intro a b h₃
      apply Quot.sound
      simp only
      rw [Quot.sound h₃]
      apply h₀
    . 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
have : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r' := rfl
conv =>
  congr
  . rhs
    lhs
    intro i
    rw [←this]
    rfl
  . rhs
    lhs
    intro i
    rw [←this]
rw [Container.Map_spec, Container.Map_spec, Container.Map_spec, Container.Map_spec]
rw [inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, h₂]
Proof state after:
no goals
Theorem: QPF.M.bisim_lemma
Proof state before:
case a.a.mk.mk
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 }
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := nx, snd := kx }) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := ny, snd := ky })
Tactic:
let f : Quot r → Quot r' :=
  by
    apply Quot.lift (Quot.lift (Quot.mk r') _) _
    . intro a b h₃
      apply Quot.sound
      simp only
      rw [Quot.sound h₃]
      apply h₀
    . 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:
case a.a.mk.mk
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 }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x 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)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := nx, snd := kx }) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := ny, snd := ky })
Theorem: QPF.M.bisim_lemma
Proof state before:
case a.a.mk.mk
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 }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x 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)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := nx, snd := kx }) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := ny, snd := ky })
Tactic:
have : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r' := rfl
Proof state after:
case a.a.mk.mk
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 }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x 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)
this : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r'
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := nx, snd := kx }) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := ny, snd := ky })
Theorem: QPF.M.bisim_lemma
Proof state before:
case a.a.mk.mk
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 }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x 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)
this : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r'
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := nx, snd := kx }) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := ny, snd := ky })
Tactic:
conv =>
  congr
  . rhs
    lhs
    intro i
    rw [←this]
    rfl
  . rhs
    lhs
    intro i
    rw [←this]
Proof state after:
case a.a.mk.mk
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 }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x 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)
this : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r'
⊢ abs (Container.Map (fun i => (f ∘ Quot.mk r ∘ Quot.mk (congr F)) i) { fst := nx, snd := kx }) =
    abs (Container.Map (fun i => (f ∘ Quot.mk r ∘ Quot.mk (congr F)) i) { fst := ny, snd := ky })
Theorem: QPF.M.bisim_lemma
Proof state before:
case a.a.mk.mk
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 }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x 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)
this : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r'
⊢ abs (Container.Map (fun i => (f ∘ Quot.mk r ∘ Quot.mk (congr F)) i) { fst := nx, snd := kx }) =
    abs (Container.Map (fun i => (f ∘ Quot.mk r ∘ Quot.mk (congr F)) i) { fst := ny, snd := ky })
Tactic:
rw [Container.Map_spec, Container.Map_spec, Container.Map_spec, Container.Map_spec]
Proof state after:
case a.a.mk.mk
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 }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x 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)
this : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r'
⊢ abs (Container.Map f (Container.Map (Quot.mk r) (Container.Map (Quot.mk (congr F)) { fst := nx, snd := kx }))) =
    abs (Container.Map f (Container.Map (Quot.mk r) (Container.Map (Quot.mk (congr F)) { fst := ny, snd := ky })))
Theorem: QPF.M.bisim_lemma
Proof state before:
case a.a.mk.mk
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 }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x 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)
this : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r'
⊢ abs (Container.Map f (Container.Map (Quot.mk r) (Container.Map (Quot.mk (congr F)) { fst := nx, snd := kx }))) =
    abs (Container.Map f (Container.Map (Quot.mk r) (Container.Map (Quot.mk (congr F)) { fst := ny, snd := ky })))
Tactic:
rw [inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, h₂]
Proof state after:
no goals