awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst : Decidable o.Dom
inst_1 : (a : α) → Decidable (f a).Dom
inst_2 : Decidable (o.bind f).Dom
pos : ∀ (h : o.Dom), (o.bind f).toOption = o.toOption.elim Option.none fun (a : α) ↦ (f a).toOption
neg : ∀ (h : ¬o.Dom), (o.bind f).toOption = o.toOption.elim Option.none fun (a : α) ↦ (f a).toOption
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun (a : α) ↦ (f a).toOption

Tactic:
by_cases h : o.Dom

Premises used: Part.Dom
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst : Decidable o.Dom
inst_1 : (a : α) → Decidable (f a).Dom
inst_2 : Decidable (o.bind f).Dom
h : o.Dom
pos : (f (o.get h)).toOption = (Option.some (o.get h)).elim Option.none fun (a : α) ↦ (f a).toOption
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun (a : α) ↦ (f a).toOption

Tactic:
simp_rw [h.toOption, h.bind]

Premises used: Part.Dom.bind, Part.Dom.toOption
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst : Decidable o.Dom
inst_1 : (a : α) → Decidable (f a).Dom
inst_2 : Decidable (o.bind f).Dom
h : o.Dom
⊢ (f (o.get h)).toOption = (Option.some (o.get h)).elim Option.none fun (a : α) ↦ (f a).toOption

Tactic:
rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst : Decidable o.Dom
inst_1 : (a : α) → Decidable (f a).Dom
inst_2 : Decidable (o.bind f).Dom
h : ¬o.Dom
neg : (o.bind f).toOption = Option.elim Option.none Option.none fun (a : α) ↦ (f a).toOption
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun (a : α) ↦ (f a).toOption

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_1
β : Type u_2
f : α → Part β
o : Part α
inst : Decidable o.Dom
inst_1 : (a : α) → Decidable (f a).Dom
inst_2 : Decidable (o.bind f).Dom
h : ¬o.Dom
⊢ (o.bind f).toOption = Option.elim Option.none Option.none fun (a : α) ↦ (f a).toOption

Tactic:
Part.toOption_eq_none_iff.2 fun ho => h ho.of_bind

Premises used: Iff.mpr, Part.toOption_eq_none_iff, Part.Dom.of_bind
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst : Decidable o.Dom
inst_1 : (a : α) → Decidable (f a).Dom
inst_2 : Decidable (o.bind f).Dom
h : ¬o.Dom
⊢ (o.bind f).toOption = Option.elim Option.none Option.none fun (a : α) ↦ (f a).toOption

Tactic:
exact Part.toOption_eq_none_iff.2 fun ho => h ho.of_bind

Premises used: Iff.mpr, Part.toOption_eq_none_iff, Part.Dom.of_bind
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_4
f : Part α
g : α → Part β
k : β → Part γ
a : γ
simp :
  (∃ (a_1 : β), (∃ (a : α), a ∈ f ∧ a_1 ∈ g a) ∧ a ∈ k a_1) ↔
    ∃ (a_1 : α), a_1 ∈ f ∧ ∃ (a_2 : β), a_2 ∈ g a_1 ∧ a ∈ k a_2
⊢ a ∈ (f.bind g).bind k ↔ Membership.mem (γ := Part γ) (f.bind fun (x : α) ↦ (g x).bind k) a

Tactic:
simp only [mem_bind_iff]

Premises used: Part.mem_bind_iff
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_4
f : Part α
g : α → Part β
k : β → Part γ
a : γ
⊢ (∃ (a_1 : β), (∃ (a : α), a ∈ f ∧ a_1 ∈ g a) ∧ a ∈ k a_1) ↔
    ∃ (a_1 : α), a_1 ∈ f ∧ ∃ (a_2 : β), a_2 ∈ g a_1 ∧ a ∈ k a_2

Tactic:
⟨fun ⟨_, ⟨_, h₁, h₂⟩, h₃⟩ => ⟨_, h₁, _, h₂, h₃⟩,
           fun ⟨_, h₁, _, h₂, h₃⟩ => ⟨_, ⟨_, h₁, h₂⟩, h₃⟩⟩

Premises used: _private.0.Part.bind_assoc.match_2, Membership.mem, Exists, _private.0.Part.bind_assoc.match_1, And, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_4
f : Part α
g : α → Part β
k : β → Part γ
a : γ
⊢ (∃ (a_1 : β), (∃ (a : α), a ∈ f ∧ a_1 ∈ g a) ∧ a ∈ k a_1) ↔
    ∃ (a_1 : α), a_1 ∈ f ∧ ∃ (a_2 : β), a_2 ∈ g a_1 ∧ a ∈ k a_2

Tactic:
exact ⟨fun ⟨_, ⟨_, h₁, h₂⟩, h₃⟩ => ⟨_, h₁, _, h₂, h₃⟩,
           fun ⟨_, h₁, _, h₂, h₃⟩ => ⟨_, ⟨_, h₁, h₂⟩, h₃⟩⟩
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
rw : Eq.{u_4 + 1} (α := Part γ) (x.bind fun (x : α) ↦ (some (f x)).bind g) (x.bind fun (y : α) ↦ g (f y))
⊢ (map f x).bind g = x.bind fun (y : α) ↦ g (f y)

Tactic:
rw [← bind_some_eq_map, bind_assoc]

Premises used: Part.bind_some_eq_map, Part.bind_assoc
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → β
x : Part α
g : β → Part γ
⊢ Eq.{u_4 + 1} (α := Part γ) (x.bind fun (x : α) ↦ (some (f x)).bind g) (x.bind fun (y : α) ↦ g (f y))

Tactic:
simp
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
rw :
  Eq.{u_4 + 1} (α := Part γ) (x.bind fun (x : α) ↦ (f x).bind fun (y : β) ↦ some (g y))
    (x.bind fun (y : α) ↦ map g (f y))
⊢ map g (x.bind f) = x.bind fun (y : α) ↦ map g (f y)

Tactic:
rw [← bind_some_eq_map, bind_assoc]

Premises used: Part.bind_some_eq_map, Part.bind_assoc
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ Eq.{u_4 + 1} (α := Part γ) (x.bind fun (x : α) ↦ (f x).bind fun (y : β) ↦ some (g y))
    (x.bind fun (y : α) ↦ map g (f y))

Tactic:
simp [bind_some_eq_map]

Premises used: Part.bind_some_eq_map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
o : Part α
⊢ map g (map f o) = map (g ∘ f) o

Tactic:
simp [map, Function.comp_assoc]

Premises used: Function.comp_assoc, Part.map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ ∀ {α β : Type u_4}, Eq (α := α → Part β → Part α) Functor.mapConst (Functor.map ∘ const β)

Tactic:
simp [Functor.mapConst, Functor.map]

Premises used: Functor.mapConst, Functor.map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
α_1 : Type u_4
f : Part α_1
mk : ∀ (Dom : Prop) (get : Dom → α_1), id <$> { Dom := Dom, get := get : Part α_1 } = { Dom := Dom, get := get }
⊢ id <$> f = f

Tactic:
cases f
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
α_1 : Type u_4
Dom : Prop
get : Dom → α_1
⊢ id <$> { Dom := Dom, get := get : Part α_1 } = { Dom := Dom, get := get }

Tactic:
rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
α_1 β_1 : Type u_4
x : Part α_1
y : Part β_1
⊢ (x <* y).Dom ↔ (const β_1 <$> x <*> y).Dom

Tactic:
simp [SeqLeft.seqLeft, Part.bind, assert, Seq.seq, const, (· <$> ·), and_comm]

Premises used: Part.bind, and_comm, Seq.seq, SeqLeft.seqLeft, Part.assert, Function.const, Functor.map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
α_1 β_1 : Type u_4
x : Part α_1
y : Part β_1
⊢ Dom (α := β_1) (x *> y) ↔ Dom (α := β_1) (const α_1 id <$> x <*> y)

Tactic:
simp [SeqRight.seqRight, Part.bind, assert, Seq.seq, const, (· <$> ·)]

Premises used: Part.bind, Seq.seq, Part.assert, Function.const, SeqRight.seqRight, Functor.map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
α_1 β_1 : Type u_4
x : α_1 → β_1
y : Part α_1
⊢ Dom (pure x <*> y) ↔ (x <$> y).Dom

Tactic:
simp [Seq.seq, Part.bind, assert, (· <$> ·), pure]

Premises used: Pure.pure, Part.bind, Seq.seq, Part.assert, Functor.map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
α_1 β_1 : Type u_4
x : Part (α_1 → β_1)
y : Part α_1
⊢ (Dom (α := β_1) do
      let x ← x
      x <$> y) ↔
    (x <*> y).Dom

Tactic:
simp [(· >>= ·), Part.bind, assert, Seq.seq, (· <$> ·)]

Premises used: Part.bind, Seq.seq, Part.assert, Bind.bind, Functor.map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
f : α → α
H : ∀ (x : α), f x = x
o : Part α
rw : map id o = o
⊢ map f o = o

Tactic:
rw [show f = id from funext H]

Premises used: funext
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map id o = o

Tactic:
id_map o

Premises used: LawfulFunctor.id_map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map id o = o

Tactic:
exact id_map o

Premises used: LawfulFunctor.id_map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x : Part α
rw : map (fun (y : α) ↦ y) x = x
⊢ x.bind some = x

Tactic:
rw [bind_some_eq_map]

Premises used: Part.bind_some_eq_map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
x : Part α
⊢ map (fun (y : α) ↦ y) x = x

Tactic:
simp [map_id']

Premises used: Part.map_id'
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
a : α
⊢ pure a = some a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Part
Goal:
α β : Type u_4
f : α → β
o : Part α
⊢ f <$> o = map f o

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Part
Goal:
α β : Type u_4
f : Part α
g : α → Part β
⊢ f >>= g = f.bind g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Part
Goal:
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
mp : x >>= f ≤ y → ∀ (a : α), a ∈ x → f a ≤ y
mpr : (∀ (a : α), a ∈ x → f a ≤ y) → x >>= f ≤ y
⊢ x >>= f ≤ y ↔ ∀ (a : α), a ∈ x → f a ≤ y

Tactic:
constructor
-- Module: Mathlib.Data.Part
Goal:
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
⊢ b ∈ x >>= f → b ∈ y

Tactic:
have h := h b
-- Module: Mathlib.Data.Part
Goal:
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h_1 : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : b ∈ x >>= f → b ∈ y
⊢ ∀ (x_1 : α), x_1 ∈ x → b ∈ f x_1 → b ∈ y

Tactic:
simp only [and_imp, bind_eq_bind, mem_bind_iff, exists_imp] at h

Premises used: Part.mem_bind_iff, and_imp, exists_imp, Part.bind_eq_bind
-- Module: Mathlib.Data.Part
Goal:
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h_1 : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : ∀ (x_1 : α), x_1 ∈ x → b ∈ f x_1 → b ∈ y
⊢ b ∈ f a → b ∈ y

Tactic:
apply h _ h'
-- Module: Mathlib.Data.Part
Goal:
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
h' : b ∈ x >>= f
⊢ ∃ (a : α), a ∈ x ∧ b ∈ f a

Tactic:
simp only [bind_eq_bind, mem_bind_iff] at h'

Premises used: Part.mem_bind_iff, Part.bind_eq_bind
-- Module: Mathlib.Data.Part
Goal:
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
h' : ∃ (a : α), a ∈ x ∧ b ∈ f a
mpr : ∀ (a : α) (h₀ : a ∈ x) (h₁ : b ∈ f a), b ∈ y
⊢ b ∈ y

Tactic:
rcases h' with ⟨a, h₀, h₁⟩
-- Module: Mathlib.Data.Part
Goal:
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : ∀ (a : α), a ∈ x → f a ≤ y
b : β
a : α
h₀ : a ∈ x
h₁ : b ∈ f a
⊢ b ∈ y

Tactic:
apply h _ h₀ _ h₁
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
dsimp : (∃ (h_1 : p), o.get ⋯ = a) ↔ p ∧ ∃ (h : o.Dom), o.get h = a
⊢ a ∈ restrict p o h ↔ p ∧ a ∈ o

Tactic:
dsimp [restrict, mem_eq]

Premises used: Part.restrict, Part.mem_eq
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
mp : (∃ (h_1 : p), o.get ⋯ = a) → p ∧ ∃ (h : o.Dom), o.get h = a
mpr : (p ∧ ∃ (h : o.Dom), o.get h = a) → ∃ (h_1 : p), o.get ⋯ = a
⊢ (∃ (h_1 : p), o.get ⋯ = a) ↔ p ∧ ∃ (h : o.Dom), o.get h = a

Tactic:
constructor
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
h₁ : o.get ⋯ = a
⊢ p ∧ ∃ (h : o.Dom), o.get h = a

Tactic:
⟨h₀, ⟨_, h₁⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
h₁ : o.get ⋯ = a
⊢ p ∧ ∃ (h : o.Dom), o.get h = a

Tactic:
exact ⟨h₀, ⟨_, h₁⟩⟩
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
w : o.Dom
h₂ : o.get w = a
⊢ ∃ (h_1 : p), o.get ⋯ = a

Tactic:
⟨h₀, h₂⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
w : o.Dom
h₂ : o.get w = a
⊢ ∃ (h_1 : p), o.get ⋯ = a

Tactic:
exact ⟨h₀, h₂⟩
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
p : Prop
f : p → Part α
⊢ ∀ (h : p), (f h).Dom → (assert p f).Dom

Tactic:
Exists.intro

Premises used: Exists.intro
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
f : Part α
g : α → Part β
⊢ ∀ (h : f.Dom), (g (f.get h)).Dom → (f.bind g).Dom

Tactic:
assert_defined

Premises used: Part.assert_defined
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
β : Type u_2
f : Part α
g : α → Part β
⊢ (f.bind g).Dom ↔ ∃ (h : f.Dom), (g (f.get h)).Dom

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Mul α
a b : Part α
⊢ a * b = do
    let y ← a
    map (fun (x : α) ↦ y * x) b

Tactic:
rfl

Premises used: Part.bind, rfl, Part.map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := Part α) 1 (some 1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Inv α
a : Part α
⊢ a⁻¹ = map (fun (x : α) ↦ x⁻¹) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Div α
a b : Part α
⊢ a / b = do
    let y ← a
    map (fun (x : α) ↦ y / x) b

Tactic:
rfl

Premises used: Part.bind, rfl, Part.map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Mod α
a b : Part α
⊢ a % b = do
    let y ← a
    map (fun (x : α) ↦ y % x) b

Tactic:
rfl

Premises used: Part.bind, rfl, Part.map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Append α
a b : Part α
⊢ a ++ b = do
    let y ← a
    map (fun (x : α) ↦ y ++ x) b

Tactic:
rfl

Premises used: Part.bind, rfl, Part.map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Inter α
a b : Part α
⊢ a ∩ b = do
    let y ← a
    map (fun (x : α) ↦ y ∩ x) b

Tactic:
rfl

Premises used: Part.bind, rfl, Part.map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Union α
a b : Part α
⊢ a ∪ b = do
    let y ← a
    map (fun (x : α) ↦ y ∪ x) b

Tactic:
rfl

Premises used: Part.bind, rfl, Part.map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : SDiff α
a b : Part α
⊢ a \ b = do
    let y ← a
    map (fun (x : α) ↦ y \ x) b

Tactic:
rfl

Premises used: Part.bind, rfl, Part.map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : One α
⊢ Membership.mem (γ := Part α) 1 1

Tactic:
⟨trivial, rfl⟩

Premises used: Part.Mem, trivial, Exists.intro, rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
simp : (a * b).get ⋯ = a.get ⋯ * b.get ⋯
⊢ (a * b).get ⋯ = ma * mb

Tactic:
simp only [← ha.2, ← hb.2]
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Mul α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ (a * b).get ⋯ = a.get ⋯ * b.get ⋯

Tactic:
rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Mul α
a b : Part α
hab : (a * b).Dom
⊢ a.Dom

Tactic:
hab.1
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Mul α
a b : Part α
hab : (a * b).Dom
⊢ b.Dom

Tactic:
hab.2
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Mul α
a b : Part α
hab : (a * b).Dom
⊢ (a * b).get hab = a.get ⋯ * b.get ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Mul α
a b : α
⊢ some a * some b = some (a * b)

Tactic:
simp [mul_def]

Premises used: Part.mul_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Inv α
a : Part α
ma : α
ha : ma ∈ a
simp : ∃ (a_1 : α), a_1 ∈ a ∧ a_1⁻¹ = ma⁻¹
⊢ ma⁻¹ ∈ a⁻¹

Tactic:
simp [inv_def]

Premises used: Part.inv_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ∃ (a_1 : α), a_1 ∈ a ∧ a_1⁻¹ = ma⁻¹

Tactic:
aesop
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Inv α
a : α
⊢ (some a)⁻¹ = some a⁻¹

Tactic:
rfl

Premises used: Part.some, rfl, Part.map
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
simp : ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 / a = ma / mb
⊢ ma / mb ∈ a / b

Tactic:
simp [div_def]

Premises used: Part.div_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 / a = ma / mb

Tactic:
aesop
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Div α
a b : Part α
hab : (a / b).Dom
⊢ a.Dom

Tactic:
hab.1
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Div α
a b : Part α
hab : (a / b).Dom
⊢ b.Dom

Tactic:
hab.2
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Div α
a b : Part α
hab : (a / b).Dom
simp : get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y / x) b) ⋯ = a.get ⋯ / b.get ⋯
⊢ (a / b).get hab = a.get ⋯ / b.get ⋯

