awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
x x_1 : α ≃. β
x_2 : α
x_3 : β
pos :
  Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β) ((x_1 : (a : α) → Option β) x_2 : Option β) →
    (x : (a : α) → Option β) x_2 = some x_3 → (x_1 : (a : α) → Option β) x_2 = some x_3
⊢ (if
          Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β)
            ((x_1 : (a : α) → Option β) x_2 : Option β) then
        (x : (a : α) → Option β) x_2
      else none) =
      some x_3 →
    (x_1 : (a : α) → Option β) x_2 = some x_3
have neg : ¬Eq.{v + 1} (α := Option β) ((x : (a : α) → Option β) x_2 : Option β) ((x_1 : (a : α) → Option β) x_2 : Option β) →
  False → (x_1 : (a : α) → Option β) x_2 = some x_3
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.PEquiv (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
H : Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
⊢ Membership.mem (γ := Option β)
    (({
            toFun := fun (a : α) ↦
              if
                  Eq.{v + 1} (α := Option β) ((g : (a : α) → Option β) a : Option β)
                    ((h : (a : α) → Option β) a : Option β) then
                (g : (a : α) → Option β) a
              else none,
            invFun := fun (b : β) ↦
              if
                  Eq.{u + 1} (α := Option α) ((g.symm : (a : β) → Option α) b : Option α)
                    ((h.symm : (a : β) → Option α) b : Option α) then
                (g.symm : (a : β) → Option α) b
              else none,
            inv := ⋯ } :
          (a : α) → Option β)
        a :
      Option β)
    b
have hf : Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
Tactic: have hf := fg a b H
-- Lean 4 proof step from Mathlib.Data.PEquiv (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
H : Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
hf : Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
⊢ Membership.mem (γ := Option β)
    (({
            toFun := fun (a : α) ↦
              if
                  Eq.{v + 1} (α := Option β) ((g : (a : α) → Option β) a : Option β)
                    ((h : (a : α) → Option β) a : Option β) then
                (g : (a : α) → Option β) a
              else none,
            invFun := fun (b : β) ↦
              if
                  Eq.{u + 1} (α := Option α) ((g.symm : (a : β) → Option α) b : Option α)
                    ((h.symm : (a : β) → Option α) b : Option α) then
                (g.symm : (a : β) → Option α) b
              else none,
            inv := ⋯ } :
          (a : α) → Option β)
        a :
      Option β)
    b
have hg : Membership.mem (γ := Option β) ((h : (a : α) → Option β) a : Option β) b
Tactic: have hg := gh a b H
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
H : Membership.mem (γ := Option β) ((f : (a : α) → Option β) a : Option β) b
hf : Membership.mem (γ := Option β) ((g : (a : α) → Option β) a : Option β) b
hg : Membership.mem (γ := Option β) ((h : (a : α) → Option β) a : Option β) b
⊢ Membership.mem (γ := Option β)
    (({
            toFun := fun (a : α) ↦
              if
                  Eq.{v + 1} (α := Option β) ((g : (a : α) → Option β) a : Option β)
                    ((h : (a : α) → Option β) a : Option β) then
                (g : (a : α) → Option β) a
              else none,
            invFun := fun (b : β) ↦
              if
                  Eq.{u + 1} (α := Option α) ((g.symm : (a : β) → Option α) b : Option α)
                    ((h.symm : (a : β) → Option α) b : Option α) then
                (g.symm : (a : β) → Option α) b
              else none,
            inv := ⋯ } :
          (a : α) → Option β)
        a :
      Option β)
    b
have simp : ∀ (H : (f : (a : α) → Option β) a = some b) (hf : (g : (a : α) → Option β) a = some b)
  (hg : (h : (a : α) → Option β) a = some b),
  (if Eq.{v + 1} (α := Option β) ((g : (a : α) → Option β) a : Option β) ((h : (a : α) → Option β) a : Option β) then
      (g : (a : α) → Option β) a
    else none) =
    some b
Tactic: simp only [Option.mem_def, PEquiv.coe_mk_apply] at *
Cleared hypotheses: H, hf, hg
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
H : (f : (a : α) → Option β) a = some b
hf : (g : (a : α) → Option β) a = some b
hg : (h : (a : α) → Option β) a = some b
⊢ (if Eq.{v + 1} (α := Option β) ((g : (a : α) → Option β) a : Option β) ((h : (a : α) → Option β) a : Option β) then
      (g : (a : α) → Option β) a
    else none) =
    some b
have rw : (if some b = (h : (a : α) → Option β) a then some b else none) = some b
Tactic: rw [hf, hg, if_pos rfl]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
H : (f : (a : α) → Option β) a = some b
hf : (g : (a : α) → Option β) a = some b
hg : (h : (a : α) → Option β) a = some b
rw : (if some b = (h : (a : α) → Option β) a then some b else none) = some b
⊢ (if Eq.{v + 1} (α := Option β) ((g : (a : α) → Option β) a : Option β) ((h : (a : α) → Option β) a : Option β) then
      (g : (a : α) → Option β) a
    else none) =
    some b
have rw₁ : (if some b = some b then some b else none) = some b
Tactic: rw [hf, hg, if_pos rfl]
-- Lean 4 proof step from Mathlib.Data.PEquiv (goal)
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type x
inst : DecidableEq α
inst_1 : DecidableEq β
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
H : (f : (a : α) → Option β) a = some b
hf : (g : (a : α) → Option β) a = some b
hg : (h : (a : α) → Option β) a = some b
rw : (if some b = (h : (a : α) → Option β) a then some b else none) = some b
rw₁ : (if some b = some b then some b else none) = some b
⊢ (if Eq.{v + 1} (α := Option β) ((g : (a : α) → Option β) a : Option β) ((h : (a : α) → Option β) a : Option β) then
      (g : (a : α) → Option β) a
    else none) =
    some b
have rw₂ : some b = some b
Tactic: rw [hf, hg, if_pos rfl]
-- 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
x : (p : α → Prop) × (Subtype p → β)
p : α → Prop
f : Subtype p → β
⊢ Eq (α := (p : α → Prop) × (Subtype p → β))
    ((fun (f : α →. β) ↦
        (Sigma.mk (β := fun (p : α → Prop) ↦ Subtype p → β) (fun (a : α) ↦ (f a).Dom) f.asSubtype :
          (p : α → Prop) × (Subtype p → β)))
      ((fun (f : (p : α → Prop) × (Subtype p → β)) (x : α) ↦
          ({ Dom := f.fst (β := fun (p : α → Prop) ↦ Subtype p → β) x,
              get := fun (h : f.fst (β := fun (p : α → Prop) ↦ Subtype p → β) x) ↦
                f.snd (β := fun (p : α → Prop) ↦ Subtype p → β)
                  (Subtype.mk (p := f.fst (β := fun (p : α → Prop) ↦ Subtype p → β)) x h) } :
            Part β))
        (Sigma.mk (β := fun (p : α → Prop) ↦ Subtype p → β) p f)))
    (Sigma.mk (β := fun (p : α → Prop) ↦ Subtype p → β) p f)
have dsimp : Eq (α := (p : α → Prop) × (Subtype p → β))
  (Sigma.mk (β := fun (p : α → Prop) ↦ Subtype p → β) (fun (a : α) ↦ p a)
    (asSubtype fun (x : α) ↦ { Dom := p x, get := fun (h : p x) ↦ f (Subtype.mk (p := p) x h) } :
      (s :
          (↑(Dom.{u_1, u_2} (β := β) fun (x : α) ↦ { Dom := p x, get := fun (h : p x) ↦ f (Subtype.mk (p := p) x h) }) :
            Type u_1)) →
        β))
  (Sigma.mk (β := fun (p : α → Prop) ↦ Subtype p → β) p f)
Tactic: dsimp
-- 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
α_1 : Type u_7
f : α →. α_1
⊢ id <$> f = f
have h : ∀ (a : α), (id <$> f) a = f a
Tactic: funext a
-- 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
α_1 : Type u_7
f : α →. α_1
a : α
⊢ Part.map id (f a) = f a
have h : ∀ (Dom : Prop) (get : Dom → α_1), Part.map id { Dom := Dom, get := get : Part α_1 } = { Dom := Dom, get := get }
Tactic: cases f a
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
⊢ (f a).Dom
have h₁ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a
Tactic: let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
Goal:
α : 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
⊢ (f a).Dom
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: let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
Goal:
α : 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₂ :
  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
have h₃ : 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] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
Goal:
α : 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'
have h₁ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a
Tactic: let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
Goal:
α : 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
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix 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' sorry :
          Part β))
      a h₁ :
    Part β)
  b
