mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

Tactic:
obtain ⟨q₂, hx₂, hy₂⟩ := exists_rat_btwn (max_lt h hy)
  obtain ⟨q₁, hx₁, hq₁₂⟩ := exists_rat_btwn hx₂
  have : (0 : K) < q₂ := (le_max_right _ _).trans_lt hx₂
  norm_cast at hq₁₂ this
  obtain ⟨q, hq, hq₁, hq₂⟩ := exists_pow_btwn hn hq₁₂ this
  refine ⟨q, hq, (le_max_left _ _).trans_lt <| hx₁.trans ?_, hy₂.trans' ?_⟩ <;> assumption_mod_cast

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
n m : ℕ
m0 : 0 < m
⊢ n ≤ n * m

Tactic:
]

Goal state after:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
n m : ℕ
m0 : 0 < m
⊢ n ≤ n * m
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K✝ : Type u_4
K : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
⊢ ∀ (x : K), ∃ n, x ≤ ↑n

Tactic:
]

Goal state after:
G : Type u_1
M : Type u_2
R : Type u_3
K✝ : Type u_4
K : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
⊢ ∀ (x : K), ∃ n, x ≤ ↑n
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: case mp
α : Type u_1
l : List α
a : α
⊢ (∃ l_1, l_1 ~ [a] ∧ l <+ l_1) → l = [] ∨ l = [a]

Tactic:
]

Goal state after:
case mp
α : Type u_1
l : List α
a : α
⊢ (∃ l_1, l_1 ~ [a] ∧ l <+ l_1) → l = [] ∨ l = [a]
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: case mp
α : Type u_1
l : List α
a : α
s : List α
hla : s ~ [a]
h : l = [] ∨ l = [a]
⊢ l = [] ∨ l = [a]

Tactic:
]

Goal state after:
case mp
α : Type u_1
l : List α
a : α
s : List α
hla : s ~ [a]
h : l = [] ∨ l = [a]
⊢ l = [] ∨ l = [a]
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: case h.left
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
sublist : w <+ map f l₂
x : List α
perm : map f x ~ map f l₁
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ x ~ l₁

Tactic:
]

Goal state after:
case h.left
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
sublist : w <+ map f l₂
x : List α
perm : map f x ~ map f l₁
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ x ~ l₁
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p : P
⊢ {1} = {1}

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p : P
h : p₁ = p₂
⊢ p₁ = p₂

Tactic:
]

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p : P
h : p₁ = p₂
⊢ p₁ = p₂
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p : P
h : p /ₛ p₁ = p /ₛ p₂
⊢ p = p

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ p₁ /ₛ p₂ = p₁ /ₛ p₂

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v : G
p₁ p₂ : P
⊢ p₁ /ₛ p₂ = p₁ /ₛ p₂

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ / v₂ * (p₁ /ₛ p₂) = v₁ / v₂ * (p₁ /ₛ p₂)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₂) * ((p₃ /ₛ p₁) / (p₃ /ₛ p₂)) = 1

Tactic:
]

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₂) * ((p₃ /ₛ p₁) / (p₃ /ₛ p₂)) = 1
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₂ / v₁ = p₁ /ₛ p₂ ↔ v₂ / v₁ = p₁ /ₛ p₂

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ p₄ : P
⊢ (p₁ /ₛ p₃) / (p₂ /ₛ p₄) = (p₁ /ₛ p₃) / (p₂ /ₛ p₄)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ y = x ↔ y = x

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_5
P : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x ↦ 2 • x
y x₁ x₂ : P
hy : x₁ = x₂
⊢ x₁ = x₂

Tactic:
]

Goal state after:
G : Type u_5
P : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x ↦ 2 • x
y x₁ x₂ : P
hy : x₁ = x₂
⊢ x₁ = x₂
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ a ∈ s ↔ a ∈ s

Tactic:
]

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

Goal state before:
pp: case empty
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
t : Multiset α
h : Rel r 0 t
⊢ countP (r x) 0 = countP (r x) 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p l₁ = countP p (l₁.diff l₂ ++ l₂)

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p l₁ = countP p (l₁.diff l₂ ++ l₂)
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ (countP (r x) bs + if r x y then 1 else 0) = countP (r x) bs + if r x b then 1 else 0

