awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
od : Prop
o : od → α
pd : Prop
p : pd → α
H1 : { Dom := od, get := o : Part α }.Dom ↔ { Dom := pd, get := p : Part α }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o : Part α }.Dom) (h₂ : { Dom := pd, get := p : Part α }.Dom),
    { Dom := od, get := o : Part α }.get h₁ = { Dom := pd, get := p }.get h₂
⊢ od = pd

Tactic:
have t : od = pd := propext H1
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
od : Prop
o : od → α
pd : Prop
p : pd → α
H1 : { Dom := od, get := o : Part α }.Dom ↔ { Dom := pd, get := p : Part α }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o : Part α }.Dom) (h₂ : { Dom := pd, get := p : Part α }.Dom),
    { Dom := od, get := o : Part α }.get h₁ = { Dom := pd, get := p }.get h₂
t : od = pd
refl :
  ∀ (p : od → α) (H1 : { Dom := od, get := o : Part α }.Dom ↔ { Dom := od, get := p : Part α }.Dom)
    (H2 :
      ∀ (h₁ : { Dom := od, get := o : Part α }.Dom) (h₂ : { Dom := od, get := p : Part α }.Dom),
        { Dom := od, get := o : Part α }.get h₁ = { Dom := od, get := p }.get h₂),
    { Dom := od, get := o : Part α } = { Dom := od, get := p }
⊢ { Dom := od, get := o : Part α } = { Dom := pd, get := p }

Tactic:
cases t
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
od : Prop
o p : od → α
H1 : { Dom := od, get := o : Part α }.Dom ↔ { Dom := od, get := p : Part α }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o : Part α }.Dom) (h₂ : { Dom := od, get := p : Part α }.Dom),
    { Dom := od, get := o : Part α }.get h₁ = { Dom := od, get := p }.get h₂
refl refl₁ : { Dom := od, get := p : Part α } = { Dom := od, get := p }
⊢ { Dom := od, get := o : Part α } = { Dom := od, get := p }

Tactic:
rw [show o = p from funext fun p => H2 p p]

Premises used: funext
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : α
o : Part α
⊢ (a ∈ o) = ∃ (h : o.Dom), o.get h = a

Tactic:
rfl

Premises used: Part.Mem, rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
h : o.Dom
⊢ o.get h ∈ o

Tactic:
⟨_, rfl⟩

Premises used: Part.Mem, Exists.intro, rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
p : Prop
o : p → α
a : α
⊢ a ∈ { Dom := p, get := o : Part α } ↔ ∃ (h : p), o h = a

Tactic:
Iff.rfl

Premises used: Part.Mem, Iff.rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o p : Part α
H : ∀ (a : α), a ∈ o ↔ a ∈ p
⊢ o = p

