awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
X : Type u_2
f : X → (↑F : (α : Type u_2) → Type (max u_2 uA uB)) X
x₀ : X
n : ℕ
fst : F.A
snd : F.B fst → X
e_approx :
  Eq (α := CofixA F (n + 1)) (CofixA.intro fst fun (i : F.B fst) ↦ sCorec f (snd i) n)
    (CofixA.intro fst fun (i : F.B fst) ↦ ((M.corec f ∘ snd) i).approx n)
⊢ Eq (α := CofixA F (n + 1))
    (CofixA.intro (Sigma.fst (β := fun (x : F.A) ↦ F.B x → X) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd))
      fun (i : F.B (Sigma.fst (β := fun (x : F.A) ↦ F.B x → X) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd))) ↦
      sCorec f (Sigma.snd (β := fun (x : F.A) ↦ F.B x → X) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd) i) n)
    (CofixA.intro
      ((F.map (M.corec f) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd)).fst (β := fun (x : F.A) ↦ F.B x → F.M))
      fun
        (i :
          F.B
            ((F.map (M.corec f) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd)).fst (β := fun (x : F.A) ↦
              F.B x → F.M))) ↦
      ((F.map (M.corec f) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd)).snd (β := fun (x : F.A) ↦ F.B x → F.M)
            i).approx
        n)

Tactic:
dsimp only [PFunctor.map]

Premises used: PFunctor.map
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
X : Type u_2
f : X → (↑F : (α : Type u_2) → Type (max u_2 uA uB)) X
x₀ : X
n : ℕ
fst : F.A
snd : F.B fst → X
⊢ Eq (α := CofixA F (n + 1)) (CofixA.intro fst fun (i : F.B fst) ↦ sCorec f (snd i) n)
    (CofixA.intro fst fun (i : F.B fst) ↦ ((M.corec f ∘ snd) i).approx n)

Tactic:
congr
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
x y z : F.M
hx : Agree' 0 z x
hy : Agree' 0 z y
hrec : ∀ (ps : Path F), 0 = length ps → iselect ps x = iselect ps y
⊢ iselect [] x = iselect [] y

Tactic:
specialize hrec [] rfl

Premises used: rfl, List.nil
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
x y z : F.M
hx : Agree' 0 z x
hy : Agree' 0 z y
hrec : iselect [] x = iselect [] y
zero :
  ∀ (a : F.A) (f : F.B a → F.M) (hx : Agree' 0 z (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)))
    (hrec : iselect [] (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) = iselect [] y),
    Eq (α := CofixA F (HAdd.hAdd (α := ℕ) 0 1))
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)).approx (HAdd.hAdd (α := ℕ) 0 1))
      (y.approx (HAdd.hAdd (α := ℕ) 0 1))
⊢ Eq (α := CofixA F (HAdd.hAdd (α := ℕ) 0 1)) (x.approx (HAdd.hAdd (α := ℕ) 0 1)) (y.approx (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
induction x using PFunctor.M.casesOn'

Premises used: PFunctor.M.casesOn'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
y z : F.M
hy : Agree' 0 z y
a : F.A
f : F.B a → F.M
hx : Agree' 0 z (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f))
hrec : iselect [] (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) = iselect [] y
zero :
  ∀ (a_1 : F.A) (f_1 : F.B a_1 → F.M) (hy : Agree' 0 z (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f_1)))
    (hrec :
      iselect [] (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) =
        iselect [] (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f_1))),
    Eq (α := CofixA F (HAdd.hAdd (α := ℕ) 0 1))
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)).approx (HAdd.hAdd (α := ℕ) 0 1))
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f_1)).approx (HAdd.hAdd (α := ℕ) 0 1))
⊢ Eq (α := CofixA F (HAdd.hAdd (α := ℕ) 0 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)).approx (HAdd.hAdd (α := ℕ) 0 1))
    (y.approx (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
induction y using PFunctor.M.casesOn'

Premises used: PFunctor.M.casesOn'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
z : F.M
a : F.A
f : F.B a → F.M
hx : Agree' 0 z (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f))
a_1 : F.A
f_1 : F.B a_1 → F.M
hy : Agree' 0 z (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f_1))
hrec : a = a_1
zero :
  ∀ (f_2 : F.B a → F.M) (hy : Agree' 0 z (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f_2))),
    Eq (α := CofixA F (HAdd.hAdd (α := ℕ) 0 1))
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)).approx (HAdd.hAdd (α := ℕ) 0 1))
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f_2)).approx (HAdd.hAdd (α := ℕ) 0 1))
⊢ Eq (α := CofixA F (HAdd.hAdd (α := ℕ) 0 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)).approx (HAdd.hAdd (α := ℕ) 0 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f_1)).approx (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
subst hrec
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
z : F.M
a : F.A
f : F.B a → F.M
hx : Agree' 0 z (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f))
f_1 : F.B a → F.M
hy : Agree' 0 z (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f_1))
⊢ Eq (α := CofixA F (HAdd.hAdd (α := ℕ) 0 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)).approx (HAdd.hAdd (α := ℕ) 0 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f_1)).approx (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
simp only [approx_mk, heq_iff_eq, CofixA.intro.injEq,
      eq_iff_true_of_subsingleton, and_self]

Premises used: and_self, PFunctor.Approx.CofixA.intro.injEq, heq_iff_eq, PFunctor.M.approx_mk, eq_iff_true_of_subsingleton
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
x y z : F.M
hx : Agree' (n + 1) z x
hy : Agree' (n + 1) z y
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps x = iselect ps y
succ :
  ∀ {a : F.A} (x_1 y_1 : F.B a → F.M),
    (∀ (i : F.B a), Agree' n (x_1 i) (y_1 i)) →
      z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_1) →
        x = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y_1) →
          Eq (α := CofixA F (n + 1 + 1)) (x.approx (n + 1 + 1)) (y.approx (n + 1 + 1))
