mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case isTrue
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h✝ : a ∈ l.dedup
⊢ (a :: l).dedup = l.dedup

pp: case isFalse
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h✝ : ¬a ∈ l.dedup
⊢ (a :: l).dedup = a :: l.dedup

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h✝ : a ∈ l.dedup
⊢ (a :: l).dedup = l.dedup

case isFalse
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h✝ : ¬a ∈ l.dedup
⊢ (a :: l).dedup = a :: l.dedup
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : a ∈ l
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : ¬a ∈ l
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : a ∈ l
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : ¬a ∈ l
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : a ∈ l
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : ¬a ∈ l
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : a ∈ l
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : ¬a ∈ l
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
h : ¬a ∈ l
⊢ (a :: l).dedup = [] ↔ a :: l = []

Tactic:
· simp only [List.dedup_cons_of_notMem h, List.cons_ne_nil]

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case pos
α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h✝ : a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂

pp: case neg
α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h✝ : ¬a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = l₁ ∩ l₂

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h✝ : a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂

case neg
α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h✝ : ¬a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = l₁ ∩ l₂
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].bagInter [] = []

pp: case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
⊢ [].bagInter (head✝ :: tail✝) = []

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].bagInter [] = []

case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
⊢ [].bagInter (head✝ :: tail✝) = []
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].bagInter [] = []

pp: case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).bagInter [] = []

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].bagInter [] = []

case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).bagInter [] = []
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case pos
α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h✝ : a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)

pp: case neg
α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h✝ : ¬a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = l₁.bagInter l₂

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h✝ : a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)

case neg
α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h✝ : ¬a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = l₁.bagInter l₂
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case nil
α : Type u_1
l₁ : List α
a : α
inst✝ : DecidableEq α
l₂ : List α
h : ¬a ∈ []
⊢ [].bagInter (a :: l₂) = [].bagInter l₂

pp: case cons
α : Type u_1
l₁ : List α
a : α
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l₂ : List α), ¬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:
<;>

Goal state after:
case nil
α : Type u_1
l₁ : List α
a : α
inst✝ : DecidableEq α
l₂ : List α
h : ¬a ∈ []
⊢ [].bagInter (a :: l₂) = [].bagInter l₂

case cons
α : Type u_1
l₁ : List α
a : α
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l₂ : List α), ¬a ∈ tail✝ → tail✝.bagInter (a :: l₂) = tail✝.bagInter l₂
l₂ : List α
h : ¬a ∈ head✝ :: tail✝
⊢ (head✝ :: tail✝).bagInter (a :: l₂) = (head✝ :: tail✝).bagInter l₂
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case nil
α : Type u_1
l₁ : List α
inst✝ : DecidableEq α
a : α
⊢ [].bagInter [a] = if a ∈ [] then [a] else []

pp: case cons
α : 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:
<;>

Goal state after:
case nil
α : Type u_1
l₁ : List α
inst✝ : DecidableEq α
a : α
⊢ [].bagInter [a] = if a ∈ [] then [a] else []

case cons
α : 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 []
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case nil
α : Type u_1
a : α
inst✝ : DecidableEq α
l₂ : List α
h : ¬a ∈ []
⊢ [].bagInter (l₂.erase a) = [].bagInter l₂

pp: case cons
α : Type u_1
a : α
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, ¬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:
<;>

Goal state after:
case nil
α : Type u_1
a : α
inst✝ : DecidableEq α
l₂ : List α
h : ¬a ∈ []
⊢ [].bagInter (l₂.erase a) = [].bagInter l₂

case cons
α : Type u_1
a : α
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, ¬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₂
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case nil
α : Type u_1
a : α
inst✝ : DecidableEq α
l₂ : List α
h : ¬a ∈ l₂
⊢ ([].erase a).bagInter l₂ = [].bagInter l₂

pp: case cons
α : Type u_1
a : α
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, ¬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:
<;>

Goal state after:
case nil
α : Type u_1
a : α
inst✝ : DecidableEq α
l₂ : List α
h : ¬a ∈ l₂
⊢ ([].erase a).bagInter l₂ = [].bagInter l₂

case cons
α : Type u_1
a : α
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, ¬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₂
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ {s u : Multiset α}, s ≤ 0 → s ≤ u → s ≤ 0 ∩ u

pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
⊢ ∀ {s u : Multiset α}, s ≤ a ::ₘ t → s ≤ u → s ≤ (a ::ₘ t) ∩ u

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ {s u : Multiset α}, s ≤ 0 → s ≤ u → s ≤ 0 ∩ u

case refine_2
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
⊢ ∀ {s u : Multiset α}, s ≤ a ::ₘ t → s ≤ u → s ≤ (a ::ₘ t) ∩ u
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case pos
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝ : p a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

pp: case neg
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝ : ¬p a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝ : p a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

case neg
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝ : ¬p a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s + u - (t + u) = s - t

Tactic:
t.add_comm,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s + u - (u + t) = s - t
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case pos
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝¹ : p a
h✝ : q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

pp: case neg
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝¹ : p a
h✝ : ¬q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