Tactic:
]

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ (countP (r x) bs + if r x y then 1 else 0) = countP (r x) bs + if r x b then 1 else 0
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
H : ∀ (x : α), ¬x ∈ Quot.mk (⇑(isSetoid α)) l
⊢ Quot.mk ⇑(isSetoid α) [] = 0

Tactic:
]

Goal state after:
α : Type u_1
s : Multiset α
l : List α
H : ∀ (x : α), ¬x ∈ Quot.mk (⇑(isSetoid α)) l
⊢ Quot.mk ⇑(isSetoid α) [] = 0
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
a b : α
as bs : Multiset α
this✝² : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝¹ : a ∈ b ::ₘ bs
this✝ : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this : a ::ₘ as = b ::ₘ a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ a ::ₘ cs

Tactic:
]

Goal state after:
α : Type u_1
a b : α
as bs : Multiset α
this✝² : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝¹ : a ∈ b ::ₘ bs
this✝ : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this : a ::ₘ as = b ::ₘ a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ a ::ₘ cs
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
a : α
⊢ a ∈ a ::ₘ 0

Tactic:
]

Goal state after:
α : Type u_1
a : α
⊢ a ∈ a ::ₘ 0
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
l : List α
a : α
⊢ l = [a] ↔ l = [a]

Tactic:
]

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

Goal state before:
pp: α : Type u_1
a b : α
m : Multiset α
⊢ (a = b ∧ 0 = m ∨ a ≠ b ∧ ∃ cs, 0 = b ::ₘ cs ∧ m = a ::ₘ cs) ↔ a = b ∧ m = 0

Tactic:
]

Goal state after:
α : Type u_1
a b : α
m : Multiset α
⊢ (a = b ∧ 0 = m ∨ a ≠ b ∧ ∃ cs, 0 = b ::ₘ cs ∧ m = a ::ₘ cs) ↔ a = b ∧ m = 0
Module: Mathlib.Data.Multiset.ZeroCons

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
a b : α
⊢ 1 + 1 = 2

Tactic:
]

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

Goal state before:
pp: α : Type u_1
a : α
k n : ℕ
⊢ replicate k a ≤ replicate n a ↔ replicate k a ≤ replicate n a

Tactic:
]

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

Goal state before:
pp: α : Type u_1
a : α
k n : ℕ
⊢ replicate k a ≤ replicate n a ↔ List.replicate k a <+ List.replicate n a

Tactic:
rw [← replicate_le_coe, coe_replicate]

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

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

Tactic:
]

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

Goal state before:
pp: case mp
α : Type u_1
m : Multiset α
x : α
n : ℕ
x' : α
hx' : m ≤ replicate n x
this : x' = x
⊢ m ≤ replicate n x

Tactic:
]

Goal state after:
case mp
α : Type u_1
m : Multiset α
x : α
n : ℕ
x' : α
hx' : m ≤ replicate n x
this : x' = x
⊢ m ≤ replicate n x
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ x ::ₘ replicate n x

Tactic:
]

Goal state after:
case mpr
α : Type u_1
m : Multiset α
x : α
n : ℕ
h : m ≤ replicate n x
⊢ ∃ a, a ::ₘ m ≤ x ::ₘ replicate n x
Module: Mathlib.Data.Multiset.Replicate

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ s = t ↔ s = t

Tactic:
]

Goal state after:
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) = count a (replicate n ?e'_2.a)

pp: case e'_2.a
α : Type u_1
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ α

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
b : Multiset β
⊢ (0 = 0 ∧ b = 0 ∨ ∃ a b_1 as bs, r a b_1 ∧ Rel r as bs ∧ 0 = a ::ₘ as ∧ b = b_1 ::ₘ bs) ↔ b = 0

Tactic:
]

Goal state after:
α : Type u_1
β : Type v
r : α → β → Prop
b : Multiset β
⊢ (0 = 0 ∧ b = 0 ∨ ∃ a b_1 as bs, r a b_1 ∧ Rel r as bs ∧ 0 = a ::ₘ as ∧ b = b_1 ::ₘ bs) ↔ b = 0
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: α : Type u_1
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
b : α
hb1 : b ∈ replicate n a
hb2 : flip r x a
⊢ r a x

Tactic:
]