Tactic:
(ext' ⟨fun h => ((H _).1 ⟨h, rfl⟩).fst, fun h => ((H _).2 ⟨h, rfl⟩).fst⟩) fun _ _ =>
    ((H _).2 ⟨_, rfl⟩).snd

Premises used: Iff.mpr, Part.ext', Exists.fst, Part.get, Exists.snd, Iff.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : α
⊢ ¬Membership.mem (γ := Part α) none a

Tactic:
fun h => h.fst

Premises used: Exists.fst, Not
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : α
⊢ (some a).Dom

Tactic:
trivial

Premises used: trivial
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x : α
x_1 x_2 : Part α
ho : x_1.Dom
h : x_1.get ho = x
hp : x_2.Dom
h_1 : x_2.get hp = x
⊢ ∀ (h₁ : x_1.Dom) (h₂ : x_2.Dom), x_1.get h₁ = x_2.get h₂

Tactic:
simp [*]
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
⊢ Relator.LeftUnique fun (x1 : α) (x2 : Part α) ↦ x1 ∈ x2

Tactic:
fun _ _ _ =>
  mem_unique

Premises used: Relator.LeftUnique, Part.mem_unique
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
⊢ Relator.RightUnique fun (x1 : α) (x2 : Part α) ↦ x1 ∈ x2

Tactic:
fun _ _ _ =>
  mem_right_unique

Premises used: Part.mem_right_unique, Relator.RightUnique
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
a : α
h : a ∈ o
h' : o.Dom
⊢ o.get h' = a

Tactic:
mem_unique ⟨_, rfl⟩ h

Premises used: Exists.intro, rfl, Part.mem_unique
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
⊢ Set.Subsingleton.{u_1} (α := α) {a : α | a ∈ o}

Tactic:
fun _ ha _ hb =>
  mem_unique ha hb

Premises used: Set.Subsingleton, Part.mem_unique
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : α
ha : (some a).Dom
⊢ (some a).get ha = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : α
⊢ a ∈ some a

Tactic:
⟨trivial, rfl⟩

Premises used: Part.Mem, trivial, Exists.intro, rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a b : α
⊢ b ∈ some a ↔ b = a

Tactic:
⟨fun ⟨_, e⟩ => e.symm, fun e => ⟨trivial, e.symm⟩⟩

Premises used: _private.0.Part.mem_some_iff.match_1, trivial, Iff.intro, Exists.intro, Eq.symm, Eq
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : α
o : Part α
⊢ o = some a ↔ a ∈ o

Tactic:
⟨fun e => e.symm ▸ mem_some _, fun ⟨h, e⟩ => e ▸ ext' (iff_true_intro h) fun _ _ => rfl⟩

Premises used: Part.ext', Part.some, Eq.rec, Part.mem_some, _private.0.Part.eq_some_iff.match_1, Iff.intro, iff_true_intro, Eq.symm, Eq, rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
h : ∀ (a : α), ¬a ∈ o
⊢ ∀ (a : α), a ∈ o ↔ Membership.mem (γ := Part α) none a

Tactic:
simpa
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
⊢ o = none ↔ ¬o.Dom

Tactic:
⟨fun e => e.symm ▸ id, fun h => eq_none_iff.2 fun _ h' => h h'.fst⟩

Premises used: Iff.mpr, Eq.rec, Exists.fst, id, Part.eq_none_iff, Iff.intro, Eq.symm
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
⊢ ¬Dom.{u_1} (α := α) none

Tactic:
id

Premises used: id, Not
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x : α
h : some x = none
⊢ False

Tactic:
true_ne_false (congr_arg Dom h)

Premises used: congr_arg, Part.Dom, true_ne_false
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x : α
h : some x = none
⊢ False

Tactic:
exact true_ne_false (congr_arg Dom h)

Premises used: congr_arg, Part.Dom, true_ne_false
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x : α
⊢ none ≠ some x

Tactic:
(some_ne_none x).symm

Premises used: Part.some_ne_none, Ne.symm
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
mp : o ≠ none → ∃ (x : α), o = some x
mpr : (∃ (x : α), o = some x) → o ≠ none
⊢ o ≠ none ↔ ∃ (x : α), o = some x

Tactic:
constructor
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
mp : o.Dom → ∃ (x : α), o = some x
⊢ o ≠ none → ∃ (x : α), o = some x

Tactic:
rw [Ne, eq_none_iff', not_not]

Premises used: Classical.not_not, Part.eq_none_iff', Ne
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
⊢ o.Dom → ∃ (x : α), o = some x

Tactic:
fun h => ⟨o.get h, eq_some_iff.2 (get_mem h)⟩

Premises used: Iff.mpr, Part.eq_some_iff, Part.get_mem, Part.get, Exists.intro
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
⊢ o.Dom → ∃ (x : α), o = some x

Tactic:
exact fun h => ⟨o.get h, eq_some_iff.2 (get_mem h)⟩
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x : α
⊢ some x ≠ none

Tactic:
apply some_ne_none

Premises used: Part.some_ne_none
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
⊢ o = none ∨ ∃ (x : α), o = some x

Tactic:
or_iff_not_imp_left.2 ne_none_iff.1

Premises used: Iff.mpr, Part.ne_none_iff, Classical.or_iff_not_imp_left, Iff.mp
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) some

Tactic:
fun _ _ h =>
  congr_fun (eq_of_heq (Part.mk.inj h).2) trivial

Premises used: trivial, And.right, eq_of_heq, Function.Injective, congr_fun, Part.mk.inj
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a b : α
⊢ some a = some b ↔ a = b

Tactic:
some_injective.eq_iff

Premises used: Part.some_injective, Function.Injective.eq_iff
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : Part α
ha : a.Dom
⊢ some (a.get ha) = a

Tactic:
Eq.symm (eq_some_iff.2 ⟨ha, rfl⟩)

Premises used: Iff.mpr, Part.eq_some_iff, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : Part α
ha : a.Dom
b : α
h : a.get ha = b
⊢ a = some b

Tactic:
simp [h.symm]

Premises used: Eq.symm
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : Part α
ha : a.Dom
b : α
h : a = some b
⊢ a.get ha = b

Tactic:
simp [h]
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : Part α
ha : a.Dom
b : Part α
h : a = b
⊢ a.get ha = b.get ⋯

Tactic:
congr
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
a : α
h : o.Dom
⊢ o.get h = a ↔ a ∈ o

Tactic:
⟨fun H => ⟨h, H⟩, fun ⟨_, H⟩ => H⟩

Premises used: _private.0.Part.get_eq_iff_mem.match_1, Part.get, Iff.intro, Exists.intro, Eq
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
a : α
h : o.Dom
⊢ a = o.get h ↔ a ∈ o

Tactic:
eq_comm.trans (get_eq_iff_mem h)

Premises used: eq_comm, Part.get_eq_iff_mem, Iff.trans
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a b : Part α
ha : a.Dom
hb : b.Dom
hab : a.get ha = b.get hb
⊢ a = b

Tactic:
ext' (iff_of_true ha hb) fun _ _ => hab

Premises used: Part.ext', iff_of_true
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a b : Part α
ha : a.Dom
hb : b.Dom
⊢ a.get ha = b.get hb ↔ a = b

Tactic:
⟨eq_of_get_eq_get ha hb, get_eq_get_of_eq a ha⟩

Premises used: Part.get_eq_get_of_eq, Iff.intro, Part.eq_of_get_eq_get
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a b : Part α
ha : a.Dom
hb : a.get ha ∈ b
⊢ b.Dom

Tactic:
have hb' : b.Dom := Part.dom_iff_mem.mpr ⟨a.get ha, hb⟩
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a b : Part α
ha : a.Dom
hb : a.get ha ∈ b
hb' : b.Dom
rwa : ∀ (hb : a.get ha = b.get hb'), a = b
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hb : a = b), a = b
⊢ a = b

Tactic:
rwa [← eq_get_iff_mem hb', eq_iff_of_dom ha hb'] at hb

Premises used: Part.eq_iff_of_dom, Part.eq_get_iff_mem
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Decidable (Dom.{u_1} (α := α) none)
⊢ Eq.{u_1 + 1} (α := Option α) (toOption none) Option.none

Tactic:
dif_neg id

Premises used: id, dif_neg, Part.toOption
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : α
inst : Decidable (some a).Dom
⊢ (some a).toOption = Option.some a

Tactic:
dif_pos trivial

Premises used: trivial, dif_pos, Part.toOption
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : Part α
h : a.Dom
inst : Decidable a.Dom
d : α
⊢ a.getOrElse d = a.get h

Tactic:
dif_pos h

Premises used: dif_pos, Part.getOrElse
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : Part α
h : ¬a.Dom
inst : Decidable a.Dom
d : α
⊢ a.getOrElse d = d

Tactic:
dif_neg h

Premises used: dif_neg, Part.getOrElse
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
d : α
inst : Decidable (Dom.{u_1} (α := α) none)
⊢ getOrElse none d = d

Tactic:
none.getOrElse_of_not_dom not_none_dom d

Premises used: Part.none, Part.getOrElse_of_not_dom, Part.not_none_dom
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a d : α
inst : Decidable (some a).Dom
⊢ (some a).getOrElse d = a

Tactic:
(some a).getOrElse_of_dom (some_dom a) d

Premises used: Part.some, Part.getOrElse_of_dom, Part.some_dom
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
a : α
pos : ∀ (h : o.Dom), Membership.mem (γ := Option α) (if h : o.Dom then Option.some (o.get h) else Option.none) a ↔ a ∈ o
neg :
  ∀ (h : ¬o.Dom), Membership.mem (γ := Option α) (if h : o.Dom then Option.some (o.get h) else Option.none) a ↔ a ∈ o
⊢ Membership.mem (γ := Option α) (if h : o.Dom then Option.some (o.get h) else Option.none) a ↔ a ∈ o

Tactic:
by_cases h : o.Dom

Premises used: Part.Dom
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
a : α
h : o.Dom
⊢ Membership.mem (γ := Option α) (if h : o.Dom then Option.some (o.get h) else Option.none) a ↔ a ∈ o

Tactic:
simpa [h] using ⟨fun h => ⟨_, h⟩, fun ⟨_, h⟩ => h⟩
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
a : α
h : ¬o.Dom
neg : ¬a ∈ o
⊢ Membership.mem (γ := Option α) (if h : o.Dom then Option.some (o.get h) else Option.none) a ↔ a ∈ o

Tactic:
simp only [h, ↓reduceDIte, Option.mem_def, reduceCtorEq, false_iff]

Premises used: reduceCtorEq, reduceDIte, false_iff, Option.mem_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
a : α
h : ¬o.Dom
⊢ ¬a ∈ o

Tactic:
mt Exists.fst h

Premises used: mt, Exists.fst
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
a : α
h : ¬o.Dom
⊢ ¬a ∈ o

Tactic:
exact mt Exists.fst h

Premises used: mt, Exists.fst
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
a : α
rw : a ∈ o.toOption ↔ a ∈ o
rw₁ rw₂ : a ∈ o ↔ a ∈ o
⊢ o.toOption = Option.some a ↔ a ∈ o

Tactic:
rw [← Option.mem_def, mem_toOption]

Premises used: Part.mem_toOption, Option.mem_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
h : o.Dom
⊢ o.toOption = Option.some (o.get h)

Tactic:
dif_pos h

Premises used: dif_pos, Part.toOption
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : Part α
inst : Decidable a.Dom
⊢ a.toOption = Option.none ↔ ¬a.Dom

Tactic:
Ne.dite_eq_right_iff fun _ => Option.some_ne_none _

Premises used: Ne.dite_eq_right_iff, Part.get, Option.some_ne_none, Part.toOption
-- Module: Mathlib.Data.Part
Goal:
α : Type u_4
β : Type u_5
a : Part α
inst : Decidable a.Dom
b : β
f : α → β
pos : ∀ (h : a.Dom), a.toOption.elim b f = f (a.get h)
neg : ∀ (h : ¬a.Dom), a.toOption.elim b f = b
⊢ a.toOption.elim b f = if h : a.Dom then f (a.get h) else b

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Part
Goal:
α : Type u_4
β : Type u_5
a : Part α
inst : Decidable a.Dom
b : β
f : α → β
h : a.Dom
pos : (Option.some (a.get h)).elim b f = f (a.get h)
⊢ a.toOption.elim b f = f (a.get h)

Tactic:
rw [h.toOption]

Premises used: Part.Dom.toOption
-- Module: Mathlib.Data.Part
Goal:
α : Type u_4
β : Type u_5
a : Part α
inst : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ (Option.some (a.get h)).elim b f = f (a.get h)

Tactic:
rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_4
β : Type u_5
a : Part α
inst : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
neg : Option.elim Option.none b f = b
⊢ a.toOption.elim b f = b

Tactic:
rw [Part.toOption_eq_none_iff.2 h]

Premises used: Iff.mpr, Part.toOption_eq_none_iff
-- Module: Mathlib.Data.Part
Goal:
α : Type u_4
β : Type u_5
a : Part α
inst : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ Option.elim Option.none b f = b

Tactic:
rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_4
⊢ Dom.{u_4} (α := α) (↑Option.none : Part α) ↔ Option.isSome.{u_4} (α := α) Option.none = true

Tactic:
simp [ofOption, none]

Premises used: Part.none, Part.ofOption
-- Module: Mathlib.Data.Part
Goal:
α : Type u_4
a : α
⊢ (↑(Option.some a) : Part α).Dom ↔ (Option.some a).isSome = true

Tactic:
simp [ofOption]

Premises used: Part.ofOption
-- Module: Mathlib.Data.Part
Goal:
α : Type u_4
o : Option α
h₁ : (↑o : Part α).Dom
h₂ : { Dom := o.isSome = true, get := o.get : Part α }.Dom
none :
  ∀ (h₁ : Dom.{u_4} (α := α) (↑Option.none : Part α))
    (h₂ : Dom.{u_4} (α := α) { Dom := Option.isSome.{u_4} (α := α) Option.none = true, get := Option.get Option.none }),
    get (↑Option.none : Part α) h₁ =
      get { Dom := Option.isSome.{u_4} (α := α) Option.none = true, get := Option.get Option.none } h₂
some :
  ∀ (val : α) (h₁ : (↑(Option.some val) : Part α).Dom)
    (h₂ : { Dom := (Option.some val).isSome = true, get := (Option.some val).get : Part α }.Dom),
    (↑(Option.some val) : Part α).get h₁ =
      { Dom := (Option.some val).isSome = true, get := (Option.some val).get }.get h₂
⊢ (↑o : Part α).get h₁ = { Dom := o.isSome = true, get := o.get }.get h₂

Tactic:
cases o
-- Module: Mathlib.Data.Part
Goal:
α : Type u_4
h₁ : Dom.{u_4} (α := α) (↑Option.none : Part α)
h₂ : Dom.{u_4} (α := α) { Dom := Option.isSome.{u_4} (α := α) Option.none = true, get := Option.get Option.none }
⊢ get (↑Option.none : Part α) h₁ =
    get { Dom := Option.isSome.{u_4} (α := α) Option.none = true, get := Option.get Option.none } h₂

Tactic:
simp at h₂
-- Module: Mathlib.Data.Part
Goal:
α : Type u_4
val : α
h₁ : (↑(Option.some val) : Part α).Dom
h₂ : { Dom := (Option.some val).isSome = true, get := (Option.some val).get : Part α }.Dom
⊢ (↑(Option.some val) : Part α).get h₁ = { Dom := (Option.some val).isSome = true, get := (Option.some val).get }.get h₂

Tactic:
rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : α
o : Option α
⊢ a ∈ (↑o : Part α) ↔ a ∈ o

Tactic:
mem_ofOption

Premises used: Part.mem_ofOption
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Part α) (↑Option.none : Part α) none