⊢ Eq (α := CofixA F (n + 1 + 1)) (x.approx (n + 1 + 1)) (y.approx (n + 1 + 1))

Tactic:
cases hx
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
x y z : F.M
hy : Agree' (n + 1) z y
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps x = iselect ps y
a : F.A
x_1 y_1 : F.B a → F.M
h : ∀ (i : F.B a), Agree' n (x_1 i) (y_1 i)
h_1 : z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_1)
h_2 : x = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y_1)
succ :
  ∀ {a : F.A} (x_2 y_2 : F.B a → F.M),
    (∀ (i : F.B a), Agree' n (x_2 i) (y_2 i)) →
      z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_2) →
        y = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y_2) →
          Eq (α := CofixA F (n + 1 + 1)) (x.approx (n + 1 + 1)) (y.approx (n + 1 + 1))
⊢ Eq (α := CofixA F (n + 1 + 1)) (x.approx (n + 1 + 1)) (y.approx (n + 1 + 1))

Tactic:
cases hy
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
x y z : F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps x = iselect ps y
a : F.A
x_1 y_1 : F.B a → F.M
h : ∀ (i : F.B a), Agree' n (x_1 i) (y_1 i)
h_1 : z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_1)
h_2 : x = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y_1)
a_1 : F.A
x_2 y_2 : F.B a_1 → F.M
h_3 : ∀ (i : F.B a_1), Agree' n (x_2 i) (y_2 i)
h_4 : z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_2)
h_5 : y = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 y_2)
succ :
  ∀ (a_2 : F.A) (f : F.B a_2 → F.M)
    (hrec :
      ∀ (ps : Path F),
        n + 1 = length ps → iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)) = iselect ps y),
    M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f) =
        M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y_1) →
      Eq (α := CofixA F (n + 1 + 1)) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)).approx (n + 1 + 1))
        (y.approx (n + 1 + 1))
⊢ Eq (α := CofixA F (n + 1 + 1)) (x.approx (n + 1 + 1)) (y.approx (n + 1 + 1))

Tactic:
induction x using PFunctor.M.casesOn'

Premises used: PFunctor.M.casesOn'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
y z : F.M
a : F.A
x y_1 : F.B a → F.M
h : ∀ (i : F.B a), Agree' n (x i) (y_1 i)
h_1 : z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)
a_1 : F.A
x_1 y_2 : F.B a_1 → F.M
h_2 : ∀ (i : F.B a_1), Agree' n (x_1 i) (y_2 i)
h_3 : z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_1)
h_4 : y = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 y_2)
a_2 : F.A
f : F.B a_2 → F.M
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps → iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)) = iselect ps y
h_5 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y_1)
succ :
  ∀ (a : F.A) (f_1 : F.B a → F.M),
    M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f_1) =
        M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 y_2) →
      ∀
        (hrec :
          ∀ (ps : Path F),
            n + 1 = length ps →
              iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)) =
                iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f_1))),
        Eq (α := CofixA F (n + 1 + 1)) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)).approx (n + 1 + 1))
          ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f_1)).approx (n + 1 + 1))
⊢ Eq (α := CofixA F (n + 1 + 1)) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)).approx (n + 1 + 1))
    (y.approx (n + 1 + 1))

Tactic:
induction y using PFunctor.M.casesOn'

Premises used: PFunctor.M.casesOn'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
z : F.M
a : F.A
x y : F.B a → F.M
h : ∀ (i : F.B a), Agree' n (x i) (y i)
h_1 : z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)
a_1 : F.A
x_1 y_1 : F.B a_1 → F.M
h_2 : ∀ (i : F.B a_1), Agree' n (x_1 i) (y_1 i)
h_3 : z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_1)
a_2 : F.A
f : F.B a_2 → F.M
h_4 : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y)
a_3 : F.A
f_1 : F.B a_3 → F.M
h_5 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1) =
    M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 y_1)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1))
⊢ M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_1)

Tactic:
subst z
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
x y : F.B a → F.M
h : ∀ (i : F.B a), Agree' n (x i) (y i)
a_1 : F.A
x_1 y_1 : F.B a_1 → F.M
h_1 : ∀ (i : F.B a_1), Agree' n (x_1 i) (y_1 i)
a_2 : F.A
f : F.B a_2 → F.M
h_2 : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y)
a_3 : F.A
f_1 : F.B a_3 → F.M
h_3 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1) =
    M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 y_1)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1))
