internlm/Lean-Github huggingface dataset:
Theorem: IQPF.M.bisim_lemma
Proof 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 : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i✝¹ : I
x✝ y✝ : IContainer.M (C F) i✝¹
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
i✝ : I
x y : IContainer.M (C F) i✝
h₂✝ : r' i✝ x y
nx : IContainer.A (C F) i✝
kx : (y : IContainer.B (C F) i✝ nx) → IContainer.M (C F) (IContainer.N (C F) i✝ nx y)
ny : IContainer.A (C F) i✝
ky : (y : IContainer.B (C F) i✝ ny) → IContainer.M (C F) (IContainer.N (C F) i✝ ny y)
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := nx, snd := kx })) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := ny, snd := ky }))
i : I
⊢ ∀ (a : IContainer.M (C F) i) (b : Quot (congr F i)),
    r i (Quot.mk (congr F i) a) b →
      Quot.lift (Quot.mk (r' i))
          (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b)
          (Quot.mk (congr F i) a) =
        Quot.lift (Quot.mk (r' i))
          (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b) b
Tactic:
intro x y
Proof 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 : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i✝¹ : I
x✝¹ y✝¹ : IContainer.M (C F) i✝¹
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
i✝ : I
x✝ y✝ : IContainer.M (C F) i✝
h₂✝ : r' i✝ x✝ y✝
nx : IContainer.A (C F) i✝
kx : (y : IContainer.B (C F) i✝ nx) → IContainer.M (C F) (IContainer.N (C F) i✝ nx y)
ny : IContainer.A (C F) i✝
ky : (y : IContainer.B (C F) i✝ ny) → IContainer.M (C F) (IContainer.N (C F) i✝ ny y)
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := nx, snd := kx })) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := ny, snd := ky }))
i : I
x : IContainer.M (C F) i
y : Quot (congr F i)
⊢ r i (Quot.mk (congr F i) x) y →
    Quot.lift (Quot.mk (r' i)) (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b)
        (Quot.mk (congr F i) x) =
      Quot.lift (Quot.mk (r' i))
        (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b) y
Theorem: IQPF.M.bisim_lemma
Proof 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 : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i✝¹ : I
x✝¹ y✝¹ : IContainer.M (C F) i✝¹
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
i✝ : I
x✝ y✝ : IContainer.M (C F) i✝
h₂✝ : r' i✝ x✝ y✝
nx : IContainer.A (C F) i✝
kx : (y : IContainer.B (C F) i✝ nx) → IContainer.M (C F) (IContainer.N (C F) i✝ nx y)
ny : IContainer.A (C F) i✝
ky : (y : IContainer.B (C F) i✝ ny) → IContainer.M (C F) (IContainer.N (C F) i✝ ny y)
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := nx, snd := kx })) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := ny, snd := ky }))
i : I
x : IContainer.M (C F) i
y : Quot (congr F i)
⊢ r i (Quot.mk (congr F i) x) y →
    Quot.lift (Quot.mk (r' i)) (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b)
        (Quot.mk (congr F i) x) =
      Quot.lift (Quot.mk (r' i))
        (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b) y
Tactic:
apply Quot.inductionOn (motive := _) y
Proof 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 : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i✝¹ : I
x✝¹ y✝¹ : IContainer.M (C F) i✝¹
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
i✝ : I
x✝ y✝ : IContainer.M (C F) i✝
h₂✝ : r' i✝ x✝ y✝
nx : IContainer.A (C F) i✝
kx : (y : IContainer.B (C F) i✝ nx) → IContainer.M (C F) (IContainer.N (C F) i✝ nx y)
ny : IContainer.A (C F) i✝
ky : (y : IContainer.B (C F) i✝ ny) → IContainer.M (C F) (IContainer.N (C F) i✝ ny y)
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := nx, snd := kx })) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := ny, snd := ky }))
i : I
x : IContainer.M (C F) i
y : Quot (congr F i)
⊢ ∀ (a : IContainer.M (C F) i),
    r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) a) →
      Quot.lift (Quot.mk (r' i))
          (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b)
          (Quot.mk (congr F i) x) =
        Quot.lift (Quot.mk (r' i))
          (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b)
          (Quot.mk (congr F i) a)
Theorem: IQPF.M.bisim_lemma
Proof 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 : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i✝¹ : I
x✝¹ y✝¹ : IContainer.M (C F) i✝¹
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
i✝ : I
x✝ y✝ : IContainer.M (C F) i✝
h₂✝ : r' i✝ x✝ y✝
nx : IContainer.A (C F) i✝
kx : (y : IContainer.B (C F) i✝ nx) → IContainer.M (C F) (IContainer.N (C F) i✝ nx y)
ny : IContainer.A (C F) i✝
ky : (y : IContainer.B (C F) i✝ ny) → IContainer.M (C F) (IContainer.N (C F) i✝ ny y)
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := nx, snd := kx })) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := ny, snd := ky }))
i : I
x : IContainer.M (C F) i
y : Quot (congr F i)
⊢ ∀ (a : IContainer.M (C F) i),
    r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) a) →
      Quot.lift (Quot.mk (r' i))
          (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b)
          (Quot.mk (congr F i) x) =
        Quot.lift (Quot.mk (r' i))
          (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b)
          (Quot.mk (congr F i) a)
Tactic:
clear y
Proof 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 : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i✝¹ : I
x✝¹ y✝ : IContainer.M (C F) i✝¹
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
i✝ : I
x✝ y : IContainer.M (C F) i✝
h₂✝ : r' i✝ x✝ y
nx : IContainer.A (C F) i✝
kx : (y : IContainer.B (C F) i✝ nx) → IContainer.M (C F) (IContainer.N (C F) i✝ nx y)
ny : IContainer.A (C F) i✝
ky : (y : IContainer.B (C F) i✝ ny) → IContainer.M (C F) (IContainer.N (C F) i✝ ny y)
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := nx, snd := kx })) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := ny, snd := ky }))
i : I
x : IContainer.M (C F) i
⊢ ∀ (a : IContainer.M (C F) i),
    r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) a) →
      Quot.lift (Quot.mk (r' i))
          (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b)
          (Quot.mk (congr F i) x) =
        Quot.lift (Quot.mk (r' i))
          (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b)
          (Quot.mk (congr F i) a)
Theorem: IQPF.M.bisim_lemma
Proof 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 : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i✝¹ : I
x✝¹ y✝ : IContainer.M (C F) i✝¹
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
i✝ : I
x✝ y : IContainer.M (C F) i✝
h₂✝ : r' i✝ x✝ y
nx : IContainer.A (C F) i✝
kx : (y : IContainer.B (C F) i✝ nx) → IContainer.M (C F) (IContainer.N (C F) i✝ nx y)
ny : IContainer.A (C F) i✝
ky : (y : IContainer.B (C F) i✝ ny) → IContainer.M (C F) (IContainer.N (C F) i✝ ny y)
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := nx, snd := kx })) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := ny, snd := ky }))
i : I
x : IContainer.M (C F) i
⊢ ∀ (a : IContainer.M (C F) i),
    r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) a) →
      Quot.lift (Quot.mk (r' i))
          (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b)
          (Quot.mk (congr F i) x) =
        Quot.lift (Quot.mk (r' i))
          (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b)
          (Quot.mk (congr F i) a)
Tactic:
intro y h
Proof 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 : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i✝¹ : I
x✝¹ y✝¹ : IContainer.M (C F) i✝¹
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
i✝ : I
x✝ y✝ : IContainer.M (C F) i✝
h₂✝ : r' i✝ x✝ y✝
nx : IContainer.A (C F) i✝
kx : (y : IContainer.B (C F) i✝ nx) → IContainer.M (C F) (IContainer.N (C F) i✝ nx y)
ny : IContainer.A (C F) i✝
ky : (y : IContainer.B (C F) i✝ ny) → IContainer.M (C F) (IContainer.N (C F) i✝ ny y)
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := nx, snd := kx })) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := ny, snd := ky }))
i : I
x y : IContainer.M (C F) i
h : r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
⊢ Quot.lift (Quot.mk (r' i)) (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b)
      (Quot.mk (congr F i) x) =
    Quot.lift (Quot.mk (r' i)) (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b)
      (Quot.mk (congr F i) y)
Theorem: IQPF.M.bisim_lemma
Proof 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 : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i✝¹ : I
x✝¹ y✝¹ : IContainer.M (C F) i✝¹
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
i✝ : I
x✝ y✝ : IContainer.M (C F) i✝
h₂✝ : r' i✝ x✝ y✝
nx : IContainer.A (C F) i✝
kx : (y : IContainer.B (C F) i✝ nx) → IContainer.M (C F) (IContainer.N (C F) i✝ nx y)
ny : IContainer.A (C F) i✝
ky : (y : IContainer.B (C F) i✝ ny) → IContainer.M (C F) (IContainer.N (C F) i✝ ny y)
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := nx, snd := kx })) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := ny, snd := ky }))
i : I
x y : IContainer.M (C F) i
h : r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
⊢ Quot.lift (Quot.mk (r' i)) (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b)
      (Quot.mk (congr F i) x) =
    Quot.lift (Quot.mk (r' i)) (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b)
      (Quot.mk (congr F i) y)
Tactic:
apply Quot.sound
Proof 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 : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i✝¹ : I
x✝¹ y✝¹ : IContainer.M (C F) i✝¹
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
i✝ : I
x✝ y✝ : IContainer.M (C F) i✝
h₂✝ : r' i✝ x✝ y✝
nx : IContainer.A (C F) i✝
kx : (y : IContainer.B (C F) i✝ nx) → IContainer.M (C F) (IContainer.N (C F) i✝ nx y)
ny : IContainer.A (C F) i✝
ky : (y : IContainer.B (C F) i✝ ny) → IContainer.M (C F) (IContainer.N (C F) i✝ ny y)
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := nx, snd := kx })) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := ny, snd := ky }))
i : I
x y : IContainer.M (C F) i
h : r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
⊢ r' i x y
Theorem: IQPF.M.bisim_lemma
Proof 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 : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i✝¹ : I
x✝¹ y✝¹ : IContainer.M (C F) i✝¹
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
i✝ : I
x✝ y✝ : IContainer.M (C F) i✝
h₂✝ : r' i✝ x✝ y✝
nx : IContainer.A (C F) i✝
kx : (y : IContainer.B (C F) i✝ nx) → IContainer.M (C F) (IContainer.N (C F) i✝ nx y)
ny : IContainer.A (C F) i✝
ky : (y : IContainer.B (C F) i✝ ny) → IContainer.M (C F) (IContainer.N (C F) i✝ ny y)
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := nx, snd := kx })) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := ny, snd := ky }))
i : I
x y : IContainer.M (C F) i
h : r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
⊢ r' i x y
Tactic:
apply h
Proof state after:
no goals
Theorem: IQPF.M.bisim_lemma
Proof 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 : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i✝¹ : I
x✝ y✝ : IContainer.M (C F) i✝¹
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
i✝ : I
x y : IContainer.M (C F) i✝
h₂✝ : r' i✝ x y
nx : IContainer.A (C F) i✝
kx : (y : IContainer.B (C F) i✝ nx) → IContainer.M (C F) (IContainer.N (C F) i✝ nx y)
ny : IContainer.A (C F) i✝
ky : (y : IContainer.B (C F) i✝ ny) → IContainer.M (C F) (IContainer.N (C F) i✝ ny y)
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := nx, snd := kx })) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs { fst := ny, snd := ky }))
f : (i : I) → Quot (r i) → Quot (r' i) :=
  fun i =>
    Quot.lift
      (Quot.lift (Quot.mk (r' i))
        (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b))
      (_ :
        ∀ (x b : Quot (congr F i)),
          r i x b →
            Quot.lift (Quot.mk (r' i))
                (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b) x =
              Quot.lift (Quot.mk (r' i))
                (_ : ∀ (a b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b) b)
i : I
⊢ f i ∘ Quot.mk (r i) ∘ Quot.mk (congr F i) = Quot.mk (r' i)
Tactic:
rfl
Proof state after:
no goals
Theorem: IQPF.M.bisim_lemma
Proof state before:
case a.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 : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i : I
x y : IContainer.M (C F) i
h₂ : r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
r' : (i : I) → IContainer.M (C F) i → IContainer.M (C F) i → Prop :=
  fun i x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
⊢ r' i x y
Tactic:
apply h₂
Proof state after:
no goals
Theorem: IQPF.M.bisim
Proof 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₁
Proof 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
Theorem: IQPF.M.bisim
Proof 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)
Proof 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
Theorem: IQPF.M.bisim
Proof 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
Proof 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
Theorem: IQPF.M.bisim
Proof 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
Proof 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
Theorem: IQPF.M.bisim
Proof 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
Proof state after:
no goals
Theorem: IQPF.M.bisim
Proof 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 _ _
Proof 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✝
Theorem: IQPF.M.bisim
Proof 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
Proof 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✝