Tactic:
rfl

Premises used: rfl, Part.ofOption
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : α
⊢ (↑(Option.some a) : Part α) = some a

Tactic:
rfl

Premises used: rfl, Part.ofOption
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
P : Part α → Prop
a : Part α
hnone : P none
hsome : ∀ (a : α), P (some a)
⊢ P a

Tactic:
(Classical.em a.Dom).elim (fun h => Part.some_get h ▸ hsome _) fun h =>
    (eq_none_iff'.2 h).symm ▸ hnone

Premises used: Iff.mpr, Eq.rec, Part.eq_none_iff', Part.get, Part.some_get, Classical.em, Part.Dom, Or.elim, Eq.symm
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Option α
none : Eq.{u_1 + 1} (α := Option α) (toOption (↑Option.none : Part α)) Option.none
some : ∀ (val : α), (↑(Option.some val) : Part α).toOption = Option.some val
⊢ (↑o : Part α).toOption = o

Tactic:
cases o
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Option α) (toOption (↑Option.none : Part α)) Option.none

Tactic:
rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
val : α
⊢ (↑(Option.some val) : Part α).toOption = Option.some val

Tactic:
rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
o : Part α
inst : Decidable o.Dom
⊢ (↑o.toOption : Part α) = o

Tactic:
ext fun _ => mem_ofOption.trans mem_toOption

