awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₂ : List α
a : α
inst : DecidableEq α
l₁ : List α
h : ¬a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = l₁ ∩ l₂

Tactic:
simp [Inter.inter, List.inter, h]

Premises used: Inter.inter, List.inter
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₂ : List α
a : α
inst : DecidableEq α
l₁ : List α
pos : a ∈ l₂ → (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂
neg : ¬a ∈ l₂ → (a :: l₁) ∩ l₂ = l₁ ∩ l₂
⊢ (a :: l₁) ∩ l₂ = if a ∈ l₂ then a :: l₁ ∩ l₂ else l₁ ∩ l₂

Tactic:
split_ifs
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₂ : List α
a : α
inst : DecidableEq α
l₁ : List α
h : a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂

Tactic:
simp_all
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₂ : List α
a : α
inst : DecidableEq α
l₁ : List α
h : ¬a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = l₁ ∩ l₂

Tactic:
simp_all
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := List α) ([] ∩ []) []

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
tail_ih : tail ∩ [] = []
⊢ (head :: tail) ∩ [] = []

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
nil : Eq.{u_1 + 1} (α := List α) ([] ∩ []) []
cons : ∀ (head : α) (tail : List α), tail ∩ [] = [] → (head :: tail) ∩ [] = []
⊢ l ∩ [] = []

Tactic:
induction l with grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
a : α
inst : DecidableEq α
⊢ a ∈ l₁ ∩ l₂ → a ∈ l₁

Tactic:
mem_of_mem_filter

Premises used: List.mem_of_mem_filter
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
a : α
inst : DecidableEq α
h : a ∈ l₁ ∩ l₂
⊢ a ∈ l₂

Tactic:
simpa using of_mem_filter h

Premises used: List.of_mem_filter
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
a : α
inst : DecidableEq α
h₁ : a ∈ l₁
h₂ : a ∈ l₂
⊢ elem a l₂ = true

Tactic:
simpa using h₂
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
⊢ l₁ ∩ l₂ ⊆ l₁

Tactic:
filter_subset_self _

Premises used: List.filter_subset_self
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
⊢ l₁ ∩ l₂ ⊆ l₂

Tactic:
fun _ => mem_of_mem_inter_right

Premises used: List.Subset, List.mem_of_mem_inter_right
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l l₁ l₂ : List α
h₁ : l ⊆ l₁
h₂ : l ⊆ l₂
⊢ l ⊆ l₁ ∩ l₂

Tactic:
fun _ h =>
  mem_inter_iff.2 ⟨h₁ h, h₂ h⟩

Premises used: Iff.mpr, List.Subset, And.intro, List.mem_inter_iff
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
inst : DecidableEq α
simp : (∀ (a : α), a ∈ l₁ → ¬a ∈ l₂) ↔ l₁.Disjoint l₂
⊢ l₁ ∩ l₂ = [] ↔ l₁.Disjoint l₂

Tactic:
simp only [eq_nil_iff_forall_not_mem, mem_inter_iff, not_and]

Premises used: List.mem_inter_iff, not_and, List.eq_nil_iff_forall_not_mem
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
inst : DecidableEq α
⊢ (∀ (a : α), a ∈ l₁ → ¬a ∈ l₂) ↔ l₁.Disjoint l₂

Tactic:
rfl
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ : List α
p : α → Prop
inst : DecidableEq α
h : ∀ (x : α), x ∈ l₁ → p x
l₂ : List α
⊢ ∀ (x : α), x ∈ l₁ ∩ l₂ → p x

Tactic:
BAll.imp_left (fun _ => mem_of_mem_inter_left) h

Premises used: List.mem_of_mem_inter_left, BAll.imp_left
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₂ : List α
p : α → Prop
inst : DecidableEq α
l₁ : List α
h : ∀ (x : α), x ∈ l₂ → p x
⊢ ∀ (x : α), x ∈ l₁ ∩ l₂ → p x

Tactic:
BAll.imp_left (fun _ => mem_of_mem_inter_right) h

Premises used: List.mem_of_mem_inter_right, BAll.imp_left
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
⊢ xs ∩ ys.reverse = xs ∩ ys

Tactic:
simp only [List.inter_def, elem_eq_mem, mem_reverse]

Premises used: List.inter_def, List.mem_reverse, List.elem_eq_mem
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
h : xs ⊆ ys
⊢ xs ∩ ys = xs

Tactic:
List.filter_eq_self.mpr fun _ ha => elem_eq_true_of_mem (h ha)

Premises used: Iff.mpr, List.elem_eq_true_of_mem, List.filter_eq_self
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ l₃ : List α
h : l₂ <+ l₃
⊢ l₁ ∩ l₂ <+ l₁ ∩ l₃

Tactic:
grind [inter_def, monotone_filter_right]

Premises used: List.inter_def, List.monotone_filter_right
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ l₃ : List α
h : l₁ <+ l₂
⊢ l₁ ∩ l₃ <+ l₂ ∩ l₃

Tactic:
grind [inter_def]

Premises used: List.inter_def
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
nil : Eq.{u_1 + 1} (α := List α) (List.bagInter [] []) []
cons : ∀ (head : α) (tail : List α), List.bagInter [] (head :: tail) = []
⊢ List.bagInter [] l = []

Tactic:
cases l
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := List α) (List.bagInter [] []) []

Tactic:
rfl
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
⊢ List.bagInter [] (head :: tail) = []

Tactic:
rfl
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
nil : Eq.{u_1 + 1} (α := List α) (List.bagInter [] []) []
cons : ∀ (head : α) (tail : List α), (head :: tail).bagInter [] = []
⊢ l.bagInter [] = []

Tactic:
cases l
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
⊢ (head :: tail).bagInter [] = []

Tactic:
rfl
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
a : α
inst : DecidableEq α
l₁ : List α
h : Membership.mem (γ := List α) [] a
⊢ (a :: l₁).bagInter [] = a :: l₁.bagInter (List.erase [] a)

Tactic:
grind [List.bagInter]

Premises used: List.bagInter
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
a : α
inst : DecidableEq α
l₁ : List α
head : α
tail : List α
h : a ∈ head :: tail
⊢ (a :: l₁).bagInter (head :: tail) = a :: l₁.bagInter ((head :: tail).erase a)

Tactic:
grind [List.bagInter]

Premises used: List.bagInter
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₂ : List α
a : α
inst : DecidableEq α
l₁ : List α
h : a ∈ l₂
nil : ∀ (h : Membership.mem (γ := List α) [] a), (a :: l₁).bagInter [] = a :: l₁.bagInter (List.erase [] a)
cons :
  ∀ (head : α) (tail : List α) (h : a ∈ head :: tail),
    (a :: l₁).bagInter (head :: tail) = a :: l₁.bagInter ((head :: tail).erase a)
⊢ (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)

Tactic:
cases l₂ with grind [List.bagInter]

Premises used: List.bagInter
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
a : α
inst : DecidableEq α
l₁ : List α
h : ¬Membership.mem (γ := List α) [] a
⊢ (a :: l₁).bagInter [] = l₁.bagInter []

Tactic:
grind [List.bagInter]

Premises used: List.bagInter
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
a : α
inst : DecidableEq α
l₁ : List α
head : α
tail : List α
h : ¬a ∈ head :: tail
⊢ (a :: l₁).bagInter (head :: tail) = l₁.bagInter (head :: tail)

Tactic:
grind [List.bagInter]

Premises used: List.bagInter
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₂ : List α
a : α
inst : DecidableEq α
l₁ : List α
h : ¬a ∈ l₂
nil : ∀ (h : ¬Membership.mem (γ := List α) [] a), (a :: l₁).bagInter [] = l₁.bagInter []
cons :
  ∀ (head : α) (tail : List α) (h : ¬a ∈ head :: tail), (a :: l₁).bagInter (head :: tail) = l₁.bagInter (head :: tail)
⊢ (a :: l₁).bagInter l₂ = l₁.bagInter l₂

Tactic:
cases l₂ with grind [List.bagInter]

Premises used: List.bagInter
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
a : α
inst : DecidableEq α
pos : a ∈ l₂ → (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)
neg : ¬a ∈ l₂ → (a :: l₁).bagInter l₂ = l₁.bagInter l₂
⊢ (a :: l₁).bagInter l₂ = if a ∈ l₂ then a :: l₁.bagInter (l₂.erase a) else l₁.bagInter l₂

Tactic:
split_ifs
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
a : α
inst : DecidableEq α
h : a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)

Tactic:
simp_all
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
a : α
inst : DecidableEq α
h : ¬a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = l₁.bagInter l₂

Tactic:
simp_all
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ : List α
a : α
inst : DecidableEq α
l₂ : List α
h : ¬a ∈ l₁
nil : ∀ (l₂ : List α) (h : ¬Membership.mem (γ := List α) [] a), List.bagInter [] (a :: l₂) = List.bagInter [] l₂
cons :
  ∀ (head : α) (tail : List α),
    (∀ (l₂ : List α) (h : ¬a ∈ tail), tail.bagInter (a :: l₂) = tail.bagInter l₂) →
      ∀ (l₂ : List α) (h : ¬a ∈ head :: tail), (head :: tail).bagInter (a :: l₂) = (head :: tail).bagInter l₂
⊢ l₁.bagInter (a :: l₂) = l₁.bagInter l₂

Tactic:
induction l₁ generalizing l₂
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ : List α
a : α
inst : DecidableEq α
l₂ : List α
h : ¬Membership.mem (γ := List α) [] a
⊢ List.bagInter [] (a :: l₂) = List.bagInter [] l₂

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ : List α
a : α
inst : DecidableEq α
head : α
tail : List α
tail_ih : ∀ (l₂ : List α) (h : ¬a ∈ tail), tail.bagInter (a :: l₂) = tail.bagInter l₂
l₂ : List α
h : ¬a ∈ head :: tail
⊢ (head :: tail).bagInter (a :: l₂) = (head :: tail).bagInter l₂

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
⊢ Membership.mem (γ := List α) [] a ↔ Membership.mem (γ := List α) [] a ∧ a ∈ x

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
a : α
t : List α
h : t = [] → False
⊢ Membership.mem (γ := List α) [] a ↔ a ∈ t ∧ Membership.mem (γ := List α) [] a

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
a a_1 : α
l₁ l₂ : List α
h : l₂ = [] → False
h_1 : elem a_1 l₂ = true
ih1 : a ∈ l₁.bagInter (l₂.erase a_1) ↔ a ∈ l₁ ∧ a ∈ l₂.erase a_1
⊢ a ∈ a_1 :: l₁.bagInter (l₂.erase a_1) ↔ a ∈ a_1 :: l₁ ∧ a ∈ l₂

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
a a_1 : α
l₁ l₂ : List α
h : l₂ = [] → False
h_1 : ¬elem a_1 l₂ = true
ih1 : a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂
⊢ a ∈ l₁.bagInter l₂ ↔ a ∈ a_1 :: l₁ ∧ a ∈ l₂

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l₁ l₂ : List α
case1 : ∀ (x : List α), Membership.mem (γ := List α) [] a ↔ Membership.mem (γ := List α) [] a ∧ a ∈ x
case2 :
  ∀ (t : List α), (t = [] → False) → (Membership.mem (γ := List α) [] a ↔ a ∈ t ∧ Membership.mem (γ := List α) [] a)
case3 :
  ∀ (a_1 : α) (l₁ l₂ : List α),
    (l₂ = [] → False) →
      elem a_1 l₂ = true →
        (a ∈ l₁.bagInter (l₂.erase a_1) ↔ a ∈ l₁ ∧ a ∈ l₂.erase a_1) →
          (a ∈ a_1 :: l₁.bagInter (l₂.erase a_1) ↔ a ∈ a_1 :: l₁ ∧ a ∈ l₂)
case4 :
  ∀ (a_1 : α) (l₁ l₂ : List α),
    (l₂ = [] → False) →
      ¬elem a_1 l₂ = true → (a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂) → (a ∈ l₁.bagInter l₂ ↔ a ∈ a_1 :: l₁ ∧ a ∈ l₂)
⊢ a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂

Tactic:
fun_induction List.bagInter with grind

Premises used: List.bagInter
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
a : α
x : List α
⊢ count a [] = min (count a []) (count a x)

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
a : α
t : List α
h : t = [] → False
⊢ count a [] = min (count a t) (count a [])

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
a a_1 : α
l₁ l₂ : List α
h : l₂ = [] → False
h_1 : elem a_1 l₂ = true
ih1 : count a (l₁.bagInter (l₂.erase a_1)) = min (count a l₁) (count a (l₂.erase a_1))
⊢ count a (a_1 :: l₁.bagInter (l₂.erase a_1)) = min (count a (a_1 :: l₁)) (count a l₂)

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
a a_1 : α
l₁ l₂ : List α
h : l₂ = [] → False
h_1 : ¬elem a_1 l₂ = true
ih1 : count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂)
⊢ count a (l₁.bagInter l₂) = min (count a (a_1 :: l₁)) (count a l₂)

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l₁ l₂ : List α
case1 : ∀ (x : List α), count a [] = min (count a []) (count a x)
case2 : ∀ (t : List α), (t = [] → False) → count a [] = min (count a t) (count a [])
case3 :
  ∀ (a_1 : α) (l₁ l₂ : List α),
    (l₂ = [] → False) →
      elem a_1 l₂ = true →
        count a (l₁.bagInter (l₂.erase a_1)) = min (count a l₁) (count a (l₂.erase a_1)) →
          count a (a_1 :: l₁.bagInter (l₂.erase a_1)) = min (count a (a_1 :: l₁)) (count a l₂)
case4 :
  ∀ (a_1 : α) (l₁ l₂ : List α),
    (l₂ = [] → False) →
      ¬elem a_1 l₂ = true →
        count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂) →
          count a (l₁.bagInter l₂) = min (count a (a_1 :: l₁)) (count a l₂)
⊢ count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂)

Tactic:
fun_induction List.bagInter with grind

Premises used: List.bagInter
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
⊢ Sublist.{u_1} (α := α) [] []

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
t : List α
h : t = [] → False
⊢ [] <+ t

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l₁ l₂ : List α
h : l₂ = [] → False
h_1 : elem a l₂ = true
ih1 : l₁.bagInter (l₂.erase a) <+ l₁
⊢ a :: l₁.bagInter (l₂.erase a) <+ a :: l₁

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l₁ l₂ : List α
h : l₂ = [] → False
h_1 : ¬elem a l₂ = true
ih1 : l₁.bagInter l₂ <+ l₁
⊢ l₁.bagInter l₂ <+ a :: l₁

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
case1 : ∀ (x : List α), Sublist.{u_1} (α := α) [] []
case2 : ∀ (t : List α), (t = [] → False) → [] <+ t
case3 :
  ∀ (a : α) (l₁ l₂ : List α),
    (l₂ = [] → False) → elem a l₂ = true → l₁.bagInter (l₂.erase a) <+ l₁ → a :: l₁.bagInter (l₂.erase a) <+ a :: l₁
case4 :
  ∀ (a : α) (l₁ l₂ : List α), (l₂ = [] → False) → ¬elem a l₂ = true → l₁.bagInter l₂ <+ l₁ → l₁.bagInter l₂ <+ a :: l₁
⊢ l₁.bagInter l₂ <+ l₁

Tactic:
fun_induction List.bagInter with grind

Premises used: List.bagInter
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ : List α
inst : DecidableEq α
a : α
⊢ [a].bagInter l₁ = if a ∈ l₁ then [a] else []

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ : List α
inst : DecidableEq α
a : α
nil : List.bagInter [] [a] = if Membership.mem (γ := List α) [] a then [a] else []
cons :
  ∀ (head : α) (tail : List α),
    (tail.bagInter [a] = if a ∈ tail then [a] else []) →
      (head :: tail).bagInter [a] = if a ∈ head :: tail then [a] else []
⊢ l₁.bagInter [a] = if a ∈ l₁ then [a] else []

Tactic:
induction l₁
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ : List α
inst : DecidableEq α
a : α
⊢ List.bagInter [] [a] = if Membership.mem (γ := List α) [] a then [a] else []

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ : List α
inst : DecidableEq α
a head : α
tail : List α
tail_ih : tail.bagInter [a] = if a ∈ tail then [a] else []
⊢ (head :: tail).bagInter [a] = if a ∈ head :: tail then [a] else []

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
a : α
inst : DecidableEq α
h : ¬a ∈ l₁
nil : ∀ {l₂ : List α} (h : ¬Membership.mem (γ := List α) [] a), List.bagInter [] (l₂.erase a) = List.bagInter [] l₂
cons :
  ∀ (head : α) (tail : List α),
    (∀ {l₂ : List α} (h : ¬a ∈ tail), tail.bagInter (l₂.erase a) = tail.bagInter l₂) →
      ∀ {l₂ : List α} (h : ¬a ∈ head :: tail), (head :: tail).bagInter (l₂.erase a) = (head :: tail).bagInter l₂
⊢ l₁.bagInter (l₂.erase a) = l₁.bagInter l₂

