Theorem: IQPF.M.bisim_lemma (CoInd/QPF/MIdx.lean)

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 : M F i), r i x y → x = y
Tactic:
intro i x
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 : M F i
⊢ ∀ (y : M F i), r i x y → x = y

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 : M F i
⊢ ∀ (y : M F i), r i x y → x = y
Tactic:
apply Quot.inductionOn (motive := _) x
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 : M F i
⊢ ∀ (a : IContainer.M (C F) i) (y : M F i), r i (Quot.mk (congr F i) a) y → Quot.mk (congr F i) a = y

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 : M F i
⊢ ∀ (a : IContainer.M (C F) i) (y : M F i), r i (Quot.mk (congr F i) a) y → Quot.mk (congr F i) a = y
Tactic:
clear x
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
⊢ ∀ (a : IContainer.M (C F) i) (y : M F i), r i (Quot.mk (congr F i) a) y → Quot.mk (congr F i) a = y

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
⊢ ∀ (a : IContainer.M (C F) i) (y : M F i), r i (Quot.mk (congr F i) a) y → Quot.mk (congr F i) a = y
Tactic:
intro x y
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 : IContainer.M (C F) i
y : M F i
⊢ r i (Quot.mk (congr F i) x) y → Quot.mk (congr F i) x = y

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 : IContainer.M (C F) i
y : M F i
⊢ r i (Quot.mk (congr F i) x) y → Quot.mk (congr F i) x = y
Tactic:
apply Quot.inductionOn (motive := _) y
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 : IContainer.M (C F) i
y : M F i
⊢ ∀ (a : IContainer.M (C F) i),
    r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) a) → Quot.mk (congr F i) x = Quot.mk (congr F i) a

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 : IContainer.M (C F) i
y : M F i
⊢ ∀ (a : IContainer.M (C F) i),
    r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) a) → Quot.mk (congr F i) x = Quot.mk (congr F i) a
Tactic:
clear y
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 : 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.mk (congr F i) x = Quot.mk (congr F i) a

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 : 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.mk (congr F i) x = Quot.mk (congr F i) a
Tactic:
intro y h₂
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
h₂ : r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
⊢ Quot.mk (congr F i) x = Quot.mk (congr F i) y

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
h₂ : r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
⊢ Quot.mk (congr F i) x = Quot.mk (congr F i) y
Tactic:
apply Quot.sound
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
h₂ : r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
⊢ congr F i x y

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
h₂ : r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)
⊢ congr F i x y
Tactic:
let r' i x y := r i (Quot.mk _ x) (Quot.mk _ y)
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
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)
⊢ congr F i x y

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
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)
⊢ congr F i x y
Tactic:
apply congr.coinduction r'
State after:
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)
⊢ ∀ (i : I) (x y : IContainer.M (C F) i), r' i x y → ↑(precongr F) r' i x y

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

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)
⊢ ∀ (i : I) (x y : IContainer.M (C F) i), r' i x y → ↑(precongr F) r' i x y

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:
. clear h₂
  intro i x y h₂
  simp only [precongr, map_quot]
  have h₂ := h₁ i _ _ h₂
  simp only [destruct, destruct.f] at h₂
  generalize IContainer.M.destruct x = x at *
  generalize IContainer.M.destruct y = y at *
  cases x with | mk nx kx =>
  cases y with | mk ny ky =>
  let f i : Quot (r i) → Quot (r' i) :=
    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 : ∀ i, f i ∘ Quot.mk (r _) ∘ Quot.mk (congr F _) = Quot.mk (r' _) := by intro i; rfl
  conv =>
    congr
    . rhs
      lhs
      intro i
      rw [←this]
      rfl
    . rhs
      lhs
      intro i
      rw [←this]
  rw [IContainer.Map_spec, IContainer.Map_spec, IContainer.Map_spec, IContainer.Map_spec]
  rw [inst.abs_imap, inst.abs_imap, inst.abs_imap, inst.abs_imap, inst.abs_imap, inst.abs_imap, h₂]
State after:
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

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₂
State after:
no goals

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)
⊢ ∀ (i : I) (x y : IContainer.M (C F) i), r' i x y → ↑(precongr F) r' i x y
Tactic:
clear h₂
State after:
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
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), r' i x y → ↑(precongr F) r' i x y

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
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), r' i x y → ↑(precongr F) r' i x y
Tactic:
intro i x y h₂
State after:
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✝
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
⊢ ↑(precongr F) r' i x y

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✝
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
⊢ ↑(precongr F) r' i x y
Tactic:
simp only [precongr, map_quot]
State after:
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✝
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
⊢ abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        (IContainer.M.destruct x)) =
    abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        (IContainer.M.destruct y))

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✝
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
⊢ abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        (IContainer.M.destruct x)) =
    abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        (IContainer.M.destruct y))
Tactic:
have h₂ := h₁ i _ _ h₂
State after:
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✝
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
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i)) (destruct (Quot.mk (congr F i) x)) =
    IFunctor.imap (fun i => Quot.mk (r i)) (destruct (Quot.mk (congr F i) y))
⊢ abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        (IContainer.M.destruct x)) =
    abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        (IContainer.M.destruct y))

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✝
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
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i)) (destruct (Quot.mk (congr F i) x)) =
    IFunctor.imap (fun i => Quot.mk (r i)) (destruct (Quot.mk (congr F i) y))
⊢ abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        (IContainer.M.destruct x)) =
    abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        (IContainer.M.destruct y))
Tactic:
simp only [destruct, destruct.f] at h₂
State after:
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✝
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
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs (IContainer.M.destruct x))) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs (IContainer.M.destruct y)))
⊢ abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        (IContainer.M.destruct x)) =
    abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        (IContainer.M.destruct y))

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✝
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
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs (IContainer.M.destruct x))) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs (IContainer.M.destruct y)))
⊢ abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        (IContainer.M.destruct x)) =
    abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        (IContainer.M.destruct y))
Tactic:
generalize IContainer.M.destruct x = x at *
State after:
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✝
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
x : IContainer.Obj (C F) (IContainer.M (C F)) i
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i)) (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs x)) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs (IContainer.M.destruct y)))
⊢ abs (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)) x) =
    abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        (IContainer.M.destruct y))

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✝
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
x : IContainer.Obj (C F) (IContainer.M (C F)) i
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i)) (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs x)) =
    IFunctor.imap (fun i => Quot.mk (r i))
      (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs (IContainer.M.destruct y)))
⊢ abs (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)) x) =
    abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        (IContainer.M.destruct y))
Tactic:
generalize IContainer.M.destruct y = y at *
State after:
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✝
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✝
x y : IContainer.Obj (C F) (IContainer.M (C F)) i
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i)) (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs x)) =
    IFunctor.imap (fun i => Quot.mk (r i)) (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs y))
⊢ abs (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)) x) =
    abs (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)) y)

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✝
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✝
x y : IContainer.Obj (C F) (IContainer.M (C F)) i
h₂ :
  IFunctor.imap (fun i => Quot.mk (r i)) (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs x)) =
    IFunctor.imap (fun i => Quot.mk (r i)) (IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1) (abs y))
⊢ abs (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)) x) =
    abs (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)) y)
Tactic:
cases x with | mk nx kx =>
cases y with | mk ny ky =>
let f i : Quot (r i) → Quot (r' i) :=
  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 : ∀ i, f i ∘ Quot.mk (r _) ∘ Quot.mk (congr F _) = Quot.mk (r' _) := by intro i; rfl
conv =>
  congr
  . rhs
    lhs
    intro i
    rw [←this]
    rfl
  . rhs
    lhs
    intro i
    rw [←this]
rw [IContainer.Map_spec, IContainer.Map_spec, IContainer.Map_spec, IContainer.Map_spec]
rw [inst.abs_imap, inst.abs_imap, inst.abs_imap, inst.abs_imap, inst.abs_imap, inst.abs_imap, h₂]
State after:
no goals

State before:
case a.a.mk
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✝
y : IContainer.Obj (C F) (IContainer.M (C F)) i
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)
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 y))
⊢ abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        { fst := nx, snd := kx }) =
    abs (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y)) y)
Tactic:
cases y with | mk ny ky =>
let f i : Quot (r i) → Quot (r' i) :=
  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 : ∀ i, f i ∘ Quot.mk (r _) ∘ Quot.mk (congr F _) = Quot.mk (r' _) := by intro i; rfl
conv =>
  congr
  . rhs
    lhs
    intro i
    rw [←this]
    rfl
  . rhs
    lhs
    intro i
    rw [←this]
rw [IContainer.Map_spec, IContainer.Map_spec, IContainer.Map_spec, IContainer.Map_spec]
rw [inst.abs_imap, inst.abs_imap, inst.abs_imap, inst.abs_imap, inst.abs_imap, inst.abs_imap, h₂]
State after:
no goals

State before:
case a.a.mk.mk
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 }))
⊢ abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        { fst := nx, snd := kx }) =
    abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        { fst := ny, snd := ky })
Tactic:
let f i : Quot (r i) → Quot (r' i) :=
  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
State after:
case a.a.mk.mk
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)
⊢ abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        { fst := nx, snd := kx }) =
    abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        { fst := ny, snd := ky })

State before:
case a.a.mk.mk
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)
⊢ abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        { fst := nx, snd := kx }) =
    abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        { fst := ny, snd := ky })
Tactic:
have : ∀ i, f i ∘ Quot.mk (r _) ∘ Quot.mk (congr F _) = Quot.mk (r' _) := by intro i; rfl
State after:
case a.a.mk.mk
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)
this : ∀ (i : I), f i ∘ Quot.mk (r i) ∘ Quot.mk (congr F i) = Quot.mk (r' i)
⊢ abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        { fst := nx, snd := kx }) =
    abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        { fst := ny, snd := ky })

State before:
case a.a.mk.mk
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)
this : ∀ (i : I), f i ∘ Quot.mk (r i) ∘ Quot.mk (congr F i) = Quot.mk (r' i)
⊢ abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        { fst := nx, snd := kx }) =
    abs
      (IContainer.Map (fun i => Quot.mk fun x y => r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) y))
        { fst := ny, snd := ky })
Tactic:
conv =>
  congr
  . rhs
    lhs
    intro i
    rw [←this]
    rfl
  . rhs
    lhs
    intro i
    rw [←this]
State after:
case a.a.mk.mk
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)
this : ∀ (i : I), f i ∘ Quot.mk (r i) ∘ Quot.mk (congr F i) = Quot.mk (r' i)
⊢ abs (IContainer.Map (fun i => f i ∘ Quot.mk (r i) ∘ Quot.mk (congr F i)) { fst := nx, snd := kx }) =
    abs (IContainer.Map (fun i => f i ∘ Quot.mk (r i) ∘ Quot.mk (congr F i)) { fst := ny, snd := ky })

State before:
case a.a.mk.mk
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)
this : ∀ (i : I), f i ∘ Quot.mk (r i) ∘ Quot.mk (congr F i) = Quot.mk (r' i)
⊢ abs (IContainer.Map (fun i => f i ∘ Quot.mk (r i) ∘ Quot.mk (congr F i)) { fst := nx, snd := kx }) =
    abs (IContainer.Map (fun i => f i ∘ Quot.mk (r i) ∘ Quot.mk (congr F i)) { fst := ny, snd := ky })
Tactic:
rw [IContainer.Map_spec, IContainer.Map_spec, IContainer.Map_spec, IContainer.Map_spec]
State after:
case a.a.mk.mk
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)
this : ∀ (i : I), f i ∘ Quot.mk (r i) ∘ Quot.mk (congr F i) = Quot.mk (r' i)
⊢ abs
      (IContainer.Map (fun i => f i)
        (IContainer.Map (fun i => Quot.mk (r i))
          (IContainer.Map (fun i => Quot.mk (congr F i)) { fst := nx, snd := kx }))) =
    abs
      (IContainer.Map (fun i => f i)
        (IContainer.Map (fun i => Quot.mk (r i))
          (IContainer.Map (fun i => Quot.mk (congr F i)) { fst := ny, snd := ky })))

State before:
case a.a.mk.mk
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)
this : ∀ (i : I), f i ∘ Quot.mk (r i) ∘ Quot.mk (congr F i) = Quot.mk (r' i)
⊢ abs
      (IContainer.Map (fun i => f i)
        (IContainer.Map (fun i => Quot.mk (r i))
          (IContainer.Map (fun i => Quot.mk (congr F i)) { fst := nx, snd := kx }))) =
    abs
      (IContainer.Map (fun i => f i)
        (IContainer.Map (fun i => Quot.mk (r i))
          (IContainer.Map (fun i => Quot.mk (congr F i)) { fst := ny, snd := ky })))
Tactic:
rw [inst.abs_imap, inst.abs_imap, inst.abs_imap, inst.abs_imap, inst.abs_imap, inst.abs_imap, h₂]
State after:
no goals

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

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 b : Quot (congr F i)), r i a b → Quot.lift (Quot.mk (r' i)) ?m.25601 a = Quot.lift (Quot.mk (r' i)) ?m.25601 b

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 b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b

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 b : Quot (congr F i)), r i a b → Quot.lift (Quot.mk (r' i)) ?m.25601 a = Quot.lift (Quot.mk (r' i)) ?m.25601 b
Tactic:
. intro a b h₃
  apply Quot.sound
  simp only
  rw [Quot.sound h₃]
  apply h₀
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
⊢ ∀ (a b : Quot (congr F i)),
    r 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) 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

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 b : Quot (congr F i)),
    r 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) 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; 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
State after:
no goals

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 b : IContainer.M (C F) i), congr F i a b → Quot.mk (r' i) a = Quot.mk (r' i) b
Tactic:
intro a b h₃
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
a b : IContainer.M (C F) i
h₃ : congr F i a b
⊢ Quot.mk (r' i) a = Quot.mk (r' i) b

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 b : IContainer.M (C F) i
h₃ : congr F i a b
⊢ Quot.mk (r' i) a = Quot.mk (r' i) b
Tactic:
apply Quot.sound
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
a b : IContainer.M (C F) i
h₃ : congr F i a b
⊢ r' i a b

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
a b : IContainer.M (C F) i
h₃ : congr F i a b
⊢ r' i a b
Tactic:
simp only
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
a b : IContainer.M (C F) i
h₃ : congr F i a b
⊢ r i (Quot.mk (congr F i) a) (Quot.mk (congr F i) b)

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
a b : IContainer.M (C F) i
h₃ : congr F i a b
⊢ r i (Quot.mk (congr F i) a) (Quot.mk (congr F i) b)
Tactic:
rw [Quot.sound h₃]
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
a b : IContainer.M (C F) i
h₃ : congr F i a b
⊢ r i (Quot.mk (congr F i) b) (Quot.mk (congr F i) b)

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
a b : IContainer.M (C F) i
h₃ : congr F i a b
⊢ r i (Quot.mk (congr F i) b) (Quot.mk (congr F i) b)
Tactic:
apply h₀
State after:
no goals

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 b : Quot (congr F i)),
    r 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) 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
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 : Quot (congr F i)
⊢ ∀ (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

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 : Quot (congr F i)
⊢ ∀ (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
Tactic:
apply Quot.inductionOn (motive := _) x
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 : Quot (congr F 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

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 : Quot (congr F 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:
clear x
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
⊢ ∀ (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

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
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

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
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)

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
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)

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
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)

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
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

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
State after:
no goals

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:
intro i
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 }))
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)

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
State after:
no goals

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₂
State after:
no goals