Premises used: Part.mem_ofOption, Part.mem_toOption, Part.ext, Iff.trans
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
this : (p : Prop) → Decidable p
o : Option α
⊢ (↑o : Part α).toOption = (↑o : Part α).toOption

Tactic:
congr
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
inl : ∀ (h : x = none), x ≤ y ∨ y ≤ x
inr : ∀ (b : α) (h₀ : x = some b), x ≤ y ∨ y ≤ x
⊢ x ≤ y ∨ y ≤ x

Tactic:
rcases Part.eq_none_or_eq_some x with (h | ⟨b, h₀⟩)

Premises used: Part.eq_none_or_eq_some
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
inl : none ≤ y ∨ y ≤ none
⊢ x ≤ y ∨ y ≤ x

Tactic:
rw [h]
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
inl : none ≤ y
⊢ none ≤ y ∨ y ≤ none

Tactic:
left
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
h : x = none
⊢ none ≤ y

Tactic:
apply OrderBot.bot_le _

Premises used: OrderBot.bot_le
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
inr : y ≤ x
⊢ x ≤ y ∨ y ≤ x

Tactic:
right
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
b' : α
h₁ : b' ∈ y
inr : ∀ (h₀ : b ∈ x) (b' : α) (h₁ : b' ∈ y), b' ∈ x
⊢ b' ∈ x

Tactic:
rw [Part.eq_some_iff] at h₀

Premises used: Part.eq_some_iff
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
⊢ b ∈ z

Tactic:
have hx := hx _ h₀
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x y z : Part α
hx_1 : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
⊢ b' ∈ z

Tactic:
have hy := hy _ h₁
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x y z : Part α
hx_1 : x ≤ z
hy_1 : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
hy : b' ∈ z
⊢ b = b'

Tactic:
have hx := Part.mem_unique hx hy
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x y z : Part α
hx_1 : x ≤ z
hy_1 : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx_2 : b ∈ z
hy : b' ∈ z
hx : b = b'
inr : ∀ (h₁ : b ∈ y) (hy : b ∈ z), b ∈ x
⊢ b' ∈ x

Tactic:
subst hx
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x y z : Part α
hx_1 : x ≤ z
hy_1 : y ≤ z
b : α
h₀ : b ∈ x
hx : b ∈ z
h₁ : b ∈ y
hy : b ∈ z
⊢ b ∈ x

Tactic:
h₀
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x y z : Part α
hx_1 : x ≤ z
hy_1 : y ≤ z
b : α
h₀ : b ∈ x
hx : b ∈ z
h₁ : b ∈ y
hy : b ∈ z
⊢ b ∈ x

Tactic:
exact h₀
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
f : α → β
o : Part α
b : β
⊢ b ∈ map f o ↔ ∃ (a : α), a ∈ o ∧ f a = b