h_4 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_1)
⊢ Eq (α := (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M)
    (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_1)

Tactic:
have := mk_inj ‹_›
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
x y : F.B a → F.M
h : ∀ (i : F.B a), Agree' n (x i) (y i)
a_1 : F.A
x_1 y_1 : F.B a_1 → F.M
h_1 : ∀ (i : F.B a_1), Agree' n (x_1 i) (y_1 i)
a_2 : F.A
f : F.B a_2 → F.M
h_2 : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y)
a_3 : F.A
f_1 : F.B a_3 → F.M
h_3 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1) =
    M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 y_1)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1))
h_4 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_1)
this :
  Eq (α := (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M)
    (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_1)
succ :
  ∀ (y : F.B a → F.M),
    M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1) =
        M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y) →
      (∀ (i : F.B a), Agree' n (x i) (y i)) →
        M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) =
            M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) →
          Eq (α := CofixA F (n + 1 + 1)) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)).approx (n + 1 + 1))
            ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1)).approx (n + 1 + 1))
⊢ Eq (α := CofixA F (n + 1 + 1)) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)).approx (n + 1 + 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1)).approx (n + 1 + 1))

Tactic:
cases this
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
x y : F.B a → F.M
h : ∀ (i : F.B a), Agree' n (x i) (y i)
a_1 : F.A
f : F.B a_1 → F.M
h_1 : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y)
a_2 : F.A
f_1 : F.B a_2 → F.M
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1))
y_1 : F.B a → F.M
h_2 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y_1)
h_3 : ∀ (i : F.B a), Agree' n (x i) (y_1 i)
h_4 : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)
⊢ Eq (α := (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M)
    (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)

Tactic:
have := mk_inj ‹_›
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
x y : F.B a → F.M
h : ∀ (i : F.B a), Agree' n (x i) (y i)
a_1 : F.A
x_1 y_1 : F.B a_1 → F.M
h_1 : ∀ (i : F.B a_1), Agree' n (x_1 i) (y_1 i)
a_2 : F.A
f : F.B a_2 → F.M
h_2 : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y)
a_3 : F.A
f_1 : F.B a_3 → F.M
h_3 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1) =
    M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 y_1)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1))
h_4 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_1)
succ :
  ∀ (y : F.B a → F.M),
    M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1) =
        M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y) →
      (∀ (i : F.B a), Agree' n (x i) (y i)) →
        M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) =
            M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) →
          Eq (α := CofixA F (n + 1 + 1)) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)).approx (n + 1 + 1))
            ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1)).approx (n + 1 + 1))
⊢ Eq (α := CofixA F (n + 1 + 1)) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)).approx (n + 1 + 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1)).approx (n + 1 + 1))

Tactic:
iterate 3 (have := mk_inj ‹_›; cases this)
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
n_ih_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a_1 : F.A
f : F.B a_1 → F.M
h₂ : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)
a_2 : F.A
f_1 : F.B a_2 → F.M
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1))
f₁ : F.B a → F.M
h₁ :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁)
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃)
succ :
  Eq (α := CofixA F (n + 1 + 1)) (CofixA.intro a_1 fun (j : F.B a_1) ↦ (f j).approx (n + 1))
    (CofixA.intro a_2 fun (j : F.B a_2) ↦ (f_1 j).approx (n + 1))
⊢ Eq (α := CofixA F (n + 1 + 1)) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f)).approx (n + 1 + 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1)).approx (n + 1 + 1))

Tactic:
simp only [approx_mk]

Premises used: PFunctor.M.approx_mk
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
n_ih_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a_1 : F.A
f : F.B a_1 → F.M
h₂ : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)
a_2 : F.A
f_1 : F.B a_2 → F.M
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1))
f₁ : F.B a → F.M
h₁ :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁)
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃)
⊢ Eq (α := (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M)
    (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁)

Tactic:
have := mk_inj h₁
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
n_ih_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a_1 : F.A
f : F.B a_1 → F.M
h₂ : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)
a_2 : F.A
f_1 : F.B a_2 → F.M
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1))
f₁ : F.B a → F.M
h₁ :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁)
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃)
this :
  Eq (α := (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M)
    (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁)
succ :
  ∀
    (hrec :
      ∀ (ps : Path F),
        n + 1 = length ps →
          iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f)) =
            iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁)))
    (h₁ :
      M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁) =
        M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁)),
    Eq (α := CofixA F (n + 1 + 1)) (CofixA.intro a_1 fun (j : F.B a_1) ↦ (f j).approx (n + 1))
      (CofixA.intro a fun (j : F.B a) ↦ (f₁ j).approx (n + 1))
⊢ Eq (α := CofixA F (n + 1 + 1)) (CofixA.intro a_1 fun (j : F.B a_1) ↦ (f j).approx (n + 1))
    (CofixA.intro a_2 fun (j : F.B a_2) ↦ (f_1 j).approx (n + 1))

Tactic:
cases this