Tactic:
simp [div_def]

Premises used: Part.div_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Div α
a b : Part α
hab : (a / b).Dom
⊢ get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y / x) b) ⋯ = a.get ⋯ / b.get ⋯

Tactic:
aesop
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Div α
a b : α
⊢ some a / some b = some (a / b)

Tactic:
simp [div_def]

Premises used: Part.div_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Mod α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
simp : ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 % a = ma % mb
⊢ ma % mb ∈ a % b

Tactic:
simp [mod_def]

Premises used: Part.mod_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Mod α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 % a = ma % mb

Tactic:
aesop
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Mod α
a b : Part α
hab : (a % b).Dom
⊢ a.Dom

Tactic:
hab.1
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Mod α
a b : Part α
hab : (a % b).Dom
⊢ b.Dom

Tactic:
hab.2
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Mod α
a b : Part α
hab : (a % b).Dom
simp : get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y % x) b) ⋯ = a.get ⋯ % b.get ⋯
⊢ (a % b).get hab = a.get ⋯ % b.get ⋯

Tactic:
simp [mod_def]

Premises used: Part.mod_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Mod α
a b : Part α
hab : (a % b).Dom
⊢ get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y % x) b) ⋯ = a.get ⋯ % b.get ⋯

Tactic:
aesop
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Mod α
a b : α
⊢ some a % some b = some (a % b)

Tactic:
simp [mod_def]

Premises used: Part.mod_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Append α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
simp : ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 ++ a = ma ++ mb
⊢ ma ++ mb ∈ a ++ b

Tactic:
simp [append_def]

Premises used: Part.append_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Append α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 ++ a = ma ++ mb

Tactic:
aesop
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Append α
a b : Part α
hab : (a ++ b).Dom
⊢ a.Dom

Tactic:
hab.1
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Append α
a b : Part α
hab : (a ++ b).Dom
⊢ b.Dom

Tactic:
hab.2
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Append α
a b : Part α
hab : (a ++ b).Dom
simp : get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y ++ x) b) ⋯ = a.get ⋯ ++ b.get ⋯
⊢ (a ++ b).get hab = a.get ⋯ ++ b.get ⋯

Tactic:
simp [append_def]

Premises used: Part.append_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Append α
a b : Part α
hab : (a ++ b).Dom
⊢ get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y ++ x) b) ⋯ = a.get ⋯ ++ b.get ⋯

Tactic:
aesop
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Append α
a b : α
⊢ some a ++ some b = some (a ++ b)

Tactic:
simp [append_def]

Premises used: Part.append_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Inter α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
simp : ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 ∩ a = ma ∩ mb
⊢ ma ∩ mb ∈ a ∩ b

Tactic:
simp [inter_def]

Premises used: Part.inter_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Inter α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 ∩ a = ma ∩ mb

Tactic:
aesop
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Inter α
a b : Part α
hab : (a ∩ b).Dom
⊢ a.Dom

Tactic:
hab.1
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Inter α
a b : Part α
hab : (a ∩ b).Dom
⊢ b.Dom

Tactic:
hab.2
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Inter α
a b : Part α
hab : (a ∩ b).Dom
simp : get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y ∩ x) b) ⋯ = a.get ⋯ ∩ b.get ⋯
⊢ (a ∩ b).get hab = a.get ⋯ ∩ b.get ⋯