Tactic:
⟨fun hb => match b, hb with
    | _, ⟨_, rfl⟩ => ⟨_, ⟨_, rfl⟩, rfl⟩,
    fun ⟨_, h₁, h₂⟩ => h₂ ▸ mem_map f h₁⟩

Premises used: Membership.mem, Exists, Eq.rec, Part.get, And, And.intro, Iff.intro, Exists.intro, Part.mem_map, Eq, _private.0.Part.mem_map_iff.match_2, rfl, _private.0.Part.mem_map_iff.match_1, Part.map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : β
⊢ ¬a ∈ map f none

Tactic:
simp
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ map f (some a) = some (f a)

Tactic:
eq_some_iff.2 <| mem_map f <| mem_some _

Premises used: Iff.mpr, Part.eq_some_iff, Part.mem_some, Part.mem_map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
p : Prop
f : p → Part α
a : α
⊢ a ∈ assert p f ↔ ∃ (h : p), a ∈ f h

Tactic:
⟨fun ha => match a, ha with
    | _, ⟨_, rfl⟩ => ⟨_, ⟨_, rfl⟩⟩,
    fun ⟨_, h⟩ => mem_assert _ h⟩

Premises used: _private.0.Part.mem_assert_iff.match_2, _private.0.Part.mem_assert_iff.match_1, Part.assert._proof_1, Membership.mem, Exists, Part.assert._proof_2, Part.assert, Iff.intro, Exists.intro, Part.mem_assert, rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
p : Prop
f : p → Part α
h : p
H : ∀ (a : α), a ∈ assert p f ↔ a ∈ f h
⊢ assert p f = f h

