awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
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
⊢ Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
have 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))
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
Cleared hypotheses: n, x, y, z, hx, hy, hrec
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
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))
⊢ Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
have 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))
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
Cleared hypotheses: n, x, y, z, hx, hy, hrec
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
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
⊢ x = y
have H₁ : ∀ (i : ℕ), x.approx i = y.approx i
Tactic: apply ext'
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
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
⊢ Eq (α := CofixA F (i + 1)) (x.approx (i + 1)) (y.approx (i + 1))
have H₁ : Agree' i x x
Tactic: apply ext_aux x y x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
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
⊢ Eq (α := CofixA F (i + 1)) (x.approx (i + 1)) (y.approx (i + 1))
have H₂ : Agree' i x y
Tactic: apply ext_aux x y x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
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
⊢ Eq (α := CofixA F (i + 1)) (x.approx (i + 1)) (y.approx (i + 1))
have H₃ : ∀ (ps : Path F), i = length ps → iselect ps x = iselect ps y
Tactic: apply ext_aux x y x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
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' i x x
have H₁ : Agree (x.approx i) (x.approx (i + 1))
Tactic: rw [← agree_iff_agree']
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
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' i x y
have H₁ : Agree (y.approx i) (y.approx (i + 1))
Tactic: rw [← agree_iff_agree', i_ih]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
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
⊢ iselect ps x = iselect ps y
have i_ih₁ : Eq (α := CofixA F (length ps)) (x.approx (length ps)) (y.approx (length ps))
Tactic: cases H'
Cleared hypotheses: i, i_ih, H'
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
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 : ℕ
⊢ x.approx i = y.approx i
have H₁ : Eq (α := CofixA F 0) (x.approx 0) (y.approx 0)
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
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
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)
⊢ x.approx i = y.approx i
have H₂ : ∀ (i : ℕ) (i_ih : x.approx i = y.approx i), Eq (α := CofixA F (i + 1)) (x.approx (i + 1)) (y.approx (i + 1))
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
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
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₂
⊢ 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)
have 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)
Tactic: induction s₁ using PFunctor.M.casesOn' with | _ a f
Cleared hypotheses: s₁, h₀, hh
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
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₂
⊢ 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)
have 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)
Tactic: induction s₂ using PFunctor.M.casesOn' with | _ a' f'
Cleared hypotheses: s₂, h₀, hh
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
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'))
⊢ 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)
have 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)
Tactic: obtain rfl : a = a' := bisim.head h₀
Cleared hypotheses: a', f', h₀, hh
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
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'))
⊢ 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)
have f₁ : ∀ (i : F.B a), R (f i) (f' i)
Tactic: exists rfl, a, f, f', rfl, rfl
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
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' : 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)
have f₁ : ∀ (i : F.Idx) (ps : List F.Idx)
  (ps_ih :
    ∀ (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 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))
  (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 (i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) ∨
      IsPath (i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f'))),
  iselect (i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) =
      iselect (i :: 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 (i :: 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 (i :: 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: induction ps generalizing a f f' with
  | nil =>
    exists rfl, a, f, f', rfl, rfl
    apply bisim.tail h₀
  | cons i ps ps_ih => ?_
Cleared hypotheses: ps, a, f, f', h₀, hh
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Inhabited F.M
inst_1 : DecidableEq F.A
bisim : IsBisimulation R
i : F.Idx
ps : List F.Idx
ps_ih :
  ∀ (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 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)
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 (i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) ∨
    IsPath (i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f'))
⊢ iselect (i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) =
      iselect (i :: 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 (i :: 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 (i :: 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)
have f₁ : ∀ (a' : F.A) (i : F.B a')
  (hh :
    IsPath (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)) ∨
      IsPath (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 (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')) ∧
    ∃ (a_1 : F.A) (f_1 : F.B a_1 → F.M) (f'_1 : F.B a_1 → F.M),
      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)) =
          M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f_1) ∧
        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')) =
            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 ⟨a', i⟩ := i
Cleared hypotheses: i, hh
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Inhabited F.M
inst_1 : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (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 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)
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'))
a' : F.A
i : F.B a'
hh :
  IsPath (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)) ∨
    IsPath (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'))
⊢ a = a'
have inl : ∀
  (hh :
    IsPath (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))),
  a = a'
Tactic: rcases hh with hh | hh
Cleared hypotheses: hh
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Inhabited F.M
inst_1 : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (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 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)
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'))
a' : F.A
i : F.B a'
hh :
  IsPath (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)) ∨
    IsPath (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'))
inl :
  ∀
    (hh :
      IsPath (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))),
    a = a'
⊢ a = a'
have inr : ∀
  (hh :
    IsPath (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'))),
  a = a'
Tactic: rcases hh with hh | hh
Cleared hypotheses: hh