Tactic: let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
Goal:
α : 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₂ :
  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
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
have h₃ : 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] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
Goal:
α : 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₂ :
  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
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
have h₃ : ∃ (h : (f a).Dom),
  Membership.mem (γ := Part β)
    (match (motive := β ⊕ α → Part β) e : (f a).get h with
      | Sum.inl b => Part.some b
      | Sum.inr 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 β))
          a' sorry :
      Part β)
    b
Tactic: simp only [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 : β
h : b ∈ f.fix a
h₁ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a
h₂ :
  ∃ (h : (f a).Dom),
    Membership.mem (γ := Part β)
      (match (motive := β ⊕ α → Part β) e : (f a).get h with
        | Sum.inl b => Part.some b
        | Sum.inr 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 β))
            a' ⋯ :
        Part β)
      b
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
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 : β
h : b ∈ f.fix a
h₁ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a
h₂ :
  ∃ (h : (f a).Dom),
    Membership.mem (γ := Part β)
      (match (motive := β ⊕ α → Part β) e : (f a).get h with
        | Sum.inl b => Part.some b
        | Sum.inr 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 β))
            a' ⋯ :
        Part β)
      b
h₃ : (f a).Dom
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
have h₄ : Membership.mem (γ := Part β)
  (match (motive := β ⊕ α → Part β) e : (f a).get h₃ with
    | Sum.inl b => Part.some b
    | Sum.inr 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 β))
        a' sorry :
    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 : β
