mathlib-initiative/mathlib-tactics huggingface dataset:
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₁ • p₁ /ₛ v₂ • p₂ = v₁ / v₂ * (p₁ /ₛ p₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ 0 < countP p (Quot.mk (⇑(isSetoid α)) _l) ↔ ∃ a, a ∈ Quot.mk (⇑(isSetoid α)) _l ∧ p a

Tactic:
by

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₁

Tactic:
by

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₁ • p₁ = v₂ • p₂ ↔ v₂ / v₁ = p₁ /ₛ p₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ countP p (Quot.mk (⇑(isSetoid α)) _l) = 0 ↔ ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) _l → ¬p a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ countP p (Quot.mk (⇑(isSetoid α)) _l) = card (Quot.mk (⇑(isSetoid α)) _l) ↔
    ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) _l → p a

Tactic:
by

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:
by

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
s t : Set P
⊢ v • s /ₛ v • t = s /ₛ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hs : Quot.mk (⇑(isSetoid α)) l = Quot.mk (⇑(isSetoid α)) l'
hp : ∀ (x : α), x ∈ Quot.mk (⇑(isSetoid α)) l → p x = p' x
⊢ countP p (Quot.mk (⇑(isSetoid α)) l) = countP p' (Quot.mk (⇑(isSetoid α)) l')

Tactic:
by

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
P : Type u_3
P' : Type u_4
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Torsor G P
inst✝ : Torsor G' P'
s₁ s₂ : Set P
t₁ t₂ : Set P'
⊢ s₁ ×ˢ t₁ /ₛ s₂ ×ˢ t₂ = (s₁ /ₛ s₂) ×ˢ (t₁ /ₛ t₂)

Tactic:
by

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
⊢ -(x -ᵥ (pointReflection x) y) = -(y -ᵥ x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s s' : Multiset α
hs : s = s'
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
hp : ∀ (x : α), x ∈ s → p x = p' x
⊢ countP p s = countP p' s'

Tactic:
by

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
⊢ -(y -ᵥ (pointReflection x) y) = -(2 • (y -ᵥ x))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ count a ↑l = List.count a l

Tactic:
by

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
⊢ (pointReflection x) y = y ↔ y = x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
⊢ count a {b} = if a = b then 1 else 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a x✝¹ : { x // x ∈ s }
x✝ : x✝¹ ∈ s.attach
⊢ (a = x✝¹) = (↑a = ↑x✝¹)

Tactic:
by

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 : (pointReflection x₁) y = (pointReflection x₂) y
⊢ x₁ = x₂

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: G : Type u_5
inst✝ : AddCommGroup G
x : G
⊢ pointReflection x = Equiv.subLeft (2 • x)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁴ : Group G
inst✝³ : Torsor G P
inst✝² : SMul G Q
inst✝¹ : SDiv G Q
inst✝ : Nonempty Q
f : Q → P
hf : Injective f
smul : ∀ (c : G) (x : Q), f (c • x) = c • f x
sdiv : ∀ (x y : Q), x /ₛ y = f x /ₛ f y
x y : Q
⊢ f ((x /ₛ y) • y) = f x

Tactic:
by

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

Goal state before:
pp: G : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁴ : Group G
inst✝³ : Torsor G P
inst✝² : SMul G Q
inst✝¹ : SDiv G Q
inst✝ : Nonempty Q
f : Q → P
hf : Injective f
smul : ∀ (c : G) (x : Q), f (c • x) = c • f x
sdiv : ∀ (x y : Q), x /ₛ y = f x /ₛ f y
c : G
x : Q
⊢ c • x /ₛ x = c

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: G : Type u_1
P : Type u_2
Q : Type u_3
inst✝³ : Group G
inst✝² : Torsor G P
inst✝¹ : SMul G Q
inst✝ : SDiv G Q
f : P → Q
hf : Surjective f
smul : ∀ (c : G) (x : P), f (c • x) = c • f x
sdiv : ∀ (x y : P), x /ₛ y = f x /ₛ f y
⊢ ∀ (p₁ p₂ : Q), (p₁ /ₛ p₂) • p₂ = p₁

Tactic:
by

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

Goal state before:
pp: G : Type u_1
P : Type u_2
Q : Type u_3
inst✝³ : Group G
inst✝² : Torsor G P
inst✝¹ : SMul G Q
inst✝ : SDiv G Q
f : P → Q
hf : Surjective f
smul : ∀ (c : G) (x : P), f (c • x) = c • f x
sdiv : ∀ (x y : P), x /ₛ y = f x /ₛ f y
⊢ ∀ (g : G) (p : Q), g • p /ₛ p = g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ count a s = s.card ↔ ∀ (x : α), x ∈ s → a = x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
_l₁ _l₂ : List α
⊢ (isSetoid α) _l₁ _l₂ ↔ ∀ (a : α), count a ⟦_l₁⟧ = count a ⟦_l₂⟧

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
x✝¹ x✝ : List α
⊢ ⟦x✝¹⟧ ≤ ⟦x✝⟧ ↔ ∀ (a : α), count a ⟦x✝¹⟧ ≤ count a ⟦x✝⟧

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
p : α → Bool
⊢ countP p l < l.length ↔ ∃ a, a ∈ l ∧ p a = false

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ count a l < l.length ↔ ∃ b, b ∈ l ∧ b ≠ a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
l : List α
a : α
⊢ countP p (l.erase a) = countP p l - if a ∈ l ∧ p a = true then 1 else 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
b : α
l₂ : List α
⊢ count a (l₁.diff (b :: l₂)) = count a l₁ - count a (b :: l₂)

Tactic:
by

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₁.diff l₂) = countP p l₁ - countP p l₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
l : List α
f : α → β
hf : Function.Injective f
x : α
⊢ count (f x) (map f l) = count x l

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
_l : List α
⊢ Nodup (Quot.mk (⇑(isSetoid α)) _l) ↔ ∀ (a : α), count a (Quot.mk (⇑(isSetoid α)) _l) ≤ 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Multiset α
inst✝ : DecidableEq α
_l : List α
⊢ Nodup (Quot.mk (⇑(isSetoid α)) _l) ↔
    ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) _l → count a (Quot.mk (⇑(isSetoid α)) _l) = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