pp: case pos
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝¹ : ¬p a
h✝ : q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

pp: case neg
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝¹ : ¬p a
h✝ : ¬q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝¹ : p a
h✝ : q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

case neg
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝¹ : p a
h✝ : ¬q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

case pos
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝¹ : ¬p a
h✝ : q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

case neg
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝¹ : ¬p a
h✝ : ¬q a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t

Tactic:
simpa using add_union_distrib (a ::ₘ 0) s t

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case pos
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h✝ : p a
⊢ map (fun x ↦ f x) {a} = (some {f a}).getD 0

pp: case neg
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h✝ : ¬p a
⊢ map (fun x ↦ f x) 0 = none.getD 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h✝ : p a
⊢ map (fun x ↦ f x) {a} = (some {f a}).getD 0

case neg
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h✝ : ¬p a
⊢ map (fun x ↦ f x) 0 = none.getD 0
Module: Mathlib.Data.List.Induction

Goal state before:
pp: α : Type u_1
motive : List α → Sort u_2
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
⊢ reverseRec nil append_singleton [] = nil

Tactic:
by grind [reverseRec]

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
x✝ : s.Nodup ∧ t.Nodup
h₁ : s.Nodup
h₂ : t.Nodup
a : α
⊢ max (count a s) (count a t) ≤ 1

Tactic:
exact max_le (nodup_iff_count_le_one.1 h₁ a) (nodup_iff_count_le_one.1 h₂ a)

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
a : α
h : p a
⊢ count a (s - filter p s) = count a (filter (fun a ↦ ¬p a) s)

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
a : α
h : ¬p a
⊢ count a (s - filter p s) = count a (filter (fun a ↦ ¬p a) s)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
a : α
h : p a
⊢ count a (s - filter p s) = count a (filter (fun a ↦ ¬p a) s)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
a : α
h : ¬p a
⊢ count a (s - filter p s) = count a (filter (fun a ↦ ¬p a) s)
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case mp.nil
α : Type u_1
x y : α
bs : List α
h : [] ++ [x] ++ bs = [y]
⊢ x = y

pp: case mp.cons
α : Type u_1
x y head✝ : α
tail✝ bs : List α
h : head✝ :: tail✝ ++ [x] ++ bs = [y]
⊢ x = y

Tactic:
<;>

Goal state after:
case mp.nil
α : Type u_1
x y : α
bs : List α
h : [] ++ [x] ++ bs = [y]
⊢ x = y

case mp.cons
α : Type u_1
x y head✝ : α
tail✝ bs : List α
h : head✝ :: tail✝ ++ [x] ++ bs = [y]
⊢ x = y
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case mp.nil
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ w✝ : List α
h : [] ++ head✝¹ :: head✝ :: tail✝ ++ w✝ = [x]
⊢ head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x]

pp: case mp.cons
α : Type u_1
xs : List α
x head✝² head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ w✝ : List α
h : head✝ :: tail✝ ++ head✝² :: head✝¹ :: tail✝¹ ++ w✝ = [x]
⊢ head✝² :: head✝¹ :: tail✝¹ = [] ∨ head✝² :: head✝¹ :: tail✝¹ = [x]

Tactic:
<;>

Goal state after:
case mp.nil
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ w✝ : List α
h : [] ++ head✝¹ :: head✝ :: tail✝ ++ w✝ = [x]
⊢ head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x]

case mp.cons
α : Type u_1
xs : List α
x head✝² head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ w✝ : List α
h : head✝ :: tail✝ ++ head✝² :: head✝¹ :: tail✝¹ ++ w✝ = [x]
⊢ head✝² :: head✝¹ :: tail✝¹ = [] ∨ head✝² :: head✝¹ :: tail✝¹ = [x]
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case nil
α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g []).inits = map (map g) [].inits

pp: case append_singleton
α : Type u_1
l : List α
β : Type u_3
g : α → β
l✝ : List α
a✝¹ : α
a✝ : (map g l✝).inits = map (map g) l✝.inits
⊢ (map g (l✝ ++ [a✝¹])).inits = map (map g) (l✝ ++ [a✝¹]).inits

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g []).inits = map (map g) [].inits

case append_singleton
α : Type u_1
l : List α
β : Type u_3
g : α → β
l✝ : List α
a✝¹ : α
a✝ : (map g l✝).inits = map (map g) l✝.inits
⊢ (map g (l✝ ++ [a✝¹])).inits = map (map g) (l✝ ++ [a✝¹]).inits
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case nil
α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g []).tails = map (map g) [].tails

pp: case append_singleton
α : Type u_1
l : List α
β : Type u_3
g : α → β
l✝ : List α
a✝¹ : α
a✝ : (map g l✝).tails = map (map g) l✝.tails
⊢ (map g (l✝ ++ [a✝¹])).tails = map (map g) (l✝ ++ [a✝¹]).tails

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g []).tails = map (map g) [].tails

