awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f g : α →. β
H1 : ∀ (a : α), a ∈ f.Dom ↔ a ∈ g.Dom
H2 : ∀ (a : α) (p : a ∈ f.Dom) (q : a ∈ g.Dom), f.fn a p = g.fn a q
⊢ f = g

Tactic:
funext fun a => Part.ext' (H1 a) (H2 a)

Premises used: Part.ext', PFun, funext
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f g : α →. β
H : ∀ (a : α) (b : β), b ∈ f a ↔ b ∈ g a
⊢ f = g

Tactic:
funext fun a => Part.ext (H a)

Premises used: PFun, Part.ext, funext
-- Module: Mathlib.Data.PFun
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 → β
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)
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.Data.PFun
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 → β))
    (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:
congr
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
x : α
y : β
fxy : y ∈ f x
domx : x ∈ f.Dom
⊢ f.asSubtype (Subtype.mk (p := fun (x : α) ↦ x ∈ f.Dom) x domx) = y

Tactic:
Part.mem_unique (Part.get_mem _) fxy

Premises used: Part.get_mem, Part.mem_unique
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ (↑f : α →. β) a = Part.some (f a)

Tactic:
rfl

Premises used: PFun.lift, rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ (↑f : α →. β).Dom = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
⊢ Injective (α := α → β) PFun.lift

Tactic:
fun _ _ h =>
  funext fun a => Part.some_injective <| congr_fun h a

Premises used: Part.some_injective, funext, Function.Injective, congr_fun
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
s : Set α
h : s ⊆ f.Dom
a : α
b : β
⊢ b ∈ f.restrict (p := s) h a ↔ a ∈ s ∧ b ∈ f a

Tactic:
simp [restrict]

Premises used: PFun.restrict
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
b : β
⊢ b ∈ res f s a ↔ a ∈ s ∧ f a = b

Tactic:
simp [res, @eq_comm _ b]

Premises used: PFun.res, eq_comm
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ res f Set.univ = (↑f : α →. β)

Tactic:
rfl

Premises used: PFun.res, Set.Mem, PFun.restrict, Set.univ, setOf, Part.restrict, PFun.lift, rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β
x : α
⊢ x ∈ f.Dom ↔ ∃ (y : β), (x, y) ∈ f.graph

Tactic:
Part.dom_iff_mem

Premises used: Part.Mem, PFun.graph, Set.Mem, setOf, Part.dom_iff_mem, PFun.Dom
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
b : β
⊢ (∃ (x : True), f a = b) ↔ f a = b

Tactic:
simp
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α →. β
g : β → α →. γ
a : α
⊢ f.bind g a = (f a).bind fun (b : β) ↦ g b a

Tactic:
rfl

Premises used: PFun.bind, rfl
-- Module: Mathlib.Data.PFun
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
h : ∀ (a : α), (id <$> f) a = f a
⊢ id <$> f = f

Tactic:
funext a
-- Module: Mathlib.Data.PFun
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 : α
h : ∀ (Dom : Prop) (get : Dom → α_1), Part.map id { Dom := Dom, get := get : Part α_1 } = { Dom := Dom, get := get }
⊢ Part.map id (f a) = f a

Tactic:
cases f a
-- Module: Mathlib.Data.PFun
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 : α
Dom : Prop
get : Dom → α_1
⊢ Part.map id { Dom := Dom, get := get : Part α_1 } = { Dom := Dom, get := get }

Tactic:
rfl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
p : Set α
x : β
⊢ p ⊆ Dom (PFun.pure x)

Tactic:
p.subset_univ

Premises used: Set.subset_univ, setOf, PFun.Dom
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_7
β γ : Type u_8
p : Set α
f : α →. β
g : β → α →. γ
H1 : p ⊆ f.Dom
H2 : ∀ (x : β), p ⊆ (g x).Dom
⊢ p ⊆ (f >>= g).Dom

Tactic:
fun a ha =>
  (⟨H1 ha, H2 _ ha⟩ : a ∈ (f >>= g).Dom)

Premises used: Set.Mem, setOf, Part.get, Set.Subset, Exists.intro, PFun.Dom
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
⊢ Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) a