Tactic:
ext
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
p : Prop
f : p → Part α
h : p
a : α
⊢ a ∈ assert p f ↔ a ∈ f h

Tactic:
simp_all
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
p : Prop
f : p → Part α
h : ¬p
H : ∀ (a : α), a ∈ assert p f ↔ Membership.mem (γ := Part α) none a
⊢ assert p f = none

Tactic:
ext
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
p : Prop
f : p → Part α
h : ¬p
a : α
⊢ a ∈ assert p f ↔ Membership.mem (γ := Part α) none a

Tactic:
simp_all
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
f : Part α
g : α → Part β
b : β
⊢ b ∈ f.bind g ↔ ∃ (a : α), a ∈ f ∧ b ∈ g a

Tactic:
⟨fun hb => match b, hb with
    | _, ⟨⟨_, _⟩, rfl⟩ => ⟨_, ⟨_, rfl⟩, ⟨_, rfl⟩⟩,
    fun ⟨_, h₁, h₂⟩ => mem_bind h₁ h₂⟩

Premises used: Part.bind, Part.assert._proof_1, Membership.mem, Exists, Part.get, _private.0.Part.mem_bind_iff.match_2, And, Part.assert._proof_2, And.intro, Iff.intro, Exists.intro, _private.0.Part.mem_bind_iff.match_1, Part.Dom, Part.mem_bind, rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
H : ∀ (b : β), b ∈ o.bind f ↔ b ∈ f (o.get h)
⊢ o.bind f = f (o.get h)

Tactic:
ext b
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
H : (∃ (a : α), a ∈ o ∧ b ∈ f a) ↔ b ∈ f (o.get h)
⊢ b ∈ o.bind f ↔ b ∈ f (o.get h)

Tactic:
simp only [Part.mem_bind_iff]

Premises used: Part.mem_bind_iff
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ (a : α), a ∈ o ∧ b ∈ f a) ↔ b ∈ f (o.get h)

Tactic:
⟨?_, fun hb => ⟨o.get h, Part.get_mem _, hb⟩⟩

Premises used: Part.get_mem, Part.get, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
H : (∃ (a : α), a ∈ o ∧ b ∈ f a) → b ∈ f (o.get h)
⊢ (∃ (a : α), a ∈ o ∧ b ∈ f a) ↔ b ∈ f (o.get h)

Tactic:
refine ⟨?_, fun hb => ⟨o.get h, Part.get_mem _, hb⟩⟩
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
a : α
ha : a ∈ o
hb H H₁ H₂ H₃ : b ∈ f a
⊢ b ∈ f (o.get h)

Tactic:
rwa [Part.get_eq_of_mem ha]

Premises used: Part.get_eq_of_mem
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
f : α → Part β
a : Part α
h : (a.bind f).Dom
⊢ a.Dom

Tactic:
h.1
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
f : α → Part β
a : β
⊢ ¬a ∈ Part.bind none f

Tactic:
simp
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → Part β
⊢ ∀ (a_1 : β), a_1 ∈ (some a).bind f ↔ a_1 ∈ f a

Tactic:
simp
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
o : Part α
a : α
h : a ∈ o
f : α → Part β
rw : (some a).bind f = f a
rw₁ rw₂ : f a = f a
⊢ o.bind f = f a

Tactic:
rw [eq_some_iff.2 h, bind_some]

Premises used: Iff.mpr, Part.eq_some_iff, Part.bind_some
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : Part α
⊢ ∀ (a : β), Membership.mem (γ := Part β) (x.bind fun (y : α) ↦ some (f y)) a ↔ a ∈ map f x

Tactic:
simp [eq_comm]

Premises used: eq_comm