mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
⊢ a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂

Tactic:
by_cases ha : a ∈ l₁ <;> simp [ha, count_eq_zero_of_not_mem]

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

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

Tactic:
ih hb2

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
inst✝² : IsTrans α r
inst✝¹ : Std.Symm r
x : α
inst✝ : DecidablePred (r x)
y : α
s : Multiset α
ih : ∀ {t : Multiset α}, Rel r s t → countP (r x) s = countP (r x) t
b : α
bs : Multiset α
hb1 : r y b
hb2 : Rel r s bs
h : Rel r (y ::ₘ s) (b ::ₘ bs)
⊢ (countP (r x) bs + if r x y then 1 else 0) = countP (r x) bs + if r x b then 1 else 0
Module: Mathlib.Data.Multiset.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:
induction s using Multiset.induction_on generalizing t with
  | empty => rw [rel_zero_left.mp h]
  | cons y s ih =>
    obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp h
    rw [countP_cons, countP_cons, ih hb2]
    simp only [Nat.add_right_inj]
    exact (if_congr ⟨fun h => _root_.trans h hb1, fun h => _root_.trans h (symm hb1)⟩ rfl rfl)

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 rw [eq_nil_iff_forall_not_mem.mpr H]; rfl

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
a : α
t' : Multiset α
h : s ≤ t'
⊢ ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → ¬a ∈ ↑l₁ → a ∈ ↑l₂ → a ::ₘ ↑l₁ ≤ ↑l₂

Tactic:
introv s m₁ m₂

Goal state after:
α : Type u_1
s✝ t : Multiset α
a : α
t' : Multiset α
h : s✝ ≤ t'
l₁ l₂ : List α
s : l₁ <+ l₂
m₁ : ¬a ∈ ↑l₁
m₂ : a ∈ ↑l₂
⊢ a ::ₘ ↑l₁ ≤ ↑l₂
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]; simp

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]; simp

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

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

Tactic:
exact s.erase_cons_tail hab.symm

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

Goal state before:
pp: case mp
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ f a = b

Tactic:
rw [← mem_singleton, ← h, ha, map_singleton, mem_singleton]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
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 : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun x ↦ i ↑x ⋯) s.attach
⊢ map (fun x ↦ f ↑x) s.attach = map g t

Tactic:
by rw [this, Multiset.map_map]; exact map_congr rfl fun x _ => h _ _

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

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ ↑s.toList = 0 ↔ s = 0

Tactic:
coe_toList

Goal state after:
α : Type u_1
s : Multiset α
⊢ s = 0 ↔ s = 0
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
⊢ a ∈ ↑s.toList ↔ a ∈ s

Tactic:
coe_toList

Goal state after:
α : Type u_1
a : α
s : Multiset α
⊢ a ∈ s ↔ a ∈ s
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ (↑s.toList).card = s.card

Tactic:
coe_toList