⊢ count a s = if a ∈ s then 1 else 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
inst✝ : IsEmpty α
⊢ ∀ (a : Multiset α), a = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
⊢ ∀ {s t : Multiset α}, a ::ₘ s = a ::ₘ t ↔ s = t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
⊢ ∀ (s : Multiset α), p s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
C : Multiset α → Sort u_3
C_0 : C 0
C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)
C_cons_heq :
  ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)
m : Multiset α
x✝² x✝¹ : List α
h : x✝² ≈ x✝¹
a✝ : α
l✝ l'✝ : List α
b✝ : C ⟦l✝⟧
b'✝ : C ⟦l'✝⟧
hl : l✝ ~ l'✝
x✝ : b✝ ≍ b'✝
⊢ C_cons a✝ ⟦l✝⟧ b✝ ≍ C_cons a✝ ⟦l'✝⟧ b'✝

Tactic:
by

Goal state after:
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 α)) l = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Multiset α
l✝ : List α
hl : Quot.mk (⇑(isSetoid α)) l✝ ≠ 0
a : α
l : List α
x✝ : Quot.mk (⇑(isSetoid α)) (a :: l) ≠ 0
⊢ a ∈ Quot.mk (⇑(isSetoid α)) (a :: l)

Tactic:
by

Goal state after:
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
⊢ a ∈ bs

Tactic:
by

Goal state after:
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
⊢ a ::ₘ as = b ::ₘ a ::ₘ cs

Tactic:
by