Tactic:
induction l₁ generalizing l₂
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
a : α
inst : DecidableEq α
l₂ : List α
h : ¬Membership.mem (γ := List α) [] a
⊢ List.bagInter [] (l₂.erase a) = List.bagInter [] l₂

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
a : α
inst : DecidableEq α
head : α
tail : List α
tail_ih : ∀ {l₂ : List α} (h : ¬a ∈ tail), tail.bagInter (l₂.erase a) = tail.bagInter l₂
l₂ : List α
h : ¬a ∈ head :: tail
⊢ (head :: tail).bagInter (l₂.erase a) = (head :: tail).bagInter l₂

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
a : α
inst : DecidableEq α
h : ¬a ∈ l₂
nil : ∀ {l₂ : List α} (h : ¬a ∈ l₂), (List.erase [] a).bagInter l₂ = List.bagInter [] l₂
cons :
  ∀ (head : α) (tail : List α),
    (∀ {l₂ : List α} (h : ¬a ∈ l₂), (tail.erase a).bagInter l₂ = tail.bagInter l₂) →
      ∀ {l₂ : List α} (h : ¬a ∈ l₂), ((head :: tail).erase a).bagInter l₂ = (head :: tail).bagInter l₂
⊢ (l₁.erase a).bagInter l₂ = l₁.bagInter l₂

Tactic:
induction l₁ generalizing l₂
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
a : α
inst : DecidableEq α
l₂ : List α
h : ¬a ∈ l₂
⊢ (List.erase [] a).bagInter l₂ = List.bagInter [] l₂

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
a : α
inst : DecidableEq α
head : α
tail : List α
tail_ih : ∀ {l₂ : List α} (h : ¬a ∈ l₂), (tail.erase a).bagInter l₂ = tail.bagInter l₂
l₂ : List α
h : ¬a ∈ l₂
⊢ ((head :: tail).erase a).bagInter l₂ = (head :: tail).bagInter l₂

Tactic:
grind
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
⊢ List.bagInter [] l₂ = [] ↔ [] ∩ l₂ = []

