α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
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₁
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
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')
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
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₁
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
rw [WellFounded.fixFEq] at h₂
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  ∃ h,
    b ∈
      match e : Part.get (f a) h with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        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' (_ : Acc (fun y x => Sum.inr y ∈ f x) a')
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
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')
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
simp at h₂
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
h₃ :
  b ∈
    match e : Part.get (f a) h₂ with
    | Sum.inl b => Part.some b
    | Sum.inr a' =>
      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' (_ : Acc (fun y x => Sum.inr y ∈ f x) a')
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ :
  ∃ h,
    b ∈
      match e : Part.get (f a) h with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        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' (_ : Acc (fun y x => Sum.inr y ∈ f x) a')
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
cases' h₂ with h₂ h₃
case intro.h_1
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
b✝ : β
heq✝ : Part.get (f a) h₂ = Sum.inl b✝
h₃ : b = b✝
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'

case intro.h_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
a'✝ : α
heq✝ : Part.get (f a) h₂ = Sum.inr 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'✝ (_ : Acc (fun y x => Sum.inr y ∈ f x) a'✝)
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
h₃ :
  b ∈
    match e : Part.get (f a) h₂ with
    | Sum.inl b => Part.some b
    | Sum.inr a' =>
      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' (_ : Acc (fun y x => Sum.inr y ∈ f x) a')
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
split at h₃ <;> simp at h₃
case intro.h_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
a'✝ : α
heq✝ : Part.get (f a) h₂ = Sum.inr 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'✝ (_ : Acc (fun y x => Sum.inr y ∈ f x) a'✝)
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
case intro.h_1
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
b✝ : β
heq✝ : Part.get (f a) h₂ = Sum.inl b✝
h₃ : b = b✝
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'

case intro.h_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
a'✝ : α
heq✝ : Part.get (f a) h₂ = Sum.inr 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'✝ (_ : Acc (fun y x => Sum.inr y ∈ f x) a'✝)
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
next e => subst b; refine' Or.inl ⟨h₂, e⟩
no goals
case intro.h_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
a'✝ : α
heq✝ : Part.get (f a) h₂ = Sum.inr 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'✝ (_ : Acc (fun y x => Sum.inr y ∈ f x) a'✝)
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
next e => exact Or.inr ⟨_, ⟨_, e⟩, Part.mem_assert _ h₃⟩
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
b✝ : β
e : Part.get (f a) h₂ = Sum.inl b✝
h : b✝ ∈ fix f a
⊢ Sum.inl b✝ ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b✝ ∈ fix f a'
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
b✝ : β
e : Part.get (f a) h₂ = Sum.inl b✝
h₃ : b = b✝
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
subst b
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
b✝ : β
e : Part.get (f a) h₂ = Sum.inl b✝
h : b✝ ∈ fix f a
⊢ Sum.inl b✝ ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b✝ ∈ fix f a'
refine' Or.inl ⟨h₂, e⟩
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h : b ∈ fix f a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
a'✝ : α
e : Part.get (f a) h₂ = Sum.inr 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'✝ (_ : Acc (fun y x => Sum.inr y ∈ f x) a'✝)
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
exact Or.inr ⟨_, ⟨_, e⟩, Part.mem_assert _ h₃⟩
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h : Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f 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
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h : Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f a'
⊢ b ∈ fix f a
simp [fix]
case inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
⊢ ∃ 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

