[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
x : PFunctor.M (last P)
i : Fin2 n
inst✝ : Inhabited (B (drop P) (PFunctor.M.head x) i)
a : (last P).A := PFunctor.M.head x
f : PFunctor.B (last P) (PFunctor.M.head x) → PFunctor.M (last P) := PFunctor.M.children x
⊢ ∀ (a_1 : (last P).A) (f_1 : PFunctor.B (last P) a_1 → PFunctor.M (last P)),
    (fun x_1 => PFunctor.M.dest x = { fst := a, snd := f }) (PFunctor.M.mk { fst := a_1, snd := f_1 })
[PROOFSTEP]
intros
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
x : PFunctor.M (last P)
i : Fin2 n
inst✝ : Inhabited (B (drop P) (PFunctor.M.head x) i)
a : (last P).A := PFunctor.M.head x
f : PFunctor.B (last P) (PFunctor.M.head x) → PFunctor.M (last P) := PFunctor.M.children x
a✝ : (last P).A
f✝ : PFunctor.B (last P) a✝ → PFunctor.M (last P)
⊢ PFunctor.M.dest x = { fst := a, snd := f }
[PROOFSTEP]
simp [PFunctor.M.dest_mk, PFunctor.M.children_mk]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
x : PFunctor.M (last P)
i : Fin2 n
inst✝ : Inhabited (B (drop P) (PFunctor.M.head x) i)
a : (last P).A := PFunctor.M.head x
f : PFunctor.B (last P) (PFunctor.M.head x) → PFunctor.M (last P) := PFunctor.M.children x
a✝ : (last P).A
f✝ : PFunctor.B (last P) a✝ → PFunctor.M (last P)
⊢ PFunctor.M.dest x = { fst := PFunctor.M.head x, snd := PFunctor.M.children x }
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
⊢ MvFunctor (M P)
[PROOFSTEP]
delta M
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
⊢ MvFunctor fun α => Obj (mp P) α
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
c : B (drop P) a i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
[PROOFSTEP]
rw [h, M.corecShape, PFunctor.M.dest_corec] at h'
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : (PFunctor.M.corec fun b => { fst := g₀ b, snd := g₂ b }) <$> { fst := g₀ b, snd := g₂ b } = { fst := a, snd := f }
c : B (drop P) a i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
[PROOFSTEP]
cases h'
[GOAL]
case refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
h : x = corecShape P g₀ g₂ b
c : B (drop P) (g₀ b) i
⊢ g₀ b = g₀ b
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
j : PFunctor.B (last P) a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
[PROOFSTEP]
rw [h, M.corecShape, PFunctor.M.dest_corec] at h'
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : (PFunctor.M.corec fun b => { fst := g₀ b, snd := g₂ b }) <$> { fst := g₀ b, snd := g₂ b } = { fst := a, snd := f }
j : PFunctor.B (last P) a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
⊢ a = g₀ b
[PROOFSTEP]
cases h'
[GOAL]
case refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
h : x = corecShape P g₀ g₂ b
j : PFunctor.B (last P) (g₀ b)
c : Path P (((PFunctor.M.corec fun b => { fst := g₀ b, snd := g₂ b }) ∘ g₂ b) j) i
⊢ g₀ b = g₀ b
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
j : PFunctor.B (last P) a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
h₀ : a = g₀ b
⊢ f j = corecShape P g₀ g₂ (g₂ b (castLastB P h₀ j))
[PROOFSTEP]
rw [h, M.corecShape, PFunctor.M.dest_corec] at h'
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : (PFunctor.M.corec fun b => { fst := g₀ b, snd := g₂ b }) <$> { fst := g₀ b, snd := g₂ b } = { fst := a, snd := f }
j : PFunctor.B (last P) a
c : Path P (f j) i
h : x = corecShape P g₀ g₂ b
h₀ : a = g₀ b
⊢ f j = corecShape P g₀ g₂ (g₂ b (castLastB P h₀ j))
[PROOFSTEP]
cases h'
[GOAL]
case refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g₀ : β → P.A
g₁ : (b : β) → B (drop P) (g₀ b) ⟹ α
g₂ : (b : β) → PFunctor.B (last P) (g₀ b) → β
x✝ : PFunctor.M (last P)
b : β
x : PFunctor.M (last P)
i : Fin2 n
h : x = corecShape P g₀ g₂ b
j : PFunctor.B (last P) (g₀ b)
h₀ : g₀ b = g₀ b
c : Path P (((PFunctor.M.corec fun b => { fst := g₀ b, snd := g₂ b }) ∘ g₂ b) j) i
⊢ ((PFunctor.M.corec fun b => { fst := g₀ b, snd := g₂ b }) ∘ g₂ b) j = corecShape P g₀ g₂ (g₂ b (castLastB P h₀ j))
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
x : PFunctor.M (last P)
a₁ : P.A
f₁ : PFunctor.B (last P) a₁ → PFunctor.M (last P)
h₁ : PFunctor.M.dest x = { fst := a₁, snd := f₁ }
a₂ : P.A
f₂ : PFunctor.B (last P) a₂ → PFunctor.M (last P)
h₂ : PFunctor.M.dest x = { fst := a₂, snd := f₂ }
f' : Path P x ⟹ α
⊢ dest' P h₁ f' = dest' P h₂ f'
[PROOFSTEP]
cases h₁.symm.trans h₂
[GOAL]
case refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
x : PFunctor.M (last P)
a₁ : P.A
f₁ : PFunctor.B (last P) a₁ → PFunctor.M (last P)
h₁ : PFunctor.M.dest x = { fst := a₁, snd := f₁ }
f' : Path P x ⟹ α
h₂ : PFunctor.M.dest x = { fst := a₁, snd := f₁ }
⊢ dest' P h₁ f' = dest' P h₂ f'
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
⊢ dest P (corec P g x) = (TypeVec.id ::: corec P g) <$$> g x
[PROOFSTEP]
trans
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
⊢ dest P (corec P g x) = ?m.39771
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
⊢ ?m.39771 = (TypeVec.id ::: corec P g) <$$> g x
n : ℕ P : MvPFunctor (n + 1) α : TypeVec n β : Type u g : β → Obj P (α ::: β) x : β ⊢ Obj P (α ::: M P α)
[PROOFSTEP]
apply M.dest_corec'
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
⊢ { fst := (g x).fst,
      snd :=
        splitFun (dropFun (g x).snd)
          ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘
            lastFun (g x).snd) } =
    (TypeVec.id ::: corec P g) <$$> g x
[PROOFSTEP]
cases' g x with a f
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
⊢ { fst := { fst := a, snd := f }.fst,
      snd :=
        splitFun (dropFun { fst := a, snd := f }.snd)
          ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘
            lastFun { fst := a, snd := f }.snd) } =
    (TypeVec.id ::: corec P g) <$$> { fst := a, snd := f }
[PROOFSTEP]
dsimp
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
⊢ { fst := a,
      snd :=
        splitFun (dropFun f)
          ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) } =
    (TypeVec.id ::: corec P g) <$$> { fst := a, snd := f }
[PROOFSTEP]
rw [MvPFunctor.map_eq]
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
⊢ { fst := a,
      snd :=
        splitFun (dropFun f)
          ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) } =
    { fst := a, snd := (TypeVec.id ::: corec P g) ⊚ f }
[PROOFSTEP]
congr
[GOAL]
case mk.e_snd
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
⊢ splitFun (dropFun f)
      ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) =
    (TypeVec.id ::: corec P g) ⊚ f
[PROOFSTEP]
conv =>
  rhs
  rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
| splitFun (dropFun f)
      ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) =
    (TypeVec.id ::: corec P g) ⊚ f
[PROOFSTEP]
  rhs
  rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
| splitFun (dropFun f)
      ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) =
    (TypeVec.id ::: corec P g) ⊚ f
[PROOFSTEP]
  rhs
  rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
| splitFun (dropFun f)
      ((corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd) ∘ lastFun f) =
    (TypeVec.id ::: corec P g) ⊚ f
[PROOFSTEP]
rhs
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
β : Type u
g : β → Obj P (α ::: β)
x : β
a : P.A
f : B P a ⟹ α ::: β
| (TypeVec.id ::: corec P g) ⊚ f
[PROOFSTEP]
rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a' : P.A
f' : TypeVec.drop (B P a') ⟹ α
f₁' : TypeVec.last (B P a') → M P α
e₁ : dest P { fst := a₁, snd := f₁ } = { fst := a', snd := splitFun f' f₁' }
⊢ ∃ g₁' e₁', f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }
[PROOFSTEP]
generalize ef : @splitFun n _ (append1 α (M P α)) f' f₁' = ff at e₁
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a' : P.A
f' : TypeVec.drop (B P a') ⟹ α
f₁' : TypeVec.last (B P a') → M P α
ff : B P a' ⟹ α ::: M P α
ef : splitFun f' f₁' = ff
e₁ : dest P { fst := a₁, snd := f₁ } = { fst := a', snd := ff }
⊢ ∃ g₁' e₁', f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }
[PROOFSTEP]
let he₁' := PFunctor.M.dest a₁
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a' : P.A
f' : TypeVec.drop (B P a') ⟹ α
f₁' : TypeVec.last (B P a') → M P α
ff : B P a' ⟹ α ::: M P α
ef : splitFun f' f₁' = ff
e₁ : dest P { fst := a₁, snd := f₁ } = { fst := a', snd := ff }
he₁' : PFunctor.Obj (last P) (PFunctor.M (last P)) := PFunctor.M.dest a₁
⊢ ∃ g₁' e₁', f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }
[PROOFSTEP]
rcases e₁' : he₁' with ⟨a₁', g₁'⟩
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a' : P.A
f' : TypeVec.drop (B P a') ⟹ α
f₁' : TypeVec.last (B P a') → M P α
ff : B P a' ⟹ α ::: M P α
ef : splitFun f' f₁' = ff
e₁ : dest P { fst := a₁, snd := f₁ } = { fst := a', snd := ff }
he₁' : PFunctor.Obj (last P) (PFunctor.M (last P)) := PFunctor.M.dest a₁
a₁' : (last P).A
g₁' : PFunctor.B (last P) a₁' → PFunctor.M (last P)
e₁' : he₁' = { fst := a₁', snd := g₁' }
⊢ ∃ g₁' e₁', f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }
[PROOFSTEP]
rw [M.dest_eq_dest' _ e₁'] at e₁
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a' : P.A
f' : TypeVec.drop (B P a') ⟹ α
f₁' : TypeVec.last (B P a') → M P α
ff : B P a' ⟹ α ::: M P α
ef : splitFun f' f₁' = ff
he₁' : PFunctor.Obj (last P) (PFunctor.M (last P)) := PFunctor.M.dest a₁
a₁' : (last P).A
g₁' : PFunctor.B (last P) a₁' → PFunctor.M (last P)
e₁' : he₁' = { fst := a₁', snd := g₁' }
e₁ : dest' P e₁' f₁ = { fst := a', snd := ff }
⊢ ∃ g₁' e₁', f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }
[PROOFSTEP]
cases e₁
[GOAL]
case mk.refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a' : P.A
f' : TypeVec.drop (B P a') ⟹ α
f₁' : TypeVec.last (B P a') → M P α
he₁' : PFunctor.Obj (last P) (PFunctor.M (last P)) := PFunctor.M.dest a₁
g₁' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₁' : he₁' = { fst := a', snd := g₁' }
ef : splitFun f' f₁' = splitFun (pathDestLeft P e₁' f₁) fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }
⊢ ∃ g₁' e₁', f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }
[PROOFSTEP]
exact ⟨_, e₁', splitFun_inj ef⟩
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
x y : M P α
r : R x y
⊢ x = y
[PROOFSTEP]
cases' x with a₁ f₁
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
y : M P α
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
r : R { fst := a₁, snd := f₁ } y
⊢ { fst := a₁, snd := f₁ } = y
[PROOFSTEP]
cases' y with a₂ f₂
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
⊢ { fst := a₁, snd := f₁ } = { fst := a₂, snd := f₂ }
[PROOFSTEP]
dsimp [mp] at *
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
⊢ { fst := a₁, snd := f₁ } = { fst := a₂, snd := f₂ }
[PROOFSTEP]
have : a₁ = a₂ :=
  by
  refine' PFunctor.M.bisim (fun a₁ a₂ => ∃ x y, R x y ∧ x.1 = a₁ ∧ y.1 = a₂) _ _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
  rintro _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
  rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h'⟩
  rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
  rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', _, rfl⟩
  rw [e₁', e₂']
  exact ⟨_, _, _, rfl, rfl, fun b => ⟨_, _, h' b, rfl, rfl⟩⟩
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
⊢ a₁ = a₂
[PROOFSTEP]
refine' PFunctor.M.bisim (fun a₁ a₂ => ∃ x y, R x y ∧ x.1 = a₁ ∧ y.1 = a₂) _ _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
⊢ ∀ (x y : PFunctor.M (last P)),
    (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) x y →
      ∃ a f f',
        PFunctor.M.dest x = { fst := a, snd := f } ∧
          PFunctor.M.dest y = { fst := a, snd := f' } ∧
            ∀ (i : PFunctor.B (last P) a), (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) (f i) (f' i)
[PROOFSTEP]
rintro _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
[GOAL]
case intro.mk.intro.mk.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁✝ : (mp P).A
f₁✝ : B (mp P) a₁✝ ⟹ α
a₂✝ : (mp P).A
f₂✝ : B (mp P) a₂✝ ⟹ α
r✝ : R { fst := a₁✝, snd := f₁✝ } { fst := a₂✝, snd := f₂✝ }
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
⊢ ∃ a f f',
    PFunctor.M.dest { fst := a₁, snd := f₁ }.fst = { fst := a, snd := f } ∧
      PFunctor.M.dest { fst := a₂, snd := f₂ }.fst = { fst := a, snd := f' } ∧
        ∀ (i : PFunctor.B (last P) a), (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) (f i) (f' i)
[PROOFSTEP]
rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h'⟩
[GOAL]
case intro.mk.intro.mk.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁✝ : (mp P).A
f₁✝ : B (mp P) a₁✝ ⟹ α
a₂✝ : (mp P).A
f₂✝ : B (mp P) a₂✝ ⟹ α
r✝ : R { fst := a₁✝, snd := f₁✝ } { fst := a₂✝, snd := f₂✝ }
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
a' : P.A
f' : TypeVec.drop (B P a') ⟹ TypeVec.drop (α ::: M P α)
f₁' f₂' : TypeVec.last (B P a') → TypeVec.last (α ::: M P α)
e₁ : dest P { fst := a₁, snd := f₁ } = { fst := a', snd := splitFun f' f₁' }
e₂ : dest P { fst := a₂, snd := f₂ } = { fst := a', snd := splitFun f' f₂' }
h' : ∀ (i : TypeVec.last (B P a')), R (f₁' i) (f₂' i)
⊢ ∃ a f f',
    PFunctor.M.dest { fst := a₁, snd := f₁ }.fst = { fst := a, snd := f } ∧
      PFunctor.M.dest { fst := a₂, snd := f₂ }.fst = { fst := a, snd := f' } ∧
        ∀ (i : PFunctor.B (last P) a), (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) (f i) (f' i)
[PROOFSTEP]
rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
[GOAL]
case intro.mk.intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁✝ : (mp P).A
f₁✝ : B (mp P) a₁✝ ⟹ α
a₂✝ : (mp P).A
f₂✝ : B (mp P) a₂✝ ⟹ α
r✝ : R { fst := a₁✝, snd := f₁✝ } { fst := a₂✝, snd := f₂✝ }
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
a' : P.A
f₂' : TypeVec.last (B P a') → TypeVec.last (α ::: M P α)
g₁' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₁' : PFunctor.M.dest a₁ = { fst := a', snd := g₁' }
e₂ : dest P { fst := a₂, snd := f₂ } = { fst := a', snd := splitFun (pathDestLeft P e₁' f₁) f₂' }
h' : ∀ (i : TypeVec.last (B P a')), R ((fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }) i) (f₂' i)
e₁ :
  dest P { fst := a₁, snd := f₁ } =
    { fst := a', snd := splitFun (pathDestLeft P e₁' f₁) fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x } }
⊢ ∃ a f f',
    PFunctor.M.dest { fst := a₁, snd := f₁ }.fst = { fst := a, snd := f } ∧
      PFunctor.M.dest { fst := a₂, snd := f₂ }.fst = { fst := a, snd := f' } ∧
        ∀ (i : PFunctor.B (last P) a), (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) (f i) (f' i)
[PROOFSTEP]
rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', _, rfl⟩
[GOAL]
case intro.mk.intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁✝ : (mp P).A
f₁✝ : B (mp P) a₁✝ ⟹ α
a₂✝ : (mp P).A
f₂✝ : B (mp P) a₂✝ ⟹ α
r✝ : R { fst := a₁✝, snd := f₁✝ } { fst := a₂✝, snd := f₂✝ }
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
a' : P.A
g₁' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₁' : PFunctor.M.dest a₁ = { fst := a', snd := g₁' }
e₁ :
  dest P { fst := a₁, snd := f₁ } =
    { fst := a', snd := splitFun (pathDestLeft P e₁' f₁) fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x } }
g₂' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₂' : PFunctor.M.dest a₂ = { fst := a', snd := g₂' }
left✝ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ :
  dest P { fst := a₂, snd := f₂ } =
    { fst := a', snd := splitFun (pathDestLeft P e₁' f₁) fun x => { fst := g₂' x, snd := pathDestRight P e₂' f₂ x } }
