awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂)
f₁ : F.B a → F.M
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₃)
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₁))
⊢ 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_1 f) (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₂)
f₁ : F.B a → F.M
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₃)
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₁))
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_1 f) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)
succ :
  ∀
    (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₂))
    (hrec :
      ∀ (ps : Path F),
        n + 1 = length ps →
          iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)) =
            iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))),
    Eq (α := CofixA F (n + 1 + 1)) (CofixA.intro a fun (j : F.B a) ↦ (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 fun (j : F.B a) ↦ (f₁ j).approx (n + 1))

Tactic:
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)
f₁ : F.B a → F.M
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₃)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))
succ :
  Eq (α := F.B a → CofixA F (n + 1)) (fun (j : F.B a) ↦ (f₂ j).approx (n + 1)) fun (j : F.B a) ↦ (f₁ j).approx (n + 1)
⊢ Eq (α := CofixA F (n + 1 + 1)) (CofixA.intro a fun (j : F.B a) ↦ (f₂ j).approx (n + 1))
    (CofixA.intro a fun (j : F.B a) ↦ (f₁ j).approx (n + 1))

Tactic:
congr
-- 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)
f₁ : F.B a → F.M
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₃)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))
succ : ∀ (i : F.B a), Eq (α := CofixA F (n + 1)) ((f₂ i).approx (n + 1)) ((f₁ i).approx (n + 1))
⊢ Eq (α := F.B a → CofixA F (n + 1)) (fun (j : F.B a) ↦ (f₂ j).approx (n + 1)) fun (j : F.B a) ↦ (f₁ j).approx (n + 1)

Tactic:
ext i
-- 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)
f₁ : F.B a → F.M
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₃)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))
i : F.B a
succ : Agree' n (f₃ i) (f₂ i)
succ₁ : Agree' n (f₃ i) (f₁ i)
succ₂ : ∀ (ps : Path F), n = length ps → iselect ps (f₂ i) = iselect ps (f₁ i)
succ₃ : F.M
⊢ Eq (α := CofixA F (n + 1)) ((f₂ i).approx (n + 1)) ((f₁ i).approx (n + 1))

Tactic:
apply n_ih
-- 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)
f₁ : F.B a → F.M
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₃)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))
i : F.B a
⊢ Agree' n (f₃ i) (f₂ i)

Tactic:
solve_by_elim
-- 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)
f₁ : F.B a → F.M
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₃)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))
i : F.B a
⊢ Agree' n (f₃ i) (f₁ i)

Tactic:
solve_by_elim
-- 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)
f₁ : F.B a → F.M
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₃)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))
i : F.B a
ps : Path F
h : n = length ps
⊢ 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 (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₁))

Tactic:
specialize hrec (⟨_, i⟩ :: ps) (congr_arg _ h)

Premises used: List.cons, congr_arg, Sigma.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)
f₁ : F.B a → F.M
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₃)
i : F.B a
ps : Path F
h : n = length ps
hrec :
  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 (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) = iselect ps (f₁ i)

Tactic:
simp only [iselect_cons] at hrec

Premises used: PFunctor.M.iselect_cons
-- 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)
f₁ : F.B a → F.M
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₃)
i : F.B a
ps : Path F
h : n = length ps
hrec : iselect ps (f₂ i) = iselect ps (f₁ i)
⊢ iselect ps (f₂ i) = iselect ps (f₁ i)

Tactic:
hrec
-- 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)
f₁ : F.B a → F.M
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₃)
i : F.B a
ps : Path F
h : n = length ps
hrec : iselect ps (f₂ i) = iselect ps (f₁ i)
⊢ iselect ps (f₂ i) = iselect ps (f₁ i)

Tactic:
exact hrec
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
n : ℕ
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
zero :
  ∀ (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),
    Eq (α := CofixA F (HAdd.hAdd (α := ℕ) 0 1)) (x.approx (HAdd.hAdd (α := ℕ) 0 1)) (y.approx (HAdd.hAdd (α := ℕ) 0 1))
succ :
  ∀ (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),
    Eq (α := CofixA F (n + 1 + 1)) (x.approx (n + 1 + 1)) (y.approx (n + 1 + 1))
⊢ Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))

