mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

Tactic:
by_cases hb : b ∈ s

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a₁ a₂ b₁ b₂ : α
⊢ Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Tactic:
simp only [Ici_inter_Iic.symm, Ici_inter_Ici.symm, Iic_inter_Iic.symm]

Goal state after:
α : Type u_1
inst✝ : Lattice α
a₁ a₂ b₁ b₂ : α
⊢ Ici a₁ ∩ Iic b₁ ∩ (Ici a₂ ∩ Iic b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iic b₁ ∩ Iic b₂)
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb✝ : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
x : α
hbx : b < x
⊢ x = b * (x / b)

Tactic:
mul_div_cancel₀ _ hb.ne'

Goal state after:
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb✝ : 0 ≤ b
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
hb : 0 < b
x : α
hbx : b < x
⊢ x = x
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ a
n : ℕ
h : n = 0
⊢ a / ↑n ≤ a

Tactic:
simpa [h]

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

Goal state before:
pp: case inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| + |q - r| * ↑n * (B + 1) ^ (n - 1) ≤ ε
h : 0 = |q - r|
⊢ |q - r| * ↑n * max |q| |r| ^ (n - 1) < ε

Tactic:
simpa only [← h, zero_mul] using hε

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

Goal state before:
pp: case mpr.nil.cons
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
hl : [].length = (head✝ :: tail✝).length
⊢ [] = head✝ :: tail✝

Tactic:
cases hl

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

Goal state before:
pp: case mpr.cons.nil
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝.length = l2.length → tail✝ = l2
hl : (head✝ :: tail✝).length = [].length
⊢ head✝ :: tail✝ = []

Tactic:
cases hl

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
n : ℤ
⊢ zpow' 0 n = 0

