α : Type u_2
β : Type u_3
γ : Type ?u.33763
δ : Type ?u.33766
ε : Type ?u.33769
ι : Type ?u.33772
C : α → Sort u_1
f : α →. β ⊕ α
b : β
a : α
h : b ∈ fix f a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fixInduction h fun a' h ih =>
      Sum.casesOn (motive := fun x => Part.get (f a') (_ : (f a').Dom) = x → C a') (Part.get (f a') (_ : (f a').Dom))
        (fun b' e =>
          let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inl b');
          hbase a' (_ : Sum.inl b ∈ f a'))
        (fun a'' e =>
          let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inr a'');
          hind a' a'' (_ : b ∈ fix f a'') e (ih a'' e))
        (_ : Part.get (f a') (_ : (f a').Dom) = Part.get (f a') (_ : (f a').Dom))) =
    hbase a fa
α : Type u_2
β : Type u_3
γ : Type ?u.33763
δ : Type ?u.33766
ε : Type ?u.33769
ι : Type ?u.33772
C : α → Sort u_1
f : α →. β ⊕ α
b : β
a : α
h : b ∈ fix f a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ fixInduction' h hbase hind = hbase a fa
unfold fixInduction'
α : Type u_2
β : Type u_3
γ : Type ?u.33763
δ : Type ?u.33766
ε : Type ?u.33769
ι : Type ?u.33772
C : α → Sort u_1
f : α →. β ⊕ α
b : β
a : α
h : b ∈ fix f a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ Sum.casesOn (motive := fun x => Part.get (f a) (_ : (f a).Dom) = x → C a) (Part.get (f a) (_ : (f a).Dom))
      (fun b' e =>
        let_fun e := (_ : ∃ h, Part.get (f a) h = Sum.inl b');
        hbase a (_ : Sum.inl b ∈ f a))
      (fun a'' e =>
        let_fun e := (_ : ∃ h, Part.get (f a) h = Sum.inr a'');
        hind a a'' (_ : b ∈ fix f a'') e
          ((fun a' h' =>
              fixInduction (_ : b ∈ fix f a') fun a' h ih =>
                Sum.casesOn (motive := fun x => Part.get (f a') (_ : (f a').Dom) = x → C a')
                  (Part.get (f a') (_ : (f a').Dom))
                  (fun b' e =>
                    let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inl b');
                    hbase a' (_ : Sum.inl b ∈ f a'))
                  (fun a'' e =>
                    let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inr a'');
                    hind a' a'' (_ : b ∈ fix f a'') e (ih a'' e))
                  (_ : Part.get (f a') (_ : (f a').Dom) = Part.get (f a') (_ : (f a').Dom)))
            a'' e))
      (_ : Part.get (f a) (_ : (f a).Dom) = Part.get (f a) (_ : (f a).Dom)) =
    hbase a fa
α : Type u_2
β : Type u_3
γ : Type ?u.33763
δ : Type ?u.33766
ε : Type ?u.33769
ι : Type ?u.33772
C : α → Sort u_1
f : α →. β ⊕ α
b : β
a : α
h : b ∈ fix f a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fixInduction h fun a' h ih =>
      Sum.casesOn (motive := fun x => Part.get (f a') (_ : (f a').Dom) = x → C a') (Part.get (f a') (_ : (f a').Dom))
        (fun b' e =>
          let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inl b');
          hbase a' (_ : Sum.inl b ∈ f a'))
        (fun a'' e =>
          let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inr a'');
          hind a' a'' (_ : b ∈ fix f a'') e (ih a'' e))
        (_ : Part.get (f a') (_ : (f a').Dom) = Part.get (f a') (_ : (f a').Dom))) =
    hbase a fa
rw [fixInduction_spec]
α : Type u_2
β : Type u_3
γ : Type ?u.33763
δ : Type ?u.33766
ε : Type ?u.33769
ι : Type ?u.33772
C : α → Sort u_1
f : α →. β ⊕ α
b : β
a : α
h : b ∈ fix f a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fun x e =>
      Sum.casesOn (motive := fun y => Part.get (f a) (_ : (f a).Dom) = y → C a) x
          (fun val =>
            (fun b' e =>
                let_fun e := (_ : ∃ h, Part.get (f a) h = Sum.inl b');
                hbase a (_ : Sum.inl b ∈ f a))
              val)
          (fun val =>
            (fun a'' e =>
                let_fun e := (_ : ∃ h, Part.get (f a) h = Sum.inr a'');
                hind a a'' (_ : b ∈ fix f a'') e
                  ((fun a' h' =>
                      fixInduction (_ : b ∈ fix f a') fun a' h ih =>
                        Sum.casesOn (motive := fun x => Part.get (f a') (_ : (f a').Dom) = x → C a')
                          (Part.get (f a') (_ : (f a').Dom))
                          (fun b' e =>
                            let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inl b');
                            hbase a' (_ : Sum.inl b ∈ f a'))
                          (fun a'' e =>
                            let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inr a'');
                            hind a' a'' (_ : b ∈ fix f a'') e (ih a'' e))
                          (_ : Part.get (f a') (_ : (f a').Dom) = Part.get (f a') (_ : (f a').Dom)))
                    a'' e))
              val)
          (_ : Part.get (f a) (_ : (f a).Dom) = x) =
        hbase a fa)
    (Sum.inl b) (_ : Sum.inl b = Sum.inl b)