Tactic:
let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h
-- Module: Mathlib.Data.PFun
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
⊢ 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:
let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h
-- Module: Mathlib.Data.PFun
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
⊢ 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:
rw [WellFounded.fixF_eq] at h₂

Premises used: WellFounded.fixF_eq
-- Module: Mathlib.Data.PFun
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
⊢ (f a).Dom

Tactic:
h₂.fst.fst

Premises used: Exists.fst
-- Module: Mathlib.Data.PFun
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
⊢ (f a).Dom

Tactic:
exact h₂.fst.fst

Premises used: Exists.fst
-- Module: Mathlib.Data.PFun
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
⊢ ∃ (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

Tactic:
simp only [Part.mem_assert_iff] at h₂

Premises used: Part.mem_assert_iff
-- Module: Mathlib.Data.PFun
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
⊢ (f a).Dom

Tactic:
obtain ⟨h₂, h₃⟩ := h₂
-- Module: Mathlib.Data.PFun
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
⊢ 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

Tactic:
obtain ⟨h₂, h₃⟩ := h₂
-- Module: Mathlib.Data.PFun
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'
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' ⋯ :
                Part β))
            a' ⋯ :
          Part β)
        b),
    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'

Tactic:
split at h₃
-- Module: Mathlib.Data.PFun
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
⊢ b = b_1

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

Premises used: Part.mem_some_iff
-- Module: Mathlib.Data.PFun
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
subst : ∀ (h : b_1 ∈ f.fix a), Sum.inl b_1 ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b_1 ∈ f.fix a'
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
subst b
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
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 ∈ f.fix a
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
Or.inl ⟨h₂, e⟩

Premises used: Exists.intro, Or.inl
-- Module: Mathlib.Data.PFun
Goal:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
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 ∈ f.fix a
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
exact Or.inl ⟨h₂, e⟩

Premises used: Or.inl
-- Module: Mathlib.Data.PFun
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 : β
heq : (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:
next e => simp only [Part.mem_some_iff] at h₃; subst b; exact Or.inl ⟨h₂, e⟩

Premises used: Part.mem_some_iff, Or.inl
-- Module: Mathlib.Data.PFun
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
a' : α
e : (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' ⋯ :
            Part β))
        a' ⋯ :
      Part β)
    b
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
Or.inr ⟨_, ⟨_, e⟩, Part.mem_assert _ h₃⟩

Premises used: And.intro, Exists.intro, Part.mem_assert, Or.inr
-- Module: Mathlib.Data.PFun
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
a' : α
e : (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' ⋯ :
            Part β))
        a' ⋯ :
      Part β)
    b
⊢ Sum.inl b ∈ f a ∨ ∃ (a' : α), Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
exact Or.inr ⟨_, ⟨_, e⟩, Part.mem_assert _ h₃⟩

Premises used: Or.inr
-- Module: Mathlib.Data.PFun
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'
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' ⋯ :
              Part β))
          a h :
        Part β)
      b
⊢ b ∈ f.fix a

Tactic:
simp only [fix, Part.mem_assert_iff]

Premises used: PFun.fix, Part.mem_assert_iff
-- Module: Mathlib.Data.PFun
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
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' ⋯ :
                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:
rcases h with (⟨h₁, h₂⟩ | ⟨a', h, 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
⊢ ∃ (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 : β
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
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' ⋯ :
            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 : β
h₁ : (f a).Dom
h₂ : (f a).get h₁ = Sum.inl b
y : α
h' : Sum.inr y ∈ f a
⊢ Acc (fun (x y : α) ↦ Sum.inr x ∈ f y) y

Tactic:
injection Part.mem_unique ⟨h₁, h₂⟩ h'

Premises used: Exists.intro, Part.mem_unique