mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
⊢ image2 (fun a b ↦ f b a) t s = image2 g t s

Tactic:
simp_rw [h_comm]

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ici a ∩ Iic c ∩ Icc b b = {b}

Tactic:
simp [hab, hbc]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
s : Set α
a : α
⊢ BddAbove (insert a s) ↔ BddAbove s

Tactic:
by
  simp only [insert_eq, bddAbove_union, bddAbove_singleton, true_and]

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

Goal state before:
pp: case cons.cons
α : Type u_1
β : Type u_2
r : α → β → Prop
l u✝ : List α
u : α
l₁✝ l₂✝¹ : List α
_hlu : l₁✝ ~ l₂✝¹
ih : ∀ {v : List β}, Forall₂ r l₂✝¹ v → (Forall₂ r ∘r Perm) l₁✝ v
b✝ : β
l₂✝ : List β
hab : r u b✝
huv' : Forall₂ r l₂✝¹ l₂✝
l₂ : List β
h₁₂ : Forall₂ r l₁✝ l₂
h₂₃ : l₂ ~ l₂✝
⊢ (Forall₂ r ∘r Perm) (u :: l₁✝) (b✝ :: l₂✝)

Tactic:
exact ⟨_ :: l₂, Forall₂.cons hab h₁₂, h₂₃.cons _⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ ((fun x1 x2 ↦ x1 = map f x2) ∘r fun x1 x2 ↦ x1 ~ x2) = fun x1 x2 ↦ x1 ~ map f x2

Tactic:
by
  conv_rhs => rw [← Relation.comp_eq_fun (map f)]
  simp only [← forall₂_eq_eq_eq, forall₂_map_right_iff, forall₂_comp_perm_eq_perm_comp_forall₂]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