α : Type u_2
β : Type u_3
γ : Type ?u.33763
δ : Type ?u.33766
ε : Type ?u.33769
ι : Type ?u.33772
C : α → Sort u_1
f : α →. β ⊕ α
b : β
a : α
h : b ∈ fix f a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ Sum.casesOn (motive := fun x => Part.get (f a) (_ : (f a).Dom) = x → C a) (Part.get (f a) (_ : (f a).Dom))
      (fun b' e =>
        let_fun e := (_ : ∃ h, Part.get (f a) h = Sum.inl b');
        hbase a (_ : Sum.inl b ∈ f a))
      (fun a'' e =>
        let_fun e := (_ : ∃ h, Part.get (f a) h = Sum.inr a'');
        hind a a'' (_ : b ∈ fix f a'') e
          ((fun a' h' =>
              fixInduction (_ : b ∈ fix f a') fun a' h ih =>
                Sum.casesOn (motive := fun x => Part.get (f a') (_ : (f a').Dom) = x → C a')
                  (Part.get (f a') (_ : (f a').Dom))
                  (fun b' e =>
                    let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inl b');
                    hbase a' (_ : Sum.inl b ∈ f a'))
                  (fun a'' e =>
                    let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inr a'');
                    hind a' a'' (_ : b ∈ fix f a'') e (ih a'' e))
                  (_ : Part.get (f a') (_ : (f a').Dom) = Part.get (f a') (_ : (f a').Dom)))
            a'' e))
      (_ : Part.get (f a) (_ : (f a).Dom) = Part.get (f a) (_ : (f a).Dom)) =
    hbase a fa
refine' Eq.rec (motive := fun x e =>
    Sum.casesOn (motive := fun y => (f a).get (dom_of_mem_fix h) = y → C a) x _ _
    (Eq.trans (Part.get_eq_of_mem fa (dom_of_mem_fix h)) e) = hbase a fa) _
  (Part.get_eq_of_mem fa (dom_of_mem_fix h)).symm
no goals
α : Type u_2
β : Type u_3
γ : Type ?u.33763
δ : Type ?u.33766
ε : Type ?u.33769
ι : Type ?u.33772
C : α → Sort u_1
f : α →. β ⊕ α
b : β
a : α
h : b ∈ fix f a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ fix f a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fun x e =>
      Sum.casesOn (motive := fun y => Part.get (f a) (_ : (f a).Dom) = y → C a) x
          (fun val =>
            (fun b' e =>
                let_fun e := (_ : ∃ h, Part.get (f a) h = Sum.inl b');
                hbase a (_ : Sum.inl b ∈ f a))
              val)
          (fun val =>
            (fun a'' e =>
                let_fun e := (_ : ∃ h, Part.get (f a) h = Sum.inr a'');
                hind a a'' (_ : b ∈ fix f a'') e
                  ((fun a' h' =>
                      fixInduction (_ : b ∈ fix f a') fun a' h ih =>
                        Sum.casesOn (motive := fun x => Part.get (f a') (_ : (f a').Dom) = x → C a')
                          (Part.get (f a') (_ : (f a').Dom))
                          (fun b' e =>
                            let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inl b');
                            hbase a' (_ : Sum.inl b ∈ f a'))
                          (fun a'' e =>
                            let_fun e := (_ : ∃ h, Part.get (f a') h = Sum.inr a'');
                            hind a' a'' (_ : b ∈ fix f a'') e (ih a'' e))
                          (_ : Part.get (f a') (_ : (f a').Dom) = Part.get (f a') (_ : (f a').Dom)))
                    a'' e))
              val)
          (_ : Part.get (f a) (_ : (f a).Dom) = x) =
        hbase a fa)
    (Sum.inl b) (_ : Sum.inl b = Sum.inl b)
simp