mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_1
α : Type u_1
s : Multiset α
a : α
hs : s ⊂ {a}
b : α
hb : b ∈ s
⊢ {a} ⊆ s

pp: case refine_2
α : Type u_1
s : Multiset α
a : α
⊢ s = 0 → s ⊂ {a}

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
s : Multiset α
a : α
hs : s ⊂ {a}
b : α
hb : b ∈ s
⊢ {a} ⊆ s
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_2
α : Type u_1
s : Multiset α
a : α
⊢ s = 0 → s ⊂ {a}

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
s : Multiset α
a : α
⊢ s = 0 → s ⊂ {a}
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_2
α : Type u_1
s : Multiset α
a : α
⊢ s = 0 → s ⊂ {a}

Tactic:
· rintro rfl
    simp

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

Goal state before:
pp: case refine_1
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ (∀ (x : α), x ∈ 0 → r x x) → Rel r 0 0

pp: case refine_2
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ ∀ (a : α) (s : Multiset α),
    ((∀ (x : α), x ∈ s → r x x) → Rel r s s) → (∀ (x : α), x ∈ a ::ₘ s → r x x) → Rel r (a ::ₘ s) (a ::ₘ s)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ (∀ (x : α), x ∈ 0 → r x x) → Rel r 0 0
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: case mp
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ (∃ a, a ::ₘ m ≤ replicate (n + 1) x) → m ≤ replicate n x

pp: case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ m ≤ replicate n x → ∃ a, a ::ₘ m ≤ replicate (n + 1) x

Tactic:
·

Goal state after:
case mp
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ (∃ a, a ::ₘ m ≤ replicate (n + 1) x) → m ≤ replicate n x
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_2
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ ∀ (a : α) (s : Multiset α),
    ((∀ (x : α), x ∈ s → r x x) → Rel r s s) → (∀ (x : α), x ∈ a ::ₘ s → r x x) → Rel r (a ::ₘ s) (a ::ₘ s)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ ∀ (a : α) (s : Multiset α),
    ((∀ (x : α), x ∈ s → r x x) → Rel r s s) → (∀ (x : α), x ∈ a ::ₘ s → r x x) → Rel r (a ::ₘ s) (a ::ₘ s)
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ m ≤ replicate n x → ∃ a, a ::ₘ m ≤ replicate (n + 1) x

Tactic:
·

Goal state after:
case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ m ≤ replicate n x → ∃ a, a ::ₘ m ≤ replicate (n + 1) x
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mp
α : Type u_1
s t : Multiset α
⊢ Rel (fun x1 x2 ↦ x1 = x2) s t → s = t

pp: case mpr
α : Type u_1
s t : Multiset α
⊢ s = t → Rel (fun x1 x2 ↦ x1 = x2) s t

Tactic:
·

Goal state after:
case mp
α : Type u_1
s t : Multiset α
⊢ Rel (fun x1 x2 ↦ x1 = x2) s t → s = t
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mpr
α : Type u_1
s t : Multiset α
⊢ s = t → Rel (fun x1 x2 ↦ x1 = x2) s t

Tactic:
·

Goal state after:
case mpr
α : Type u_1
s t : Multiset α
⊢ s = t → Rel (fun x1 x2 ↦ x1 = x2) s t
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: case e'_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = List.count a (List.replicate n ?convert_1)

pp: case e'_3.h₁
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ b = a ↔ (?convert_1 == a) = true

pp: case convert_1
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ α

Tactic:
·

Goal state after:
case e'_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = List.count a (List.replicate n ?convert_1)
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case nil
α : Type u
h : ∀ (a : α), ¬[a, a] <+ []
⊢ [].Nodup

pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (a : α), ¬[a, a] <+ tail✝) → tail✝.Nodup
h : ∀ (a : α), ¬[a, a] <+ head✝ :: tail✝
⊢ (head✝ :: tail✝).Nodup

Tactic:
·

Goal state after:
case nil
α : Type u
h : ∀ (a : α), ¬[a, a] <+ []
⊢ [].Nodup
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: case e'_3.h₁
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ b = a ↔ (b == a) = true

Tactic:
·

Goal state after:
case e'_3.h₁
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ b = a ↔ (b == a) = true
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case inl
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨j, hj⟩
hij : i < j
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

pp: case inr.inl
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi hj : i < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨i, hj⟩
⊢ ⟨i, hi⟩ = ⟨i, hj⟩

pp: case inr.inr
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨j, hj⟩
hji : j < i
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
·

Goal state after:
case inl
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨j, hj⟩
hij : i < j
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case inr.inl
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi hj : i < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨i, hj⟩
⊢ ⟨i, hi⟩ = ⟨i, hj⟩

pp: case inr.inr
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨j, hj⟩
hji : j < i
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
·

Goal state after:
case inr.inl
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi hj : i < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨i, hj⟩
⊢ ⟨i, hi⟩ = ⟨i, hj⟩
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case inr.inr
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨j, hj⟩
hji : j < i
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
·

Goal state after:
case inr.inr
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨j, hj⟩
hji : j < i
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mp
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ Rel r (a ::ₘ as) bs → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'

pp: case mpr
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ (∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs') → Rel r (a ::ₘ as) bs

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ Rel r (a ::ₘ as) bs → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
Module: Mathlib.Data.Set.List

Goal state before:
pp: case refine_1
α : Type u_1
l : List α
n : ℕ
⊢ l[n]? ∈ insert none (range (some ∘ l.get))

pp: case refine_2
α : Type u_1
l : List α
⊢ none ∈ range fun x ↦ l[x]?

pp: case refine_3
α : Type u_1
l : List α
⊢ range (some ∘ l.get) ⊆ range fun x ↦ l[x]?

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
l : List α
n : ℕ
⊢ l[n]? ∈ insert none (range (some ∘ l.get))
Module: Mathlib.Data.Set.List

Goal state before:
pp: case refine_2
α : Type u_1
l : List α
⊢ none ∈ range fun x ↦ l[x]?

pp: case refine_3
α : Type u_1
l : List α
⊢ range (some ∘ l.get) ⊆ range fun x ↦ l[x]?

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
l : List α
⊢ none ∈ range fun x ↦ l[x]?
Module: Mathlib.Data.Set.List

Goal state before:
pp: case refine_3
α : Type u_1
l : List α
⊢ range (some ∘ l.get) ⊆ range fun x ↦ l[x]?

Tactic:
·

Goal state after:
case refine_3
α : Type u_1
l : List α
⊢ range (some ∘ l.get) ⊆ range fun x ↦ l[x]?
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case pos
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
hx : tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

pp: case neg
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
hx : ¬tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

Tactic:
·

Goal state after:
case pos
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
hx : tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case neg
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
hx : ¬tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

Tactic:
·

Goal state after:
case neg
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
hx : ¬tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mp.cons.inl
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs✝ : Multiset β
m : Multiset α
b : β
bs : Multiset β
as : Multiset α
ha'b : r a b
h : Rel r as bs
ih : ∀ {as_1 : Multiset α}, a ::ₘ as_1 = as → ∃ b bs', r a b ∧ Rel r as_1 bs' ∧ bs = b ::ₘ bs'
hm : a ::ₘ as = a ::ₘ as
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'

pp: case mp.cons.inr
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
_h : a ≠ a'
cs : Multiset α
eq₁ : as = a' ::ₘ cs
eq₂ : as' = a ::ₘ cs
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'

Tactic:
·

Goal state after:
case mp.cons.inl
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs✝ : Multiset β
m : Multiset α
b : β
bs : Multiset β
as : Multiset α
ha'b : r a b
h : Rel r as bs
ih : ∀ {as_1 : Multiset α}, a ::ₘ as_1 = as → ∃ b bs', r a b ∧ Rel r as_1 bs' ∧ bs = b ::ₘ bs'
hm : a ::ₘ as = a ::ₘ as
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mp.cons.inr
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
_h : a ≠ a'
cs : Multiset α
eq₁ : as = a' ::ₘ cs
eq₂ : as' = a ::ₘ cs
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'

Tactic:
·

Goal state after:
case mp.cons.inr
α : Type u_1
β : Type v
r : α → β → Prop
a : α
bs✝ : Multiset β
m : Multiset α
a' : α
b : β
as' : Multiset α
bs : Multiset β
ha'b : r a' b
h : Rel r as' bs
ih : ∀ {as : Multiset α}, a ::ₘ as = as' → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
as : Multiset α
hm : a ::ₘ as = a' ::ₘ as'
_h : a ≠ a'
cs : Multiset α
eq₁ : as = a' ::ₘ cs
eq₂ : as' = a ::ₘ cs
⊢ ∃ b_1 bs', r a b_1 ∧ Rel r as bs' ∧ b ::ₘ bs = b_1 ::ₘ bs'
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case neg.inl
α : Type u
x hd : α
hl : [] ≠ [x] ↔ [] = [] ∨ ∃ y, y ∈ [] ∧ y ≠ x
h : [hd].Nodup
⊢ [hd] ≠ [x] ↔ [hd] = [] ∨ ∃ y, y ∈ [hd] ∧ y ≠ x

pp: case neg.inr
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

Tactic:
·

Goal state after:
case neg.inl
α : Type u
x hd : α
hl : [] ≠ [x] ↔ [] = [] ∨ ∃ y, y ∈ [] ∧ y ≠ x
h : [hd].Nodup
⊢ [hd] ≠ [x] ↔ [hd] = [] ∨ ∃ y, y ∈ [hd] ∧ y ≠ x
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ (∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs') → Rel r (a ::ₘ as) bs

Tactic:
·

Goal state after:
case mpr
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ (∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs') → Rel r (a ::ₘ as) bs
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case neg.inr
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

Tactic:
·

Goal state after:
case neg.inr
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
Module: Mathlib.Data.Multiset.AddSub

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

pp: case inr
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a b : α
h : a ∈ s
hab : a ≠ b
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ (a ::ₘ s).erase a = a ::ₘ s.erase a
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case inr
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a b : α
h : a ∈ s
hab : a ≠ b
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a b : α
h : a ∈ s
hab : a ≠ b
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ::ₘ s = t → a ∈ t ∧ s = t.erase a

pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ t ∧ s = t.erase a → a ::ₘ s = t

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ::ₘ s = t → a ∈ t ∧ s = t.erase a
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ t ∧ s = t.erase a → a ::ₘ s = t

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ t ∧ s = t.erase a → a ::ₘ s = t
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case cons.inl
α : Type u_1
β : Type v
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
a✝ : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a = x
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b

pp: case cons.inr
α : Type u_1
β : Type v
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
a✝ : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a ∈ s
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b

Tactic:
·

Goal state after:
case cons.inl
α : Type u_1
β : Type v
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
a✝ : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a = x
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case cons.inr
α : Type u_1
β : Type v
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
a✝ : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a ∈ s
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b

Tactic:
·

Goal state after:
case cons.inr
α : Type u_1
β : Type v
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
a✝ : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a ∈ s
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_1
α : Type u_1
m2 : Multiset α
r : α → α → Prop
⊢ ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ 0 → r a b) → m1.card = card 0 → Rel r m1 0

pp: case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
⊢ ∀ (a : α) (s : Multiset α),
    (∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ s → r a b) → m1.card = s.card → Rel r m1 s) →
      ∀ {m1 : Multiset α},
        (∀ (a_2 b : α), a_2 ∈ m1 → b ∈ a ::ₘ s → r a_2 b) → m1.card = (a ::ₘ s).card → Rel r m1 (a ::ₘ s)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
m2 : Multiset α
r : α → α → Prop
⊢ ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ 0 → r a b) → m1.card = card 0 → Rel r m1 0
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case cons.inl.inl
α : Type u
β : Type v
f : α → β
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
y✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y✝) ∧ (map f tl).Nodup
h₃ : f y✝ = f y✝
⊢ y✝ = y✝

