-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem iselect_eq_default [DecidableEq F.A] [Inhabited (M F)] (ps : Path F) (x : M F)
    (h : ¬IsPath ps x) : iselect ps x = head default

Proof state:
case pos.h.a
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ M.mk ⟨a, x_f⟩ = M.mk ⟨a, ?pos.h.f✝⟩

Tactic:
rfl

Result:
no goals

Proof state:
case pos.h
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)

Tactic:
constructor <;> try rfl

Result:
case pos.h.a
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ IsPath ps_tail (x_f i)

Proof state:
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps : Path F
x : F.M
h : ¬IsPath ps x
⊢ iselect ps x = default.head

Tactic:
induction' ps with ps_hd ps_tail ps_ih generalizing x

Result:
case nil
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
x : F.M
h : ¬IsPath [] x
⊢ iselect [] x = default.head

case cons
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_hd : F.Idx
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → iselect ps_tail x = default.head
x : F.M
h : ¬IsPath (ps_hd :: ps_tail) x
⊢ iselect (ps_hd :: ps_tail) x = default.head

Proof state:
case pos.h
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ False

Tactic:
apply h

Result:
case pos.h
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)

Proof state:
case pos
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
⊢ (isubtree ps_tail (x_f (cast ⋯ i))).head = default.head

Tactic:
rw [ps_ih]

Result:
case pos.h
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
⊢ ¬IsPath ps_tail (x_f (cast ⋯ i))

Proof state:
case nil
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
x : F.M
h : ¬IsPath [] x
⊢ IsPath [] x

Tactic:
constructor

Result:
no goals

Proof state:
case neg
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩)
h'' : ¬a = x_a
⊢ ((M.mk ⟨x_a, x_f⟩).casesOn' fun a' f => if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default).head =
    default.head

Tactic:
simp [*]

Result:
no goals

Proof state:
case pos
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩)
h'' : a = x_a
⊢ ((M.mk ⟨x_a, x_f⟩).casesOn' fun a' f => if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default).head =
    default.head

Tactic:
subst x_a

Result:
case pos
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_f : F.B a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨a, x_f⟩)
⊢ ((M.mk ⟨a, x_f⟩).casesOn' fun a' f => if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default).head =
    default.head

Proof state:
case nil
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
x : F.M
h : ¬IsPath [] x
⊢ False

Tactic:
apply h

Result:
case nil
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
x : F.M
h : ¬IsPath [] x
⊢ IsPath [] x

Proof state:
case cons
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_hd : F.Idx
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → iselect ps_tail x = default.head
x : F.M
h : ¬IsPath (ps_hd :: ps_tail) x
⊢ iselect (ps_hd :: ps_tail) x = default.head

Tactic:
obtain ⟨a, i⟩ := ps_hd

Result:
case cons.mk
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → iselect ps_tail x = default.head
x : F.M
a : F.A
i : F.B a
h : ¬IsPath (⟨a, i⟩ :: ps_tail) x
⊢ iselect (⟨a, i⟩ :: ps_tail) x = default.head

Proof state:
case cons.mk.f
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩)
⊢ ((M.mk ⟨x_a, x_f⟩).casesOn' fun a' f => if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default).head =
    default.head

Tactic:
by_cases h'' : a = x_a

Result:
case pos
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩)
h'' : a = x_a
⊢ ((M.mk ⟨x_a, x_f⟩).casesOn' fun a' f => if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default).head =
    default.head

case neg
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩)
h'' : ¬a = x_a
⊢ ((M.mk ⟨x_a, x_f⟩).casesOn' fun a' f => if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default).head =
    default.head

Proof state:
case cons.mk.f
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → iselect ps_tail x = default.head
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩)
⊢ iselect (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩) = default.head

Tactic:
simp only [iselect, isubtree] at ps_ih ⊢

Result:
case cons.mk.f
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M), ¬IsPath ps_tail x → (isubtree ps_tail x).head = default.head
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h : ¬IsPath (⟨a, i⟩ :: ps_tail) (M.mk ⟨x_a, x_f⟩)
⊢ ((M.mk ⟨x_a, x_f⟩).casesOn' fun a' f => if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default).head =
    default.head