Tactic:
simp
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
b : α
l₁ l₂ : List α
pos : ∀ (h : b ∈ l₂), (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []
neg : ∀ (h : ¬b ∈ l₂), (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []

Tactic:
by_cases h : b ∈ l₂
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
b : α
l₁ l₂ : List α
h : b ∈ l₂
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []

Tactic:
simp [h]
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []

Tactic:
simpa [h] using bagInter_nil_iff_inter_nil l₁ l₂
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
inst : DecidableEq α
⊢ l₁.bagInter l₂ = [] ↔ l₁.Disjoint l₂

Tactic:
(bagInter_nil_iff_inter_nil _ _).trans inter_eq_nil_iff_disjoint

Premises used: List.inter_eq_nil_iff_disjoint, Iff.trans, List.bagInter_nil_iff_inter_nil
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
inst : DecidableEq α
h : l₁.Nodup
x : α
⊢ List.count x (l₁.bagInter l₂) ≤ 1

Tactic:
grind [List.count_bagInter]

Premises used: List.count_bagInter
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
inst : DecidableEq α
h : l₂.Nodup
x : α
⊢ List.count x (l₁.bagInter l₂) ≤ 1

Tactic:
grind [List.count_bagInter]

Premises used: List.count_bagInter
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l₂ : List α
⊢ List.bagInter [] l₂ <+ [] ∩ l₂

Tactic:
simp
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
ih : ∀ {l₂ : List α}, tail.bagInter l₂ <+ tail ∩ l₂
l₂ : List α
cons : (if head ∈ l₂ then head :: tail.bagInter (l₂.erase head) else tail.bagInter l₂) <+ (head :: tail) ∩ l₂
⊢ (head :: tail).bagInter l₂ <+ (head :: tail) ∩ l₂

Tactic:
rw [cons_bagInter]

Premises used: List.cons_bagInter
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
ih : ∀ {l₂ : List α}, tail.bagInter l₂ <+ tail ∩ l₂
l₂ : List α
cons : head ∈ l₂ → head :: tail.bagInter (l₂.erase head) <+ (head :: tail) ∩ l₂
cons₁ : ¬head ∈ l₂ → tail.bagInter l₂ <+ (head :: tail) ∩ l₂
⊢ (if head ∈ l₂ then head :: tail.bagInter (l₂.erase head) else tail.bagInter l₂) <+ (head :: tail) ∩ l₂

Tactic:
split
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
ih : ∀ {l₂ : List α}, tail.bagInter l₂ <+ tail ∩ l₂
l₂ : List α
h : head ∈ l₂
⊢ head ∈ l₂

Tactic:
assumption
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
ih : ∀ {l₂ : List α}, tail.bagInter l₂ <+ tail ∩ l₂
l₂ : List α
h : head ∈ l₂
cons : tail.bagInter (l₂.erase head) <+ tail ∩ l₂
⊢ head :: tail.bagInter (l₂.erase head) <+ (head :: tail) ∩ l₂

Tactic:
rw [inter_cons_of_mem _ (by assumption), cons_sublist_cons]

Premises used: List.cons_sublist_cons, List.inter_cons_of_mem
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
ih : ∀ {l₂ : List α}, tail.bagInter l₂ <+ tail ∩ l₂
l₂ : List α
h : head ∈ l₂
⊢ l₂.erase head <+ l₂

Tactic:
grind [erase_sublist]

Premises used: List.erase_sublist
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
ih : ∀ {l₂ : List α}, tail.bagInter l₂ <+ tail ∩ l₂
l₂ : List α
h : head ∈ l₂
⊢ tail.bagInter (l₂.erase head) <+ tail ∩ l₂

Tactic:
exact ih.trans <| Sublist.inter_left (by grind [erase_sublist])

Premises used: List.Sublist.trans, List.Sublist.inter_left
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
ih : ∀ {l₂ : List α}, tail.bagInter l₂ <+ tail ∩ l₂
l₂ : List α
h : ¬head ∈ l₂
⊢ tail.bagInter l₂ <+ (head :: tail) ∩ l₂

Tactic:
simp_all
-- Module: Mathlib.Data.List.Lattice
Goal:
α : Type u_1
l₁ l₂ : List α
inst : DecidableEq α
nil : ∀ {l₂ : List α}, List.bagInter [] l₂ <+ [] ∩ l₂
cons :
  ∀ (head : α) (tail : List α) (ih : ∀ {l₂ : List α}, tail.bagInter l₂ <+ tail ∩ l₂) {l₂ : List α},
    (head :: tail).bagInter l₂ <+ (head :: tail) ∩ l₂
⊢ l₁.bagInter l₂ <+ l₁ ∩ l₂

Tactic:
induction l₁ generalizing l₂ with
  | nil => simp
  | cons _ _ ih =>
    rw [cons_bagInter]
    split
    · rw [inter_cons_of_mem _ (by assumption), cons_sublist_cons]
      exact ih.trans <| Sublist.inter_left (by grind [erase_sublist])
    · simp_all

Premises used: List.cons_bagInter, List.cons_sublist_cons, List.inter_cons_of_mem, List.Sublist.cons, List.Sublist.inter_left, List.nil
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
l : List α
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | x ∈ l} ∅ ↔ l = []

Tactic:
Set.eq_empty_iff_forall_notMem.trans eq_nil_iff_forall_not_mem.symm

Premises used: Set.eq_empty_iff_forall_notMem, Iff.trans, Iff.symm, List.eq_nil_iff_forall_not_mem
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
x : α
hx : ¬Membership.mem (γ := List α) [] x
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ length.{u_1} (α := α) []} n
m : ℕ
hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ length.{u_1} (α := α) []} m
h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ insertIdx [] k x) n) ((fun (k : ℕ) ↦ insertIdx [] k x) m)
⊢ n = m

Tactic:
simp_all [Set.mem_singleton_iff, Set.setOf_eq_eq_singleton, length]

Premises used: Set.setOf_eq_eq_singleton, Set.mem_singleton_iff, List.length
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
x hd : α
tl : List α
IH :
  ∀ (hx : ¬x ∈ tl) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} m)
    (h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ tl.insertIdx k x) n) ((fun (k : ℕ) ↦ tl.insertIdx k x) m)), n = m
hx : ¬x ∈ hd :: tl
n : ℕ
hn : n ≤ tl.length + 1
m : ℕ
hm : m ≤ tl.length + 1
h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) n) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) m)
⊢ ¬x = hd ∧ ¬x ∈ tl

Tactic:
simp only [mem_cons, not_or] at hx

Premises used: not_or, List.mem_cons