⊢ (map ((fun x ↦ zpow' x.2 x.1) ∘ fun x ↦ (-x.1, x.2)) l).prod = (map ((fun x ↦ x⁻¹) ∘ fun x ↦ zpow' x.2 x.1) l).prod

Tactic:
congr! 2

Goal state after:
case e'_4
M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
⊢ ((fun x ↦ zpow' x.2 x.1) ∘ fun x ↦ (-x.1, x.2)) = (fun x ↦ x⁻¹) ∘ fun x ↦ zpow' x.2 x.1
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℤ
⊢ (map ((fun x ↦ zpow' x.2 x.1) ∘ fun x ↦ (r * x.1, x.2)) l).prod =
    (map ((fun x ↦ zpow' x r) ∘ fun x ↦ zpow' x.2 x.1) l).prod

Tactic:
congr! 2

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℤ
⊢ ((fun x ↦ zpow' x.2 x.1) ∘ fun x ↦ (r * x.1, x.2)) = (fun x ↦ zpow' x r) ∘ fun x ↦ zpow' x.2 x.1
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mp
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ → x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Tactic:
simp only [append_eq_append_iff, cons_eq_append_iff, cons_eq_cons]
    rintro (⟨c, rfl, ⟨rfl, rfl, rfl⟩ | ⟨d, rfl, rfl⟩⟩ |
      ⟨c, rfl, ⟨rfl, rfl, rfl⟩ | ⟨d, rfl, rfl⟩⟩) <;> simp_all

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

Goal state before:
pp: x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ x /. n / (x /. d) = d /. n

Tactic:
rw [div_eq_mul_inv, inv_divInt, mul_comm, divInt_mul_divInt_cancel hx]

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

Goal state before:
pp: q : ℚ≥0
⊢ q * ↑q.den = ↑q.num

Tactic:
ext
  push_cast
  rw [← Int.cast_natCast, ← den_coe, ← Int.cast_natCast q.num, ← num_coe]
  exact Rat.mul_den_eq_num _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ a ^ m * a ∣ a ^ m * 1

Tactic:
rw [← pow_succ, mul_one]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
h : a ^ n ∣ a ^ m
hmn : m < n
⊢ a ^ (m + 1) ∣ a ^ m
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
⊢ Injective NNRat.cast

Tactic:
rintro p q hpq
  rw [NNRat.cast_def, NNRat.cast_def, Commute.div_eq_div_iff] at hpq
  on_goal 1 => rw [← p.num_div_den, ← q.num_div_den, div_eq_div_iff]
  · norm_cast at hpq ⊢
  any_goals norm_cast
  any_goals apply den_ne_zero
  exact Nat.cast_commute ..

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

Goal state before:
pp: q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
    c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den

Tactic:
rw [Int.mul_assoc, Int.mul_assoc, mul_eq_mul_left_iff, or_iff_not_imp_right]

Goal state after:
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ ¬c = 0 →
    ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
      (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n' : ℕ
a : R
⊢ n' • a = ↑n' * a

Tactic:
simp only [nsmul_eq_mul]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ image2 l s t, x ≤ b

Tactic:
forall_mem_image2,

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ ∀ (b : γ), l a₀ b₀ ≤ b ↔ ∀ x ∈ s, ∀ y ∈ t, l x y ≤ b
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
P : ι → α → Prop
⊢ ⋂ i, {x | P i x} = {x | ∀ (i : ι), P i x}

Tactic:
ext
  exact mem_iInter

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ ⋃ i, ⋃ j, s i j = univ ↔ ∀ (a : α), ∃ i j, a ∈ s i j

Tactic:
simp only [iUnion_eq_univ_iff, mem_iUnion]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝¹² : Max α
inst✝¹¹ : Min α
inst✝¹⁰ : LE α
inst✝⁹ : LT α
inst✝⁸ : SupSet α
inst✝⁷ : InfSet α
inst✝⁶ : Top α
inst✝⁵ : Bot α
inst✝⁴ : Compl α
inst✝³ : HImp α
inst✝² : HNot α
inst✝¹ : SDiff α
inst✝ : CompletelyDistribLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
map_hnot : ∀ (a : α), f (￢a) = ￢f a
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
ι✝ : Type u
κ✝ : ι✝ → Type u
g : (a : ι✝) → κ✝ a → α
⊢ f (⨅ a, ⨆ b, g a b) = f (⨆ g_1, ⨅ a, g a (g_1 a))

Tactic:
by
    simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range,
      iInf_iSup_eq]

Goal state after:
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
h : Ioc a b = Ioc c d
⊢ a < b

Tactic:
grind [Set.nonempty_Ioc]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
⊢ b' ≤ f a → b' ∈ lowerBounds (f '' Icc a b)

Tactic:
intro hb'

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
hb' : b' ≤ f a
⊢ b' ∈ lowerBounds (f '' Icc a b)
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
this : y ∈ Ici x
⊢ False

Tactic:
rw [h, mem_singleton_iff] at this

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
this : y = x
⊢ False
Module: Mathlib.Data.Set.Pairwise.Basic

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

Tactic:
by rw [this]

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : 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
this : x.2 = y.2
⊢ (fun p ↦ f p.1 p.2) y = (fun a ↦ f a x.2) y.1

Tactic:
by rw [this]

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
⊢ Ι a b ∪ Ι b c = Ι a c

Tactic:
by
  wlog hac : a ≤ c generalizing a c
  · rw [uIoc_comm, union_comm, uIoc_comm, this _ (le_of_not_ge hac), uIoc_comm]
    rwa [uIcc_comm]
  rw [uIcc_of_le hac] at h
  rw [uIoc_of_le h.1, uIoc_of_le h.2, uIoc_of_le hac, Ioc_union_Ioc_eq_Ioc h.1 h.2]

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
⊢ (a ⊓ b)⁻ᵐ = a⁻ᵐ ⊔ b⁻ᵐ

Tactic:
by
  simp [leOnePart, inv_inf, sup_sup_distrib_right]

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

Goal state before:
pp: i n : ℕ
h✝ : 1 < 2
⊢ 1 + (n + 1)! ≤ (1 + (n + 1))!

Tactic:
rw [← Nat.add_assoc, factorial_succ (1 + n), Nat.add_mul, Nat.one_mul, Nat.add_comm 1 n,
        Nat.add_le_add_iff_right]
      exact Nat.mul_pos n.succ_pos n.succ.factorial_pos

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

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f (x / y) = f (y / x)

Tactic:
by rw [← inv_div, map_inv_eq_map]

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

Goal state before:
pp: case pos
n k : ℕ
h : n < k
⊢ n.descFactorial k = 0

pp: case neg
n k : ℕ
h : ¬n < k
⊢ n.descFactorial k = (n - k + 1).ascFactorialBinary k

Tactic:
· rw [descFactorial_of_lt h]

Goal state after:
case neg
n k : ℕ
h : ¬n < k
⊢ n.descFactorial k = (n - k + 1).ascFactorialBinary k
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: case inr.e_a
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑q⁻¹ = (↑q)⁻¹

Tactic:
rw [cast_inv_of_ne_zero hq]

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

Goal state before:
pp: k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑k + ↑k * q = 0 + ↑k * (q + 1)

Tactic:
Nat.mul_succ,

Goal state after:
k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑k + ↑k * q = 0 + (↑k * q + ↑k)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ ⌈↑⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉

Tactic:
by
  obtain rfl | ha := ha.eq_or_lt
  · simp
  have : 0 < a - 1 := by linarith
  refine le_antisymm (ceil_le.2 <| div_le_self (by positivity) ha.le) <| ?_
  rw [le_ceil_iff, sub_lt_comm, div_eq_mul_inv, ← mul_one_sub,
    ← lt_div_iff₀ (sub_pos.2 <| inv_lt_one_of_one_lt₀ ha)]
  convert ceil_lt_add_one (R := k) _
  field

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

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : q.den.Coprime q.num.natAbs
this : (↑q.den).natAbs = q.den
⊢ q_inv.num = ↑q.den ∧ q_inv.den = q.num.natAbs

Tactic:
rw [← this] at coprime_q_denom_q_num

Goal state after:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : (↑q.den).natAbs.Coprime q.num.natAbs
this : (↑q.den).natAbs = q.den
⊢ q_inv.num = ↑q.den ∧ q_inv.den = q.num.natAbs
Module: Mathlib.Data.Multiset.Count

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

Tactic:
simp [List.countP_cons]

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

Goal state before:
pp: case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : (hd :: tl).Nodup
⊢ map (update f x y) (hd :: tl) =
    if x ∈ hd :: tl then (map f (hd :: tl)).set (idxOf x (hd :: tl)) y else map f (hd :: tl)

Tactic:
rw [nodup_cons] at hl

Goal state after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
f : α → β
x : α
y : β
hd : α
tl : List α
ihl : tl.Nodup → map (update f x y) tl = if x ∈ tl then (map f tl).set (idxOf x tl) y else map f tl
hl : ¬hd ∈ tl ∧ tl.Nodup
⊢ map (update f x y) (hd :: tl) =
    if x ∈ hd :: tl then (map f (hd :: tl)).set (idxOf x (hd :: tl)) y else map f (hd :: tl)
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case pos
α : 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
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

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
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Tactic:
· cases hxy
    simp

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
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : x ∈ xs
⊢ xs ∪ ys = xs.dedup ++ ys

Tactic:
ih h.2

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : ¬x ∈ ys ∧ xs.Disjoint ys
hx : x ∈ xs
⊢ xs.dedup ++ ys = xs.dedup ++ ys
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : x ∈ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂

Tactic:
simp only [*, inter_cons_of_notMem, false_or, mem_append, inter_cons_of_mem,
        not_false_iff]
      exact perm_cons_append_cons _ l_ih

Goal state after:
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ { val := m.dedup.dedup, nodup := ⋯ } = { val := m.dedup, nodup := ⋯ }

Tactic:
dedup_idem

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

Goal state before:
pp: case pos
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : x ∈ s
⊢ count (f x) (map f s) = count x s

pp: case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
⊢ count (f x) (map f s) = count x s

Tactic:
· exact count_map_eq_count f _ hf.injOn _ H

Goal state after:
case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
⊢ count (f x) (map f s) = count x s
Module: Mathlib.Data.Finset.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
⊢ s.PairwiseDisjoint fun x ↦ filter (fun x_1 ↦ f x_1 = x) t

Tactic:
rintro i - j - h u hi hj x hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
i j : β
h : i ≠ j
u : Finset α
hi : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) i
hj : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
⊢ x ∈ ⊥
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
⊢ ({x}.erase x)ᶜ = univ

Tactic:
erase_singleton,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
⊢ ∅ᶜ = univ
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
s : Finset α
x✝ : α
⊢ x✝ ∈ map (Embedding.refl α) s ↔ x✝ ∈ s

Tactic:
by simpa only [mem_map, exists_prop] using! exists_eq_right

Goal state after:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : DecidableEq α
⊢ #{a, b} = 2 ↔ a ≠ b

Tactic:
by
  aesop (add simp card_insert_eq_ite)

Goal state after:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
a b c : α
inst✝ : DecidableEq α
⊢ #{a, b, c} = 3 ↔ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
by
  aesop (add simp card_insert_eq_ite)

Goal state after:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ #(filter p s) = 0 ↔ ∀ x ∈ s, ¬p x

Tactic:
rw [card_eq_zero, filter_eq_empty_iff]

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

Goal state before:
pp: case mp
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : Injective ⇑f
⊢ ∀ (i : Fin n), f i.castSucc ≠ f i.succ

Tactic:
i

Goal state after:
case mp
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : Injective ⇑f
i : Fin n
⊢ f i.castSucc ≠ f i.succ
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun i ↦ f ↑i ⋯) (range n).attach
⊢ #s = #(image (fun i ↦ f ↑i ⋯) (range n).attach)

Tactic:
by rw [this]

Goal state after:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case calc_2.mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
a : α
ha : a ∈ s
h : i a ha ∈ t
⊢ i a ha ∈ image (fun a ↦ i ↑a ⋯) s.attach

Tactic:
exact mem_image.2 ⟨⟨a, ha⟩, by simp⟩

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

Goal state before:
pp: case mp
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f
⊢ ∀ (i : Fin n), r (f i.castSucc) (f i.succ)

Tactic:
i

Goal state after:
case mp
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f
i : Fin n
⊢ r (f i.castSucc) (f i.succ)
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
⊢ ∃ k, k < b ∧ k + 1 ≤ b ∧ b = a + k + 1

Tactic:
obtain ⟨k, hk⟩ : ∃ k : ℕ, (b : ℕ) = a + k + 1 := Nat.exists_eq_add_of_lt h

Goal state after:
case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
⊢ ∃ k, k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
t : Finset β
inst✝ : DecidableEq β
h : #s ≤ #t
⊢ image f s = t ↔ Set.BijOn f ↑s ↑t

Tactic:
grind [injOn_of_surjOn_of_card_le, Set.BijOn, image_eq_iff_surjOn_mapsTo]

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

Goal state before:
pp: α : Type u
n : ℕ
c : α
⊢ (ofFn fun x ↦ c) = replicate (n + 1) c

Tactic:
replicate,

Goal state after:
α : Type u
n : ℕ
c : α
⊢ (ofFn fun x ↦ c) = c :: replicate n c
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
x y : Fin (n + 1)
h : x ≠ y
hxy : x < y
⊢ ∃ z, y.succAbove z = x

pp: case inr
n : ℕ
x y : Fin (n + 1)
h : x ≠ y
hyx : y < x
⊢ ∃ z, y.succAbove z = x

Tactic:
exacts [⟨_, succAbove_castPred_of_lt _ _ hxy⟩, ⟨_, succAbove_pred_of_lt _ _ hyx⟩]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

Tactic:
· rw [succAbove_of_castSucc_lt _ _ h, succAbove_castSucc_of_lt _ _ h]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc.succAbove (j.predAbove i) = i

Tactic:
succAbove_predAbove (Fin.ne_of_gt h)

Goal state after:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ i = i
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ (∃ a b c, True ∧ True ∧ True ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) ↔ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
true_and

Goal state after:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 3 < #s ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
by
  classical
    simp_rw [lt_iff_add_one_le, le_card_iff_exists_subset_card, reduceAdd, card_eq_four,
      ← exists_and_left, exists_comm (α := Finset α)]
    constructor
    · rintro ⟨a, b, c, d, t, hsub, hab, hac, had, hbc, hbd, hcd, rfl⟩
      exact ⟨a, b, c, d, by simp_all [insert_subset_iff]⟩
    · rintro ⟨a, b, c, d, ha, hb, hc, hd, hab, hac, had, hbc, hbd, hcd⟩
      exact ⟨a, b, c, d, {a, b, c, d}, by simp_all [insert_subset_iff]⟩

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

Goal state before:
pp: case cons
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

Tactic:
by_cases hx : x = y
    · simp [hx, cons_sublist_cons, singleton_sublist]
    · rw [duplicate_cons_iff_of_ne hx, IH]
      refine ⟨sublist_cons_of_sublist y, fun h => ?_⟩
      cases h
      · assumption
      · contradiction

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
⊢ snoc p x (last n) = x

Tactic:
simp [snoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
H : l.Nodup
i : Fin l.length
⊢ (fun x ↦ ⟨idxOf (↑x) l, ⋯⟩) ((fun i ↦ ⟨l.get i, ⋯⟩) i) = i

Tactic:
by simp only [List.get_idxOf, Fin.eta, H]

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
⊢ fold op (op b₁ b₂) s₁ = op (fold op b₁ s₁) (fold op b₂ 0)

Tactic:
fold_zero,

Goal state after:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
⊢ fold op (op b₁ b₂) s₁ = op (fold op b₁ s₁) b₂