awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ a = a'
have inl : ∀ (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))),
  a = a
Tactic: cases isPath_cons hh
Cleared hypotheses: a', 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'))
⊢ a = a'
have inr : ∀ (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'))),
  a = a
Tactic: cases isPath_cons hh
Cleared hypotheses: a', i, hh
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
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'))),
    (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f))).head =
        (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f'))).head ∧
      ∃ (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'))
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'))
⊢ (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))).head =
      (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'))).head ∧
    ∃ (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)
have h₁ : R (f i) (f' i)
Tactic: have h₁ := bisim.tail h₀ 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
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'))),
    (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f))).head =
        (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f'))).head ∧
      ∃ (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'))
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'))
h₁ : R (f i) (f' i)
a₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a₀ f₀)
a₁ : F.A
f₁ : F.B a₁ → F.M
h' : f' i = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a₁ f₁)
⊢ (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))).head =
      (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'))).head ∧
    ∃ (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)
have f₂ : (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a₀ f₀))).head =
    (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a₁ f₁))).head ∧
  ∃ (a : F.A) (f : F.B a → F.M) (f' : F.B a → 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 f) ∧
      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 f') ∧
        ∀ (i : F.B a), R (f i) (f' i)
Tactic: simp only [h, h', isubtree_cons] at ps_ih ⊢
-- 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'))),
    (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f))).head =
        (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f'))).head ∧
      ∃ (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'))
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₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) 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₁))
h' : f' i = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a₀ f₁)
⊢ (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a₀ f₀))).head =
      (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a₀ f₁))).head ∧
    ∃ (a : F.A) (f : F.B a → F.M) (f' : F.B a → 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 f) ∧
        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 f') ∧
          ∀ (i : F.B a), R (f i) (f' i)
have f₂ : 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₁))
Tactic: apply ps_ih _ _ _ h₁
-- 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'))),
    (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f))).head =
        (isubtree ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f'))).head ∧
      ∃ (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'))
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₀ : F.A
f₀ : F.B a₀ → F.M
h : f i = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) 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₁))
h' : f' i = 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₀)) ∨
    IsPath ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a₀ f₁))
