awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
h : Agree' n x y
mpr : ∀ (x y : F.M) (h : Agree' 0 x y), Agree (n := 0) (x.approx 0) (y.approx (HAdd.hAdd (α := ℕ) 0 1))
mpr₁ :
  ∀ (n : ℕ) (n_ih : ∀ (x y : F.M) (h : Agree' n x y), Agree (x.approx n) (y.approx (n + 1))) (x y : F.M)
    (h : Agree' (n + 1) x y), Agree (n := n + 1) (x.approx (n + 1)) (y.approx (n + 1 + 1))
⊢ Agree (x.approx n) (y.approx (n + 1))

Tactic:
induction n generalizing x y with
    | zero => constructor
    | succ _ n_ih =>
      obtain - | @⟨_, a, x', y'⟩ := h
      induction x using PFunctor.M.casesOn' with | _ x_a x_f
      induction y using PFunctor.M.casesOn' with | _ y_a y_f
      simp only [approx_mk]
      have h_a_1 := mk_inj ‹M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩›
      cases h_a_1
      replace h_a_2 := mk_inj ‹M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩›
      cases h_a_2
      constructor
      intro i
      apply n_ih
      simp [*]

Premises used: PFunctor.M.casesOn', PFunctor.M.approx_mk, Nat.zero, Nat.succ
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
r : F.M → Sort u_2
x : (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M
f : (x : (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M) → r (M.mk x)
⊢ M.cases (r := r) f (M.mk x) = f x

Tactic:
rfl

Premises used: Eq.mpr, PFunctor.Obj, PFunctor.M, cast, PFunctor.M.cases, PFunctor.M.children, PFunctor.M.dest, PFunctor.M.head, PFunctor.Approx.children', rfl, PFunctor.M.Approx.sMk, PFunctor.Approx.head', PFunctor.M.mk
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
r : F.M → Sort u_2
x : (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M
f : (x : (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M) → r (M.mk x)
⊢ (M.mk x).casesOn (r := r) f = f x

Tactic:
cases_mk x f

Premises used: PFunctor.M.casesOn, PFunctor.M.cases_mk
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
r : F.M → Sort u_2
a : F.A
x : F.B a → F.M
f : (a : F.A) → (f : F.B a → F.M) → r (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 x)).casesOn' (r := r) f = f a x

Tactic:
@cases_mk F r ⟨a, x⟩ (fun ⟨a, g⟩ => f a g)

Premises used: PFunctor.M.casesOn, PFunctor.M.casesOn', PFunctor.M.cases_mk, PFunctor.M.casesOn'.match_1, Sigma.mk, PFunctor.M.mk
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
xs : Path F
a a' : F.A
f : F.B a → F.M
i : F.B a'
generalize :
  ∀ (x : F.M) (h : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f) = x),
    IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a' i :: xs) x → a = a'
⊢ IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a' i :: xs) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) →
    a = a'

Tactic:
generalize h : M.mk ⟨a, f⟩ = x

Premises used: Sigma.mk, PFunctor.M.mk
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
xs : Path F
a a' : F.A
f : F.B a → F.M
i : F.B a'
f_1 : F.B a' → F.M
h_1 : IsPath xs (f_1 i)
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_1)
cons :
  ∀ {i : F.B a},
    IsPath xs (f i) →
      ∀
        (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)),
        a = a
⊢ a = a'

Tactic:
cases mk_inj h

Premises used: PFunctor.M.mk_inj
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
h_1 : IsPath xs (f i)
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)
⊢ a = a

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
generalize :
  ∀ (x : F.M) (h : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f) = x),
    IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: xs) x → IsPath xs (f i)
⊢ IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: xs) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) →
    IsPath xs (f i)

Tactic:
generalize h : M.mk ⟨a, f⟩ = x

Premises used: Sigma.mk, PFunctor.M.mk
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
f_1 : F.B a → F.M
hp : IsPath xs (f_1 i)
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_1)
⊢ IsPath xs (f i)

Tactic:
cases mk_inj h

Premises used: PFunctor.M.mk_inj
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
f_1 : F.B a → F.M
hp : IsPath xs (f_1 i)
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_1)
hp₁ : IsPath xs (f i)
⊢ 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)