pp: case cons.inl.inr
α : Type u
β : Type v
f : α → β
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f x✝) ∧ (map f tl).Nodup
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝

pp: case cons.inr.inl
α : Type u
β : Type v
f : α → β
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y✝) ∧ (map f tl).Nodup
h₃ : f x✝ = f y✝
⊢ x✝ = y✝

pp: case cons.inr.inr
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ (map f tl).Nodup
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝

Tactic:
·

Goal state after:
case cons.inl.inl
α : Type u
β : Type v
f : α → β
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
y✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y✝) ∧ (map f tl).Nodup
h₃ : f y✝ = f y✝
⊢ y✝ = y✝
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
⊢ ∀ (a : α) (s : Multiset α),
    (∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ s → r a b) → m1.card = s.card → Rel r m1 s) →
      ∀ {m1 : Multiset α},
        (∀ (a_2 b : α), a_2 ∈ m1 → b ∈ a ::ₘ s → r a_2 b) → m1.card = (a ::ₘ s).card → Rel r m1 (a ::ₘ s)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
⊢ ∀ (a : α) (s : Multiset α),
    (∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ s → r a b) → m1.card = s.card → Rel r m1 s) →
      ∀ {m1 : Multiset α},
        (∀ (a_2 b : α), a_2 ∈ m1 → b ∈ a ::ₘ s → r a_2 b) → m1.card = (a ::ₘ s).card → Rel r m1 (a ::ₘ s)
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case cons.inl.inr
α : Type u
β : Type v
f : α → β
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f x✝) ∧ (map f tl).Nodup
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝

pp: case cons.inr.inl
α : Type u
β : Type v
f : α → β
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y✝) ∧ (map f tl).Nodup
h₃ : f x✝ = f y✝
⊢ x✝ = y✝

pp: case cons.inr.inr
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ (map f tl).Nodup
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝

Tactic:
·

Goal state after:
case cons.inl.inr
α : Type u
β : Type v
f : α → β
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f x✝) ∧ (map f tl).Nodup
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case cons.inr.inl
α : Type u
β : Type v
f : α → β
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y✝) ∧ (map f tl).Nodup
h₃ : f x✝ = f y✝
⊢ x✝ = y✝

pp: case cons.inr.inr
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ (map f tl).Nodup
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝

Tactic:
·

Goal state after:
case cons.inr.inl
α : Type u
β : Type v
f : α → β
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y✝) ∧ (map f tl).Nodup
h₃ : f x✝ = f y✝
⊢ x✝ = y✝
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case mp
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ (∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs') →
    ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

pp: case mpr
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ (∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁) →
    ∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ (∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs') →
    ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case cons.inr.inr
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ (map f tl).Nodup
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝

Tactic:
·

Goal state after:
case cons.inr.inr
α : Type u
β : Type v
f : α → β
hd : α
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
d : (∀ (x : α), x ∈ tl → f x ≠ f hd) ∧ (map f tl).Nodup
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
h₂ : y✝ ∈ tl
h₃ : f x✝ = f y✝
⊢ x✝ = y✝