awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x : F (Fix F)
rw : (mk ∘ dest) <$> x = x
⊢ rec (Functor.map mk) (mk x) = x

Tactic:
rw [Fix.rec_eq, ← Fix.dest, ← comp_map]

Premises used: QPF.Fix.rec_eq, QPF.Fix.dest, QPF.comp_map
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x : F (Fix F)
rhs : x
| (mk ∘ dest) <$> x = x

Tactic:
rhs
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x : F (Fix F)
rw : id <$> x
| x

Tactic:
rw [← id_map x]

Premises used: QPF.id_map
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x : F (Fix F)
rw : id <$> x
| (mk ∘ dest) <$> x = x

Tactic:
rhs
    rw [← id_map x]

Premises used: QPF.id_map
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x : F (Fix F)
conv : (mk ∘ dest) <$> x = id <$> x
⊢ (mk ∘ dest) <$> x = x

Tactic:
conv =>
    rhs
    rw [← id_map x]

Premises used: QPF.id_map
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x : F (Fix F)
e_a : ∀ (x : Fix F), (mk ∘ dest) x = id x
⊢ (mk ∘ dest) <$> x = id <$> x

Tactic:
congr with x
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x_1 : F (Fix F)
x : Fix F
⊢ (mk ∘ dest) x = id x

Tactic:
apply Fix.mk_dest

Premises used: QPF.Fix.mk_dest
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (Fix.mk x)
x_1 : Fix F
x : (P F).W
mk :
  ∀ (a : (P F).A) (f : (P F).B a → WType (α := (P F).A) (P F).B)
    (ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))),
    p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (WType.mk (β := (P F).B) a f))
⊢ p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) x)

Tactic:
induction x with | _ a f ih
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (Fix.mk x)
x : Fix F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
mk : p ⟦WType.mk (β := (P F).B) a f⟧
⊢ p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (WType.mk (β := (P F).B) a f))

Tactic:
change p ⟦⟨a, f⟩⟧

Premises used: Quotient.mk, WType.mk
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (Fix.mk x)
x : Fix F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
mk : p (Fix.mk (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)))
⊢ p ⟦WType.mk (β := (P F).B) a f⟧

Tactic:
rw [← Fix.ind_aux a f]

Premises used: QPF.Fix.ind_aux
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (Fix.mk x)
x : Fix F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
mk : Liftp p (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧))
⊢ p (Fix.mk (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧)))

Tactic:
apply h
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (Fix.mk x)
x : Fix F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
mk :
  ∃ (a_1 : (P F).A) (f_1 : (P F).B a_1 → Fix F),
    Eq (α := F (Fix F)) (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧))
        (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a_1 f_1)) ∧
      ∀ (i : (P F).B a_1), p (f_1 i)
⊢ Liftp p (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧))

Tactic:
rw [liftp_iff]

Premises used: QPF.liftp_iff
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x : Fix F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
⊢ ∃ (a_1 : (P F).A) (f_1 : (P F).B a_1 → Fix F),
    Eq (α := F (Fix F)) (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧))
        (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a_1 f_1)) ∧
      ∀ (i : (P F).B a_1), p (f_1 i)

Tactic:
⟨_, _, rfl, ?_⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (Fix.mk x)
x : Fix F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
mk : ∀ (i : (P F).B a), p ⟦f i⟧
⊢ ∃ (a_1 : (P F).A) (f_1 : (P F).B a_1 → Fix F),
    Eq (α := F (Fix F)) (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧))
        (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a_1 f_1)) ∧
      ∀ (i : (P F).B a_1), p (f_1 i)

Tactic:
refine ⟨_, _, rfl, ?_⟩
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x : Fix F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
⊢ ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))

Tactic:
ih
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x : Fix F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
⊢ ∀ (i : (P F).B a), p ⟦f i⟧

Tactic:
convert! ih
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
g : α → F α
x : α
rw :
  Eq (α := (↑(P F) : (α : Type (max u_1 u)) → Type (max (max u_1 u) u u_1)) (PFunctor.M.{u, u_1} (P F)))
    (PFunctor.M.dest (PFunctor.M.corec (fun (x : α) ↦ repr (g x)) x))
    ((P F).map (PFunctor.M.corec fun (x : α) ↦ repr (g x)) (repr (g x)))
rw₁ rw₂ :
  Eq (α := (↑(P F) : (α : Type (max u_1 u)) → Type (max (max u_1 u) u u_1)) (PFunctor.M.{u, u_1} (P F)))
    ((P F).map (PFunctor.M.corec fun (x : α) ↦ repr (g x)) (repr (g x)))
    ((P F).map (PFunctor.M.corec fun (x : α) ↦ repr (g x)) (repr (g x)))
⊢ Eq (α := (↑(P F) : (α : Type (max u_1 u)) → Type (max (max u_1 u) u u_1)) (PFunctor.M.{u, u_1} (P F)))
    (PFunctor.M.dest (corecF g x)) ((P F).map (corecF g) (repr (g x)))

Tactic:
rw [corecF, PFunctor.M.dest_corec]

Premises used: PFunctor.M.dest_corec, QPF.corecF
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
dsimp : Eq (α := F (Cofix F)) (Quot.mk Mcongr <$> abs x.dest) (Quot.mk Mcongr <$> abs y.dest)
⊢ Eq.{u + 1} (α := F (Cofix F)) ((fun (x : (P F).M) ↦ (Quot.mk Mcongr <$> abs x.dest : F (Cofix F))) x)
    ((fun (x : (P F).M) ↦ (Quot.mk Mcongr <$> abs x.dest : F (Cofix F))) y)

Tactic:
dsimp
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x_1 y_1 : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x_1 y_1
x y : (P F).M
h : r x y
⊢ Mcongr x y

Tactic:
⟨r, pr, h⟩

Premises used: QPF.Mcongr, And.intro, Exists.intro
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x_1 y_1 : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x_1 y_1
x y : (P F).M
h : r x y
⊢ Mcongr x y

Tactic:
exact ⟨r, pr, h⟩
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
⊢ ∀ (x y : (P F).M), r x y → Mcongr x y

Tactic:
have : ∀ x y, r x y → Mcongr x y := by
        intro x y h
        exact ⟨r, pr, h⟩
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
rw : (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
⊢ Eq (α := F (Cofix F)) (Quot.mk Mcongr <$> abs x.dest) (Quot.mk Mcongr <$> abs y.dest)

Tactic:
rw [← Quot.factor_mk_eq _ _ this]

Premises used: Quot.factor_mk_eq
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
lhs : (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest
| (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest

Tactic:
lhs
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
rw : (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
| (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest

Tactic:
rw [comp_map, ← abs_map, pr rxy, abs_map, ← comp_map]

Premises used: QPF.abs_map, QPF.comp_map
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
rw : (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
| (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest

Tactic:
lhs
        rw [comp_map, ← abs_map, pr rxy, abs_map, ← comp_map]

Premises used: QPF.abs_map, QPF.comp_map
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
conv : (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
conv₁ : (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
⊢ (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest

Tactic:
conv =>
        lhs
        rw [comp_map, ← abs_map, pr rxy, abs_map, ← comp_map]

Premises used: QPF.abs_map, QPF.comp_map
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
lhs : dest (corec g x)
| Eq (α := F (Cofix F)) (dest (corec g x)) (corec g <$> g x)

Tactic:
lhs
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
rw : Quot.lift (r := Mcongr) (fun (x : (P F).M) ↦ Quot.mk Mcongr <$> abs x.dest) ⋯ (Quot.mk Mcongr (corecF g x))
| dest (corec g x)

Tactic:
rw [Cofix.dest, Cofix.corec]

Premises used: QPF.Cofix.corec, QPF.Cofix.dest
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
rw : Quot.lift (r := Mcongr) (fun (x : (P F).M) ↦ Quot.mk Mcongr <$> abs x.dest) ⋯ (Quot.mk Mcongr (corecF g x))
| Eq (α := F (Cofix F)) (dest (corec g x)) (corec g <$> g x)

Tactic:
lhs
    rw [Cofix.dest, Cofix.corec]

Premises used: QPF.Cofix.corec, QPF.Cofix.dest
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
conv :
  Eq (α := F (Cofix F))
    (Quot.lift (r := Mcongr) (fun (x : (P F).M) ↦ Quot.mk Mcongr <$> abs x.dest) ⋯ (Quot.mk Mcongr (corecF g x)))
    (corec g <$> g x)
⊢ Eq (α := F (Cofix F)) (dest (corec g x)) (corec g <$> g x)

Tactic:
conv =>
    lhs
    rw [Cofix.dest, Cofix.corec]

Premises used: QPF.Cofix.corec, QPF.Cofix.dest
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
dsimp : Eq (α := F (Cofix F)) (Quot.mk Mcongr <$> abs (PFunctor.M.dest (corecF g x))) (corec g <$> g x)
⊢ Eq (α := F (Cofix F))
    (Quot.lift (r := Mcongr) (fun (x : (P F).M) ↦ Quot.mk Mcongr <$> abs x.dest) ⋯ (Quot.mk Mcongr (corecF g x)))
    (corec g <$> g x)

Tactic:
dsimp
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
rw : Eq (α := F (Cofix F)) ((Quot.mk Mcongr ∘ corecF g) <$> g x) (corec g <$> g x)
⊢ Eq (α := F (Cofix F)) (Quot.mk Mcongr <$> abs (PFunctor.M.dest (corecF g x))) (corec g <$> g x)

Tactic:
rw [corecF_eq, abs_map, abs_repr, ← comp_map]

Premises used: QPF.abs_repr, QPF.abs_map, QPF.corecF_eq, QPF.comp_map
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ Eq (α := F (Cofix F)) ((Quot.mk Mcongr ∘ corecF g) <$> g x) (corec g <$> g x)

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x y : Cofix F
rxy : r x y
h' : ∀ (x : Cofix F), r' x x
h₁ : ∀ (x y : Cofix F), r' x y → Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest
a : r' x y
⊢ x = y

Tactic:
apply Cofix.bisim_aux r'

Premises used: _private.0.QPF.Cofix.bisim_aux
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y : Cofix F
rxy : r x_1 y
x : Cofix F
h' : x = x
⊢ r' x x

Tactic:
left
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y : Cofix F
rxy : r x_1 y
x : Cofix F
⊢ x = x

Tactic:
rfl
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F
rxy : r x_1 y_1
x y : Cofix F
r'xy : r' x y
h₁ : ∀ (r'xy : x = y), Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest
h₂ : ∀ (r'xy : r x y), Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest
⊢ Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest

Tactic:
rcases r'xy with r'xy | r'xy
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F
rxy : r x_1 y_1
x y : Cofix F
r'xy : x = y
h₁ h₂ : Quot.mk r' <$> y.dest = Quot.mk r' <$> y.dest
⊢ Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest

Tactic:
rw [r'xy]
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F
rxy : r x_1 y_1
x y : Cofix F
r'xy : r x y
⊢ ∀ (x y : Cofix F), r x y → r' x y

Tactic:
have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F
rxy : r x_1 y_1
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
h₁ : (Quot.factor r r' this ∘ Quot.mk r) <$> x.dest = (Quot.factor r r' this ∘ Quot.mk r) <$> y.dest
⊢ Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest

Tactic:
rw [← Quot.factor_mk_eq _ _ this]

Premises used: Quot.factor_mk_eq
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F
rxy : r x_1 y_1
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
h₁ :
  (Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this ∘ Quot.mk r) <$> x.dest =
    (Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this ∘ Quot.mk r) <$> y.dest
⊢ (Quot.factor r r' this ∘ Quot.mk r) <$> x.dest = (Quot.factor r r' this ∘ Quot.mk r) <$> y.dest

Tactic:
dsimp [r']
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F
rxy : r x_1 y_1
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
h₁ :
  Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this <$> Quot.mk r <$> x.dest =
    Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest
⊢ (Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this ∘ Quot.mk r) <$> x.dest =
    (Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this ∘ Quot.mk r) <$> y.dest

Tactic:
rw [@comp_map _ q _ _ _ (Quot.mk r), @comp_map _ q _ _ _ (Quot.mk r)]

Premises used: QPF.comp_map, Quot.mk
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F
rxy : r x_1 y_1
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
h₁ h₂ :
  Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest =
    Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest
⊢ Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this <$> Quot.mk r <$> x.dest =
    Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest

Tactic:
rw [h _ _ r'xy]
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x y : Cofix F
rxy a : r x y
⊢ r' x y

Tactic:
right
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ r x y

Tactic:
rxy
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ r x y

Tactic:
exact rxy
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
h₁ : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
⊢ ∀ (x y : Cofix F), r x y → x = y

Tactic:
apply Cofix.bisim_rel

Premises used: QPF.Cofix.bisim_rel
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
h₁ :
  ∀ (a : (P F).A) (f₀ f₁ : (P F).B a → Cofix F)
    (dxeq : x.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₀))
    (dyeq : y.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₁))
    (h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)), Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
⊢ Quot.mk r <$> x.dest = Quot.mk r <$> y.dest

Tactic:
rcases (liftr_iff r _ _).mp (h x y rxy) with ⟨a, f₀, f₁, dxeq, dyeq, h'⟩

Premises used: Iff.mp, QPF.liftr_iff
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a → Cofix F
dxeq : x.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₀)
dyeq : y.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₁)
h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
h₁ :
  Eq (α := F (Quot r)) (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Quot r) a (Quot.mk r ∘ f₀)))
    (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Quot r) a (Quot.mk r ∘ f₁)))
⊢ Quot.mk r <$> x.dest = Quot.mk r <$> y.dest

Tactic:
rw [dxeq, dyeq, ← abs_map, ← abs_map, PFunctor.map_eq, PFunctor.map_eq]

Premises used: QPF.abs_map, PFunctor.map_eq
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a → Cofix F
dxeq : x.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₀)
dyeq : y.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₁)
h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
h₁ : ∀ (i : (P F).B a), (Quot.mk r ∘ f₀) i = (Quot.mk r ∘ f₁) i
⊢ Eq (α := F (Quot r)) (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Quot r) a (Quot.mk r ∘ f₀)))
    (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Quot r) a (Quot.mk r ∘ f₁)))

Tactic:
congr 2 with i
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a → Cofix F
dxeq : x.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₀)
dyeq : y.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₁)
h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
i : (P F).B a
h₁ : r (f₀ i) (f₁ i)
⊢ (Quot.mk r ∘ f₀) i = (Quot.mk r ∘ f₁) i

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a → Cofix F
dxeq : x.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₀)
dyeq : y.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₁)
h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
i : (P F).B a
⊢ r (f₀ i) (f₁ i)

Tactic:
apply h'
-- Module: Mathlib.Data.QPF.Univariate.Basic
Goal:
F : Type u → Type u
q : QPF F
α : Type u_1
Q : α → Prop
u v : α → Cofix F
h :
  ∀ (x : α),
    Q x →
      ∃ (a : (P F).A) (f : (P F).B a → Cofix F) (f' : (P F).B a → Cofix F),
        (u x).dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f) ∧
          (v x).dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f') ∧
            ∀ (i : (P F).B a), ∃ (x' : α), Q x' ∧ f i = u x' ∧ f' i = v x'
x_1 : α
Qx : Q x_1
R : (w z : Cofix F) → Prop := fun (w z : Cofix F) ↦ ∃ (x' : α), Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F
h_1 : R x y
x' : α
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
rcases :
  ∀ (a : (P F).A) (f f' : (P F).B a → Cofix F)
    (ux'eq : (u x').dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f))
    (vx'eq : (v x').dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f'))
    (h' : ∀ (i : (P F).B a), ∃ (x' : α), Q x' ∧ f i = u x' ∧ f' i = v x'), Liftr R x.dest y.dest
⊢ Liftr R x.dest y.dest

Tactic:
rcases h x' Qx' with ⟨a, f, f', ux'eq, vx'eq, h'⟩