Tactic:
induction n generalizing x y z with
  | zero =>
    specialize hrec [] rfl
    induction x using PFunctor.M.casesOn'
    induction y using PFunctor.M.casesOn'
    simp only [iselect_nil] at hrec
    subst hrec
    simp only [approx_mk, heq_iff_eq, CofixA.intro.injEq,
      eq_iff_true_of_subsingleton, and_self]
  | succ n n_ih =>
    cases hx
    cases hy
    induction x using PFunctor.M.casesOn'
    induction y using PFunctor.M.casesOn'
    subst z
    iterate 3 (have := mk_inj ‹_›; cases this)
    rename_i n_ih a f₃ f₂ hAgree₂ _ _ h₂ _ _ f₁ h₁ hAgree₁ clr
    simp only [approx_mk]
    have := mk_inj h₁
    cases this; clear h₁
    have := mk_inj h₂
    cases this; clear h₂
    congr
    ext i
    apply n_ih
    · solve_by_elim
    · solve_by_elim
    introv h
    specialize hrec (⟨_, i⟩ :: ps) (congr_arg _ h)
    simp only [iselect_cons] at hrec
    exact hrec

Premises used: PFunctor.M.casesOn', and_self, PFunctor.Approx.CofixA.intro.injEq, heq_iff_eq, PFunctor.M.iselect_nil, PFunctor.M.approx_mk, Nat.zero, Nat.succ, eq_iff_true_of_subsingleton, PFunctor.M.iselect_cons, List.nil
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
H₁ : ∀ (i : ℕ), x.approx i = y.approx i
⊢ x = y

Tactic:
apply ext'

Premises used: PFunctor.M.ext'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ Eq (α := CofixA F 0) (x.approx 0) (y.approx 0)

Tactic:
subsingleton
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
H₁ : Agree' i x x
H₂ : Agree' i x y
H₃ : ∀ (ps : Path F), i = length ps → iselect ps x = iselect ps y
⊢ Eq (α := CofixA F (i + 1)) (x.approx (i + 1)) (y.approx (i + 1))

Tactic:
apply ext_aux x y x

Premises used: PFunctor.M.ext_aux
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
H₁ : Agree (x.approx i) (x.approx (i + 1))
⊢ Agree' i x x

Tactic:
rw [← agree_iff_agree']

Premises used: PFunctor.M.agree_iff_agree'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree (x.approx i) (x.approx (i + 1))

Tactic:
apply x.consistent

Premises used: PFunctor.MIntl.consistent
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
H₁ : Agree (y.approx i) (y.approx (i + 1))
⊢ Agree' i x y

Tactic:
rw [← agree_iff_agree', i_ih]

Premises used: PFunctor.M.agree_iff_agree'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree (y.approx i) (y.approx (i + 1))

Tactic:
apply y.consistent

Premises used: PFunctor.MIntl.consistent
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), (isubtree ps x).head = (isubtree ps y).head
i : ℕ
i_ih : x.approx i = y.approx i
ps : Path F
H' : i = length ps
⊢ Eq (α := CofixA F (length ps)) (x.approx (length ps)) (y.approx (length ps))

Tactic:
cases H'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), (isubtree ps x).head = (isubtree ps y).head
ps : Path F
i_ih : Eq (α := CofixA F (length ps)) (x.approx (length ps)) (y.approx (length ps))
⊢ iselect ps x = iselect ps y

Tactic:
apply H ps
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
H₁ : Eq (α := CofixA F 0) (x.approx 0) (y.approx 0)
H₂ : ∀ (i : ℕ) (i_ih : x.approx i = y.approx i), Eq (α := CofixA F (i + 1)) (x.approx (i + 1)) (y.approx (i + 1))
⊢ x.approx i = y.approx i

Tactic:
induction i with
  | zero => subsingleton
  | succ i i_ih =>
    apply ext_aux x y x
    · rw [← agree_iff_agree']
      apply x.consistent
    · rw [← agree_iff_agree', i_ih]
      apply y.consistent
    introv H'
    dsimp only [iselect] at H
    cases H'
    apply H ps

Premises used: PFunctor.M.iselect, PFunctor.MIntl.consistent, PFunctor.M.agree_iff_agree', PFunctor.M.ext_aux, Nat.zero, Nat.succ
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Inhabited F.M
inst_1 : DecidableEq F.A
bisim : IsBisimulation R
s₁ s₂ : F.M
ps : Path F
h₀ : R s₁ s₂
hh : IsPath ps s₁ ∨ IsPath ps s₂
f :
  ∀ (a : F.A) (f : F.B a → F.M) (h₀ : R (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) s₂)
    (hh : IsPath ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) ∨ IsPath ps s₂),
    iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) = iselect ps s₂ ∧
      ∃ (a_1 : F.A) (f_1 : F.B a_1 → F.M) (f' : F.B a_1 → F.M),
        isubtree ps (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_1 f_1) ∧
          isubtree ps s₂ = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f') ∧ ∀ (i : F.B a_1), R (f_1 i) (f' i)
⊢ iselect ps s₁ = iselect ps s₂ ∧
    ∃ (a : F.A) (f : F.B a → F.M) (f' : F.B a → F.M),
      isubtree ps s₁ = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f) ∧
        isubtree ps s₂ = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f') ∧ ∀ (i : F.B a), R (f i) (f' i)

