α : Type u_1
β : Type u_2
γ : Type ?u.19159
δ : Type ?u.19162
ε : Type ?u.19165
ι : Type ?u.19168
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a h₁
⊢ (f a).Dom
α : Type u_1
β : Type u_2
γ : Type ?u.19159
δ : Type ?u.19162
ε : Type ?u.19165
ι : Type ?u.19168
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
⊢ (f a).Dom
let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h
α : Type u_1
β : Type u_2
γ : Type ?u.19159
δ : Type ?u.19162
ε : Type ?u.19165
ι : Type ?u.19168
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  b ∈
    Part.assert (f a).Dom fun hf =>
      match e : Part.get (f a) hf with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun y p =>
            WellFounded.fixF
              (fun a IH =>
                Part.assert (f a).Dom fun hf =>
                  match e : Part.get (f a) hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
              y (_ : Acc (fun y x => Sum.inr y ∈ f x) y))
          a' (_ : ∃ h, Part.get (f a) h = Sum.inr a')
⊢ (f a).Dom
α : Type u_1
β : Type u_2
γ : Type ?u.19159
δ : Type ?u.19162
ε : Type ?u.19165
ι : Type ?u.19168
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH =>
        Part.assert (f a).Dom fun hf =>
          match e : Part.get (f a) hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
      a h₁
⊢ (f a).Dom
rw [WellFounded.fixFEq] at h₂
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.19159
δ : Type ?u.19162
ε : Type ?u.19165
ι : Type ?u.19168
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  b ∈
    Part.assert (f a).Dom fun hf =>
      match e : Part.get (f a) hf with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun y p =>
            WellFounded.fixF
              (fun a IH =>
                Part.assert (f a).Dom fun hf =>
                  match e : Part.get (f a) hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' (_ : ∃ h, Part.get (f a) h = Sum.inr a'))
              y (_ : Acc (fun y x => Sum.inr y ∈ f x) y))
          a' (_ : ∃ h, Part.get (f a) h = Sum.inr a')
⊢ (f a).Dom
exact h₂.fst.fst