Goal state after:
α : Type u_1
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
b : α
hb1 : b ∈ replicate n a
hb2 : flip r x a
⊢ r a x
Module: Mathlib.Data.Multiset.Replicate

Goal state before:
pp: α : Type u_1
s : Multiset α
h : ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
a : α
le : a ::ₘ a ::ₘ 0 ≤ s
t : Multiset α
s_eq : s = a ::ₘ a ::ₘ t
⊢ s = a ::ₘ a ::ₘ t

Tactic:
]

Goal state after:
α : Type u_1
s : Multiset α
h : ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t
a : α
le : a ::ₘ a ::ₘ 0 ≤ s
t : Multiset α
s_eq : s = a ::ₘ a ::ₘ t
⊢ s = a ::ₘ a ::ₘ t
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
a : Multiset α
⊢ (a = 0 ∧ 0 = 0 ∨ ∃ a_1 b as bs, r a_1 b ∧ Rel r as bs ∧ a = a_1 ::ₘ as ∧ 0 = b ::ₘ bs) ↔ a = 0

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ {l | ∀ (x : α), x ∈ l → x ∈ s} = {l | ∀ (x : α), x ∈ l → x ∈ s}

Tactic:
]

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ (∃ y, l.get y = x) ↔ ∃ n, l.get n = x

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_1
l : List α
⊢ (range fun x ↦ l[x]?) = insert none (range (some ∘ l.get))
Module: Mathlib.Data.Set.List

Goal state before:
pp: α : Type u_1
β : Type u_2
l✝ : List α
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
l : List α
H : ∀ (x : α), x ∈ l → p x
⊢ l ∈ {l | ∀ (x : α), x ∈ l → x ∈ Set.range c}

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
l✝ : List α
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
l : List α
H : ∀ (x : α), x ∈ l → p x
⊢ l ∈ {l | ∀ (x : α), x ∈ l → x ∈ Set.range c}
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 = [] ∨ ∃ y, y ∈ tl ∧ y ≠ 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 = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
Module: Mathlib.Data.Multiset.ZeroCons

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

Tactic:
]

Goal state after:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
⊢ (∃ b_1 bs', flip r b b_1 ∧ Rel (flip r) bs bs' ∧ as = b_1 ::ₘ bs') ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ {a} + (s + t) = {a} + (s + t)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ a ::ₘ (s + t) = a ::ₘ (s + t)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
a : α
as' : Multiset α
⊢ r a b ∧ Rel r as' bs ∧ as = a ::ₘ as' ↔ r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ s ≤ a ::ₘ s

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ s ≤ a ::ₘ s
Module: Mathlib.Data.Multiset.AddSub

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

Tactic:
]

Goal state after:
α : 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: α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : a ∈ t
⊢ s + t.erase a = s + t.erase a

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : ¬a ∈ t
⊢ s.erase a + t = s.erase a + t

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
h : a ::ₘ s.erase a ≤ a ::ₘ t
m : a ∈ s
⊢ s.erase a ≤ t

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
h : a ::ₘ s.erase a ≤ a ::ₘ t
m : a ∈ s
⊢ s.erase a ≤ t
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ s.card.pred = s.card.pred

pp: case pos.hc
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ a ∈ s

Tactic:
]

Goal state after:
case pos.hc
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ a ∈ s
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ s.card = s.card

pp: case neg.hnc
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ ¬a ∈ s

Tactic:
]

Goal state after:
case neg.hnc
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ ¬a ∈ s
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = count a ↑(l.erase a)

Tactic:
]

Goal state after:
case e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = count a ↑(l.erase a)
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case e'_3
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = count a ↑l

Tactic:
]

Goal state after:
case e'_3
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = count a ↑l
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case e'_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = count a ↑(l.erase b)

Tactic:
]

Goal state after:
case e'_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = count a ↑(l.erase b)
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case e'_3
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = count a ↑l

Tactic:
]

Goal state after:
case e'_3
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = count a ↑l
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
xs : List α
n m : Fin xs.length
h : xs.get n = xs.get m
hne : n ≠ m
⊢ ¬Injective xs.get

Tactic:
]

Goal state after:
α : Type u
xs : List α
n m : Fin xs.length
h : xs.get n = xs.get m
hne : n ≠ m
⊢ ¬Injective xs.get
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s ≤ t + u ↔ s ≤ t + u

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ≤ s + t

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ≤ s + t
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
⊢ count x l ≤ 1 ↔ 0 < count x l → count x l = 1

