awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
inl :
  Membership.mem (γ := Part β)
    (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
      match (motive := β ⊕ α → Part β) e : (f a).get hf with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun (y : α) (p : Sum.inr y ∈ f a) ↦
            (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
                (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
                  (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                      match (motive := β ⊕ α → Part β) e : (f a).get hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' ⋯ :
                    Part β))
                y ⋯ :
              Part β))
          a' ⋯)
    b
⊢ Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a ⋯ :
      Part β)
    b

Tactic:
rw [WellFounded.fixF_eq]

Premises used: WellFounded.fixF_eq
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
inl :
  Membership.mem (γ := Part β)
    (match (motive := β ⊕ α → Part β) e : (f a).get h₁ with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun (y : α) (p : Sum.inr y ∈ f a) ↦
            (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
                (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
                  (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                      match (motive := β ⊕ α → Part β) e : (f a).get hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' ⋯ :
                    Part β))
                y ⋯ :
              Part β))
          a' ⋯ :
      Part β)
    b
⊢ Membership.mem (γ := Part β)
    (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
      match (motive := β ⊕ α → Part β) e : (f a).get hf with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun (y : α) (p : Sum.inr y ∈ f a) ↦
            (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
                (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
                  (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                      match (motive := β ⊕ α → Part β) e : (f a).get hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' ⋯ :
                    Part β))
                y ⋯ :
              Part β))
          a' ⋯)
    b

Tactic:
apply Part.mem_assert h₁

Premises used: Part.mem_assert
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
h_1 : ∀ (b_1 : β), (f a).get h₁ = Sum.inl b_1 → b ∈ Part.some b_1
h_2 :
  ∀ (a' : α) (heq : (f a).get h₁ = Sum.inr a'),
    Membership.mem (γ := Part β)
      ((fun (y : α) (p : Sum.inr y ∈ f a) ↦
          (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
              (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
                (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                    match (motive := β ⊕ α → Part β) e : (f a).get hf with
                    | Sum.inl b => Part.some b
                    | Sum.inr a' => IH a' ⋯ :
                  Part β))
              y ⋯ :
            Part β))
        a' ⋯)
      b
⊢ Membership.mem (γ := Part β)
    (match (motive := β ⊕ α → Part β) e : (f a).get h₁ with
      | Sum.inl b => Part.some b
      | Sum.inr a' =>
        (fun (y : α) (p : Sum.inr y ∈ f a) ↦
            (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
                (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
                  (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                      match (motive := β ⊕ α → Part β) e : (f a).get hf with
                      | Sum.inl b => Part.some b
                      | Sum.inr a' => IH a' ⋯ :
                    Part β))
                y ⋯ :
              Part β))
          a' ⋯ :
      Part β)
    b

Tactic:
split
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
b_1 : β
e : (f a).get h₁ = Sum.inl b_1
⊢ b = b_1

Tactic:
injection h₂.symm.trans e with h

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
b_1 : β
e : (f a).get h₁ = Sum.inl b_1
h : b = b_1
⊢ b ∈ Part.some b_1

Tactic:
simp [h]
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
b_1 : β
heq : (f a).get h₁ = Sum.inl b_1
⊢ b ∈ Part.some b_1

Tactic:
next e =>
          injection h₂.symm.trans e with h; simp [h]
-- Module: Mathlib.Data.PFun
Goal:
α : 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'
⊢ Membership.mem (γ := Part β)
    ((fun (y : α) (p : Sum.inr y ∈ f a) ↦
        (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
            (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
              (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                  match (motive := β ⊕ α → Part β) e : (f a).get hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' ⋯ :
                Part β))
            y ⋯ :
          Part β))
      a' ⋯)
    b

Tactic:
injection h₂.symm.trans e

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Data.PFun
Goal:
α : 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'),
    Membership.mem (γ := Part β)
      (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
          (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
            (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                match (motive := β ⊕ α → Part β) e : (f a).get hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' ⋯ :
              Part β))
          a' h :
        Part β)
      b

Tactic:
simp only [fix, Part.mem_assert_iff] at h₃

Premises used: PFun.fix, Part.mem_assert_iff
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ :
  ∃ (h : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a'),
    Membership.mem (γ := Part β)
      (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
          (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
            (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                match (motive := β ⊕ α → Part β) e : (f a).get hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' ⋯ :
              Part β))
          a' h :
        Part β)
      b
⊢ Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a'

Tactic:
obtain ⟨h₃, h₄⟩ := h₃
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ :
  ∃ (h : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a'),
    Membership.mem (γ := Part β)
      (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
          (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
            (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                match (motive := β ⊕ α → Part β) e : (f a).get hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' ⋯ :
              Part β))
          a' h :
        Part β)
      b
h₄ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a'
⊢ Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a' h₄ :
      Part β)
    b

Tactic:
obtain ⟨h₃, h₄⟩ := h₃
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a'
h₄ :
  Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a' h₃ :
      Part β)
    b
⊢ ∃ (h : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a),
    Membership.mem (γ := Part β)
      (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
          (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
            (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                match (motive := β ⊕ α → Part β) e : (f a).get hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' ⋯ :
              Part β))
          a h :
        Part β)
      b

Tactic:
⟨⟨_, fun y h' => ?_⟩, ?_⟩

Premises used: Exists.intro, Acc.intro
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a'
h₄ :
  Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a' h₃ :
      Part β)
    b
inr : ∀ (y : α) (h' : Sum.inr y ∈ f a), Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) y
inr₁ :
  Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a ⋯ :
      Part β)
    b
⊢ ∃ (h : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a),
    Membership.mem (γ := Part β)
      (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
          (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
            (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                match (motive := β ⊕ α → Part β) e : (f a).get hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' ⋯ :
              Part β))
          a h :
        Part β)
      b

Tactic:
refine ⟨⟨_, fun y h' => ?_⟩, ?_⟩
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a'
h₄ :
  Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a' h₃ :
      Part β)
    b
y : α
h' : Sum.inr y ∈ f a
⊢ a' = y

Tactic:
injection Part.mem_unique h h' with e

Premises used: Part.mem_unique
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a'
h₄ :
  Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a' h₃ :
      Part β)
    b
y : α
h' : Sum.inr y ∈ f a
e : a' = y
⊢ Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) y

Tactic:
e ▸ h₃

Premises used: Eq.rec
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a'
h₄ :
  Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a' h₃ :
      Part β)
    b
y : α
h' : Sum.inr y ∈ f a
e : a' = y
⊢ Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) y

Tactic:
exact e ▸ h₃
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a'
h₄ :
  Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a' h₃ :
      Part β)
    b
⊢ (f a).Dom

Tactic:
obtain ⟨h₁, h₂⟩ := h
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h : Sum.inr a' ∈ f a
h₃ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a'
h₄ :
  Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a' h₃ :
      Part β)
    b
h₁ : (f a).Dom
⊢ (f a).get h₁ = Sum.inr a'

Tactic:
obtain ⟨h₁, h₂⟩ := h
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
a' : α
h₃ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a'
h₄ :
  Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a' h₃ :
      Part β)
    b
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inr a'
⊢ Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a ⋯ :
      Part β)
    b

Tactic:
grind [WellFounded.fixF_eq]

Premises used: WellFounded.fixF_eq
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
b : β
a : α
hb : Sum.inl b ∈ f a
rw : Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
⊢ b ∈ f.fix a

Tactic:
rw [PFun.mem_fix_iff]

Premises used: PFun.mem_fix_iff
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
b : β
a : α
hb : Sum.inl b ∈ f a
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
Or.inl hb

Premises used: Or.inl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
b : β
a : α
hb : Sum.inl b ∈ f a
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
exact Or.inl hb

Premises used: Or.inl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
H : ∀ (b : β), b ∈ f.fix a ↔ b ∈ f.fix a'
⊢ f.fix a = f.fix a'

Tactic:
ext b
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
H : b ∈ f.fix a → b ∈ f.fix a'
H₁ : b ∈ f.fix a' → b ∈ f.fix a
⊢ b ∈ f.fix a ↔ b ∈ f.fix a'

