awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFunctor.Univariate.M
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₂
H : ∀ (ps : Path F), iselect ps s₁ = iselect ps s₂
⊢ s₁ = s₂

Tactic:
apply ext

Premises used: PFunctor.M.ext
-- Module: Mathlib.Data.PFunctor.Univariate.M
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₂
neg : ∀ (h : ¬(IsPath ps s₁ ∨ IsPath ps s₂)), iselect ps s₁ = iselect ps s₂
⊢ iselect ps s₁ = iselect ps s₂

Tactic:
by_cases h : IsPath ps s₁ ∨ IsPath ps s₂

Premises used: PFunctor.M.IsPath
-- Module: Mathlib.Data.PFunctor.Univariate.M
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₂ ∧
    ∃ (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
-- Module: Mathlib.Data.PFunctor.Univariate.M
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 :
  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)
⊢ iselect ps s₁ = iselect ps s₂

Tactic:
H.left

Premises used: And.left
-- Module: Mathlib.Data.PFunctor.Univariate.M
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 :
  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)
⊢ iselect ps s₁ = iselect ps s₂

Tactic:
exact H.left

Premises used: And.left
-- Module: Mathlib.Data.PFunctor.Univariate.M
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₂)
⊢ ¬IsPath ps s₁ ∧ ¬IsPath ps s₂

Tactic:
rw [not_or] at h

Premises used: not_or
-- Module: Mathlib.Data.PFunctor.Univariate.M
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₂
⊢ ¬IsPath ps s₁

Tactic:
obtain ⟨h₀, h₁⟩ := h
-- Module: Mathlib.Data.PFunctor.Univariate.M
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₁
⊢ ¬IsPath ps s₂

Tactic:
obtain ⟨h₀, h₁⟩ := h
-- Module: Mathlib.Data.PFunctor.Univariate.M
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₁
h₁ : ¬IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂

Tactic:
simp only [iselect_eq_default, *, not_false_iff]

Premises used: PFunctor.M.iselect_eq_default, not_false_iff
-- Module: Mathlib.Data.PFunctor.Univariate.M
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₂
neg 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₂
⊢ ∀ (s₁ s₂ : F.M), R s₁ s₂ → s₁ = 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]

Premises used: not_or, not_false_iff
-- Module: Mathlib.Data.PFunctor.Univariate.M
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)
rw₁ rw₂ : P.map (M.corec g) (g x) = P.map (M.corec g) (g x)
⊢ (M.corec g x).dest = P.map (M.corec g) (g x)

Tactic:
rw [corec_def, dest_mk]

Premises used: PFunctor.M.dest_mk, PFunctor.M.corec_def
-- Module: Mathlib.Data.PFunctor.Univariate.M
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
haveI : ∀ (this : Inhabited P.A), x = y
⊢ x = y

Tactic:
haveI := Inhabited.mk x.head
-- Module: Mathlib.Data.PFunctor.Univariate.M
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
apply : IsBisimulation R
⊢ x = y

Tactic:
apply eq_of_bisim R _ _ _ h'

Premises used: PFunctor.M.eq_of_bisim
-- Module: Mathlib.Data.PFunctor.Univariate.M
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'
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)
⊢ IsBisimulation R

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.M
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'))
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'
⊢ a = a'

Tactic:
rcases h _ _ ih with ⟨a'', g, g', h₀, h₁, h₂⟩
-- Module: Mathlib.Data.PFunctor.Univariate.M
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
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)
⊢ R (f i) (f' i)

Tactic:
rcases h _ _ ih with ⟨a'', g, g', h₀, h₁, h₂⟩
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
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'' : 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)
⊢ (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f)).dest.fst (β := fun (x : P.A) ↦ P.B x → P.M) =
    Sigma.fst (β := fun (x : P.A) ↦ P.B x → P.M) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g)

Tactic:
replace h₀ := congr_arg Sigma.fst h₀
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
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'' : 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₂ : ∀ (i : P.B a''), R (g i) (g' i)
h₀ :
  (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f)).dest.fst (β := fun (x : P.A) ↦ P.B x → P.M) =
    Sigma.fst (β := fun (x : P.A) ↦ P.B x → P.M) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g)
⊢ (M.mk (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a' f')).dest.fst (β := fun (x : P.A) ↦ P.B x → P.M) =
    Sigma.fst (β := fun (x : P.A) ↦ P.B x → P.M) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g')