Goal state after:
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 = a ::ₘ b ::ₘ cs

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a b : α
as bs : Multiset α
⊢ a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a b : α
⊢ b ∈ {a} ↔ b = a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
⊢ a ∈ {a}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a b : α
⊢ {a} = {b} ↔ a = b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a b : α
m : Multiset α
⊢ {a} = b ::ₘ m ↔ a = b ∧ m = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ a ::ₘ s ⊆ t ↔ a ∈ t ∧ s ⊆ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ 0 ⊂ s ↔ s ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
⊢ {a} ⊆ s ↔ a ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
l : List α
this : l <+~ a :: l ∧ ¬l ~ a :: l
⊢ Quot.mk (⇑(isSetoid α)) l < a ::ₘ Quot.mk (⇑(isSetoid α)) l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
this : ∀ {t' : Multiset α}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t'
⊢ s ≤ a ::ₘ t → s ≤ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
⊢ s ≤ a ::ₘ t ↔ s ≤ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
a : α
hs : ¬a ∈ s
⊢ a ::ₘ s ≤ t ↔ a ∈ t ∧ s ≤ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
l : List α
⊢ Quot.mk (⇑(isSetoid α)) l ≤ {a} ↔ Quot.mk (⇑(isSetoid α)) l = 0 ∨ Quot.mk (⇑(isSetoid α)) l = {a}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
⊢ s < {a} ↔ s = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
⊢ {a}.card = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a b : α
⊢ {a, b}.card = 2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Multiset α
e : s = 0
⊢ s.card = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Multiset α
n : ℕ
⊢ (∃ a t, a ::ₘ t = s ∧ t.card = n) → s.card = n + 1

Tactic:
by

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:
by

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

Goal state before:
pp: α : Type u_1
s : Multiset α
n : ℕ
⊢ s.card = n + 1 ↔ ∃ a t, a ::ₘ t = s ∧ t.card = n

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
r : α → β → Prop
hr : Relator.BiUnique r
⊢ (fun x1 x2 ↦ x1 ↔ x2) [].Nodup [].Nodup

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
r : α → β → Prop
hr : Relator.BiUnique r
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
hab : r a✝ b✝
h : Forall₂ r l₁✝ l₂✝
⊢ (fun x1 x2 ↦ x1 ↔ x2) (a✝ :: l₁✝).Nodup (b✝ :: l₂✝).Nodup

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
r p : α → β → Prop
s : Multiset α
t : Multiset β
hst : Rel r s t
h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b
⊢ Rel p s t

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ (∀ (a : α), ¬[a, a] <+ l) → l.Nodup

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
b : Multiset β
⊢ Rel r 0 b ↔ b = 0

Tactic:
rw [rel_iff]

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
inst✝ : DecidableEq α
a b : α
n : ℕ
⊢ count a (replicate n b) = if b = a then n else 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
b : Multiset β
⊢ Rel r 0 b ↔ b = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ count a (Quot.mk (⇑(isSetoid α)) _l) ↔ replicate n a ≤ Quot.mk (⇑(isSetoid α)) _l

Tactic:
by

Goal state after:
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
⊢ r a x

Tactic:
by

Goal state after:
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 ::ₘ 0 + t
⊢ s = a ::ₘ a ::ₘ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
a : Multiset α
⊢ Rel r a 0 ↔ a = 0

Tactic:
rw [rel_iff]

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.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
a : Multiset α
⊢ Rel r a 0 ↔ a = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
⊢ l[i] = l[j] ↔ i = j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ range (map f) = {l | ∀ (x : β), x ∈ l → x ∈ range f}

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ range l.get = {x | x ∈ l}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ (range fun x ↦ l[x]?) = insert none (some '' {x | x ∈ l})

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
d : α
⊢ (range fun n ↦ l[n]?.getD d) = (fun o ↦ o.getD d) '' range fun x ↦ l[x]?

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.Nodup ↔ ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
d : α
⊢ ((fun o ↦ o.getD d) '' range fun x ↦ l[x]?) = insert d {x | x ∈ l}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Inhabited α
l : List α
⊢ range l.getI = insert default {x | x ∈ l}

Tactic:
by

Goal state after:
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
⊢ ∃ y, map c y = l

Tactic:
by

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

Goal state before:
pp: α : 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'

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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:
by

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

Goal state before:
pp: α : 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
this : ∃ y, y ∈ hd :: tl ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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.erase a

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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 + t).erase a = s + t.erase a

Tactic:
by

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 + t).erase a = s.erase a + t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ s.erase a < s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
⊢ s.card = t.card

Tactic:
by

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

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

Tactic:
by

Goal state after: