awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : 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'
inl :
  ∀ (h₁ : (f a).Dom) (h₂ : (f a).get h₁ = Sum.inl 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
⊢ ∃ (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
have inr : ∀ (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' sorry :
              Part β))
          a h :
        Part β)
      b
Tactic: rcases h with (⟨h₁, h₂⟩ | ⟨a', h, h₃⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : 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),
    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
have inl : ∀ (y : α) (h' : Sum.inr y ∈ f a), Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) y
Tactic: refine ⟨⟨_, fun y h' => ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
inl : ∀ (y : α) (h' : Sum.inr y ∈ f a), Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) y
⊢ ∃ (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
have inl₁ : 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' sorry :
          Part β))
      a sorry :
    Part β)
  b
Tactic: refine ⟨⟨_, fun y h' => ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl 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
have 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' sorry :
                  Part β))
              y sorry :
            Part β))
        a' sorry)
  b
Tactic: rw [WellFounded.fixF_eq]
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl 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
have 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' sorry :
                  Part β))
              y sorry :
            Part β))
        a' sorry :
    Part β)
  b
Tactic: apply Part.mem_assert h₁
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl 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
have h_1 : ∀ (b_1 : β), (f a).get h₁ = Sum.inl b_1 → b ∈ Part.some b_1
Tactic: split
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
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
⊢ 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
have 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' sorry :
                Part β))
            y sorry :
          Part β))
      a' sorry)
    b
Tactic: split
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
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 ∈ Part.some b_1
have h : b = b_1
Tactic: injection h₂.symm.trans e with h
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
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
have 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' sorry :
            Part β))
        a' h :
      Part β)
    b
Tactic: simp only [fix, Part.mem_assert_iff] at h₃
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
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
have h₄ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a'
Tactic: obtain ⟨h₃, h₄⟩ := h₃
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
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'
⊢ ∃ (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
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' sorry :
          Part β))
      a' h₄ :
    Part β)
  b
Tactic: obtain ⟨h₃, h₄⟩ := h₃
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
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
have inr : ∀ (y : α) (h' : Sum.inr y ∈ f a), Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) y
Tactic: refine ⟨⟨_, fun y h' => ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
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
⊢ ∃ (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
have 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' sorry :
          Part β))
      a sorry :
    Part β)
  b
Tactic: refine ⟨⟨_, fun y h' => ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
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
⊢ Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) y
have e : a' = y
Tactic: injection Part.mem_unique h h' with e
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
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
⊢ 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
have h₁ : (f a).Dom
Tactic: obtain ⟨h₁, h₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
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
⊢ 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
have h₂ : (f a).get h₁ = Sum.inr a'
Tactic: obtain ⟨h₁, h₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
b : β
a : α
hb : Sum.inl b ∈ f a
⊢ b ∈ f.fix a
have rw : Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
Tactic: rw [PFun.mem_fix_iff]
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
⊢ f.fix a = f.fix a'
have H : ∀ (b : β), b ∈ f.fix a ↔ b ∈ f.fix a'
Tactic: ext b
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ f.fix a ↔ b ∈ f.fix a'
have H : b ∈ f.fix a → b ∈ f.fix a'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
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'
⊢ b ∈ f.fix a ↔ b ∈ f.fix a'
have H₁ : b ∈ f.fix a' → b ∈ f.fix a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
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'
have H : ∀ (h' : Sum.inl b ∈ f a), b ∈ f.fix a'
Tactic: obtain h' | ⟨a, h', e'⟩ := mem_fix_iff.1 h
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
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'
⊢ b ∈ f.fix a'
have H₁ : ∀ (a_1 : α) (h' : Sum.inr a_1 ∈ f a) (e' : b ∈ f.fix a_1), b ∈ f.fix a'
Tactic: obtain h' | ⟨a, h', e'⟩ := mem_fix_iff.1 h
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
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
have H : Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
Tactic: rw [PFun.mem_fix_iff]
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
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'
⊢ C a
have 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' sorry :
              Part β))
          a sorry :
        Part β)
      b) →
  C a
Tactic: have h₂ := (Part.mem_assert_iff.1 h).snd
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
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
⊢ C a
have pf : ∀ (a : α) (hf : (f a).Dom) (a' : α) (e : (f a).get hf = Sum.inr a'), Sum.inr a' ∈ f a
Tactic: generalize_proofs at h₂
Cleared hypotheses: h₂