case append_singleton
α : Type u_1
l : List α
β : Type u_3
g : α → β
l✝ : List α
a✝¹ : α
a✝ : (map g l✝).tails = map (map g) l✝.tails
⊢ (map g (l✝ ++ [a✝¹])).tails = map (map g) (l✝ ++ [a✝¹]).tails
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case hl
α : Type u_1
l : List α
n : ℕ
⊢ (take n l).inits.length = (take (n + 1) l.inits).length

pp: case h
α : Type u_1
l : List α
n : ℕ
⊢ ∀ (i : ℕ) (h₁ : i < (take n l).inits.length) (h₂ : i < (take (n + 1) l.inits).length),
    (take n l).inits[i] = (take (n + 1) l.inits)[i]

Tactic:
<;>

Goal state after:
case hl
α : Type u_1
l : List α
n : ℕ
⊢ (take n l).inits.length = (take (n + 1) l.inits).length

case h
α : Type u_1
l : List α
n : ℕ
⊢ ∀ (i : ℕ) (h₁ : i < (take n l).inits.length) (h₂ : i < (take (n + 1) l.inits).length),
    (take n l).inits[i] = (take (n + 1) l.inits)[i]
Module: Mathlib.Data.List.Infix

Goal state before:

Tactic:
<;>

Goal state after:
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case h
α : Type u_1
l : List α
n : ℕ
⊢ ∀ (i : ℕ), i < min n l.length + 1 → min i (min n l.length) = min i l.length

Tactic:
<;>

Goal state after:
case h
α : Type u_1
l : List α
n : ℕ
⊢ ∀ (i : ℕ), i < min n l.length + 1 → min i (min n l.length) = min i l.length
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_5
s t : Finset α
h : Disjoint s t
a : α
⊢ a ∈ s.disjUnion t h ↔ a ∈ s ∨ a ∈ t

Tactic:
rcases s with ⟨⟨s⟩⟩

Goal state after:
case mk
α : Type u_5
t : Finset α
a : α
val✝ : Multiset α
s : List α
nodup✝ : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
h : Disjoint { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ } t
⊢ a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ }.disjUnion t h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ } ∨ a ∈ t
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: case empty
α : Type u_1
hm : Nodup 0
⊢ { val := 0, nodup := hm }.Nonempty ↔ 0 ≠ 0

pp: case cons
α : Type u_1
a✝¹ : α
s✝ : Multiset α
a✝ : ∀ {hm : s✝.Nodup}, { val := s✝, nodup := hm }.Nonempty ↔ s✝ ≠ 0
hm : (a✝¹ ::ₘ s✝).Nodup
⊢ { val := a✝¹ ::ₘ s✝, nodup := hm }.Nonempty ↔ a✝¹ ::ₘ s✝ ≠ 0

Tactic:
<;>

Goal state after:
case empty
α : Type u_1
hm : Nodup 0
⊢ { val := 0, nodup := hm }.Nonempty ↔ 0 ≠ 0

case cons
α : Type u_1
a✝¹ : α
s✝ : Multiset α
a✝ : ∀ {hm : s✝.Nodup}, { val := s✝, nodup := hm }.Nonempty ↔ s✝ ≠ 0
hm : (a✝¹ ::ₘ s✝).Nodup
⊢ { val := a✝¹ ::ₘ s✝, nodup := hm }.Nonempty ↔ a✝¹ ::ₘ s✝ ≠ 0
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: case fst
α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝ : f a × ((i : α) → i ∈ s → f i)
⊢ (consPiProd f has (prodPiCons f has x✝)).1 = x✝.1

pp: case snd
α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝¹ : f a × ((i : α) → i ∈ s → f i)
x✝ : α
hi : x✝ ∈ s
⊢ (consPiProd f has (prodPiCons f has x✝¹)).2 x✝ hi = x✝¹.2 x✝ hi

Tactic:
<;>

Goal state after:
case fst
α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝ : f a × ((i : α) → i ∈ s → f i)
⊢ (consPiProd f has (prodPiCons f has x✝)).1 = x✝.1

case snd
α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝¹ : f a × ((i : α) → i ∈ s → f i)
x✝ : α
hi : x✝ ∈ s
⊢ (consPiProd f has (prodPiCons f has x✝¹)).2 x✝ hi = x✝¹.2 x✝ hi
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t✝ : Finset α
a b : α
f : α → β
t : Finset α
x : α
h : x ∉ t
⊢ (fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩) ((fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) none) = none

pp: case some
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t✝ : Finset α
a b : α
f : α → β
t : Finset α
x : α
h : x ∉ t
y : ↥t
⊢ (fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩) ((fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) (some y)) = some y

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t✝ : Finset α
a b : α
f : α → β
t : Finset α
x : α
h : x ∉ t
⊢ (fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩) ((fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) none) = none

case some
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t✝ : Finset α
a b : α
f : α → β
t : Finset α
x : α
h : x ∉ t
y : ↥t
⊢ (fun y ↦ if h : ↑y = x then none else some ⟨↑y, ⋯⟩) ((fun y ↦ y.elim ⟨x, ⋯⟩ fun z ↦ ⟨↑z, ⋯⟩) (some y)) = some y