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

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
⊢ f (x - a) = f x - b

Tactic:
simpa using

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
⊢ f (x - a) = f x - b
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℕ
⊢ f (x - ↑n) = f x - n • b

Tactic:
simpa using

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℕ
⊢ f (x - ↑n) = f x - n • b
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
⊢ ∃! k, 1 ≤ g / a ^ k ∧ g / a ^ k < a

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ k * a
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! m, b / a ^ m ∈ Ico c (c * a)

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! m, a ^ m * c ≤ b ∧ b < a * (a ^ m * c)
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! x, b * a ^ (Equiv.neg ℤ) x ∈ Ico c (c * a)

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! x, a ^ x * c ≤ b ∧ b < a * (a ^ x * c)
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! x, b * a ^ (Equiv.addRight 1) x ∈ Ioc c (c * a)

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! x, b * a ^ x ≤ c ∧ c < b * a ^ x * a
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! x, b / a ^ (Equiv.neg ℤ) x ∈ Ioc c (c * a)

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! x, b * a ^ x ∈ Ioc c (c * a)
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
n : ℤ
⊢ f (n • a) = f 0 + n • b

Tactic:
simpa using

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
n : ℤ
⊢ f (n • a) = f 0 + n • b
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
n : ℤ
⊢ f (x - n • a) = f x - n • b

Tactic:
simpa using

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
n : ℤ
⊢ f (x + -(n • a)) = f x + -(n • b)
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
this✝ : ∀ (x y : G), x < y → x ∈ Ico l (l + a) → R (f x) (f y)
hx : x ∉ Ico l (l + a)
m : ℤ
hm : x - m • a ∈ Ico l (l + a)
this : R (f (x - m • a)) (f (y - m • a))
⊢ R (f x) (f y)

Tactic:
simpa using

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
this✝ : ∀ (x y : G), x < y → x ∈ Ico l (l + a) → R (f x) (f y)
hx : x ∉ Ico l (l + a)
m : ℤ
hm : x - m • a ∈ Ico l (l + a)
this : R (f (x - m • a)) (f (y - m • a))
⊢ R (f x) (f y)
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
this : 0 < 1 - fract q
⊢ 0 < (1 - fract q) * ↑q.den

Tactic:
exact mul_pos this (by exact mod_cast q.pos)

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

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : n < 0
⊢ l + 0 • a ≤ x

Tactic:
simpa using

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : n < 0
⊢ l ≤ x
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
hny : y - 0 • a ∈ Ioc l (l + a)
⊢ y ∈ Icc l (l + a)

Tactic:
simpa using

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
hny : y - 0 • a ∈ Ioc l (l + a)
⊢ l ≤ y ∧ y ≤ l + a
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: G✝ : Type u_1
M : Type u_2
A✝ : Type u_3
B✝ : Type u_4
α : Type u_5
β : Type u_6
G : Type u_7
A : Type u_8
B : Type u_9
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
f : A → B
⊢ (fun x ↦ f (1⁻¹ • x)) = f

Tactic:
simp only [inv_one, one_smul]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
m : α
hm : IsUnit m
⊢ Function.Bijective fun a ↦ m • a

Tactic:
lift m to αˣ using hm

Goal state after:
α : Type u_5
β : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
m : αˣ
⊢ Function.Bijective fun a ↦ ↑m • a
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
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
⊢ ¬y ≤ (↑0 * δ) ^ n

Tactic:
simpa using

Goal state after:
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
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
⊢ 0 < y
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
x : K
x0 : 0 < x
⊢ ∃ q, 0 < q ∧ ↑q < x

Tactic:
simpa using

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x : K
x0 : 0 < x
⊢ ∃ q, 0 < q ∧ ↑q < x
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.toNat ≤ n.toNat • m

Tactic:
simpa using

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.toNat ≤ ↑n.toNat * m
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case coe.coe
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
y : M
hxy : 0 < ↑y
x : M
⊢ ∃ n, ↑x ≤ n • ↑y

Tactic:
simpa using

Goal state after:
case coe.coe
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
y : M
hxy : 0 < ↑y
x : M
⊢ ∃ n, x ≤ n • y
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
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
y : M
hxy : 0 < ↑y
x : M
⊢ 0 < y

Tactic:
simpa using