Tactic:
cases mk_inj h

Premises used: PFunctor.M.mk_inj
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
hp : IsPath xs (f i)
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)
⊢ IsPath xs (f i)

Tactic:
hp
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
hp : IsPath xs (f i)
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)
⊢ IsPath xs (f i)

Tactic:
exact hp
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
X : Type u_1
f_1 : X → (↑F : (α : Type u_1) → Type (max u_1 uA uB)) X
inst : DecidableEq F.A
inst_1 : Inhabited F.M
a : F.A
i : F.B a
ps : List F.Idx
x : F.M
a' : F.A
f : F.B a' → F.M
h : a = a'
rw rw₁ : F.B a' = F.B a'
⊢ F.B a = F.B a'

Tactic:
rw [h]
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
x : F.M
h : ¬IsPath [] x
nil : False
⊢ iselect [] x = head default

Tactic:
exfalso
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
x : F.M
h : ¬IsPath [] x
nil : IsPath [] x
⊢ False

Tactic:
apply h
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
x : F.M
h : ¬IsPath [] x
⊢ IsPath [] x

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_hd : F.Idx
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), iselect ps_tail x = head default
x : F.M
h : ¬IsPath (ps_hd :: ps_tail) x
cons :
  ∀ (a : F.A) (i : F.B a) (h : ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail) x),
    iselect (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail) x = head default
⊢ iselect (ps_hd :: ps_tail) x = head default

Tactic:
obtain ⟨a, i⟩ := ps_hd
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), iselect ps_tail x = head default
x : F.M
a : F.A
i : F.B a
h : ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail) x
cons :
  ∀ (x_a : F.A) (x_f : F.B x_a → F.M)
    (h :
      ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
          (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f))),
    iselect (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
        (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f)) =
      head default
⊢ iselect (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail) x = head default

Tactic:
induction x using PFunctor.M.casesOn' with | _ x_a x_f

Premises used: PFunctor.M.casesOn'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), iselect ps_tail x = head default
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f))
cons :
  Eq.{uA + 1} (α := F.A)
    (head
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f)).casesOn' (r := fun (x : F.M) ↦ F.M)
        fun (a' : F.A) (f : F.B a' → F.M) ↦ if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default))
    (head default)
⊢ iselect (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f)) =
    head default

Tactic:
simp only [iselect, isubtree] at ps_ih ⊢

Premises used: PFunctor.M.iselect, PFunctor.M.isubtree
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f))
pos :
  ∀ (h'' : a = x_a),
    Eq.{uA + 1} (α := F.A)
      (head
        ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f)).casesOn' (r := fun (x : F.M) ↦ F.M)
          fun (a' : F.A) (f : F.B a' → F.M) ↦ if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default))
      (head default)
neg :
  ∀ (h'' : ¬a = x_a),
    Eq.{uA + 1} (α := F.A)
      (head
        ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f)).casesOn' (r := fun (x : F.M) ↦ F.M)
          fun (a' : F.A) (f : F.B a' → F.M) ↦ if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default))
      (head default)
⊢ Eq.{uA + 1} (α := F.A)
    (head
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f)).casesOn' (r := fun (x : F.M) ↦ F.M)
        fun (a' : F.A) (f : F.B a' → F.M) ↦ if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default))
    (head default)

Tactic:
by_cases h'' : a = x_a
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f))
h'' : a = x_a
pos :
  ∀ (x_f : F.B a → F.M)
    (h :
      ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
          (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))),
    Eq.{uA + 1} (α := F.A)
      (head
        ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f)).casesOn' (r := fun (x : F.M) ↦ F.M)
          fun (a' : F.A) (f : F.B a' → F.M) ↦ if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default))
      (head default)
⊢ Eq.{uA + 1} (α := F.A)
    (head
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f)).casesOn' (r := fun (x : F.M) ↦ F.M)
        fun (a' : F.A) (f : F.B a' → F.M) ↦ if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default))
    (head default)