Tactic:
]

Goal state after:
α : Type u
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
⊢ count x l ≤ 1 ↔ 0 < count x l → count x l = 1
Module: Mathlib.Data.Multiset.AddSub

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

Tactic:
]

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

Goal state before:
pp: α : Type u
a : α
l₁ l₂ : List α
⊢ (l₁ ++ a :: l₂).Nodup ↔ (a :: (l₁ ++ l₂)).Nodup

Tactic:
simp only [nodup_append', not_or, and_left_comm, and_assoc, nodup_cons, mem_append,
    disjoint_cons_right]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
h : t ≤ s
⊢ {a} + (s - t) = {a} + (s - t)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : t ≤ s
⊢ s.card = s.card

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a t < count a s ↔ count a t < count a s

Tactic:
]

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

Goal state before:
pp: case refine_1
α : Type u_1
m2 : Multiset α
r : α → α → Prop
m : Multiset α
_h : ∀ (a b : α), a ∈ m → b ∈ 0 → r a b
hc : m.card = card 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : m.card = t.card + 1
⊢ Rel r m (a ::ₘ t)

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : m.card = t.card + 1
⊢ Rel r m (a ::ₘ t)
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
u : α
⊢ (l.concat u).reverse.Nodup ↔ ¬u ∈ l ∧ l.Nodup

Tactic:
]

Goal state after:
α : Type u
l : List α
u : α
⊢ (l.concat u).reverse.Nodup ↔ ¬u ∈ l ∧ l.Nodup
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ (∃ bs₀_1 bs₁_1, Rel (flip r) bs₀ bs₀_1 ∧ Rel (flip r) bs₁ bs₁_1 ∧ as = bs₀_1 + bs₁_1) ↔
    ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁

Tactic:
]

Goal state after:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ (∃ bs₀_1 bs₁_1, Rel (flip r) bs₀ bs₀_1 ∧ Rel (flip r) bs₁ bs₁_1 ∧ as = bs₀_1 + bs₁_1) ↔
    ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case empty
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
s u : Multiset α
r1 : Rel r s 0
r2 : Rel r 0 u
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
hl : ¬l = []
h : a = l[l.length - 1]
⊢ (l[l.length - 1] :: l.dropLast).Nodup ↔ ([l.getLast hl] ++ l.dropLast).Nodup

Tactic:
]

Goal state after:
case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
hl : ¬l = []
h : a = l[l.length - 1]
⊢ (l[l.length - 1] :: l.dropLast).Nodup ↔ ([l.getLast hl] ++ l.dropLast).Nodup
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
⊢ count a s ≤ count a t

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : s.Nodup
h : a ∈ s - t
h' : a ∈ t
⊢ count a s ≤ count a t
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : l₁ <+: l₂
hne : l₂ ≠ []
hl : l₂.getLast hne ∈ l₁
hnd : l₂.Nodup
⊢ l₁ = l₂

Tactic:
by
  grind [List.IsPrefix]

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

Goal state before:
pp: α : Type u
β : Type v
l₁ : List α
f : α → List β
⊢ (Pairwise (fun a b ↦ (f a).Disjoint (f b)) l₁ ∧ ∀ (x : α), x ∈ l₁ → (f x).Nodup) ↔
    Pairwise (Disjoint on f) l₁ ∧ ∀ (x : α), x ∈ l₁ → (f x).Nodup

Tactic:
]

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

Goal state before:
pp: α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : f a = some b
b' : β
bm' : f a' = some b'
e : b = b'
⊢ b ∈ f a

Tactic:
]

Goal state after:
α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : f a = some b
b' : β
bm' : f a' = some b'
e : b = b'
⊢ b ∈ f a
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
a : α
h : ¬a ∈ l
h' : l.Nodup
⊢ (l ++ [a]).Nodup

Tactic:
]

Goal state after:
α : Type u
l : List α
a : α
h : ¬a ∈ l
h' : l.Nodup
⊢ (l ++ [a]).Nodup
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : a ∈ l
⊢ l.Nodup

Tactic:
]

Goal state after:
α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : a ∈ l
⊢ l.Nodup