-- Mathlib/Data/PFunctor/Multivariate/W.lean
theorem w_ind {α : TypeVec n} {C : P.W α → Prop}
    (ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α),
        (∀ i, C (f i)) → C (P.wMk a f' f)) :
    ∀ x, C x

Proof state:
case mk.ih
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih :
  ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α),
    (∀ (i : P.last.B a), C (f i)) → C ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn f' fun i => (f i).snd⟩
a✝ : P.wp.A
f✝ : P.wp.B a✝ ⟹ α
a : P.A
f : P.last.B a → P.last.W
f' : P.WPath (WType.mk a f) ⟹ α
ih' : ∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩
ih'' : (∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩) →
  C ⟨WType.mk a fun i => f i, P.wPathCasesOn (P.wPathDestLeft f') fun i => P.wPathDestRight f' i⟩ :=
  ih a (P.wPathDestLeft f') fun i => ⟨f i, P.wPathDestRight f' i⟩
⊢ C ⟨WType.mk a f, f'⟩

Tactic:
rw [wPathCasesOn_eta] at ih''

Result:
case mk.ih
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih :
  ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α),
    (∀ (i : P.last.B a), C (f i)) → C ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn f' fun i => (f i).snd⟩
a✝ : P.wp.A
f✝ : P.wp.B a✝ ⟹ α
a : P.A
f : P.last.B a → P.last.W
f' : P.WPath (WType.mk a f) ⟹ α
ih' : ∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩
ih'' : (∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩) → C ⟨WType.mk a fun i => f i, f'⟩
⊢ C ⟨WType.mk a f, f'⟩

Proof state:
case mk.ih
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih :
  ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α),
    (∀ (i : P.last.B a), C (f i)) → C ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn f' fun i => (f i).snd⟩
a✝ : P.wp.A
f✝ : P.wp.B a✝ ⟹ α
a : P.A
f : P.last.B a → P.last.W
f' : P.WPath (WType.mk a f) ⟹ α
ih' : ∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩
ih'' : (∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩) → C ⟨WType.mk a fun i => f i, f'⟩
⊢ C ⟨WType.mk a f, f'⟩

Tactic:
apply ih''

Result:
case mk.ih
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih :
  ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α),
    (∀ (i : P.last.B a), C (f i)) → C ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn f' fun i => (f i).snd⟩
a✝ : P.wp.A
f✝ : P.wp.B a✝ ⟹ α
a : P.A
f : P.last.B a → P.last.W
f' : P.WPath (WType.mk a f) ⟹ α
ih' : ∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩
ih'' : (∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩) → C ⟨WType.mk a fun i => f i, f'⟩
⊢ ∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩

Proof state:
case mk.ih
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih :
  ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α),
    (∀ (i : P.last.B a), C (f i)) → C ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn f' fun i => (f i).snd⟩
a✝ : P.wp.A
f✝ : P.wp.B a✝ ⟹ α
a : P.A
f : P.last.B a → P.last.W
f' : P.WPath (WType.mk a f) ⟹ α
ih' : ∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩
ih'' : (∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩) → C ⟨WType.mk a fun i => f i, f'⟩
⊢ ∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩

Tactic:
apply ih'

Result:
no goals

Proof state:
case mk.ih
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih :
  ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α),
    (∀ (i : P.last.B a), C (f i)) → C ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn f' fun i => (f i).snd⟩
a✝ : P.wp.A
f✝ : P.wp.B a✝ ⟹ α
a : P.A
f : P.last.B a → P.last.W
f' : P.WPath (WType.mk a f) ⟹ α
ih' : ∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩
ih'' : (∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩) →
  C
    ⟨WType.mk a fun i => ⟨f i, P.wPathDestRight f' i⟩.fst,
      P.wPathCasesOn (P.wPathDestLeft f') fun i => ⟨f i, P.wPathDestRight f' i⟩.snd⟩ :=
  ih a (P.wPathDestLeft f') fun i => ⟨f i, P.wPathDestRight f' i⟩
⊢ C ⟨WType.mk a f, f'⟩

Tactic:
dsimp at ih''

Result:
case mk.ih
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih :
  ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α),
    (∀ (i : P.last.B a), C (f i)) → C ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn f' fun i => (f i).snd⟩
a✝ : P.wp.A
f✝ : P.wp.B a✝ ⟹ α
a : P.A
f : P.last.B a → P.last.W
f' : P.WPath (WType.mk a f) ⟹ α
ih' : ∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩
ih'' : (∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩) →
  C ⟨WType.mk a fun i => f i, P.wPathCasesOn (P.wPathDestLeft f') fun i => P.wPathDestRight f' i⟩ :=
  ih a (P.wPathDestLeft f') fun i => ⟨f i, P.wPathDestRight f' i⟩
⊢ C ⟨WType.mk a f, f'⟩

Proof state:
case mk
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α), (∀ (i : P.last.B a), C (f i)) → C (P.wMk a f' f)
a : P.wp.A
f : P.wp.B a ⟹ α
⊢ C ⟨a, f⟩

Tactic:
apply @wp_ind n P α fun a f => C ⟨a, f⟩

Result:
case mk.ih
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α), (∀ (i : P.last.B a), C (f i)) → C (P.wMk a f' f)
a : P.wp.A
f : P.wp.B a ⟹ α
⊢ ∀ (a : P.A) (f : P.last.B a → P.last.W) (f' : P.WPath (WType.mk a f) ⟹ α),
    (∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩) → C ⟨WType.mk a f, f'⟩

Proof state:
case mk.ih
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α), (∀ (i : P.last.B a), C (f i)) → C (P.wMk a f' f)
a : P.wp.A
f : P.wp.B a ⟹ α
⊢ ∀ (a : P.A) (f : P.last.B a → P.last.W) (f' : P.WPath (WType.mk a f) ⟹ α),
    (∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩) → C ⟨WType.mk a f, f'⟩

Tactic:
intro a f f' ih'

Result:
case mk.ih
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α), (∀ (i : P.last.B a), C (f i)) → C (P.wMk a f' f)
a✝ : P.wp.A
f✝ : P.wp.B a✝ ⟹ α
a : P.A
f : P.last.B a → P.last.W
f' : P.WPath (WType.mk a f) ⟹ α
ih' : ∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩
⊢ C ⟨WType.mk a f, f'⟩

Proof state:
case mk.ih
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih : ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α), (∀ (i : P.last.B a), C (f i)) → C (P.wMk a f' f)
a✝ : P.wp.A
f✝ : P.wp.B a✝ ⟹ α
a : P.A
f : P.last.B a → P.last.W
f' : P.WPath (WType.mk a f) ⟹ α
ih' : ∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩
⊢ C ⟨WType.mk a f, f'⟩

Tactic:
dsimp [wMk] at ih

Result:
case mk.ih
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
C : P.W α → Prop
ih :
  ∀ (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α),
    (∀ (i : P.last.B a), C (f i)) → C ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn f' fun i => (f i).snd⟩
a✝ : P.wp.A
f✝ : P.wp.B a✝ ⟹ α
a : P.A
f : P.last.B a → P.last.W
f' : P.WPath (WType.mk a f) ⟹ α
ih' : ∀ (i : P.last.B a), C ⟨f i, P.wPathDestRight f' i⟩
⊢ C ⟨WType.mk a f, f'⟩