case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : b ∈ fix f 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
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h : Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ fix f 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
rcases h with (⟨h₁, h₂⟩ | ⟨a', h, h₃⟩)
case inl.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
y : α
h' : Sum.inr y ∈ f a
⊢ Acc (fun x y => Sum.inr x ∈ f y) y

case inl.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
⊢ 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 (_ : Acc (fun x y => Sum.inr x ∈ f y) a)
case inl.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
⊢ ∃ 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
refine' ⟨⟨_, fun y h' => _⟩, _⟩
no goals
case inl.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
y : α
h' : Sum.inr y ∈ f a
⊢ Acc (fun x y => Sum.inr x ∈ f y) y
injection Part.mem_unique ⟨h₁, h₂⟩ h'
case inl.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
⊢ 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')
case inl.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
⊢ 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 (_ : Acc (fun x y => Sum.inr x ∈ f y) a)
rw [WellFounded.fixFEq]
case inl.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
⊢ b ∈
    match e : Part.get (f a) h₁ 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')
case inl.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
⊢ 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')
apply Part.mem_assert h₁
case inl.intro.refine'_2.h_1
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
b✝ : β
heq✝ : Part.get (f a) h₁ = Sum.inl b✝
⊢ b ∈ Part.some b✝

case inl.intro.refine'_2.h_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
a'✝ : α
heq✝ : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (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'✝)
case inl.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
⊢ b ∈
    match e : Part.get (f a) h₁ 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')
split
case inl.intro.refine'_2.h_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
a'✝ : α
heq✝ : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (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'✝)
case inl.intro.refine'_2.h_1
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
b✝ : β
heq✝ : Part.get (f a) h₁ = Sum.inl b✝
⊢ b ∈ Part.some b✝

case inl.intro.refine'_2.h_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
a'✝ : α
heq✝ : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (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'✝)
next e =>
  injection h₂.symm.trans e with h; simp [h]
no goals
case inl.intro.refine'_2.h_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
a'✝ : α
heq✝ : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (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'✝)
next e =>
  injection h₂.symm.trans e
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
b✝ : β
e : Part.get (f a) h₁ = Sum.inl b✝
h : b = b✝
⊢ b ∈ Part.some b✝
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
b✝ : β
e : Part.get (f a) h₁ = Sum.inl b✝
⊢ b ∈ Part.some b✝
injection h₂.symm.trans e with h
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
b✝ : β
e : Part.get (f a) h₁ = Sum.inl b✝
h : b = b✝
⊢ b ∈ Part.some b✝
simp [h]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inl b
a'✝ : α
e : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (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'✝)
injection h₂.symm.trans e
case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ :
  ∃ 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
⊢ ∃ 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
case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : b ∈ fix f 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
simp [fix] at h₃
case inr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ 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₃
⊢ ∃ 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
case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ :
  ∃ 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
⊢ ∃ 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
cases' h₃ with h₃ h₄
case inr.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ 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₃
y : α
h' : Sum.inr y ∈ f a
⊢ Acc (fun x y => Sum.inr x ∈ f y) y

case inr.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ 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₃
⊢ 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 (_ : Acc (fun x y => Sum.inr x ∈ f y) a)
case inr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ 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₃
⊢ ∃ 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
refine' ⟨⟨_, fun y h' => _⟩, _⟩
case inr.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ 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₃
y : α
h' : Sum.inr y ∈ f a
e : a' = y
⊢ Acc (fun x y => Sum.inr x ∈ f y) y
case inr.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ 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₃
y : α
h' : Sum.inr y ∈ f a
⊢ Acc (fun x y => Sum.inr x ∈ f y) y
injection Part.mem_unique h h' with e
no goals
case inr.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ 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₃
y : α
h' : Sum.inr y ∈ f a
e : a' = y
⊢ Acc (fun x y => Sum.inr x ∈ f y) y
exact e ▸ h₃
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
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₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
⊢ 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 (_ : Acc (fun x y => Sum.inr x ∈ f y) a)
case inr.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ 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₃
⊢ 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 (_ : Acc (fun x y => Sum.inr x ∈ f y) a)
cases' h with h₁ h₂
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
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₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
⊢ 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'_1 =>
        (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'_1 (_ : ∃ h, Part.get (f a) h = Sum.inr a'_1)
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
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₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
⊢ 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 (_ : Acc (fun x y => Sum.inr x ∈ f y) a)
rw [WellFounded.fixFEq]
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
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₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
⊢ b ∈
    match e : Part.get (f a) h₁ with
    | Sum.inl b => Part.some b
    | Sum.inr a'_1 =>
      (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'_1 (_ : ∃ h, Part.get (f a) h = Sum.inr a'_1)
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
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₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
⊢ 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'_1 =>
        (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'_1 (_ : ∃ h, Part.get (f a) h = Sum.inr a'_1)
apply Part.mem_assert h₁
case inr.intro.intro.intro.refine'_2.intro.h_1
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
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₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
b✝ : β
heq✝ : Part.get (f a) h₁ = Sum.inl b✝
⊢ b ∈ Part.some b✝

case inr.intro.intro.intro.refine'_2.intro.h_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
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₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
a'✝ : α
heq✝ : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (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'✝)
case inr.intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
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₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
⊢ b ∈
    match e : Part.get (f a) h₁ with
    | Sum.inl b => Part.some b
    | Sum.inr a'_1 =>
      (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'_1 (_ : ∃ h, Part.get (f a) h = Sum.inr a'_1)
split
case inr.intro.intro.intro.refine'_2.intro.h_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
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₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
a'✝ : α
heq✝ : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (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'✝)
case inr.intro.intro.intro.refine'_2.intro.h_1
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
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₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
b✝ : β
heq✝ : Part.get (f a) h₁ = Sum.inl b✝
⊢ b ∈ Part.some b✝

case inr.intro.intro.intro.refine'_2.intro.h_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
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₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
a'✝ : α
heq✝ : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (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'✝)
next e =>
  injection h₂.symm.trans e
no goals
case inr.intro.intro.intro.refine'_2.intro.h_2
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
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₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
a'✝ : α
heq✝ : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (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'✝)
next e =>
  injection h₂.symm.trans e; subst a'; exact h₄
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
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₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
b✝ : β
e : Part.get (f a) h₁ = Sum.inl b✝
⊢ b ∈ Part.some b✝
injection h₂.symm.trans e
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
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₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
a'✝ : α
e : Part.get (f a) h₁ = Sum.inr a'✝
val_eq✝ : a' = a'✝
⊢ b ∈
    (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'✝)
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
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₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
a'✝ : α
e : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (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'✝)
injection h₂.symm.trans e
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
a'✝ : α
e : Part.get (f a) h₁ = Sum.inr 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₃
h₂ : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (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'✝)
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
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₃
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = Sum.inr a'
a'✝ : α
e : Part.get (f a) h₁ = Sum.inr a'✝
val_eq✝ : a' = a'✝
⊢ b ∈
    (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'✝)
subst a'
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.19607
δ : Type ?u.19610
ε : Type ?u.19613
ι : Type ?u.19616
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
a'✝ : α
e : Part.get (f a) h₁ = Sum.inr 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₃
h₂ : Part.get (f a) h₁ = Sum.inr a'✝
⊢ b ∈
    (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'✝)
exact h₄