h : b ∈ f.fix a
h₁ : Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a
h₂ : (f a).Dom
h₃ :
  Membership.mem (γ := Part β)
    (match (motive := β ⊕ α → Part β) e : (f a).get h₂ with
      | Sum.inl b => Part.some b
      | Sum.inr 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 β))
          a' ⋯ :
      Part β)
    b
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
have h_1 : ∀ (b_1 : β),
  (f a).get h₂ = Sum.inl b_1 → ∀ (h₃ : b ∈ Part.some b_1), Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
Tactic: split at h₃
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : 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
h₃ :
  Membership.mem (γ := Part β)
    (match (motive := β ⊕ α → Part β) e : (f a).get h₂ with
      | Sum.inl b => Part.some b
      | Sum.inr 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 β))
          a' ⋯ :
      Part β)
    b
h_1 :
  ∀ (b_1 : β),
    (f a).get h₂ = Sum.inl b_1 →
      ∀ (h₃ : b ∈ Part.some b_1), Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
have h_2 : ∀ (a' : α) (heq : (f a).get h₂ = Sum.inr 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' sorry :
              Part β))
          a' sorry :
        Part β)
      b),
  Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
Tactic: split at h₃
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.Data.PFun (hypothesis)
Goal:
α : 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_1 : β
e : (f a).get h₂ = Sum.inl b_1
h₃ : b ∈ Part.some b_1
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
have h₄ : b = b_1
Tactic: simp only [Part.mem_some_iff] at h₃
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.Data.PFun (goal)
Goal:
α : 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_1 : β
e : (f a).get h₂ = Sum.inl b_1
h₃ : b = b_1
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
have subst : ∀ (h : b_1 ∈ f.fix a), Sum.inl b_1 ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b_1 ∈ f.fix a'
Tactic: subst b
Cleared hypotheses: b, h, h₃
-- 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'
⊢ b ∈ f.fix a
have simp : ∃ (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]
-- 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'
⊢ ∃ (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 : ∀ (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' sorry :
              Part β))
          a h :
        Part β)
      b
Tactic: rcases h with (⟨h₁, h₂⟩ | ⟨a', h, h₃⟩)
Cleared hypotheses: h