Goal state after:
α : Type u_1
s : Multiset α
⊢ s.card = s.card
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 n xs = (List.take n' xs.reverse).reverse

Tactic:
take_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 n xs = (List.drop (xs.length - n') xs).reverse.reverse
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
⊢ dropSlice n m xs ~ ys ∩ dropSlice n m xs

Tactic:
simp only [dropSlice_eq]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.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
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
this : count x (filter (fun a ↦ f x = f a) s) = (filter (fun a ↦ f x = f a) s).card
⊢ countP (fun x_1 ↦ f x = x_1) (map f s) = count x s

Tactic:
countP_map,

Goal state after:
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
this : count x (filter (fun a ↦ f x = f a) s) = (filter (fun a ↦ f x = f a) s).card
⊢ (filter (fun a ↦ f x = f a) s).card = count x s
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : ¬x = y
⊢ min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0

Tactic:
· simp only [h, if_false, Nat.zero_min]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
hn : n ≠ 0
x : α
⊢ x ∈ (replicate n a).toFinset ↔ x ∈ {a}

Tactic:
simp [hn, List.mem_replicate]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ insert a (sᶜ.erase a) = sᶜ

Tactic:
insert_erase (mem_compl.2 ha)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun a ↦ insert a s) ↑sᶜ

Tactic:
rw [coe_compl]
  exact s.insert_inj_on

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

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
ha : a ∉ s
x : α
hx : x ∈ cons a s ha
⊢ ⟨x, hx⟩ ∈ (cons a s ha).attach ↔ ⟨x, hx⟩ ∈ cons ⟨a, ⋯⟩ (map { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ } s.attach) ⋯

Tactic:
simpa using hx

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a x : α
hx : x ∈ insert a s
⊢ ⟨x, hx⟩ ∈ (insert a s).attach ↔ ⟨x, hx⟩ ∈ insert ⟨a, ⋯⟩ (image (fun x ↦ ⟨↑x, ⋯⟩) s.attach)

Tactic:
simpa using hx

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

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

Tactic:
exact lt_of_le_of_ne (f.monotone (Fin.castSucc_le_succ i)) (hf i)

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

Goal state before:
pp: k : ℕ
i j : Fin k
⊢ i ≍ j ↔ ↑i = ↑j

Tactic:
simp [val_eq_val]

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

Goal state before:
pp: n : ℕ
⊢ univ = Finset.cons 0 (map { toFun := succ, inj' := ⋯ } univ) ⋯

Tactic:
by
  simp [map_eq_image]

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

Goal state before:
pp: n : ℕ
⊢ univ = Finset.cons (last n) (map castSuccEmb univ) ⋯

Tactic:
by
  simp [map_eq_image]

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
⊢ univ = Finset.cons p (map p.succAboveEmb univ) ⋯

Tactic:
by
  simp [map_eq_image]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ i.predAbove (last (n + 1)) = last n

Tactic:
by
  rw [predAbove_of_castSucc_lt _ _ (castSucc_lt_last _), pred_last]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
h : Injective f
b : β
w : b ∉ Set.range f
⊢ b ∉ map { toFun := f, inj' := h } univ

Tactic:
rwa [← mem_coe, coe_map, coe_univ, Set.image_univ]

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

Goal state before:
pp: α : Type u_4
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ (∃! a, p a) ↔ #{x | p x} = 1

Tactic:
by
  rw [Finset.card_eq_one]
  refine exists_congr fun x => ?_
  simp only [Subset.antisymm_iff, subset_singleton_iff', singleton_subset_iff, and_comm,
    mem_filter_univ]

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

Goal state before:
pp: case refine_1
α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l

pp: case refine_2
α : Type u_1
l : List α
x y : α
h : y = x ∧ x ∈ l ∨ x ∈+ l
⊢ x ∈+ y :: l

Tactic:
· obtain hm | hm := h
    · exact Or.inl ⟨rfl, hm⟩
    · exact Or.inr hm

Goal state after:
case refine_2
α : Type u_1
l : List α
x y : α
h : y = x ∧ x ∈ l ∨ x ∈+ l
⊢ x ∈+ y :: l
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
i : Fin n
⊢ «repeat» 1 a (Fin.cast ⋯ i) = (a ∘ Fin.cast h) (Fin.cast ⋯ i)

Tactic:
simp [modNat, Nat.mod_eq_of_lt i.is_lt]

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
inst✝ : DecidableEq α
⊢ x ∈+ l ↔ 2 ≤ count x l

Tactic:
simp [replicate_succ, duplicate_iff_sublist, ← replicate_sublist_iff]

Goal state after:
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ card α ≤ 1 ↔ Subsingleton α

Tactic:
exact card_le_one_iff_subsingleton

Goal state after:
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: case succ.inl
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s = n + 1
⊢ ∃ t, s ⊆ t ∧ #t = n + 1

pp: case succ.inr
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
⊢ ∃ t, s ⊆ t ∧ #t = n + 1

Tactic:
· exact ⟨s, subset_rfl, hn'⟩

Goal state after:
case succ.inr
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
⊢ ∃ t, s ⊆ t ∧ #t = n + 1
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Multiset α
⊢ {x | x ∈ s}.Finite

Tactic:
simpa only [← Multiset.mem_toFinset] using! s.toFinset.finite_toSet

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

Goal state before:
pp: n : ℕ
α : Sort u_3
i : Fin (n + 1)
x✝ : α
p : Fin n → α
x : Fin (n + 1)
⊢ (i.insertNth x✝ p ∘ rev) x = i.rev.insertNth x✝ (p ∘ rev) x

Tactic:
apply insertNth_rev

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

Goal state before:
pp: α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : InjOn f s
this : Finite ↑s
⊢ SurjOn f s s

Tactic:
exact hm.restrict_surjective_iff.mp (Finite.injective_iff_surjective.mp <| hm.restrict_inj.mpr h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ Multiset.fold op (op b₂ b₁) (Multiset.map f s₁.val + Multiset.map f s₂.val) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))

Tactic:
fold_add

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha✝ : a ∈ l
ha : a ∈ l.dropLast ∨ a ∈ [l.getLast ⋯]
hlast : R (l.getLast ⋯) (l.getLast ⋯)
⊢ R a (l.getLast ⋯)

Tactic:
List.mem_singleton

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha✝ : a ∈ l
ha : a ∈ l.dropLast ∨ a = l.getLast ⋯
hlast : R (l.getLast ⋯) (l.getLast ⋯)
⊢ R a (l.getLast ⋯)
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: ι : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Multiset ι
f : ι → M
⊢ (map f ↑s.toList).prod = (map f s).prod

Tactic:
coe_toList

Goal state after:
ι : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Multiset ι
f : ι → M
⊢ (map f s).prod = (map f s).prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ (a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)

Tactic:
rotate'_cons_succ,

Goal state after:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ (l ++ [a]).rotate' n = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
a : α
l : List α
n m : ℕ
⊢ ((a :: l).rotate' (n + 1)).rotate' m = (a :: l).rotate' (n + 1 + m)

Tactic:
rotate'_cons_succ,

Goal state after:
α : Type u
a : α
l : List α
n m : ℕ
⊢ ((l ++ [a]).rotate' n).rotate' m = (a :: l).rotate' (n + 1 + m)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
⊢ [].reverse.alternatingProd = [].alternatingProd ^ (-1) ^ ([].length + 1)

Tactic:
simp only [alternatingProd_nil, one_zpow, reverse_nil]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case cons
M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
ih : op xs.prod = (map op xs).reverse.prod
⊢ op (x :: xs).prod = (map op (x :: xs)).reverse.prod

Tactic:
rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ unop l.prod = (map unop l).reverse.prod

Tactic:
← op_inj,

Goal state after:
M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ op (unop l.prod) = op (map unop l).reverse.prod
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ (a ::ₘ s) ×ˢ (t + u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u

Tactic:
by
    rw [cons_product, IH]
    simp [add_left_comm, add_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
s✝ : Finset α
t : α → Finset β
f : β → γ
this : DecidableEq α
a : α
s : Finset α
x✝ : a ∉ s
ih : image f (s.biUnion t) = s.biUnion fun a ↦ image f (t a)
⊢ image f ((insert a s).biUnion t) = (insert a s).biUnion fun a ↦ image f (t a)

Tactic:
simp only [biUnion_insert, image_union, ih]

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ SemiconjBy (↑((Units.map f) c)) (f a) (f b)

Tactic:
by rw [Units.coe_map, SemiconjBy, ← f.map_mul, hc.eq, f.map_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
f : α → β
⊢ f '' ⋂₀ S ⊆ ⋂ s ∈ S, f '' s

Tactic:
sInter_eq_biInter

Goal state after:
α : Type u_1
β : Type u_2
S : Set (Set α)
f : α → β
⊢ f '' ⋂ i ∈ S, i ⊆ ⋂ s ∈ S, f '' s
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case refine_1.refine_2
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
h : s * t = 1
hst : (s * t).Nonempty
a : α
ha : a ∈ s
b : α
hb : b ∈ t
H : ∀ {a b : α}, a ∈ s → b ∈ t → a * b = 1
x : α
hx : x ∈ t
⊢ x = b

Tactic:
· exact (eq_inv_of_mul_eq_one_right <| H ha hx).trans (inv_eq_of_mul_eq_one_right <| H ha hb)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
S : Set (Set α)
t : Set β
⊢ image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t

Tactic:
sInter_eq_biInter

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
S : Set (Set α)
t : Set β
⊢ image2 f (⋂ i ∈ S, i) t ⊆ ⋂ s ∈ S, image2 f s t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
T : Set (Set β)
⊢ image2 f s (⋂₀ T) ⊆ ⋂ t ∈ T, image2 f s t

Tactic:
sInter_eq_biInter

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
T : Set (Set β)
⊢ image2 f s (⋂ i ∈ T, i) ⊆ ⋂ t ∈ T, image2 f s t
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ {1}
⊢ x = 1

Tactic:
simpa using hx

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ⊓ K = ⊤ ⊓ K ↔ K ≤ H

Tactic:
top_inf_eq,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ⊓ K = K ↔ K ≤ H
Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s : Set Mᵐᵒᵖ
⊢ (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Tactic:
← op_inj,

Goal state after:
M : Type u_2
inst✝ : Mul M
s : Set Mᵐᵒᵖ
⊢ (closure s).unop.op = (closure (MulOpposite.op ⁻¹' s)).op
Module: Mathlib.Algebra.Group.Submonoid.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
s : Set Mᵐᵒᵖ
⊢ (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Tactic:
← op_inj,

Goal state after:
M : Type u_2
inst✝ : MulOneClass M
s : Set Mᵐᵒᵖ
⊢ (closure s).unop.op = (closure (MulOpposite.op ⁻¹' s)).op
Module: Mathlib.Algebra.Group.Subgroup.MulOpposite

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup Gᵐᵒᵖ
⊢ (normalizer ↑H).unop = normalizer ↑H.unop

Tactic:
← op_inj,

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup Gᵐᵒᵖ
⊢ (normalizer ↑H).unop.op = (normalizer ↑H.unop).op
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ (n + 2).bodd = (1 &&& n + 2 != 0)

Tactic:
simpa using bodd_eq_one_and_ne_zero n

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Encodable α
o : Option α
⊢ (Nat.casesOn (Option.casesOn o zero fun a ↦ (encode a).succ) (some none) fun m ↦ Option.map some (decode m)) = some o

Tactic:
by
    cases o <;> simp [encodek]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set Gᵐᵒᵖ
⊢ (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Tactic:
← op_inj,

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set Gᵐᵒᵖ
⊢ (closure s).unop.op = (closure (MulOpposite.op ⁻¹' s)).op
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ (∀ ⦃i j : α⦄, ((j⁻¹ * i) • s ∩ s).Nonempty → i = j) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1

Tactic:
exact ⟨fun h a ↦ by simpa using @h a 1,
    fun h i j ne ↦ by simpa [inv_mul_eq_one, eq_comm] using h _ ne⟩

Goal state after:
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case inr.inl.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Total (s i)
i : ι
a b : α i
hab : s i a b
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

pp: case inr.inl.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Total (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

Tactic:
· exact Or.inl (Lex.right _ _ hab)

Goal state after:
case inr.inl.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Total (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case inr.inl.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a b : α i
hab : s i a b
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ ⟨i, a⟩ = ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

pp: case inr.inl.inr.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a : α i
⊢ Lex r s ⟨i, a⟩ ⟨i, a⟩ ∨ ⟨i, a⟩ = ⟨i, a⟩ ∨ Lex r s ⟨i, a⟩ ⟨i, a⟩

pp: case inr.inl.inr.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ ⟨i, a⟩ = ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

Tactic:
· exact Or.inl (Lex.right _ _ hab)

Goal state after:
case inr.inl.inr.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a : α i
⊢ Lex r s ⟨i, a⟩ ⟨i, a⟩ ∨ ⟨i, a⟩ = ⟨i, a⟩ ∨ Lex r s ⟨i, a⟩ ⟨i, a⟩

case inr.inl.inr.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ ⟨i, a⟩ = ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
⊢ (foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) →
    (foldl (argAux r) o (tl ++ [hd]) = none ↔ tl ++ [hd] = [] ∧ o = none)

Tactic:
simp only [foldl_append, foldl_cons, argAux, foldl_nil, append_eq_nil_iff]

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
⊢ (foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) →
    (Option.rec (some hd) (fun val ↦ if r hd val then some hd else some val) (foldl (argAux r) o tl) = none ↔
      (tl = [] ∧ [hd] = []) ∧ o = none)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
m : α
inst✝ : DecidableEq α
⊢ (m ∈ l ∧ (∀ (a : α), a ∈ l → f a ≤ f m) ∧ ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l) → m ∈ argmax f l

Tactic:
rintro ⟨hml, ham, hma⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l
⊢ m ∈ argmax f l