have f₂ : IsPath ps (f i) ∨ IsPath ps (f' i)
Tactic: rw [← h, ← h']
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Nonempty F.M
bisim : IsBisimulation R
⊢ ∀ (s₁ s₂ : F.M), R s₁ s₂ → s₁ = s₂
have inhabit : ∀ (inhabited_h : Inhabited F.M) (s₁ s₂ : F.M), R s₁ s₂ → s₁ = s₂
Tactic: inhabit M F
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
⊢ s₁ = s₂
have H : ∀ (ps : Path F), iselect ps s₁ = iselect ps s₂
Tactic: apply ext
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
⊢ iselect ps s₁ = iselect ps s₂
have pos : ∀ (h : IsPath ps s₁ ∨ IsPath ps s₂), iselect ps s₁ = iselect ps s₂
Tactic: by_cases h : IsPath ps s₁ ∨ IsPath ps s₂
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
pos : ∀ (h : IsPath ps s₁ ∨ IsPath ps s₂), iselect ps s₁ = iselect ps s₂
⊢ iselect ps s₁ = iselect ps s₂
have neg : ∀ (h : ¬(IsPath ps s₁ ∨ IsPath ps s₂)), iselect ps s₁ = iselect ps s₂
Tactic: by_cases h : IsPath ps s₁ ∨ IsPath ps s₂
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : IsPath ps s₁ ∨ IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂
have H : 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: have H := nth_of_bisim R bisim _ _ ps Hr h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : ¬(IsPath ps s₁ ∨ IsPath ps s₂)
⊢ iselect ps s₁ = iselect ps s₂
have h₁ : ¬IsPath ps s₁ ∧ ¬IsPath ps s₂
Tactic: rw [not_or] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : ¬IsPath ps s₁ ∧ ¬IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂
have h₀ : ¬IsPath ps s₁
Tactic: obtain ⟨h₀, h₁⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : ¬IsPath ps s₁ ∧ ¬IsPath ps s₂
h₀ : ¬IsPath ps s₁
⊢ iselect ps s₁ = iselect ps s₂
have h₁ : ¬IsPath ps s₂
Tactic: obtain ⟨h₀, h₁⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
introv introv₁ introv₂ introv₃ introv₄ introv₅ : ∀ (s₁ s₂ : F.M) (Hr : R s₁ s₂), s₁ = s₂
⊢ ∀ (s₁ s₂ : F.M), R s₁ s₂ → s₁ = s₂
have H : ∀ (s₁ s₂ : F.M) (Hr : R s₁ s₂) (ps : Path F), iselect ps s₁ = iselect ps s₂
Tactic: classical
  introv Hr; apply ext
  introv
  by_cases h : IsPath ps s₁ ∨ IsPath ps s₂
  · have H := nth_of_bisim R bisim _ _ ps Hr h
    exact H.left
  · rw [not_or] at h
    obtain ⟨h₀, h₁⟩ := h
    simp only [iselect_eq_default, *, not_false_iff]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
introv introv₁ introv₂ introv₃ introv₄ introv₅ : ∀ (s₁ s₂ : F.M) (Hr : R s₁ s₂), s₁ = s₂
H H₁ : ∀ (s₁ s₂ : F.M) (Hr : R s₁ s₂) (ps : Path F), iselect ps s₁ = iselect ps s₂
⊢ ∀ (s₁ s₂ : F.M), R s₁ s₂ → s₁ = s₂
have pos : ∀ (s₁ s₂ : F.M) (Hr : R s₁ s₂) (ps : Path F) (h : IsPath ps s₁ ∨ IsPath ps s₂), iselect ps s₁ = iselect ps s₂
Tactic: classical
  introv Hr; apply ext
  introv
  by_cases h : IsPath ps s₁ ∨ IsPath ps s₂
  · have H := nth_of_bisim R bisim _ _ ps Hr h
    exact H.left
  · rw [not_or] at h
    obtain ⟨h₀, h₁⟩ := h
    simp only [iselect_eq_default, *, not_false_iff]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
introv introv₁ introv₂ introv₃ introv₄ introv₅ : ∀ (s₁ s₂ : F.M) (Hr : R s₁ s₂), s₁ = s₂
H H₁ : ∀ (s₁ s₂ : F.M) (Hr : R s₁ s₂) (ps : Path F), iselect ps s₁ = iselect ps s₂
pos : ∀ (s₁ s₂ : F.M) (Hr : R s₁ s₂) (ps : Path F) (h : IsPath ps s₁ ∨ IsPath ps s₂), iselect ps s₁ = iselect ps s₂
⊢ ∀ (s₁ s₂ : F.M), R s₁ s₂ → s₁ = s₂
have neg : ∀ (s₁ s₂ : F.M) (Hr : R s₁ s₂) (ps : Path F) (h : ¬(IsPath ps s₁ ∨ IsPath ps s₂)), iselect ps s₁ = iselect ps s₂
Tactic: classical
  introv Hr; apply ext
  introv
  by_cases h : IsPath ps s₁ ∨ IsPath ps s₂
  · have H := nth_of_bisim R bisim _ _ ps Hr h
    exact H.left
  · rw [not_or] at h
    obtain ⟨h₀, h₁⟩ := h
    simp only [iselect_eq_default, *, not_false_iff]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
x : α
⊢ (M.corec g x).dest = P.map (M.corec g) (g x)
have rw : (M.mk (P.map (M.corec g) (g x))).dest = P.map (M.corec g) (g x)
Tactic: rw [corec_def, dest_mk]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
x : α
rw : (M.mk (P.map (M.corec g) (g x))).dest = P.map (M.corec g) (g x)
⊢ (M.corec g x).dest = P.map (M.corec g) (g x)
have rw₁ : P.map (M.corec g) (g x) = P.map (M.corec g) (g x)
Tactic: rw [corec_def, dest_mk]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h :
  ∀ (x y : P.M),
    R x y →
      ∃ (a : P.A) (f : P.B a → P.M) (f' : P.B a → P.M),
        x.dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f ∧
          y.dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧ ∀ (i : P.B a), R (f i) (f' i)
x y : P.M
h' : R x y
⊢ x = y
have haveI : ∀ (this : Inhabited P.A), x = y
Tactic: haveI := Inhabited.mk x.head
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h :
  ∀ (x y : P.M),
    R x y →
      ∃ (a : P.A) (f : P.B a → P.M) (f' : P.B a → P.M),
        x.dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f ∧
          y.dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧ ∀ (i : P.B a), R (f i) (f' i)
x y : P.M
h' : R x y
this : Inhabited P.A
⊢ x = y
have apply : IsBisimulation R
Tactic: apply eq_of_bisim R _ _ _ h'
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h :
  ∀ (x y : P.M),
    R x y →
      ∃ (a : P.A) (f : P.B a → P.M) (f' : P.B a → P.M),
        x.dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f ∧
          y.dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
⊢ IsBisimulation R
have head : ∀ {a a' : P.A} {f : P.B a → P.M} {f' : P.B a' → P.M},
  R (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f))
      (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a' f')) →
    a = a'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h :
  ∀ (x y : P.M),
    R x y →
      ∃ (a : P.A) (f : P.B a → P.M) (f' : P.B a → P.M),
        x.dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f ∧
          y.dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
head :
  ∀ {a a' : P.A} {f : P.B a → P.M} {f' : P.B a' → P.M},
    R (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f))
        (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a' f')) →
      a = a'
⊢ IsBisimulation R
have tail : ∀ {a : P.A} {f f' : P.B a → P.M},
  R (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f)) (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f')) →
    ∀ (i : P.B a), R (f i) (f' i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h :
  ∀ (x y : P.M),
    R x y →
      ∃ (a : P.A) (f : P.B a → P.M) (f' : P.B a → P.M),
        x.dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f ∧
          y.dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
a a' : P.A
f : P.B a → P.M
f' : P.B a' → P.M
ih :
  R (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f)) (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a' f'))
⊢ a = a'
have head : ∀ (a'' : P.A) (g g' : P.B a'' → P.M)
  (h₀ :
    (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f)).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g)
  (h₁ :
    (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a' f')).dest =
      Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g')
  (h₂ : ∀ (i : P.B a''), R (g i) (g' i)), a = a'
Tactic: rcases h _ _ ih with ⟨a'', g, g', h₀, h₁, h₂⟩
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
h :
  ∀ (x y : P.M),
    R x y →
      ∃ (a : P.A) (f : P.B a → P.M) (f' : P.B a → P.M),
        x.dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f ∧
          y.dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧ ∀ (i : P.B a), R (f i) (f' i)
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih :
  R (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f)) (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f'))
i : P.B a
⊢ R (f i) (f' i)
have tail : ∀ (a'' : P.A) (g g' : P.B a'' → P.M)
  (h₀ :
    (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f)).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g)
  (h₁ :
    (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f')).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g')
  (h₂ : ∀ (i : P.B a''), R (g i) (g' i)), R (f i) (f' i)
Tactic: rcases h _ _ ih with ⟨a'', g, g', h₀, h₁, h₂⟩