Tactic:
constructor
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a
H : ∀ (h' : Sum.inl b ∈ f a), b ∈ f.fix a'
H₁ : ∀ (a_1 : α) (h' : Sum.inr a_1 ∈ f a) (e' : b ∈ f.fix a_1), b ∈ f.fix a'
⊢ b ∈ f.fix a'

Tactic:
obtain h' | ⟨a, h', e'⟩ := mem_fix_iff.1 h

Premises used: Iff.mp, PFun.mem_fix_iff
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a
h' : Sum.inl b ∈ f a
⊢ b ∈ f.fix a'

Tactic:
cases Part.mem_unique ha' h'

Premises used: Part.mem_unique
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a_1 a' : α
ha' : Sum.inr a' ∈ f a_1
b : β
h : b ∈ f.fix a_1
a : α
h' : Sum.inr a ∈ f a_1
e' : b ∈ f.fix a
⊢ Sum.inr a' ∈ f a_1

Tactic:
cases Part.mem_unique ha' h'

Premises used: Part.mem_unique
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a_1 a' : α
ha' : Sum.inr a' ∈ f a_1
b : β
h : b ∈ f.fix a_1
a : α
h' : Sum.inr a ∈ f a_1
e' : b ∈ f.fix a
h'₁ : Sum.inr a' ∈ f a_1
⊢ b ∈ f.fix a'

Tactic:
cases Part.mem_unique ha' h'

Premises used: Part.mem_unique
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a
h' : Sum.inr a' ∈ f a
e' : b ∈ f.fix a'
⊢ b ∈ f.fix a'

Tactic:
e'
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a
h' : Sum.inr a' ∈ f a
e' : b ∈ f.fix a'
⊢ b ∈ f.fix a'

Tactic:
exact e'
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a'
H : Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
⊢ b ∈ f.fix a

Tactic:
rw [PFun.mem_fix_iff]

Premises used: PFun.mem_fix_iff
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a'
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
Or.inr ⟨a', ha', h⟩

Premises used: And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
h : b ∈ f.fix a'
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
exact Or.inr ⟨a', ha', h⟩

Premises used: Or.inr
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
b : β
a a' : α
hb : b ∈ f.fix a
ha' : Sum.inr a' ∈ f a
rwa rwa₁ rwa₂ rwa₃ : b ∈ f.fix a
⊢ b ∈ f.fix a'

Tactic:
rwa [← fix_fwd_eq ha']

Premises used: PFun.fix_fwd_eq
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
have :
  (h₂ :
      Membership.mem (γ := Part β)
        (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
            (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
              (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
                  match (motive := β ⊕ α → Part β) e : (f a).get hf with
                  | Sum.inl b => Part.some b
                  | Sum.inr a' => IH a' ⋯ :
                Part β))
            a ⋯ :
          Part β)
        b) →
    C a
⊢ C a

Tactic:
have h₂ := (Part.mem_assert_iff.1 h).snd
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
h₂ :
  Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a ⋯ :
      Part β)
    b
⊢ ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a

Tactic:
generalize_proofs at h₂
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
h₂ :
  Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a ⋯ :
      Part β)
    b
pf : ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a
⊢ Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a

Tactic:
generalize_proofs at h₂
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
h₂ :
  Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a ⋯ :
      Part β)
    b
pf : ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a
pf₁ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a
⊢ Membership.mem (γ := Part β)
    (WellFounded.fixF (r := fun (x y : α) ↦ Sum.inr x ∈ f y) (C := fun (a : α) ↦ Part β)
        (fun (a : α) (IH : (y : α) → Sum.inr y ∈ f a → Part β) ↦
          (Part.assert (f a).Dom fun (hf : (f a).Dom) ↦
              match (motive := β ⊕ α → Part β) e : (f a).get hf with
              | Sum.inl b => Part.some b
              | Sum.inr a' => IH a' ⋯ :
            Part β))
        a pf₁ :
      Part β)
    b

Tactic:
generalize_proofs at h₂