Goal state after:
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
y : M
hxy : 0 < ↑y
x : M
⊢ 0 < y
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case coe.coe
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
y : M
hxy : 1 < ↑y
x : M
⊢ ∃ n, ↑x ≤ ↑y ^ n

Tactic:
simpa using

Goal state after:
case coe.coe
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
y : M
hxy : 1 < ↑y
x : M
⊢ ∃ n, x ≤ y ^ n
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
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
y : M
hxy : 1 < ↑y
x : M
⊢ 1 < y

Tactic:
simpa using

Goal state after:
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : MulArchimedean M
y : M
hxy : 1 < ↑y
x : M
⊢ 1 < y
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ ∀ (a_1 : List α), p a → countP p (a ::ₘ Quot.mk (⇑(isSetoid α)) a_1) = countP p (Quot.mk (⇑(isSetoid α)) a_1) + 1

Tactic:
simpa using

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ ∀ (a_1 : List α), p a → List.countP (fun b ↦ decide (p b)) (a :: a_1) = List.countP (fun b ↦ decide (p b)) a_1 + 1
Module: Mathlib.Data.Multiset.Count

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

Tactic:
simpa using

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ ∀ (a_1 : List α), ¬p a → List.countP (fun b ↦ decide (p b)) (a :: a_1) = List.countP (fun b ↦ decide (p b)) a_1
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 α
hp : ∀ (x : α), x ∈ Quot.mk (⇑(isSetoid α)) l → p x = p' x
hs : l ~ l'
⊢ ∀ (x : α), x ∈ l → decide (p x) = decide (p' x)

Tactic:
simpa using

Goal state after:
α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hp : ∀ (x : α), x ∈ Quot.mk (⇑(isSetoid α)) l → p x = p' x
hs : l ~ l'
⊢ ∀ (x : α), x ∈ l → (p x ↔ p' x)
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:
simpa using

Goal state after:
α : Type u_1
s : Multiset α
inst✝ : DecidableEq α
_l : List α
⊢ _l.Nodup ↔ ∀ (a : α), a ∈ _l → List.count a _l = 1
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case neg
α : 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
this : a ::ₘ as = a ::ₘ b ::ₘ cs
⊢ as = b ::ₘ cs

Tactic:
simpa using

Goal state after:
case neg
α : 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
this : a ::ₘ as = a ::ₘ b ::ₘ cs
⊢ as = b ::ₘ cs
Module: Mathlib.Data.Multiset.ZeroCons

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

Tactic:
rw [← cons_zero]

Goal state after:
α : Type u_1
a : α
⊢ a ∈ a ::ₘ 0
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:
simpa using

Goal state after:
α : 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₂✝
⊢ ¬a✝ ∈ l₁✝ ∧ l₁✝.Nodup ↔ ¬b✝ ∈ l₂✝ ∧ l₂✝.Nodup
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

Tactic:
simpa using

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 = x
Module: Mathlib.Data.Multiset.AddSub

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

Tactic:
simpa using

Goal state after:
α : Type u_1
s t : Multiset α
⊢ s ≤ s + t
Module: Mathlib.Data.Multiset.AddSub

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

Tactic:
simpa using

Goal state after:
α : Type u_1
s t : Multiset α
⊢ s ≤ t + s
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:
simpa using

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

Goal state before:
pp: case zero
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
⊢ Rel r (0 + u) (0 + v)

Tactic:
simpa using

Goal state after:
case zero
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
⊢ Rel r u v
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case cons
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
a✝ : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
hab : r a✝ b✝
hst : Rel r as✝ bs✝
ih : Rel r (as✝ + u) (bs✝ + v)
⊢ Rel r (a✝ ::ₘ as✝ + u) (b✝ ::ₘ bs✝ + v)

Tactic:
simpa using

Goal state after:
case cons
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
a✝ : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
hab : r a✝ b✝
hst : Rel r as✝ bs✝
ih : Rel r (as✝ + u) (bs✝ + v)
⊢ Rel r (a✝ ::ₘ (as✝ + u)) (b✝ ::ₘ (bs✝ + v))
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_2.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
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : (b ::ₘ m').card = t.card + 1
hb : b ∈ b ::ₘ m'
⊢ m'.card = t.card

Tactic:
simpa using

Goal state after:
case refine_2.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
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : (b ::ₘ m').card = t.card + 1
hb : b ∈ b ::ₘ m'
⊢ m'.card = t.card
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ take (n + 1) (b :: l) = List.filter (fun a ↦ elem a (take (n + 1) (b :: l))) (b :: l)

Tactic:
take_succ_cons,

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ b :: take n l = List.filter (fun a ↦ elem a (b :: take n l)) (b :: l)
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)
h : x ∈ y ::ₘ s
hxy : y ≠ x
⊢ x ∈ s

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
x y : α
s : Multiset α
ih : x ∈ s → map f (s.erase x) = (map f s).erase (f x)
h : x ∈ y ::ₘ s
hxy : y ≠ x
⊢ x ∈ s
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
this : (¬∀ (b : α), b ∈ pwFilter (fun x1 x2 ↦ x1 ≠ x2) l → a ≠ b) ↔ ¬∀ (b : α), b ∈ l → a ≠ b
⊢ a ∈ l.dedup ↔ a ∈ l

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
this : (¬∀ (b : α), b ∈ pwFilter (fun x1 x2 ↦ x1 ≠ x2) l → a ≠ b) ↔ ¬∀ (b : α), b ∈ l → a ≠ b
⊢ a ∈ pwFilter (fun x1 x2 ↦ x1 ≠ x2) l ↔ a ∈ l
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ (a :: l).dedup = if a ∈ l then l.dedup else a :: l.dedup

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ (a :: l).dedup = if a ∈ l then l.dedup else a :: l.dedup
Module: Mathlib.Data.List.Lattice

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

Tactic:
simpa using

Goal state after:
α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h : a ∈ l₁ ∩ l₂
⊢ a ∈ l₂
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h₁ : a ∈ l₁
h₂ : a ∈ l₂
⊢ elem a l₂ = true

Tactic:
simpa using

Goal state after:
α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h₁ : a ∈ l₁
h₂ : a ∈ l₂
⊢ a ∈ l₂
Module: Mathlib.Data.List.Lattice

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

Tactic:
simpa using

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ l₁.bagInter l₂ = [] ↔ l₁ ∩ l₂ = []
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : _root_.Disjoint (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝)
⊢ a✝.Disjoint b✝

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : _root_.Disjoint (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝)
⊢ a✝.Disjoint b✝
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
p : Multiset α → Sort u_3
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
s : Multiset α
⊢ strongDownwardInduction H s = H s fun {t₂} ht _hst ↦ strongDownwardInduction H t₂ ht

Tactic:
by
  rw [strongDownwardInduction]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
h : a ∈ t
⊢ (a ::ₘ s) ∩ t ≤ t

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
h : a ∈ t
⊢ a ::ₘ s ∩ t.erase a ≤ t
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
t s u : Multiset α
h₁ : s ≤ 0
h₂ : s ≤ u
⊢ s ≤ 0 ∩ u

Tactic:
simpa using

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
t s u : Multiset α
h₁ : s ≤ 0
h₂ : s ≤ u
⊢ s ≤ 0
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Multiset α
_l : List α
h : ∀ (x : α), x ∈ Quot.mk (⇑(isSetoid α)) _l → (p x ↔ q x)
⊢ ∀ (x : α), x ∈ _l → decide (p x) = decide (q x)

Tactic:
simpa using

Goal state after:
α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Multiset α
_l : List α
h : ∀ (x : α), x ∈ Quot.mk (⇑(isSetoid α)) _l → (p x ↔ q x)
⊢ ∀ (x : α), x ∈ _l → (p x ↔ q x)
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
s : Multiset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (b : α), p b → q b
l : List α
⊢ ∀ (a : α), decide (p a) = true → decide (q a) = true

Tactic:
simpa using

Goal state after:
α : Type u_1
s : Multiset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (b : α), p b → q b
l : List α
⊢ ∀ (a : α), p a → q a
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
x✝ : List α
h : p a
⊢ decide (p a) = true

Tactic:
simpa using

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
x✝ : List α
h : p a
⊢ p a
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
x✝ : List α
h : ¬p a
⊢ ¬decide (p a) = true

Tactic:
simpa using

Goal state after:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
x✝ : List α
h : ¬p a
⊢ ¬p a
Module: Mathlib.Data.Multiset.UnionInter

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

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s - t = s + u - (t + u)
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

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