Tactic:
replace h₁ := congr_arg Sigma.fst h₁
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
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'' : P.A
g g' : P.B a'' → P.M
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
h₀ : a = a''
h₁ : a' = a''
head : a'' = a'
head₁ head₂ : a'' = a''
⊢ a = a'

Tactic:
rw [h₀, h₁]
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
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
a'' : P.A
g g' : P.B a'' → P.M
h₀ :
  Eq (α := (↑P : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) P.M)
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g)
h₁ :
  Eq (α := (↑P : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) P.M)
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f') (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a'' g')
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
tail :
  ∀ (g' : P.B a → P.M)
    (h₁ :
      Eq (α := (↑P : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) P.M)
        (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f') (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a g'))
    (h₂ : ∀ (i : P.B a), R (f i) (g' i)), R (f i) (f' i)
⊢ R (f i) (f' i)

Tactic:
cases h₀
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
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
g' : P.B a → P.M
h₁ :
  Eq (α := (↑P : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) P.M)
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f') (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a g')
h₂ : ∀ (i : P.B a), R (f i) (g' i)
⊢ ∀ (i : P.B a), R (f i) (f' i)

Tactic:
cases h₁
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
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
h₂ : ∀ (i : P.B a), R (f i) (f' i)
⊢ R (f i) (f' i)

Tactic:
apply h₂
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
α : Type u_3
Q : α → Prop
u v : α → P.M
h :
  ∀ (x : α),
    Q x →
      ∃ (a : P.A) (f : P.B a → P.M) (f' : P.B a → P.M),
        (u x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f ∧
          (v x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧
            ∀ (i : P.B a), ∃ (x' : α), Q x' ∧ f i = u x' ∧ f' i = v x'
⊢ ∀ (x : α), Q x → u x = v x

Tactic:
fun x Qx =>
  let R := fun w z : M P => ∃ x', Q x' ∧ w = u x' ∧ z = v x'
  @M.bisim P R
    (fun _ _ ⟨x', Qx', xeq, yeq⟩ =>
      let ⟨a, f, f', ux'eq, vx'eq, h'⟩ := h x' Qx'
      ⟨a, f, f', xeq.symm ▸ ux'eq, yeq.symm ▸ vx'eq, h'⟩)
    _ _ ⟨x, Qx, rfl, rfl⟩

Premises used: _private.0.PFunctor.M.bisim'.match_1, Exists, Eq.rec, And, And.intro, _private.0.PFunctor.M.bisim'.match_2, Exists.intro, PFunctor.M.dest, Sigma.mk, Eq.symm, Eq, rfl, PFunctor.M.bisim
-- Module: Mathlib.Data.PFunctor.Univariate.M
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), R x y → x = y

Tactic:
fun x y Rxy =>
  let Q : M P × M P → Prop := fun p => R p.fst p.snd
  bisim' Q Prod.fst Prod.snd
    (fun p Qp =>
      let ⟨a, f, f', hx, hy, h'⟩ := h p.fst p.snd Qp
      ⟨a, f, f', hx, hy, fun i => ⟨⟨f i, f' i⟩, h' i, rfl, rfl⟩⟩)
    ⟨x, y⟩ Rxy

Premises used: PFunctor.M.bisim', Exists, Prod.mk, Prod.fst, And, _private.0.PFunctor.M.bisim_equiv.match_1, And.intro, Exists.intro, PFunctor.M.dest, Sigma.mk, Eq, Prod.snd, rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
h : ∀ (x : α), f x = M.corec g x
⊢ f = M.corec g

Tactic:
ext x
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
apply :
  ∀ (x : α),
    (fun (x : α) ↦ True) x →
      ∃ (a : P.A) (f_1 : P.B a → P.M) (f' : P.B a → P.M),
        (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f_1 ∧
          (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧
            ∀ (i : P.B a), ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
⊢ f x = M.corec g x

Tactic:
apply bisim' (fun _ => True) _ _ _ _ trivial

Premises used: trivial, PFunctor.M.bisim', True
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
_ :
  True →
    ∃ (a : P.A) (f_1 : P.B a → P.M) (f' : P.B a → P.M),
      (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f_1 ∧
        (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧
          ∀ (i : P.B a), ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
⊢ (fun (x : α) ↦ True) x →
    ∃ (a : P.A) (f_1 : P.B a → P.M) (f' : P.B a → P.M),
      (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f_1 ∧
        (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧
          ∀ (i : P.B a), ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Tactic:
_
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
rcases :
  ∀ (a : P.A) (f' : P.B a → α) (gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'),
    ∃ (a : P.A) (f_1 : P.B a → P.M) (f' : P.B a → P.M),
      (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f_1 ∧
        (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧
          ∀ (i : P.B a), ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
⊢ ∃ (a : P.A) (f_1 : P.B a → P.M) (f' : P.B a → P.M),
    (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f_1 ∧
      (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧
        ∀ (i : P.B a), ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Tactic:
rcases gxeq : g x with ⟨a, f'⟩
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
rw : P.map f (g x) = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
rw₁ : P.map f (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f') = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
rw₂ rw₃ :
  Eq (α := (↑P : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) P.M)
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f'))
⊢ (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')

Tactic:
rw [hyp, gxeq, PFunctor.map_eq]

Premises used: PFunctor.map_eq
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
⊢ (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')

Tactic:
have h₀ : M.dest (f x) = ⟨a, f ∘ f'⟩ := by rw [hyp, gxeq, PFunctor.map_eq]
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
h₀ : (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
rw : P.map (M.corec g) (g x) = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')
rw₁ :
  P.map (M.corec g) (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f') =
    Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')
rw₂ rw₃ :
  Eq (α := (↑P : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) P.M)
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f'))
    (Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f'))
⊢ (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')

Tactic:
rw [dest_corec, gxeq, PFunctor.map_eq]

Premises used: PFunctor.M.dest_corec, PFunctor.map_eq
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
h₀ : (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
⊢ (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')

Tactic:
have h₁ : M.dest (M.corec g x) = ⟨a, M.corec g ∘ f'⟩ := by rw [dest_corec, gxeq, PFunctor.map_eq]
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
h₀ : (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
h₁ : (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')
⊢ ∃ (a : P.A) (f_1 : P.B a → P.M) (f' : P.B a → P.M),
    (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f_1 ∧
      (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧
        ∀ (i : P.B a), ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Tactic:
⟨_, _, _, h₀, h₁, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
h₀ : (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
h₁ : (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')
refine : ∀ (i : P.B a), ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'
⊢ ∃ (a : P.A) (f_1 : P.B a → P.M) (f' : P.B a → P.M),
    (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f_1 ∧
      (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a f' ∧
        ∀ (i : P.B a), ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Tactic:
refine ⟨_, _, _, h₀, h₁, ?_⟩
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
h₀ : (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
h₁ : (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')
i : P.B a
⊢ ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'

Tactic:
⟨f' i, trivial, rfl, rfl⟩

Premises used: trivial, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → (↑P : (α : Type u_2) → Type (max u_2 uA uB)) α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
h : True
a : P.A
f' : P.B a → α
gxeq : g x = Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f'
h₀ : (f x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (f ∘ f')
h₁ : (M.corec g x).dest = Sigma.mk (β := fun (x : P.A) ↦ P.B x → P.M) a (M.corec g ∘ f')
i : P.B a
⊢ ∃ (x' : α), (fun (x : α) ↦ True) x' ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'

Tactic:
exact ⟨f' i, trivial, rfl, rfl⟩
-- Module: Mathlib.Data.PNat.Basic
Goal:
n : ℕ+
rw : 1 + ((↑n : ℕ) - 1) = (↑n : ℕ)
rw₁ rw₂ : (↑n : ℕ) = (↑n : ℕ)
⊢ 1 + n.natPred = (↑n : ℕ)

Tactic:
rw [natPred, add_tsub_cancel_iff_le.mpr <| show 1 ≤ (n : ℕ) from n.2]

Premises used: Iff.mpr, add_tsub_cancel_iff_le, PNat.natPred, Subtype.property
-- Module: Mathlib.Data.PNat.Basic
Goal:
n : ℕ+
⊢ n.natPred + 1 = (↑n : ℕ)

Tactic:
(add_comm _ _).trans n.one_add_natPred

Premises used: add_comm, PNat.one_add_natPred, Eq.trans
-- Module: Mathlib.Data.PNat.Basic
Goal:
⊢ StrictMono natPred

Tactic:
fun m _ h => Nat.pred_lt_pred m.2.ne' h

Premises used: StrictMono, LT.lt.ne', PNat.natPred, Nat.pred_lt_pred, Nat.pred, Subtype.property
-- Module: Mathlib.Data.PNat.Basic
Goal:
⊢ Monotone natPred

Tactic:
natPred_strictMono.monotone

Premises used: StrictMono.monotone, PNat.natPred_strictMono