Tactic:
simp [inter_def]

Premises used: Part.inter_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Inter α
a b : Part α
hab : (a ∩ b).Dom
⊢ get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y ∩ x) b) ⋯ = a.get ⋯ ∩ b.get ⋯

Tactic:
aesop
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Inter α
a b : α
⊢ some a ∩ some b = some (a ∩ b)

Tactic:
simp [inter_def]

Premises used: Part.inter_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Union α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
simp : ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 ∪ a = ma ∪ mb
⊢ ma ∪ mb ∈ a ∪ b

Tactic:
simp [union_def]

Premises used: Part.union_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Union α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 ∪ a = ma ∪ mb

Tactic:
aesop
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ a.Dom

Tactic:
hab.1
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ b.Dom

Tactic:
hab.2
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Union α
a b : Part α
hab : (a ∪ b).Dom
simp : get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y ∪ x) b) ⋯ = a.get ⋯ ∪ b.get ⋯
⊢ (a ∪ b).get hab = a.get ⋯ ∪ b.get ⋯

Tactic:
simp [union_def]

Premises used: Part.union_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Union α
a b : Part α
hab : (a ∪ b).Dom
⊢ get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y ∪ x) b) ⋯ = a.get ⋯ ∪ b.get ⋯

Tactic:
aesop
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : Union α
a b : α
⊢ some a ∪ some b = some (a ∪ b)

Tactic:
simp [union_def]

Premises used: Part.union_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : SDiff α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
simp : ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 \ a = ma \ mb
⊢ ma \ mb ∈ a \ b

Tactic:
simp [sdiff_def]

Premises used: Part.sdiff_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : SDiff α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ (a_1 : α), a_1 ∈ a ∧ ∃ (a : α), a ∈ b ∧ a_1 \ a = ma \ mb

Tactic:
aesop
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ a.Dom

Tactic:
hab.1
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ b.Dom

Tactic:
hab.2
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : SDiff α
a b : Part α
hab : (a \ b).Dom
simp : get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y \ x) b) ⋯ = a.get ⋯ \ b.get ⋯
⊢ (a \ b).get hab = a.get ⋯ \ b.get ⋯

Tactic:
simp [sdiff_def]

Premises used: Part.sdiff_def
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : SDiff α
a b : Part α
hab : (a \ b).Dom
⊢ get (a.bind fun (y : α) ↦ map (fun (x : α) ↦ y \ x) b) ⋯ = a.get ⋯ \ b.get ⋯

Tactic:
aesop
-- Module: Mathlib.Data.Part
Goal:
α : Type u_1
inst : SDiff α
a b : α
⊢ some a \ some b = some (a \ b)

Tactic:
simp [sdiff_def]

Premises used: Part.sdiff_def
-- Module: Mathlib.Data.Pi.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : (i : ι) → LocallyFiniteOrder (α i)
a b x : (i : ι) → α i
simp_rw simp_rw₁ :
  Membership.mem (γ := Finset ((i : ι) → α i)) (piFinset (δ := α) fun (i : ι) ↦ Icc (a i) (b i)) x ↔ a ≤ x ∧ x ≤ b
simp_rw₂ : (∀ (a_1 : ι), x a_1 ∈ Icc (a a_1) (b a_1)) ↔ a ≤ x ∧ x ≤ b
simp_rw₃ : (∀ (a_1 : ι), a a_1 ≤ x a_1 ∧ x a_1 ≤ b a_1) ↔ a ≤ x ∧ x ≤ b
simp_rw₄ : (∀ (a_1 : ι), a a_1 ≤ x a_1 ∧ x a_1 ≤ b a_1) ↔ (∀ (i : ι), a i ≤ x i) ∧ ∀ (i : ι), x i ≤ b i
⊢ Membership.mem (γ := Finset ((i : ι) → α i))
      ((fun (a b : (i : ι) → α i) ↦ (piFinset (δ := α) fun (i : ι) ↦ Icc (a i) (b i) : Finset ((a : ι) → α a))) a b) x ↔
    a ≤ x ∧ x ≤ b

Tactic:
simp_rw [mem_piFinset, mem_Icc, le_def, forall_and]

Premises used: Fintype.mem_piFinset, Finset.mem_Icc, Pi.le_def, forall_and