-- Mathlib/Data/PFun.lean
theorem mem_fix_iff {f : α →. β ⊕ α} {a : α} {b : β} :
    b ∈ f.fix a ↔ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a' :=
  ⟨fun h => by
    let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h
    rw [WellFounded.fixFEq] at h₂
    simp only [Part.mem_assert_iff] at h₂
    obtain ⟨h₂, h₃⟩ := h₂
    split at h₃
    next e => simp only [Part.mem_some_iff] at h₃; subst b; exact Or.inl ⟨h₂, e⟩
    next e => exact Or.inr ⟨_, ⟨_, e⟩, Part.mem_assert _ h₃⟩,
   fun h => by
    simp only [fix, Part.mem_assert_iff]
    rcases h with (⟨h₁, h₂⟩ | ⟨a', h, h₃⟩)
    · refine ⟨⟨_, fun y h' => ?_⟩, ?_⟩
      · injection Part.mem_unique ⟨h₁, h₂⟩ h'
      · rw [WellFounded.fixFEq]
        -- Porting note: used to be simp [h₁, h₂]
        apply Part.mem_assert h₁
        split
        next e =>
          injection h₂.symm.trans e with h; simp [h]
        next e =>
          injection h₂.symm.trans e
    · simp only [fix, Part.mem_assert_iff] at h₃
      obtain ⟨h₃, h₄⟩ := h₃
      refine ⟨⟨_, fun y h' => ?_⟩, ?_⟩
      · injection Part.mem_unique h h' with e
        exact e ▸ h₃
      · obtain ⟨h₁, h₂⟩ := h
        rw [WellFounded.fixFEq]
        -- Porting note: used to be simp [h₁, h₂, h₄]
        apply Part.mem_assert h₁
        split
        next e =>
          injection h₂.symm.trans e
        next e =>
          injection h₂.symm.trans e; subst a'; exact h₄⟩

Proof state:
α : Type u_1
β : Type u_2
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 : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a' h₃
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inr a'
b✝ : β
e : (f a).get h₁ = Sum.inl b✝
⊢ b ∈ Part.some b✝

Tactic:
injection h₂.symm.trans e

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
b✝ : β
e : (f a).get h₂ = Sum.inl b✝
h₃ : b ∈ Part.some b✝
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
simp only [Part.mem_some_iff] at h₃

Result:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
h₁ : Acc (fun x y => Sum.inr x ∈ f y) a
h₂ : (f a).Dom
b✝ : β
e : (f a).get h₂ = Sum.inl b✝
h₃ : b = b✝
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Proof state:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
⊢ b ∈ f.fix a

Tactic:
simp only [fix, Part.mem_assert_iff]

Result:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
⊢ ∃ (h : Acc (fun x y => Sum.inr x ∈ f y) a),
    b ∈
      WellFounded.fixF
        (fun a IH =>
          Part.assert (f a).Dom fun hf =>
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a h

Proof state:
case inr.intro.intro.intro.refine_2.intro.h_1
α : Type u_1
β : Type u_2
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 : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a' h₃
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inr a'
b✝ : β
heq✝ : (f a).get h₁ = Sum.inl b✝
⊢ b ∈ Part.some b✝

case inr.intro.intro.intro.refine_2.intro.h_2
α : Type u_1
β : Type u_2
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 : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a' h₃
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inr a'
a'✝ : α
heq✝ : (f a).get h₁ = Sum.inr a'✝
⊢ b ∈
    (fun y p =>
        WellFounded.fixF
          (fun a IH =>
            Part.assert (f a).Dom fun hf =>
              match e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯)
          y ⋯)
      a'✝ ⋯

Tactic:
next e =>
  injection h₂.symm.trans e

Result:
case inr.intro.intro.intro.refine_2.intro.h_2
α : Type u_1
β : Type u_2
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 : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a' h₃
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inr a'
a'✝ : α
heq✝ : (f a).get h₁ = Sum.inr a'✝
⊢ b ∈
    (fun y p =>
        WellFounded.fixF
          (fun a IH =>
            Part.assert (f a).Dom fun hf =>
              match e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯)
          y ⋯)
      a'✝ ⋯

Proof state:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h

Result:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix 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 : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a h₁
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Proof state:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
⊢ ∃ (h : Acc (fun x y => Sum.inr x ∈ f y) a),
    b ∈
      WellFounded.fixF
        (fun a IH =>
          Part.assert (f a).Dom fun hf =>
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a h

Tactic:
rcases h with (⟨h₁, h₂⟩ | ⟨a', h, h₃⟩)

Result:
case inl.intro
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
⊢ ∃ (h : Acc (fun x y => Sum.inr x ∈ f y) a),
    b ∈
      WellFounded.fixF
        (fun a IH =>
          Part.assert (f a).Dom fun hf =>
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a h

case inr.intro.intro
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : b ∈ f.fix a'
⊢ ∃ (h : Acc (fun x y => Sum.inr x ∈ f y) a),
    b ∈
      WellFounded.fixF
        (fun a IH =>
          Part.assert (f a).Dom fun hf =>
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a h

Proof state:
case inl.intro.refine_2.h_2
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
a'✝ : α
heq✝ : (f a).get h₁ = Sum.inr a'✝
⊢ b ∈
    (fun y p =>
        WellFounded.fixF
          (fun a IH =>
            Part.assert (f a).Dom fun hf =>
              match e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯)
          y ⋯)
      a'✝ ⋯

Tactic:
next e =>
  injection h₂.symm.trans e

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
a'✝ : α
e : (f a).get h₁ = Sum.inr a'✝
⊢ b ∈
    (fun y p =>
        WellFounded.fixF
          (fun a IH =>
            Part.assert (f a).Dom fun hf =>
              match e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯)
          y ⋯)
      a'✝ ⋯

Tactic:
injection h₂.symm.trans e

Result:
no goals