Tactic:
subst x_a
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_f : F.B a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))
pos : (isubtree ps_tail (x_f (cast ⋯ i))).head = head default
⊢ Eq.{uA + 1} (α := F.A)
    (head
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f)).casesOn' (r := fun (x : F.M) ↦ F.M)
        fun (a' : F.A) (f : F.B a' → F.M) ↦ if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default))
    (head default)

Tactic:
simp only [dif_pos, casesOn_mk']

Premises used: PFunctor.M.casesOn_mk', dif_pos
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_f : F.B a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))
pos : ¬IsPath ps_tail (x_f (cast ⋯ i))
⊢ (isubtree ps_tail (x_f (cast ⋯ i))).head = head default

Tactic:
rw [ps_ih]
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_f : F.B a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))
h' : IsPath ps_tail (x_f (cast ⋯ i))
pos :
  IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
    (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))
⊢ False

Tactic:
apply h
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_f : F.B a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))
h' : IsPath ps_tail (x_f (cast ⋯ i))
pos :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f)
pos₁ : IsPath ps_tail (x_f i)
pos₂ : F.B a → F.M
⊢ IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
    (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_f : F.B a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f)

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_f : F.B a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f)

Tactic:
try rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_f : F.B a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ IsPath ps_tail (x_f i)

Tactic:
apply h'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f))
h'' : ¬a = x_a
⊢ Eq.{uA + 1} (α := F.A)
    (head
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f)).casesOn' (r := fun (x : F.M) ↦ F.M)
        fun (a' : F.A) (f : F.B a' → F.M) ↦ if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default))
    (head default)

Tactic:
simp [*]
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps : Path F
x : F.M
h : ¬IsPath ps x
nil : ∀ (x : F.M) (h : ¬IsPath [] x), iselect [] x = head default
cons :
  ∀ (ps_hd : F.Idx) (ps_tail : List F.Idx)
    (ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), iselect ps_tail x = head default) (x : F.M)
    (h : ¬IsPath (ps_hd :: ps_tail) x), iselect (ps_hd :: ps_tail) x = head default
⊢ iselect ps x = head default

Tactic:
induction ps generalizing x with
  | nil =>
    exfalso
    apply h
    constructor
  | cons ps_hd ps_tail ps_ih =>
    obtain ⟨a, i⟩ := ps_hd
    induction x using PFunctor.M.casesOn' with | _ x_a x_f
    simp only [iselect, isubtree] at ps_ih ⊢
    by_cases h'' : a = x_a
    · subst x_a
      simp only [dif_pos, casesOn_mk']
      rw [ps_ih]
      intro h'
      apply h
      constructor <;> try rfl
      apply h'
    · simp [*]

Premises used: PFunctor.M.casesOn', PFunctor.M.iselect, PFunctor.M.casesOn_mk', dif_pos, List.cons, PFunctor.M.isubtree, List.nil
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x : (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M
rw rw₁ : x.fst (β := fun (x : F.A) ↦ F.B x → F.M) = x.fst (β := fun (x : F.A) ↦ F.B x → F.M)
⊢ x.fst (β := fun (x : F.A) ↦ F.B x → F.M) = (M.mk x).dest.fst (β := fun (x : F.A) ↦ F.B x → F.M)

Tactic:
rw [dest_mk]

Premises used: PFunctor.M.dest_mk
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
X : Type u_1
f : X → (↑F : (α : Type u_1) → Type (max u_1 uA uB)) X
a : F.A
x : F.B a → F.M
i : F.B (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)).head
rw rw₁ : F.B (Sigma.fst (β := fun (x : F.A) ↦ F.B x → F.M) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)) = F.B a
⊢ F.B (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)).head = F.B a

Tactic:
rw [head_mk]

Premises used: PFunctor.M.head_mk
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
a : F.A
x : F.B a → F.M
i : F.B (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)).head
H :
  ∀ (i_1 : ℕ),
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)).children i).approx i_1 = (x (cast ⋯ i)).approx i_1
⊢ (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)).children i = x (cast ⋯ i)

Tactic:
apply ext'

Premises used: PFunctor.M.ext'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
a : F.A
x : F.B a → F.M
i : F.B (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)).head
n : ℕ
⊢ ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)).children i).approx n = (x (cast ⋯ i)).approx n

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
x : (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M
i : F.Idx
⊢ Eq (α := F.M)
    (if H' : i.fst (β := fun (x : F.A) ↦ F.B x) = (M.mk x).head then
      (M.mk x).children (cast ⋯ (i.snd (β := fun (x : F.A) ↦ F.B x)))
    else default)
    (if h : i.fst (β := fun (x : F.A) ↦ F.B x) = x.fst (β := fun (x : F.A) ↦ F.B x → F.M) then
      x.snd (β := fun (x : F.A) ↦ F.B x → F.M) (cast ⋯ (i.snd (β := fun (x : F.A) ↦ F.B x)))
    else default)

Tactic:
congr with h
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps : Path F
a : F.A
f : F.B a → F.M
i : F.B a
simp : isubtree ps (f (cast ⋯ i)) = isubtree ps (f i)
⊢ isubtree (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) =
    isubtree ps (f i)

Tactic:
simp only [isubtree, dif_pos, isubtree, M.casesOn_mk']

Premises used: PFunctor.M.casesOn_mk', dif_pos, PFunctor.M.isubtree
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps : Path F
a : F.A
f : F.B a → F.M
i : F.B a
⊢ isubtree ps (f (cast ⋯ i)) = isubtree ps (f i)

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
a : F.A
f : F.B a → F.M
⊢ iselect [] (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) = a

Tactic:
rfl

Premises used: PFunctor.M.iselect, PFunctor.M.head, rfl, PFunctor.M.Approx.sMk, PFunctor.Approx.head'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps : Path F
a : F.A
f : F.B a → F.M
i : F.B a
⊢ iselect (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) =
    iselect ps (f i)

Tactic:
simp only [iselect, isubtree_cons]

Premises used: PFunctor.M.iselect, PFunctor.M.isubtree_cons
-- 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
e_approx : ∀ (n : ℕ), sCorec f x₀ n = Approx.sMk (F.map (M.corec f) (f x₀)) n
⊢ { approx := sCorec f x₀, consistent := ⋯ : F.MIntl } =
    { approx := Approx.sMk (F.map (M.corec f) (f x₀)), consistent := ⋯ }

Tactic:
congr with n
-- 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 : ℕ
e_approx : Eq (α := CofixA F 0) (sCorec f x₀ 0) (Approx.sMk (F.map (M.corec f) (f x₀)) 0)
e_approx₁ : ∀ (n : ℕ), Eq (α := CofixA F (n + 1)) (sCorec f x₀ (n + 1)) (Approx.sMk (F.map (M.corec f) (f x₀)) (n + 1))
⊢ sCorec f x₀ n = Approx.sMk (F.map (M.corec f) (f x₀)) n

Tactic:
rcases n with - | n
-- 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
⊢ Eq (α := CofixA F 0) (sCorec f x₀ 0) (Approx.sMk (F.map (M.corec f) (f x₀)) 0)

Tactic:
dsimp only [sCorec, Approx.sMk]

Premises used: PFunctor.Approx.sCorec, PFunctor.M.Approx.sMk
-- 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 : ℕ
e_approx :
  ∀ (fst : F.A) (snd : F.B fst → X),
    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)
⊢ Eq (α := CofixA F (n + 1))
    (CofixA.intro ((f x₀).fst (β := fun (x : F.A) ↦ F.B x → X))
      fun (i : F.B ((f x₀).fst (β := fun (x : F.A) ↦ F.B x → X))) ↦
      sCorec f ((f x₀).snd (β := fun (x : F.A) ↦ F.B x → X) i) n)
    (CofixA.intro ((F.map (M.corec f) (f x₀)).fst (β := fun (x : F.A) ↦ F.B x → F.M))
      fun (i : F.B ((F.map (M.corec f) (f x₀)).fst (β := fun (x : F.A) ↦ F.B x → F.M))) ↦
      ((F.map (M.corec f) (f x₀)).snd (β := fun (x : F.A) ↦ F.B x → F.M) i).approx n)

Tactic:
cases f x₀