h' :
  ∀ (i : TypeVec.last (B P a')),
    R ((fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }) i)
      ((fun x => { fst := g₂' x, snd := pathDestRight P e₂' f₂ x }) i)
⊢ ∃ a f f',
    PFunctor.M.dest { fst := a₁, snd := f₁ }.fst = { fst := a, snd := f } ∧
      PFunctor.M.dest { fst := a₂, snd := f₂ }.fst = { fst := a, snd := f' } ∧
        ∀ (i : PFunctor.B (last P) a), (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) (f i) (f' i)
[PROOFSTEP]
rw [e₁', e₂']
[GOAL]
case intro.mk.intro.mk.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁✝ : (mp P).A
f₁✝ : B (mp P) a₁✝ ⟹ α
a₂✝ : (mp P).A
f₂✝ : B (mp P) a₂✝ ⟹ α
r✝ : R { fst := a₁✝, snd := f₁✝ } { fst := a₂✝, snd := f₂✝ }
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
a' : P.A
g₁' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₁' : PFunctor.M.dest a₁ = { fst := a', snd := g₁' }
e₁ :
  dest P { fst := a₁, snd := f₁ } =
    { fst := a', snd := splitFun (pathDestLeft P e₁' f₁) fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x } }
g₂' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₂' : PFunctor.M.dest a₂ = { fst := a', snd := g₂' }
left✝ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ :
  dest P { fst := a₂, snd := f₂ } =
    { fst := a', snd := splitFun (pathDestLeft P e₁' f₁) fun x => { fst := g₂' x, snd := pathDestRight P e₂' f₂ x } }
h' :
  ∀ (i : TypeVec.last (B P a')),
    R ((fun x => { fst := g₁' x, snd := pathDestRight P e₁' f₁ x }) i)
      ((fun x => { fst := g₂' x, snd := pathDestRight P e₂' f₂ x }) i)
⊢ ∃ a f f',
    { fst := a', snd := g₁' } = { fst := a, snd := f } ∧
      { fst := a', snd := g₂' } = { fst := a, snd := f' } ∧
        ∀ (i : PFunctor.B (last P) a), (fun a₁ a₂ => ∃ x y, R x y ∧ x.fst = a₁ ∧ y.fst = a₂) (f i) (f' i)
[PROOFSTEP]
exact ⟨_, _, _, rfl, rfl, fun b => ⟨_, _, h' b, rfl, rfl⟩⟩
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁ : B (mp P) a₁ ⟹ α
a₂ : (mp P).A
f₂ : B (mp P) a₂ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₂, snd := f₂ }
this : a₁ = a₂
⊢ { fst := a₁, snd := f₁ } = { fst := a₂, snd := f₂ }
[PROOFSTEP]
subst this
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁ f₂ : B (mp P) a₁ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₁, snd := f₂ }
⊢ { fst := a₁, snd := f₁ } = { fst := a₁, snd := f₂ }
[PROOFSTEP]
congr with (i p)
[GOAL]
case mk.mk.e_snd.a.h
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁ f₂ : B (mp P) a₁ ⟹ α
r : R { fst := a₁, snd := f₁ } { fst := a₁, snd := f₂ }
i : Fin2 n
p : B (mp P) a₁ i
⊢ f₁ i p = f₂ i p
[PROOFSTEP]
induction' p with x a f h' i c x a f h' i c p IH
[GOAL]
case mk.mk.e_snd.a.h.root
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : Fin2 n
c : B (drop P) a i
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
[PROOFSTEP]
try
  rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h''⟩
  rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
  rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', e₃, rfl⟩
  cases h'.symm.trans e₁'
  cases h'.symm.trans e₂'
[GOAL]
case mk.mk.e_snd.a.h.root
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : Fin2 n
c : B (drop P) a i
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
[PROOFSTEP]
rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h''⟩
[GOAL]
case mk.mk.e_snd.a.h.root.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : Fin2 n
c : B (drop P) a i
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
a' : P.A
f' : TypeVec.drop (B P a') ⟹ TypeVec.drop (α ::: M P α)
f₁' f₂' : TypeVec.last (B P a') → TypeVec.last (α ::: M P α)
e₁ : dest P { fst := x, snd := f₁ } = { fst := a', snd := splitFun f' f₁' }
e₂ : dest P { fst := x, snd := f₂ } = { fst := a', snd := splitFun f' f₂' }
h'' : ∀ (i : TypeVec.last (B P a')), R (f₁' i) (f₂' i)
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
[PROOFSTEP]
rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
[GOAL]
case mk.mk.e_snd.a.h.root.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : Fin2 n
c : B (drop P) a i
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
a' : P.A
f₂' : TypeVec.last (B P a') → TypeVec.last (α ::: M P α)
g₁' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₁' : PFunctor.M.dest x = { fst := a', snd := g₁' }
e₂ : dest P { fst := x, snd := f₂ } = { fst := a', snd := splitFun (pathDestLeft P e₁' f₁) f₂' }
h'' : ∀ (i : TypeVec.last (B P a')), R ((fun x_1 => { fst := g₁' x_1, snd := pathDestRight P e₁' f₁ x_1 }) i) (f₂' i)
e₁ :
  dest P { fst := x, snd := f₁ } =
    { fst := a',
      snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := g₁' x_1, snd := pathDestRight P e₁' f₁ x_1 } }
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
[PROOFSTEP]
rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', e₃, rfl⟩
[GOAL]
case mk.mk.e_snd.a.h.root.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : Fin2 n
c : B (drop P) a i
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
a' : P.A
g₁' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₁' : PFunctor.M.dest x = { fst := a', snd := g₁' }
e₁ :
  dest P { fst := x, snd := f₁ } =
    { fst := a',
      snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := g₁' x_1, snd := pathDestRight P e₁' f₁ x_1 } }
g₂' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₂' : PFunctor.M.dest x = { fst := a', snd := g₂' }
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ :
  dest P { fst := x, snd := f₂ } =
    { fst := a',
      snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := g₂' x_1, snd := pathDestRight P e₂' f₂ x_1 } }
h'' :
  ∀ (i : TypeVec.last (B P a')),
    R ((fun x_1 => { fst := g₁' x_1, snd := pathDestRight P e₁' f₁ x_1 }) i)
      ((fun x_1 => { fst := g₂' x_1, snd := pathDestRight P e₂' f₂ x_1 }) i)
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
[PROOFSTEP]
cases h'.symm.trans e₁'
[GOAL]
case mk.mk.e_snd.a.h.root.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : Fin2 n
c : B (drop P) a i
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
g₂' : PFunctor.B (last P) a → PFunctor.M (last P)
e₂' : PFunctor.M.dest x = { fst := a, snd := g₂' }
e₁' : PFunctor.M.dest x = { fst := a, snd := f }
e₁ :
  dest P { fst := x, snd := f₁ } =
    { fst := a, snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := f x_1, snd := pathDestRight P e₁' f₁ x_1 } }
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ :
  dest P { fst := x, snd := f₂ } =
    { fst := a,
      snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := g₂' x_1, snd := pathDestRight P e₂' f₂ x_1 } }
h'' :
  ∀ (i : TypeVec.last (B P a)),
    R ((fun x_1 => { fst := f x_1, snd := pathDestRight P e₁' f₁ x_1 }) i)
      ((fun x_1 => { fst := g₂' x_1, snd := pathDestRight P e₂' f₂ x_1 }) i)
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
[PROOFSTEP]
cases h'.symm.trans e₂'
[GOAL]
case mk.mk.e_snd.a.h.child
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : PFunctor.B (last P) a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : B (mp P) (f i) ⟹ α), R { fst := f i, snd := f₁ } { fst := f i, snd := f₂ } → f₁ c p = f₂ c p
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
[PROOFSTEP]
try
  rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h''⟩
  rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
  rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', e₃, rfl⟩
  cases h'.symm.trans e₁'
  cases h'.symm.trans e₂'
[GOAL]
case mk.mk.e_snd.a.h.child
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : PFunctor.B (last P) a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : B (mp P) (f i) ⟹ α), R { fst := f i, snd := f₁ } { fst := f i, snd := f₂ } → f₁ c p = f₂ c p
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
[PROOFSTEP]
rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h''⟩
[GOAL]
case mk.mk.e_snd.a.h.child.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : PFunctor.B (last P) a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : B (mp P) (f i) ⟹ α), R { fst := f i, snd := f₁ } { fst := f i, snd := f₂ } → f₁ c p = f₂ c p
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
a' : P.A
f' : TypeVec.drop (B P a') ⟹ TypeVec.drop (α ::: M P α)
f₁' f₂' : TypeVec.last (B P a') → TypeVec.last (α ::: M P α)
e₁ : dest P { fst := x, snd := f₁ } = { fst := a', snd := splitFun f' f₁' }
e₂ : dest P { fst := x, snd := f₂ } = { fst := a', snd := splitFun f' f₂' }
h'' : ∀ (i : TypeVec.last (B P a')), R (f₁' i) (f₂' i)
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
[PROOFSTEP]
rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
[GOAL]
case mk.mk.e_snd.a.h.child.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : PFunctor.B (last P) a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : B (mp P) (f i) ⟹ α), R { fst := f i, snd := f₁ } { fst := f i, snd := f₂ } → f₁ c p = f₂ c p
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
a' : P.A
f₂' : TypeVec.last (B P a') → TypeVec.last (α ::: M P α)
g₁' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₁' : PFunctor.M.dest x = { fst := a', snd := g₁' }
e₂ : dest P { fst := x, snd := f₂ } = { fst := a', snd := splitFun (pathDestLeft P e₁' f₁) f₂' }
h'' : ∀ (i : TypeVec.last (B P a')), R ((fun x_1 => { fst := g₁' x_1, snd := pathDestRight P e₁' f₁ x_1 }) i) (f₂' i)
e₁ :
  dest P { fst := x, snd := f₁ } =
    { fst := a',
      snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := g₁' x_1, snd := pathDestRight P e₁' f₁ x_1 } }
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
[PROOFSTEP]
rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', e₃, rfl⟩
[GOAL]
case mk.mk.e_snd.a.h.child.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : PFunctor.B (last P) a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : B (mp P) (f i) ⟹ α), R { fst := f i, snd := f₁ } { fst := f i, snd := f₂ } → f₁ c p = f₂ c p
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
a' : P.A
g₁' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₁' : PFunctor.M.dest x = { fst := a', snd := g₁' }
e₁ :
  dest P { fst := x, snd := f₁ } =
    { fst := a',
      snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := g₁' x_1, snd := pathDestRight P e₁' f₁ x_1 } }
g₂' : PFunctor.B (last P) a' → PFunctor.M (last P)
e₂' : PFunctor.M.dest x = { fst := a', snd := g₂' }
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ :
  dest P { fst := x, snd := f₂ } =
    { fst := a',
      snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := g₂' x_1, snd := pathDestRight P e₂' f₂ x_1 } }
h'' :
  ∀ (i : TypeVec.last (B P a')),
    R ((fun x_1 => { fst := g₁' x_1, snd := pathDestRight P e₁' f₁ x_1 }) i)
      ((fun x_1 => { fst := g₂' x_1, snd := pathDestRight P e₂' f₂ x_1 }) i)
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
[PROOFSTEP]
cases h'.symm.trans e₁'
[GOAL]
case mk.mk.e_snd.a.h.child.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : PFunctor.B (last P) a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : B (mp P) (f i) ⟹ α), R { fst := f i, snd := f₁ } { fst := f i, snd := f₂ } → f₁ c p = f₂ c p
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
g₂' : PFunctor.B (last P) a → PFunctor.M (last P)
e₂' : PFunctor.M.dest x = { fst := a, snd := g₂' }
e₁' : PFunctor.M.dest x = { fst := a, snd := f }
e₁ :
  dest P { fst := x, snd := f₁ } =
    { fst := a, snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := f x_1, snd := pathDestRight P e₁' f₁ x_1 } }
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ :
  dest P { fst := x, snd := f₂ } =
    { fst := a,
      snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := g₂' x_1, snd := pathDestRight P e₂' f₂ x_1 } }
h'' :
  ∀ (i : TypeVec.last (B P a)),
    R ((fun x_1 => { fst := f x_1, snd := pathDestRight P e₁' f₁ x_1 }) i)
      ((fun x_1 => { fst := g₂' x_1, snd := pathDestRight P e₂' f₂ x_1 }) i)
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
[PROOFSTEP]
cases h'.symm.trans e₂'
[GOAL]
case mk.mk.e_snd.a.h.root.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refl.refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : Fin2 n
c : B (drop P) a i
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
e₁' : PFunctor.M.dest x = { fst := a, snd := f }
e₁ :
  dest P { fst := x, snd := f₁ } =
    { fst := a, snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := f x_1, snd := pathDestRight P e₁' f₁ x_1 } }
e₂' : PFunctor.M.dest x = { fst := a, snd := f }
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ :
  dest P { fst := x, snd := f₂ } =
    { fst := a, snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := f x_1, snd := pathDestRight P e₂' f₂ x_1 } }
h'' :
  ∀ (i : TypeVec.last (B P a)),
    R ((fun x_1 => { fst := f x_1, snd := pathDestRight P e₁' f₁ x_1 }) i)
      ((fun x_1 => { fst := f x_1, snd := pathDestRight P e₂' f₂ x_1 }) i)
⊢ f₁ i (Path.root x a f h' i c) = f₂ i (Path.root x a f h' i c)
[PROOFSTEP]
exact (congr_fun (congr_fun e₃ i) c : _)
[GOAL]
case mk.mk.e_snd.a.h.child.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refl.refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h :
  ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
a₁ : (mp P).A
f₁✝ f₂✝ : B (mp P) a₁ ⟹ α
r✝ : R { fst := a₁, snd := f₁✝ } { fst := a₁, snd := f₂✝ }
i✝ : Fin2 n
x : PFunctor.M (last P)
a : P.A
f : PFunctor.B (last P) a → PFunctor.M (last P)
h' : PFunctor.M.dest x = { fst := a, snd := f }
i : PFunctor.B (last P) a
c : Fin2 n
p : Path P (f i) c
IH : ∀ (f₁ f₂ : B (mp P) (f i) ⟹ α), R { fst := f i, snd := f₁ } { fst := f i, snd := f₂ } → f₁ c p = f₂ c p
f₁ f₂ : B (mp P) x ⟹ α
r : R { fst := x, snd := f₁ } { fst := x, snd := f₂ }
e₁' : PFunctor.M.dest x = { fst := a, snd := f }
e₁ :
  dest P { fst := x, snd := f₁ } =
    { fst := a, snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := f x_1, snd := pathDestRight P e₁' f₁ x_1 } }
e₂' : PFunctor.M.dest x = { fst := a, snd := f }
e₃ : pathDestLeft P e₁' f₁ = pathDestLeft P e₂' f₂
e₂ :
  dest P { fst := x, snd := f₂ } =
    { fst := a, snd := splitFun (pathDestLeft P e₁' f₁) fun x_1 => { fst := f x_1, snd := pathDestRight P e₂' f₂ x_1 } }
h'' :
  ∀ (i : TypeVec.last (B P a)),
    R ((fun x_1 => { fst := f x_1, snd := pathDestRight P e₁' f₁ x_1 }) i)
      ((fun x_1 => { fst := f x_1, snd := pathDestRight P e₂' f₂ x_1 }) i)
⊢ f₁ c (Path.child x a f h' i c p) = f₂ c (Path.child x a f h' i c p)
[PROOFSTEP]
exact IH _ _ (h'' _)
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
r : R x y
⊢ x = y
[PROOFSTEP]
apply M.bisim P R _ _ _ r
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
r : R x y
⊢ ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
clear r x y
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∀ (x y : M P α),
    R x y →
      ∃ a f f₁ f₂,
        dest P x = { fst := a, snd := splitFun f f₁ } ∧
          dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
introv Hr
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
Hr : R x y
⊢ ∃ a f f₁ f₂,
    dest P x = { fst := a, snd := splitFun f f₁ } ∧
      dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
specialize h _ _ Hr
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
Hr : R x y
h : (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∃ a f f₁ f₂,
    dest P x = { fst := a, snd := splitFun f f₁ } ∧
      dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
clear Hr
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
h : (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∃ a f f₁ f₂,
    dest P x = { fst := a, snd := splitFun f f₁ } ∧
      dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
revert h
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
⊢ (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y →
    ∃ a f f₁ f₂,
      dest P x = { fst := a, snd := splitFun f f₁ } ∧
        dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
rcases M.dest P x with ⟨ax, fx⟩
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
⊢ (TypeVec.id ::: Quot.mk R) <$$> { fst := ax, snd := fx } = (TypeVec.id ::: Quot.mk R) <$$> dest P y →
    ∃ a f f₁ f₂,
      { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
        dest P y = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
rcases M.dest P y with ⟨ay, fy⟩
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
ay : P.A
fy : B P ay ⟹ α ::: M P α
⊢ (TypeVec.id ::: Quot.mk R) <$$> { fst := ax, snd := fx } = (TypeVec.id ::: Quot.mk R) <$$> { fst := ay, snd := fy } →
    ∃ a f f₁ f₂,
      { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
        { fst := ay, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
intro h
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
ay : P.A
fy : B P ay ⟹ α ::: M P α
h : (TypeVec.id ::: Quot.mk R) <$$> { fst := ax, snd := fx } = (TypeVec.id ::: Quot.mk R) <$$> { fst := ay, snd := fy }
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ay, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
rw [map_eq, map_eq] at h
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
ay : P.A
fy : B P ay ⟹ α ::: M P α
h : { fst := ax, snd := (TypeVec.id ::: Quot.mk R) ⊚ fx } = { fst := ay, snd := (TypeVec.id ::: Quot.mk R) ⊚ fy }
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ay, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
injection h with h₀ h₁
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀✝ : Equivalence R
x y : M P α
ax : P.A
fx : B P ax ⟹ α ::: M P α
ay : P.A
fy : B P ay ⟹ α ::: M P α
h₀ : ax = ay
h₁ : HEq ((TypeVec.id ::: Quot.mk R) ⊚ fx) ((TypeVec.id ::: Quot.mk R) ⊚ fy)
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ay, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
subst ay
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : HEq ((TypeVec.id ::: Quot.mk R) ⊚ fx) ((TypeVec.id ::: Quot.mk R) ⊚ fy)
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ax, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
simp at h₁
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ax, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
have Hdrop : dropFun fx = dropFun fy := by
  replace h₁ := congr_arg dropFun h₁
  simpa using h₁
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
⊢ dropFun fx = dropFun fy
[PROOFSTEP]
replace h₁ := congr_arg dropFun h₁
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : dropFun ((TypeVec.id ::: Quot.mk R) ⊚ fx) = dropFun ((TypeVec.id ::: Quot.mk R) ⊚ fy)
⊢ dropFun fx = dropFun fy
[PROOFSTEP]
simpa using h₁
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ ∃ a f f₁ f₂,
    { fst := ax, snd := fx } = { fst := a, snd := splitFun f f₁ } ∧
      { fst := ax, snd := fy } = { fst := a, snd := splitFun f f₂ } ∧ ∀ (i : TypeVec.last (B P a)), R (f₁ i) (f₂ i)
[PROOFSTEP]
exists ax, dropFun fx, lastFun fx, lastFun fy
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ { fst := ax, snd := fx } = { fst := ax, snd := splitFun (dropFun fx) (lastFun fx) } ∧
    { fst := ax, snd := fy } = { fst := ax, snd := splitFun (dropFun fx) (lastFun fy) } ∧
      ∀ (i : TypeVec.last (B P ax)), R (lastFun fx i) (lastFun fy i)
[PROOFSTEP]
rw [split_dropFun_lastFun, Hdrop, split_dropFun_lastFun]
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ { fst := ax, snd := fx } = { fst := ax, snd := fx } ∧
    { fst := ax, snd := fy } = { fst := ax, snd := fy } ∧ ∀ (i : TypeVec.last (B P ax)), R (lastFun fx i) (lastFun fy i)
[PROOFSTEP]
simp
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ ∀ (i : TypeVec.last (B P ax)), R (lastFun fx i) (lastFun fy i)
[PROOFSTEP]
intro i
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
⊢ R (lastFun fx i) (lastFun fy i)
[PROOFSTEP]
replace h₁ := congr_fun (congr_fun h₁ Fin2.fz) i
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
h₁ : ((TypeVec.id ::: Quot.mk R) ⊚ fx) Fin2.fz i = ((TypeVec.id ::: Quot.mk R) ⊚ fy) Fin2.fz i
⊢ R (lastFun fx i) (lastFun fy i)
[PROOFSTEP]
simp [(· ⊚ ·), appendFun, splitFun] at h₁
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
h₁ : Quot.mk R (fx Fin2.fz i) = Quot.mk R (fy Fin2.fz i)
⊢ R (lastFun fx i) (lastFun fy i)
[PROOFSTEP]
replace h₁ := Quot.exact _ h₁
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
h₁ : EqvGen R (fx Fin2.fz i) (fy Fin2.fz i)
⊢ R (lastFun fx i) (lastFun fy i)
[PROOFSTEP]
rw [h₀.eqvGen_iff] at h₁
[GOAL]
case mk.mk
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h₀ : Equivalence R
x y : M P α
ax : P.A
fx fy : B P ax ⟹ α ::: M P α
Hdrop : dropFun fx = dropFun fy
i : TypeVec.last (B P ax)
h₁ : R (fx Fin2.fz i) (fy Fin2.fz i)
⊢ R (lastFun fx i) (lastFun fy i)
[PROOFSTEP]
exact h₁
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
r : R x y
⊢ x = y
[PROOFSTEP]
have := M.bisim₀ P (EqvGen R) ?_ ?_
[GOAL]
case refine_3
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
r : R x y
this : ∀ (x y : M P α), EqvGen R x y → x = y
⊢ x = y
[PROOFSTEP]
solve_by_elim [EqvGen.rel]
[GOAL]
case refine_1
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
r : R x y
⊢ Equivalence (EqvGen R)
[PROOFSTEP]
apply EqvGen.is_equivalence
[GOAL]
case refine_2
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
r : R x y
⊢ ∀ (x y : M P α),
    EqvGen R x y → (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y
[PROOFSTEP]
clear r x y
[GOAL]
case refine_2
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
⊢ ∀ (x y : M P α),
    EqvGen R x y → (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y
[PROOFSTEP]
introv Hr
[GOAL]
case refine_2
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
Hr : EqvGen R x y
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y
[PROOFSTEP]
have : ∀ x y, R x y → EqvGen R x y := @EqvGen.rel _ R
[GOAL]
case refine_2
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
Hr : EqvGen R x y
this : ∀ (x y : M P α), R x y → EqvGen R x y
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y
[PROOFSTEP]
induction Hr
[GOAL]
case refine_2.rel
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
this : ∀ (x y : M P α), R x y → EqvGen R x y
x✝ y✝ : M P α
a✝ : R x✝ y✝
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝
[PROOFSTEP]
rw [← Quot.factor_mk_eq R (EqvGen R) this]
[GOAL]
case refine_2.rel
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
this : ∀ (x y : M P α), R x y → EqvGen R x y
x✝ y✝ : M P α
a✝ : R x✝ y✝
⊢ (TypeVec.id ::: Quot.factor R (EqvGen R) this ∘ Quot.mk R) <$$> dest P x✝ =
    (TypeVec.id ::: Quot.factor R (EqvGen R) this ∘ Quot.mk R) <$$> dest P y✝
[PROOFSTEP]
rwa [appendFun_comp_id, ← MvFunctor.map_map, ← MvFunctor.map_map, h]
  -- porting note: `cc` was replaced with `aesop`, maybe there is a more light-weight solution?
[GOAL]
case refine_2.refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
this : ∀ (x y : M P α), R x y → EqvGen R x y
x✝ : M P α
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝
case refine_2.symm
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
this : ∀ (x y : M P α), R x y → EqvGen R x y
x✝ y✝ : M P α
a✝ : EqvGen R x✝ y✝
a_ih✝ : (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝
case refine_2.trans
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
this : ∀ (x y : M P α), R x y → EqvGen R x y
x✝ y✝ z✝ : M P α
a✝¹ : EqvGen R x✝ y✝
a✝ : EqvGen R y✝ z✝
a_ih✝¹ : (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝
a_ih✝ : (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P z✝
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P z✝
[PROOFSTEP]
all_goals aesop
[GOAL]
case refine_2.refl
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
this : ∀ (x y : M P α), R x y → EqvGen R x y
x✝ : M P α
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝
[PROOFSTEP]
aesop
[GOAL]
case refine_2.symm
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
this : ∀ (x y : M P α), R x y → EqvGen R x y
x✝ y✝ : M P α
a✝ : EqvGen R x✝ y✝
a_ih✝ : (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝
[PROOFSTEP]
aesop
[GOAL]
case refine_2.trans
n : ℕ
P : MvPFunctor (n + 1)
α : TypeVec n
R : M P α → M P α → Prop
h : ∀ (x y : M P α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y
x y : M P α
this : ∀ (x y : M P α), R x y → EqvGen R x y
x✝ y✝ z✝ : M P α
a✝¹ : EqvGen R x✝ y✝
a✝ : EqvGen R y✝ z✝
a_ih✝¹ : (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝
a_ih✝ : (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P z✝
⊢ (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x✝ = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P z✝
[PROOFSTEP]
aesop
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
x : M P α
⊢ dest P (g <$$> x) = (g ::: fun x => g <$$> x) <$$> dest P x
[PROOFSTEP]
cases' x with a f
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : (mp P).A
f : B (mp P) a ⟹ α
⊢ dest P (g <$$> { fst := a, snd := f }) = (g ::: fun x => g <$$> x) <$$> dest P { fst := a, snd := f }
[PROOFSTEP]
rw [map_eq]
[GOAL]
case mk
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : (mp P).A
f : B (mp P) a ⟹ α
⊢ dest P { fst := a, snd := g ⊚ f } = (g ::: fun x => g <$$> x) <$$> dest P { fst := a, snd := f }
[PROOFSTEP]
conv =>
  rhs
  rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : (mp P).A
f : B (mp P) a ⟹ α
| dest P { fst := a, snd := g ⊚ f } = (g ::: fun x => g <$$> x) <$$> dest P { fst := a, snd := f }
[PROOFSTEP]
  rhs
  rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : (mp P).A
f : B (mp P) a ⟹ α
| dest P { fst := a, snd := g ⊚ f } = (g ::: fun x => g <$$> x) <$$> dest P { fst := a, snd := f }
[PROOFSTEP]
  rhs
  rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : (mp P).A
f : B (mp P) a ⟹ α
| dest P { fst := a, snd := g ⊚ f } = (g ::: fun x => g <$$> x) <$$> dest P { fst := a, snd := f }
[PROOFSTEP]
rhs
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ⟹ β
a : (mp P).A
f : B (mp P) a ⟹ α
| (g ::: fun x => g <$$> x) <$$> dest P { fst := a, snd := f }
[PROOFSTEP]
rw [M.dest, M.dest', map_eq, appendFun_comp_splitFun]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ g <$$> dest P x = dest P (dropFun g <$$> x)
[PROOFSTEP]
rw [M.dest_map]
[GOAL]
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ g <$$> dest P x = (dropFun g ::: fun x => dropFun g <$$> x) <$$> dest P x
[PROOFSTEP]
congr
[GOAL]
case e_a
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ g = (dropFun g ::: fun x => dropFun g <$$> x)
[PROOFSTEP]
apply eq_of_drop_last_eq
[GOAL]
case e_a.h₀
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ dropFun g = dropFun (dropFun g ::: fun x => dropFun g <$$> x)
[PROOFSTEP]
simp
[GOAL]
case e_a.h₁
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ lastFun g = lastFun (dropFun g ::: fun x => dropFun g <$$> x)
[PROOFSTEP]
simp
[GOAL]
case e_a.h₁
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
⊢ lastFun g = fun x => dropFun g <$$> x
[PROOFSTEP]
ext1
[GOAL]
case e_a.h₁.h
n : ℕ
P : MvPFunctor (n + 1)
α β : TypeVec n
g : α ::: M P α ⟹ β ::: M P β
x : M P α
h : ∀ (x : M P α), lastFun g x = dropFun g <$$> x
x✝ : TypeVec.last (α ::: M P α)
⊢ lastFun g x✝ = dropFun g <$$> x✝
[PROOFSTEP]
apply h


[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
h : Set.Countable s
default x : α
hx : x ∈ s
⊢ enumerateCountable h default (encode { val := x, property := hx }) = x
[PROOFSTEP]
letI := h.toEncodable
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
h : Set.Countable s
default x : α
hx : x ∈ s
this : Encodable ↑s := Countable.toEncodable h
⊢ enumerateCountable h default (encode { val := x, property := hx }) = x
[PROOFSTEP]
simp [enumerateCountable, Encodable.encodek]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : Nonempty α
s : Set α
h : Set.Countable s
⊢ ∃ f, s ⊆ range f
[PROOFSTEP]
inhabit α
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : Nonempty α
s : Set α
h : Set.Countable s
inhabited_h : Inhabited α
⊢ ∃ f, s ⊆ range f
[PROOFSTEP]
exact ⟨enumerateCountable h default, subset_range_enumerate _ _⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hc : Set.Countable s
hs : Set.Nonempty s
⊢ ∃ f, s = range f
[PROOFSTEP]
rcases hc.exists_surjective hs with ⟨f, hf⟩
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hc : Set.Countable s
hs : Set.Nonempty s
f : ℕ → ↑s
hf : Surjective f
⊢ ∃ f, s = range f
[PROOFSTEP]
refine' ⟨(↑) ∘ f, _⟩
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hc : Set.Countable s
hs : Set.Nonempty s
f : ℕ → ↑s
hf : Surjective f
⊢ s = range (Subtype.val ∘ f)
[PROOFSTEP]
rw [hf.range_comp, Subtype.range_coe]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
f : α → β
⊢ Set.Countable (f '' s)
[PROOFSTEP]
rw [image_eq_range]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
f : α → β
⊢ Set.Countable (range fun x => f ↑x)
[PROOFSTEP]
haveI := hs.to_subtype
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
f : α → β
this : Countable ↑s
⊢ Set.Countable (range fun x => f ↑x)
[PROOFSTEP]
apply countable_range
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤) ↔ ∃ S, Set.Countable S ∧ (∀ (s : α), s ∈ S → p s) ∧ sSup S = ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤) → ∃ S, Set.Countable S ∧ (∀ (s : α), s ∈ S → p s) ∧ sSup S = ⊤
[PROOFSTEP]
rintro ⟨s, hps, hs⟩
[GOAL]
case mp.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
s : ℕ → α
hps : ∀ (n : ℕ), p (s n)
hs : ⨆ (n : ℕ), s n = ⊤
⊢ ∃ S, Set.Countable S ∧ (∀ (s : α), s ∈ S → p s) ∧ sSup S = ⊤
[PROOFSTEP]
refine' ⟨range s, countable_range s, forall_range_iff.2 hps, _⟩
[GOAL]
case mp.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
s : ℕ → α
hps : ∀ (n : ℕ), p (s n)
hs : ⨆ (n : ℕ), s n = ⊤
⊢ sSup (range s) = ⊤
[PROOFSTEP]
rwa [sSup_range]
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ S, Set.Countable S ∧ (∀ (s : α), s ∈ S → p s) ∧ sSup S = ⊤) → ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤
[PROOFSTEP]
rintro ⟨S, hSc, hps, hS⟩
[GOAL]
case mpr.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : Set.Countable S
hps : ∀ (s : α), s ∈ S → p s
hS : sSup S = ⊤
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤
[PROOFSTEP]
rcases eq_empty_or_nonempty S with (rfl | hne)
[GOAL]
case mpr.intro.intro.intro.inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
hSc : Set.Countable ∅
hps : ∀ (s : α), s ∈ ∅ → p s
hS : sSup ∅ = ⊤
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤
[PROOFSTEP]
rw [sSup_empty] at hS
[GOAL]
case mpr.intro.intro.intro.inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
hSc : Set.Countable ∅
hps : ∀ (s : α), s ∈ ∅ → p s
hS : ⊥ = ⊤
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤
[PROOFSTEP]
haveI := subsingleton_of_bot_eq_top hS
[GOAL]
case mpr.intro.intro.intro.inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
hSc : Set.Countable ∅
hps : ∀ (s : α), s ∈ ∅ → p s
hS : ⊥ = ⊤
this : Subsingleton α
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤
[PROOFSTEP]
rcases h with ⟨x, hx⟩
[GOAL]
case mpr.intro.intro.intro.inl.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
hSc : Set.Countable ∅
hps : ∀ (s : α), s ∈ ∅ → p s
hS : ⊥ = ⊤
this : Subsingleton α
x : α
hx : p x
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤
[PROOFSTEP]
exact ⟨fun _ => x, fun _ => hx, Subsingleton.elim _ _⟩
[GOAL]
case mpr.intro.intro.intro.inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : Set.Countable S
hps : ∀ (s : α), s ∈ S → p s
hS : sSup S = ⊤
hne : Set.Nonempty S
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤
[PROOFSTEP]
rcases(Set.countable_iff_exists_surjective hne).1 hSc with ⟨s, hs⟩
[GOAL]
case mpr.intro.intro.intro.inr.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : Set.Countable S
hps : ∀ (s : α), s ∈ S → p s
hS : sSup S = ⊤
hne : Set.Nonempty S
s : ℕ → ↑S
hs : Surjective s
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ (n : ℕ), s n = ⊤
[PROOFSTEP]
refine' ⟨fun n => s n, fun n => hps _ (s n).coe_prop, _⟩
[GOAL]
case mpr.intro.intro.intro.inr.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : Set.Countable S
hps : ∀ (s : α), s ∈ S → p s
hS : sSup S = ⊤
hne : Set.Nonempty S
s : ℕ → ↑S
hs : Surjective s
⊢ ⨆ (n : ℕ), (fun n => ↑(s n)) n = ⊤
[PROOFSTEP]
rwa [hs.iSup_comp, ← sSup_eq_iSup']
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), Set.Countable (t i)
⊢ Set.Countable (⋃ (i : ι), t i)
[PROOFSTEP]
haveI := fun a => (ht a).to_subtype
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), Set.Countable (t i)
this : ∀ (a : ι), Countable ↑(t a)
⊢ Set.Countable (⋃ (i : ι), t i)
[PROOFSTEP]
rw [iUnion_eq_range_psigma]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), Set.Countable (t i)
this : ∀ (a : ι), Countable ↑(t a)
⊢ Set.Countable (range fun a => ↑a.snd)
[PROOFSTEP]
apply countable_range
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : (a : α) → a ∈ s → Set β
hs : Set.Countable s
⊢ Set.Countable (⋃ (a : α) (h : a ∈ s), t a h) ↔ ∀ (a : α) (ha : a ∈ s), Set.Countable (t a ha)
[PROOFSTEP]
haveI := hs.to_subtype
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : (a : α) → a ∈ s → Set β
hs : Set.Countable s
this : Countable ↑s
⊢ Set.Countable (⋃ (a : α) (h : a ∈ s), t a h) ↔ ∀ (a : α) (ha : a ∈ s), Set.Countable (t a ha)
[PROOFSTEP]
rw [biUnion_eq_iUnion, countable_iUnion_iff, SetCoe.forall']
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set (Set α)
hs : Set.Countable s
⊢ Set.Countable (⋃₀ s) ↔ ∀ (a : Set α), a ∈ s → Set.Countable a
[PROOFSTEP]
rw [sUnion_eq_biUnion, hs.biUnion_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s t : Set α
⊢ Set.Countable (s ∪ t) ↔ Set.Countable s ∧ Set.Countable t
[PROOFSTEP]
simp [union_eq_iUnion, and_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
a : α
⊢ Set.Countable (insert a s) ↔ Set.Countable s
[PROOFSTEP]
simp only [insert_eq, countable_union, countable_singleton, true_and_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
⊢ Set.Countable {t | Set.Finite t ∧ t ⊆ s}
[PROOFSTEP]
haveI := hs.to_subtype
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
⊢ Set.Countable {t | Set.Finite t ∧ t ⊆ s}
[PROOFSTEP]
refine' Countable.mono _ (countable_range fun t : Finset s => Subtype.val '' (t : Set s))
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
⊢ {t | Set.Finite t ∧ t ⊆ s} ⊆ range fun t => Subtype.val '' ↑t
[PROOFSTEP]
rintro t ⟨ht, hts⟩
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
t : Set α
ht : Set.Finite t
hts : t ⊆ s
⊢ t ∈ range fun t => Subtype.val '' ↑t
[PROOFSTEP]
lift t to Set s using hts
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
t : Set ↑s
ht : Set.Finite ((fun x x_1 => x '' x_1) Subtype.val t)
⊢ (fun x x_1 => x '' x_1) Subtype.val t ∈ range fun t => Subtype.val '' ↑t
[PROOFSTEP]
lift t to Finset s using ht.of_finite_image (Subtype.val_injective.injOn _)
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
hs : Set.Countable s
this : Countable ↑s
t : Finset ↑s
ht : Set.Finite ((fun x x_1 => x '' x_1) Subtype.val ↑t)
⊢ (fun x x_1 => x '' x_1) Subtype.val ↑t ∈ range fun t => Subtype.val '' ↑t
[PROOFSTEP]
exact mem_range_self _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : Finite α
s : (a : α) → Set (π a)
hs : ∀ (a : α), Set.Countable (s a)
⊢ Set.Countable {f | ∀ (a : α), f a ∈ s a}
[PROOFSTEP]
simpa only [← mem_univ_pi] using countable_univ_pi hs
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : Set β
hs : Set.Countable s
ht : Set.Countable t
⊢ Set.Countable (s ×ˢ t)
[PROOFSTEP]
haveI : Countable s := hs.to_subtype
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : Set β
hs : Set.Countable s
ht : Set.Countable t
this : Countable ↑s
⊢ Set.Countable (s ×ˢ t)
[PROOFSTEP]
haveI : Countable t := ht.to_subtype
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : Set β
hs : Set.Countable s
ht : Set.Countable t
this✝ : Countable ↑s
this : Countable ↑t
⊢ Set.Countable (s ×ˢ t)
[PROOFSTEP]
exact (Countable.of_equiv _ <| (Equiv.Set.prod _ _).symm).to_set
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : Set β
hs : Set.Countable s
ht : Set.Countable t
f : α → β → γ
⊢ Set.Countable (Set.image2 f s t)
[PROOFSTEP]
rw [← image_prod]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
s : Set α
t : Set β
hs : Set.Countable s
ht : Set.Countable t
f : α → β → γ
⊢ Set.Countable ((fun x => f x.fst x.snd) '' s ×ˢ t)
[PROOFSTEP]
exact (hs.prod ht).image _


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
⊢ (fun s => ↑up (↑f '' ↑down s)) 1 = 1
[PROOFSTEP]
dsimp only
  -- porting note: structures do not do this automatically any more
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
⊢ ↑up (↑f '' ↑down 1) = 1
[PROOFSTEP]
rw [down_one, image_one, map_one, singleton_one, up_one]


[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
s t : Set α
a : α
x : α × α
⊢ Prod.swap x ∈ mulAntidiagonal s t a ↔ x ∈ mulAntidiagonal t s a
[PROOFSTEP]
simp [mul_comm, and_left_comm]
[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
s t : Set α
a : α
x : α × α
⊢ x.snd ∈ s ∧ x.fst ∈ t ∧ x.snd * x.fst = a ↔ x ∈ mulAntidiagonal t s a
[PROOFSTEP]
simp [mul_comm, and_left_comm]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(mulAntidiagonal s t a)
h : (↑x).fst = (↑y).fst
⊢ a = (↑y).fst * (↑x).snd
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(mulAntidiagonal s t a)
h : (↑x).fst = (↑y).fst
⊢ a = (↑x).fst * (↑x).snd
[PROOFSTEP]
exact x.2.2.2.symm
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(mulAntidiagonal s t a)
h : (↑x).snd = (↑y).snd
⊢ a = (↑x).fst * (↑y).snd
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(mulAntidiagonal s t a)
h : (↑x).snd = (↑y).snd
⊢ a = (↑x).fst * (↑x).snd
[PROOFSTEP]
exact x.2.2.2.symm
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
a✝ : α
x y : ↑(mulAntidiagonal s t a✝)
hs : IsPwo s
ht : IsPwo t
a : α
⊢ Set.Finite (mulAntidiagonal s t a)
[PROOFSTEP]
refine' not_infinite.1 fun h => _
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
a✝ : α
x y : ↑(mulAntidiagonal s t a✝)
hs : IsPwo s
ht : IsPwo t
a : α
h : Set.Infinite (mulAntidiagonal s t a)
⊢ False
[PROOFSTEP]
have h1 : (mulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o (· ≤ ·)) := fun f hf =>
  hs (Prod.fst ∘ f) fun n => (mem_mulAntidiagonal.1 (hf n)).1
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
a✝ : α
x y : ↑(mulAntidiagonal s t a✝)
hs : IsPwo s
ht : IsPwo t
a : α
h : Set.Infinite (mulAntidiagonal s t a)
h1 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
⊢ False
[PROOFSTEP]
have h2 : (mulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o (· ≤ ·)) := fun f hf =>
  ht (Prod.snd ∘ f) fun n => (mem_mulAntidiagonal.1 (hf n)).2.1
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
a✝ : α
x y : ↑(mulAntidiagonal s t a✝)
hs : IsPwo s
ht : IsPwo t
a : α
h : Set.Infinite (mulAntidiagonal s t a)
h1 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
h2 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)
⊢ False
[PROOFSTEP]
obtain ⟨g, hg⟩ := h1.exists_monotone_subseq (fun n => h.natEmbedding _ n) fun n => (h.natEmbedding _ n).2
[GOAL]
case intro
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
a✝ : α
x y : ↑(mulAntidiagonal s t a✝)
hs : IsPwo s
ht : IsPwo t
a : α
h : Set.Infinite (mulAntidiagonal s t a)
h1 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
h2 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g m))
        ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g n))
⊢ False
[PROOFSTEP]
obtain ⟨m, n, mn, h2'⟩ := h2 (fun x => (h.natEmbedding _) (g x)) fun n => (h.natEmbedding _ _).2
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
a✝ : α
x y : ↑(mulAntidiagonal s t a✝)
hs : IsPwo s
ht : IsPwo t
a : α
h : Set.Infinite (mulAntidiagonal s t a)
h1 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
h2 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g m))
        ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g n))
m n : ℕ
mn : m < n
h2' :
  (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1) ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g m))
    ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g n))
⊢ False
[PROOFSTEP]
refine' mn.ne (g.injective <| (h.natEmbedding _).injective _)
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
a✝ : α
x y : ↑(mulAntidiagonal s t a✝)
hs : IsPwo s
ht : IsPwo t
a : α
h : Set.Infinite (mulAntidiagonal s t a)
h1 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
h2 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g m))
        ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g n))
m n : ℕ
mn : m < n
h2' :
  (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1) ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g m))
    ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g n))
⊢ ↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g m) = ↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g n)
[PROOFSTEP]
exact eq_of_fst_le_fst_of_snd_le_snd _ _ _ (hg _ _ mn.le) h2'