Tactic:
simp +contextual only [zpow', true_and, ite_eq_left_iff]
  intro hn
  exact zero_zpow n hn

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

Goal state before:
pp: α : Type u
b : α
l : List α
a : α
h : a ∈ (b :: l).head?
⊢ b = a

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
hl : l ≠ []
hl' : ¬l.length - 1 ≤ idxOf (l.getLast hl) l
⊢ l.getLast hl ∈ l.dropLast

Tactic:
mem_dropLast_iff_idxOf_lt <| getLast_mem hl,

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
hl : l ≠ []
hl' : ¬l.length - 1 ≤ idxOf (l.getLast hl) l
⊢ idxOf (l.getLast hl) l < l.length - 1
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f : β → α → β
b : β
x : α
xs : List α
⊢ foldl f b (xs ++ [x]) = f (foldl f b xs) x

Tactic:
simp only [List.foldl_append, List.foldl]

Goal state after:
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q r : ℚ
⊢ q * r = mkRat (q.num * r.num) (q.den * r.den)

Tactic:
rw [mul_def, normalize_eq_mkRat]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: case h₁
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ↔ a * d ≤ c * b

Tactic:
simp [div_def', Rat.divInt_le_divInt b_pos d_pos]

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: n : ℤ
q : ℚ
⊢ (↑n + q).den = q.den

Tactic:
rw [add_comm, add_intCast_den]

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
h : ∀ (n : ℕ), f ↑n = g ↑n
r : ℚ≥0
⊢ f r = g r

Tactic:
by
    rw [← r.num_div_den, div_eq_mul_inv, map_mul, map_mul, h, eq_on_inv₀ f g]
    apply h

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
a b c : R
h : b ≤ c
⊢ swap (fun x1 x2 ↦ x1 * x2) a b ≤ swap (fun x1 x2 ↦ x1 * x2) a c

Tactic:
dsimp [swap]

Goal state after:
R : Type u
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : LE R
inst✝ : CanonicallyOrderedAdd R
a b c : R
h : b ≤ c
⊢ b * a ≤ c * a
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝ : CompleteLattice α
s : Set (ULift α)
⊢ (sSup s).down = ⨆ a ∈ s, a.down

Tactic:
rw [sSup_eq_iSup', down_iSup, iSup_subtype'']

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
⊢ ⨆ a ∈ s, f a ≤ f (⨆ a ∈ s, a)

Tactic:
exact hf.le_map_iSup₂ _

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ ⋃₀ s = ⋃ i ∈ s, i

Tactic:
by
  rw [← sUnion_image, image_id']

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
⊢ ⨆ i, f ↑i = ⨆ i, f i

Tactic:
by_cases! htriv : ∀ i, f i = ⊥
  · simp only [iSup_bot, (funext htriv : f = _)]
  refine (iSup_comp_le f _).antisymm (iSup_mono' fun i => ?_)
  by_cases hi : f i = ⊥
  · rw [hi]
    obtain ⟨i₀, hi₀⟩ := htriv
    exact ⟨⟨i₀, hi₀⟩, bot_le⟩
  · exact ⟨⟨i, hi⟩, rfl.le⟩

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_8
β : α → Type u_9
ι : Sort u_10
inst✝ : (i : α) → SupSet (β i)
f : ι → (a : α) → β a
a : α
⊢ sSup ((fun f ↦ f a) '' range f) = sSup (range fun i ↦ f i a)

Tactic:
←
    range_comp

Goal state after:
α : Type u_8
β : α → Type u_9
ι : Sort u_10
inst✝ : (i : α) → SupSet (β i)
f : ι → (a : α) → β a
a : α
⊢ sSup (range ((fun f ↦ f a) ∘ f)) = sSup (range fun i ↦ f i a)
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ (fun p ↦ f p.1 p.2) y ∈ (fun a ↦ f a y.2) '' s

Tactic:
exact mem_image_of_mem _ hy.1

Goal state after:
Module: Mathlib.Algebra.Order.Nonneg.Ring

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ ∀ (a b c : { x // 0 ≤ x }), a - b ≤ c ↔ a ≤ c + b

Tactic:
by
    rintro ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩
    simp only [sub_le_iff_le_add, Subtype.mk_le_mk, mk_sub_mk, mk_add_mk, toNonneg_le]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : k.succ ≤ n.succ
⊢ (n + 1) * (n - k)! * n.descFactorial k = n.succ !

Tactic:
Nat.mul_assoc,

Goal state after:
n k : ℕ
h : k.succ ≤ n.succ
⊢ (n + 1) * ((n - k)! * n.descFactorial k) = n.succ !
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
k : ℕ
x✝ : 2 ≤ k + 2
⊢ n.descFactorial (k + 2) < n ^ (k + 2)

Tactic:
rw [descFactorial_succ, pow_succ', Nat.mul_comm, Nat.mul_comm n]
    exact Nat.mul_lt_mul_of_le_of_lt (descFactorial_le_pow _ _) (by lia) (Nat.pow_pos <| by lia)

Goal state after:
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case mp
k m : ℕ+
h : k ∣ m
⊢ ↑k ∣ ↑m

pp: case mpr
k m : ℕ+
h : ↑k ∣ ↑m
⊢ k ∣ m

Tactic:
· rcases h with ⟨_, rfl⟩
    apply dvd_mul_right

Goal state after:
case mpr
k m : ℕ+
h : ↑k ∣ ↑m
⊢ k ∣ m
Module: Mathlib.Tactic.Ring.PNat

Goal state before:
pp: n : ℕ+
n' : ℕ
k : ℕ+
k' : ℕ
h1 : CSLiftVal n n'
h2 : CSLiftVal k k'
⊢ n' + k' = CSLift.lift (n + k)

Tactic:
simp [h1.1, h2.1, CSLift.lift]

Goal state after:
Module: Mathlib.Tactic.Ring.PNat

Goal state before:
pp: n : ℕ+
n' : ℕ
k : ℕ+
k' : ℕ
h1 : CSLiftVal n n'
h2 : CSLiftVal k k'
⊢ n' * k' = CSLift.lift (n * k)

Tactic:
simp [h1.1, h2.1, CSLift.lift]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋

Tactic:
by
  rw [le_floor, Int.cast_add]
  gcongr <;> apply floor_le

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Pow

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ a ^ (n + 3) + ↑(n + 3) * a ^ (n + 3 - 1) * b ≤ (a + b) ^ (n + 3)

Tactic:
calc
      _ ≤ a ^ (n + 3) + ↑(n + 3) * a ^ (n + 2) * b +
            ((n + 1) * (b ^ 2 * (2 * a + b) * a ^ n) + a ^ (n + 1) * b ^ 2) :=
        le_add_of_nonneg_right <| by
          apply_rules [add_nonneg, mul_nonneg, Nat.cast_nonneg, pow_nonneg, zero_le_one]
      _ = (a + b) ^ 2 * (a ^ (n + 1) + ↑(n + 1) * a ^ n * b) := by
        simp only [Nat.cast_add, Nat.cast_one, Nat.cast_ofNat, pow_succ', add_mul, mul_add,
          two_mul, pow_zero, mul_one,
          Hcomm.eq, (n.cast_commute (_ : R)).symm.left_comm, mul_assoc, (Hcomm.pow_left _).eq,
          (Hcomm.pow_left _).left_comm, Hcomm.left_comm, ← @two_add_one_eq_three R, one_mul]
        abel
      _ ≤ (a + b) ^ 2 * (a + b) ^ (n + 1) := by
        gcongr
        apply Commute.pow_add_mul_le_add_pow_of_sq_nonneg <;> assumption
      _ = (a + b) ^ (n + 3) := by simp [pow_succ', mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case mp
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
x : R
⊢ (∃ x_1 ∈ s, fract x_1 = x) → ∃ i, (∃ x_1 ∈ s, x_1 - ↑i = x) ∧ x ∈ Ico 0 1

pp: case mpr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
x : R
⊢ (∃ i, (∃ x_1 ∈ s, x_1 - ↑i = x) ∧ x ∈ Ico 0 1) → ∃ x_1 ∈ s, fract x_1 = x

Tactic:
· rintro ⟨y, hy, rfl⟩
    exact ⟨⌊y⌋, ⟨y, hy, rfl⟩, fract_nonneg y, fract_lt_one y⟩

Goal state after:
case mpr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
x : R
⊢ (∃ i, (∃ x_1 ∈ s, x_1 - ↑i = x) ∧ x ∈ Ico 0 1) → ∃ x_1 ∈ s, fract x_1 = x
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.inr.calc_1
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract ((↑q * ↑n + -↑m₀) / ↑n) = fract (↑m₁ / ↑n)

Tactic:
← sub_eq_add_neg

Goal state after:
case inr.inr.calc_1
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract ((↑q * ↑n - ↑m₀) / ↑n) = fract (↑m₁ / ↑n)
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case above
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
⊢ ∃ n, x ≤ ↑n

Tactic:
obtain ⟨n, hn⟩ := exists_int_gt x

Goal state after:
case above
R : Type u_3
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
n : ℤ
hn : x < ↑n
⊢ ∃ n, x ≤ ↑n
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: case inl
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
⊢ R (f x) (f y)

Tactic:
refine absurd ?_ hxy.not_ge

Goal state after:
case inl
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
⊢ y ≤ x
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
⊢ fract (f a) = f (fract a)

Tactic:
simp_rw [fract, map_sub, map_intCast, map_floor _ hf]

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

Goal state before:
pp: case bot
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
x : WithBot M
hxy : 0 < ⊥
⊢ ∃ n, x ≤ n • ⊥

Tactic:
| bot =>

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

Goal state before:
pp: case coe.bot
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
⊢ ∃ n, ⊥ ≤ n • ↑y

Tactic:
| bot =>

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:
simpa [h]

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:
rw [lt_iff_cons_le]
  constructor
  · rintro ⟨x', hx'⟩
    have := eq_of_mem_replicate (mem_of_le hx' (mem_cons_self _ _))
    rwa [this, replicate_succ, cons_le_cons_iff] at hx'
  · intro h
    rw [replicate_succ]
    exact ⟨x, cons_le_cons _ h⟩

Goal state after:
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:
convert! List.count_replicate (a := a)
  · rw [← coe_count, coe_replicate]
  · simp

Goal state after:
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) = List.count a (l.erase a)

Tactic:
rw [← coe_count]

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⟧ = List.count a l

Tactic:
rw [← coe_count]

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) = List.count a (l.erase b)

Tactic:
rw [← coe_count]

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⟧ = List.count a l

Tactic:
rw [← coe_count]

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
l : List α
⊢ Pairwise (fun a b ↦ b ≠ a) l ↔ l.Nodup

Tactic:
by simp only [Nodup, Ne, eq_comm]

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

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

Tactic:
grind [List.IsInfix]

Goal state after:
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:
grind [List.IsInfix]

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

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

Tactic:
grind [List.IsInfix]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
hxy : ¬y = x
⊢ f y ::ₘ map f (s.erase x) = (f y ::ₘ map f s).erase (f x)

Tactic:
(s.map f).erase_cons_tail (hf.ne hxy),

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : x ∈ xs
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup

Tactic:
rw [dedup_cons_of_mem h, dedup_cons_of_mem (mem_map_of_mem h), ih]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
⊢ (head✝ :: tail✝).bagInter l₂ <+ (head✝ :: tail✝) ∩ l₂

Tactic:
rw [cons_bagInter]
    split
    · rw [inter_cons_of_mem _ (by assumption), cons_sublist_cons]
      exact ih.trans <| Sublist.inter_left (by grind [erase_sublist])
    · simp_all

Goal state after:
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 h

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

Goal state before:
pp: α : Type u_1
n : ℕ
s t : Multiset α
ht : t.card ≤ n
_h : s < t
⊢ n - t.card < n - s.card

Tactic:
have := (card_lt_card _h); lia

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
⊢ List.drop (xs.length - n') xs = (List.drop (xs.length - n') xs).reverse.reverse

Tactic:
reverse_reverse

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
⊢ List.drop (xs.length - n') xs = List.drop (xs.length - n') xs
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
⊢ List.take n xs ++ List.drop (n + m) xs ~ ys ∩ (List.take n xs ++ List.drop (n + m) xs)

Tactic:
have h₂ := h.nodup_iff.2 h'

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
⊢ List.take n xs ++ List.drop (n + m) xs ~ ys ∩ (List.take n xs ++ List.drop (n + m) xs)
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 h

Goal state after:
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 h

Goal state after:
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 h

Goal state after:
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 h

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

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

Tactic:
· rw [cons_inter_of_neg _ h]
    exact IH ((le_cons_of_notMem <| mt (mem_of_le h₂) h).1 h₁) h₂

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
x✝ : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ s ∩ t

Tactic:
rw [← cons_erase h₁, cons_inter_of_pos _ h₂]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
x✝ : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ a ::ₘ s.erase a ∩ t.erase a
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ l ~ l'

Tactic:
rw [← Multiset.coe_eq_coe]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : l.Nodup
hl' : l'.Nodup
h : l.toFinset = l'.toFinset
⊢ ↑l = ↑l'
Module: Mathlib.Data.Multiset.Filter

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

Tactic:
simpa using h

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

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

Tactic:
refine ⟨fun h0 ↦ ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ u + s = u ∪ s ∧ s = t

case refine_2
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ s ∧ s = t → u + s = u ∪ t
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
m : ¬a ∈ s
⊢ filter p (s.erase a) = (filter p s).erase a

Tactic:
rw [erase_of_notMem m, erase_of_notMem (mt mem_of_mem_filter m)]

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

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 h

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

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

Tactic:
by
  simp only [← elem_iff]
  rfl

Goal state after: