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

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
⊢ ∀ (x y : M F), r x y → x = y
Tactic:
intro x
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : M F
⊢ ∀ (y : M F), r x y → x = y

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : M F
⊢ ∀ (y : M F), r x y → x = y
Tactic:
apply Quot.inductionOn (motive := _) x
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : M F
⊢ ∀ (a : Container.M (C F)) (y : M F), r (Quot.mk (congr F) a) y → Quot.mk (congr F) a = y

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : M F
⊢ ∀ (a : Container.M (C F)) (y : M F), r (Quot.mk (congr F) a) y → Quot.mk (congr F) a = y
Tactic:
clear x
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
⊢ ∀ (a : Container.M (C F)) (y : M F), r (Quot.mk (congr F) a) y → Quot.mk (congr F) a = y

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
⊢ ∀ (a : Container.M (C F)) (y : M F), r (Quot.mk (congr F) a) y → Quot.mk (congr F) a = y
Tactic:
intro x y
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : Container.M (C F)
y : M F
⊢ r (Quot.mk (congr F) x) y → Quot.mk (congr F) x = y

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : Container.M (C F)
y : M F
⊢ r (Quot.mk (congr F) x) y → Quot.mk (congr F) x = y
Tactic:
apply Quot.inductionOn (motive := _) y
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : Container.M (C F)
y : M F
⊢ ∀ (a : Container.M (C F)), r (Quot.mk (congr F) x) (Quot.mk (congr F) a) → Quot.mk (congr F) x = Quot.mk (congr F) a

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : Container.M (C F)
y : M F
⊢ ∀ (a : Container.M (C F)), r (Quot.mk (congr F) x) (Quot.mk (congr F) a) → Quot.mk (congr F) x = Quot.mk (congr F) a
Tactic:
clear y
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : Container.M (C F)
⊢ ∀ (a : Container.M (C F)), r (Quot.mk (congr F) x) (Quot.mk (congr F) a) → Quot.mk (congr F) x = Quot.mk (congr F) a

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : Container.M (C F)
⊢ ∀ (a : Container.M (C F)), r (Quot.mk (congr F) x) (Quot.mk (congr F) a) → Quot.mk (congr F) x = Quot.mk (congr F) a
Tactic:
intro y h₂
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ Quot.mk (congr F) x = Quot.mk (congr F) y

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ Quot.mk (congr F) x = Quot.mk (congr F) y
Tactic:
apply Quot.sound
State after:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ congr F x y

State before:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ congr F x y
Tactic:
let r' x y := r (Quot.mk _ x) (Quot.mk _ y)
State after:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ congr F x y

State before:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ congr F x y
Tactic:
apply congr.coinduction F r'
State after:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ ∀ (x y : Container.M (C F)), r' x y → ↑(precongr F) r' x y

case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ r' x y

State before:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ ∀ (x y : Container.M (C F)), r' x y → ↑(precongr F) r' x y

case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ r' x y
Tactic:
. clear h₂
  intro x y h₂
  simp only [precongr, map_quot]
  have h₂ := h₁ _ _ h₂
  simp only [destruct, destruct.f] at h₂
  generalize Container.M.destruct x = x at *
  generalize Container.M.destruct y = y at *
  cases x with | mk nx kx =>
  cases y with | mk ny ky =>
  let f : Quot r → Quot r' :=
    by
      apply Quot.lift (Quot.lift (Quot.mk r') _) _
      . intro a b h₃
        apply Quot.sound
        simp only
        rw [Quot.sound h₃]
        apply h₀
      . intro x; apply Quot.inductionOn (motive := _) x; clear x
        intro x y; apply Quot.inductionOn (motive := _) y; clear y
        intro y h
        apply Quot.sound
        apply h
  have : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r' := rfl
  conv =>
    congr
    . rhs
      lhs
      intro i
      rw [←this]
      rfl
    . rhs
      lhs
      intro i
      rw [←this]
  rw [Container.Map_spec, Container.Map_spec, Container.Map_spec, Container.Map_spec]
  rw [inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, h₂]
State after:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ r' x y

State before:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ r' x y
Tactic:
. apply h₂
State after:
no goals

State before:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ ∀ (x y : Container.M (C F)), r' x y → ↑(precongr F) r' x y
Tactic:
clear h₂
State after:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ ∀ (x y : Container.M (C F)), r' x y → ↑(precongr F) r' x y

State before:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ ∀ (x y : Container.M (C F)), r' x y → ↑(precongr F) r' x y
Tactic:
intro x y h₂
State after:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂ : r' x y
⊢ ↑(precongr F) r' x y

State before:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂ : r' x y
⊢ ↑(precongr F) r' x y
Tactic:
simp only [precongr, map_quot]
State after:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂ : r' x y
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct x)) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))

State before:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂ : r' x y
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct x)) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))
Tactic:
have h₂ := h₁ _ _ h₂
State after:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
h₂ : Quot.mk r <$> destruct (Quot.mk (congr F) x) = Quot.mk r <$> destruct (Quot.mk (congr F) y)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct x)) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))

State before:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
h₂ : Quot.mk r <$> destruct (Quot.mk (congr F) x) = Quot.mk r <$> destruct (Quot.mk (congr F) y)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct x)) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))
Tactic:
simp only [destruct, destruct.f] at h₂
State after:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs (Container.M.destruct x) =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs (Container.M.destruct y)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct x)) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))

State before:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs (Container.M.destruct x) =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs (Container.M.destruct y)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct x)) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))
Tactic:
generalize Container.M.destruct x = x at *
State after:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y : Container.M (C F)
h₂✝ : r' x✝ y
x : Container.Obj (C F) (Container.M (C F))
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs x =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs (Container.M.destruct y)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) x) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))

State before:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y : Container.M (C F)
h₂✝ : r' x✝ y
x : Container.Obj (C F) (Container.M (C F))
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs x =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs (Container.M.destruct y)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) x) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) (Container.M.destruct y))
Tactic:
generalize Container.M.destruct y = y at *
State after:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y✝ : Container.M (C F)
h₂✝ : r' x✝ y✝
x y : Container.Obj (C F) (Container.M (C F))
h₂ : Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs x = Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs y
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) x) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) y)

State before:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y✝ : Container.M (C F)
h₂✝ : r' x✝ y✝
x y : Container.Obj (C F) (Container.M (C F))
h₂ : Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs x = Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs y
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) x) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) y)
Tactic:
cases x with | mk nx kx =>
cases y with | mk ny ky =>
let f : Quot r → Quot r' :=
  by
    apply Quot.lift (Quot.lift (Quot.mk r') _) _
    . intro a b h₃
      apply Quot.sound
      simp only
      rw [Quot.sound h₃]
      apply h₀
    . intro x; apply Quot.inductionOn (motive := _) x; clear x
      intro x y; apply Quot.inductionOn (motive := _) y; clear y
      intro y h
      apply Quot.sound
      apply h
have : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r' := rfl
conv =>
  congr
  . rhs
    lhs
    intro i
    rw [←this]
    rfl
  . rhs
    lhs
    intro i
    rw [←this]
rw [Container.Map_spec, Container.Map_spec, Container.Map_spec, Container.Map_spec]
rw [inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, h₂]
State after:
no goals

State before:
case a.a.mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y✝ : Container.M (C F)
h₂✝ : r' x y✝
y : Container.Obj (C F) (Container.M (C F))
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs y
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := nx, snd := kx }) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) y)
Tactic:
cases y with | mk ny ky =>
let f : Quot r → Quot r' :=
  by
    apply Quot.lift (Quot.lift (Quot.mk r') _) _
    . intro a b h₃
      apply Quot.sound
      simp only
      rw [Quot.sound h₃]
      apply h₀
    . intro x; apply Quot.inductionOn (motive := _) x; clear x
      intro x y; apply Quot.inductionOn (motive := _) y; clear y
      intro y h
      apply Quot.sound
      apply h
have : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r' := rfl
conv =>
  congr
  . rhs
    lhs
    intro i
    rw [←this]
    rfl
  . rhs
    lhs
    intro i
    rw [←this]
rw [Container.Map_spec, Container.Map_spec, Container.Map_spec, Container.Map_spec]
rw [inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, h₂]
State after:
no goals

State before:
case a.a.mk.mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := nx, snd := kx }) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := ny, snd := ky })
Tactic:
let f : Quot r → Quot r' :=
  by
    apply Quot.lift (Quot.lift (Quot.mk r') _) _
    . intro a b h₃
      apply Quot.sound
      simp only
      rw [Quot.sound h₃]
      apply h₀
    . intro x; apply Quot.inductionOn (motive := _) x; clear x
      intro x y; apply Quot.inductionOn (motive := _) y; clear y
      intro y h
      apply Quot.sound
      apply h
State after:
case a.a.mk.mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x b : Quot (congr F)),
        r x b →
          Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) x =
            Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := nx, snd := kx }) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := ny, snd := ky })

State before:
case a.a.mk.mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x b : Quot (congr F)),
        r x b →
          Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) x =
            Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b)
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := nx, snd := kx }) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := ny, snd := ky })
Tactic:
have : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r' := rfl
State after:
case a.a.mk.mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x b : Quot (congr F)),
        r x b →
          Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) x =
            Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b)
this : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r'
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := nx, snd := kx }) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := ny, snd := ky })

State before:
case a.a.mk.mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x b : Quot (congr F)),
        r x b →
          Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) x =
            Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b)
this : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r'
⊢ abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := nx, snd := kx }) =
    abs (Container.Map (Quot.mk fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)) { fst := ny, snd := ky })
Tactic:
conv =>
  congr
  . rhs
    lhs
    intro i
    rw [←this]
    rfl
  . rhs
    lhs
    intro i
    rw [←this]
State after:
case a.a.mk.mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x b : Quot (congr F)),
        r x b →
          Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) x =
            Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b)
this : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r'
⊢ abs (Container.Map (fun i => (f ∘ Quot.mk r ∘ Quot.mk (congr F)) i) { fst := nx, snd := kx }) =
    abs (Container.Map (fun i => (f ∘ Quot.mk r ∘ Quot.mk (congr F)) i) { fst := ny, snd := ky })

State before:
case a.a.mk.mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x b : Quot (congr F)),
        r x b →
          Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) x =
            Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b)
this : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r'
⊢ abs (Container.Map (fun i => (f ∘ Quot.mk r ∘ Quot.mk (congr F)) i) { fst := nx, snd := kx }) =
    abs (Container.Map (fun i => (f ∘ Quot.mk r ∘ Quot.mk (congr F)) i) { fst := ny, snd := ky })
Tactic:
rw [Container.Map_spec, Container.Map_spec, Container.Map_spec, Container.Map_spec]
State after:
case a.a.mk.mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x b : Quot (congr F)),
        r x b →
          Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) x =
            Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b)
this : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r'
⊢ abs (Container.Map f (Container.Map (Quot.mk r) (Container.Map (Quot.mk (congr F)) { fst := nx, snd := kx }))) =
    abs (Container.Map f (Container.Map (Quot.mk r) (Container.Map (Quot.mk (congr F)) { fst := ny, snd := ky })))

State before:
case a.a.mk.mk
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
f : Quot r → Quot r' :=
  Quot.lift (Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b))
    (_ :
      ∀ (x b : Quot (congr F)),
        r x b →
          Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) x =
            Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b)
this : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r'
⊢ abs (Container.Map f (Container.Map (Quot.mk r) (Container.Map (Quot.mk (congr F)) { fst := nx, snd := kx }))) =
    abs (Container.Map f (Container.Map (Quot.mk r) (Container.Map (Quot.mk (congr F)) { fst := ny, snd := ky })))
Tactic:
rw [inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, h₂]
State after:
no goals

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
⊢ Quot r → Quot r'
Tactic:
apply Quot.lift (Quot.lift (Quot.mk r') _) _
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
⊢ ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b

F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
⊢ ∀ (a b : Quot (congr F)), r a b → Quot.lift (Quot.mk r') ?m.11689 a = Quot.lift (Quot.mk r') ?m.11689 b

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
⊢ ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b

F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
⊢ ∀ (a b : Quot (congr F)), r a b → Quot.lift (Quot.mk r') ?m.11689 a = Quot.lift (Quot.mk r') ?m.11689 b
Tactic:
. intro a b h₃
  apply Quot.sound
  simp only
  rw [Quot.sound h₃]
  apply h₀
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
⊢ ∀ (a b : Quot (congr F)),
    r a b →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) a =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
⊢ ∀ (a b : Quot (congr F)),
    r a b →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) a =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b
Tactic:
. intro x; apply Quot.inductionOn (motive := _) x; clear x
  intro x y; apply Quot.inductionOn (motive := _) y; clear y
  intro y h
  apply Quot.sound
  apply h
State after:
no goals

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
⊢ ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b
Tactic:
intro a b h₃
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
a b : Container.M (C F)
h₃ : congr F a b
⊢ Quot.mk r' a = Quot.mk r' b

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
a b : Container.M (C F)
h₃ : congr F a b
⊢ Quot.mk r' a = Quot.mk r' b
Tactic:
apply Quot.sound
State after:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
a b : Container.M (C F)
h₃ : congr F a b
⊢ r' a b

State before:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
a b : Container.M (C F)
h₃ : congr F a b
⊢ r' a b
Tactic:
simp only
State after:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
a b : Container.M (C F)
h₃ : congr F a b
⊢ r (Quot.mk (congr F) a) (Quot.mk (congr F) b)

State before:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
a b : Container.M (C F)
h₃ : congr F a b
⊢ r (Quot.mk (congr F) a) (Quot.mk (congr F) b)
Tactic:
rw [Quot.sound h₃]
State after:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
a b : Container.M (C F)
h₃ : congr F a b
⊢ r (Quot.mk (congr F) b) (Quot.mk (congr F) b)

State before:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
a b : Container.M (C F)
h₃ : congr F a b
⊢ r (Quot.mk (congr F) b) (Quot.mk (congr F) b)
Tactic:
apply h₀
State after:
no goals

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
⊢ ∀ (a b : Quot (congr F)),
    r a b →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) a =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b
Tactic:
intro x
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y : Container.M (C F)
h₂✝ : r' x✝ y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x : Quot (congr F)
⊢ ∀ (b : Quot (congr F)),
    r x b →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) x =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y : Container.M (C F)
h₂✝ : r' x✝ y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x : Quot (congr F)
⊢ ∀ (b : Quot (congr F)),
    r x b →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) x =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b
Tactic:
apply Quot.inductionOn (motive := _) x
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y : Container.M (C F)
h₂✝ : r' x✝ y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x : Quot (congr F)
⊢ ∀ (a : Container.M (C F)) (b : Quot (congr F)),
    r (Quot.mk (congr F) a) b →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) a) =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y : Container.M (C F)
h₂✝ : r' x✝ y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x : Quot (congr F)
⊢ ∀ (a : Container.M (C F)) (b : Quot (congr F)),
    r (Quot.mk (congr F) a) b →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) a) =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b
Tactic:
clear x
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
⊢ ∀ (a : Container.M (C F)) (b : Quot (congr F)),
    r (Quot.mk (congr F) a) b →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) a) =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x y : Container.M (C F)
h₂✝ : r' x y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
⊢ ∀ (a : Container.M (C F)) (b : Quot (congr F)),
    r (Quot.mk (congr F) a) b →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) a) =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) b
Tactic:
intro x y
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y✝ : Container.M (C F)
h₂✝ : r' x✝ y✝
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x : Container.M (C F)
y : Quot (congr F)
⊢ r (Quot.mk (congr F) x) y →
    Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
        (Quot.mk (congr F) x) =
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) y

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y✝ : Container.M (C F)
h₂✝ : r' x✝ y✝
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x : Container.M (C F)
y : Quot (congr F)
⊢ r (Quot.mk (congr F) x) y →
    Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
        (Quot.mk (congr F) x) =
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b) y
Tactic:
apply Quot.inductionOn (motive := _) y
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y✝ : Container.M (C F)
h₂✝ : r' x✝ y✝
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x : Container.M (C F)
y : Quot (congr F)
⊢ ∀ (a : Container.M (C F)),
    r (Quot.mk (congr F) x) (Quot.mk (congr F) a) →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) x) =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) a)

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y✝ : Container.M (C F)
h₂✝ : r' x✝ y✝
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x : Container.M (C F)
y : Quot (congr F)
⊢ ∀ (a : Container.M (C F)),
    r (Quot.mk (congr F) x) (Quot.mk (congr F) a) →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) x) =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) a)
Tactic:
clear y
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y : Container.M (C F)
h₂✝ : r' x✝ y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x : Container.M (C F)
⊢ ∀ (a : Container.M (C F)),
    r (Quot.mk (congr F) x) (Quot.mk (congr F) a) →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) x) =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) a)

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y : Container.M (C F)
h₂✝ : r' x✝ y
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x : Container.M (C F)
⊢ ∀ (a : Container.M (C F)),
    r (Quot.mk (congr F) x) (Quot.mk (congr F) a) →
      Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) x) =
        Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
          (Quot.mk (congr F) a)
Tactic:
intro y h
State after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y✝ : Container.M (C F)
h₂✝ : r' x✝ y✝
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x y : Container.M (C F)
h : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
      (Quot.mk (congr F) x) =
    Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
      (Quot.mk (congr F) y)

State before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y✝ : Container.M (C F)
h₂✝ : r' x✝ y✝
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x y : Container.M (C F)
h : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
      (Quot.mk (congr F) x) =
    Quot.lift (Quot.mk r') (_ : ∀ (a b : Container.M (C F)), congr F a b → Quot.mk r' a = Quot.mk r' b)
      (Quot.mk (congr F) y)
Tactic:
apply Quot.sound
State after:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y✝ : Container.M (C F)
h₂✝ : r' x✝ y✝
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x y : Container.M (C F)
h : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ r' x y

State before:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x✝¹ y✝¹ : Container.M (C F)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
x✝ y✝ : Container.M (C F)
h₂✝ : r' x✝ y✝
nx : (C F).A
kx : Container.B (C F) nx → Container.M (C F)
ny : (C F).A
ky : Container.B (C F) ny → Container.M (C F)
h₂ :
  Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := nx, snd := kx } =
    Quot.mk r <$> (fun x => Quot.mk (congr F) x) <$> abs { fst := ny, snd := ky }
x y : Container.M (C F)
h : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ r' x y
Tactic:
apply h
State after:
no goals

State before:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ r' x y
Tactic:
apply h₂
State after:
no goals