Tactic:
induction s₁ using PFunctor.M.casesOn' with | _ a f

Premises used: PFunctor.M.casesOn'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Inhabited F.M
inst_1 : DecidableEq F.A
bisim : IsBisimulation R
s₂ : F.M
ps : Path F
a : F.A
f : F.B a → F.M
h₀ : R (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) s₂
hh : IsPath ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) ∨ IsPath ps s₂
f₁ :
  ∀ (a' : F.A) (f' : F.B a' → F.M)
    (h₀ :
      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' f')))
    (hh :
      IsPath ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) ∨
        IsPath ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a' f'))),
    iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) =
        iselect ps (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) (f'_1 : F.B a_1 → F.M),
        isubtree ps (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_1 f_1) ∧
          isubtree ps (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_1 f'_1) ∧
            ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
⊢ iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) = iselect ps s₂ ∧
    ∃ (a_1 : F.A) (f_1 : F.B a_1 → F.M) (f' : F.B a_1 → F.M),
      isubtree ps (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_1 f_1) ∧
        isubtree ps s₂ = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f') ∧ ∀ (i : F.B a_1), R (f_1 i) (f' i)

Tactic:
induction s₂ using PFunctor.M.casesOn' with | _ a' f'

Premises used: PFunctor.M.casesOn'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Inhabited F.M
inst_1 : DecidableEq F.A
bisim : IsBisimulation R
ps : Path F
a : F.A
f : F.B a → F.M
a' : F.A
f' : F.B a' → F.M
h₀ :
  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' f'))
hh :
  IsPath ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) ∨
    IsPath ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a' f'))
⊢ a = a'

Tactic:
bisim.head h₀

Premises used: PFunctor.M.IsBisimulation.head
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Inhabited F.M
inst_1 : DecidableEq F.A
bisim : IsBisimulation R
ps : Path F
a : F.A
f : F.B a → F.M
a' : F.A
f' : F.B a' → F.M
h₀ :
  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' f'))
hh :
  IsPath ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) ∨
    IsPath ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a' f'))
f₁ :
  ∀ (f' : F.B a → F.M)
    (h₀ :
      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 f')))
    (hh :
      IsPath ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) ∨
        IsPath ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f'))),
    iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) =
        iselect ps (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) (f'_1 : F.B a_1 → F.M),
        isubtree ps (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_1 f_1) ∧
          isubtree ps (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_1 f'_1) ∧
            ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
⊢ iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) =
      iselect ps (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) (f'_1 : F.B a_1 → F.M),
      isubtree ps (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_1 f_1) ∧
        isubtree ps (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_1 f'_1) ∧
          ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)

Tactic:
obtain rfl : a = a' := bisim.head h₀

Premises used: PFunctor.M.IsBisimulation.head, rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Inhabited F.M
inst_1 : DecidableEq F.A
bisim : IsBisimulation R
a : F.A
f f' : F.B a → F.M
h₀ :
  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 f'))
hh :
  IsPath [] (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) ∨
    IsPath [] (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f'))
f₁ : ∀ (i : F.B a), R (f i) (f' i)
⊢ 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 f')) ∧
    ∃ (a_1 : F.A) (f_1 : F.B a_1 → F.M) (f'_1 : F.B a_1 → F.M),
      isubtree [] (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_1 f_1) ∧
        isubtree [] (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_1 f'_1) ∧
          ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)

Tactic:
exists rfl, a, f, f', rfl, rfl

Premises used: rfl