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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : a ∈ (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : ¬a ∈ (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup

Tactic:
· rw [dedup_cons_of_mem' h, insert_of_mem h]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : ¬a ∈ (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case neg
α : 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:
dedup_cons_of_notMem h,

Goal state after:
case neg
α : 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)
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ univ.Nontrivial ↔ Nontrivial α

Tactic:
rw [Finset.Nontrivial, Finset.coe_univ, Set.nontrivial_univ_iff]

Goal state after:
Module: Mathlib.Data.Int.DivMod

Goal state before:
pp: a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
⊢ a * (b / c) ≤ a * b / c

Tactic:
obtain rfl | hlt : c = 0 ∨ 0 < c := by lia
  · simp
  · rw [Int.le_ediv_iff_mul_le hlt, Int.mul_assoc]
    exact Int.mul_le_mul_of_nonneg_left (Int.ediv_mul_le b (Int.ne_of_gt hlt)) ha

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h : i ≠ last n
h' : i.rev ≠ 0
⊢ (i.castPred h).rev.succ = (i.rev.pred h').succ

Tactic:
succ_pred,

Goal state after:
n : ℕ
i : Fin (n + 1)
h : i ≠ last n
h' : i.rev ≠ 0
⊢ (i.castPred h).rev.succ = i.rev
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
y : β
⊢ #({x ∈ s | f x = y}) ≠ 0 ↔ y ∈ image f s

Tactic:
rw [← Nat.pos_iff_ne_zero, card_pos, fiber_nonempty_iff_mem_image]

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

Goal state before:
pp: n : ℕ
⊢ Injective predAbove

Tactic:
by
  intro i j hij
  obtain ⟨n, rfl⟩ := Nat.exists_add_one_eq.2 i.size_positive
  wlog! h : i < j generalizing i j
  · obtain h | rfl := h.lt_or_eq
    · exact (this hij.symm h).symm
    · rfl
  replace hij := congr_fun hij i.succ
  rw [predAbove_succ_self, Fin.predAbove_of_le_castSucc _ _ (by simpa),
    ← Fin.castSucc_inj, castSucc_castPred] at hij
  exact (i.castSucc_lt_succ.ne hij).elim

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

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
ha : a ≠ 0
⊢ (a.pred ha).castSucc < a

Tactic:
by rw [castSucc_pred_lt_iff, le_def]

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ ofFn (a :: l).get = a :: l

Tactic:
ofFn_succ

Goal state after:
α : Type u
a : α
l : List α
⊢ ((a :: l).get 0 :: ofFn fun i ↦ (a :: l).get i.succ) = a :: l
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(t \ s) = #t - #(s ∩ t)

Tactic:
← card_sdiff_of_subset

Goal state after:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(t \ s) = #(t \ (s ∩ t))

α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ s ∩ t ⊆ t
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
n : ℕ
a : α
f : Fin n → α
⊢ ofFn (Fin.cons a f) = a :: ofFn f

Tactic:
ofFn_succ

Goal state after:
α : Type u
n : ℕ
a : α
f : Fin n → α
⊢ (Fin.cons a f 0 :: ofFn fun i ↦ Fin.cons a f i.succ) = a :: ofFn f
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
n : ℕ
a : α
f : Fin n → α
⊢ ofFn (Fin.cons a f) = a :: ofFn f

Tactic:
rw [ofFn_succ]
  rfl

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

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

Tactic:
rwa [succAbove_of_lt_succ _ _ H, iff_true_left H, le_castSucc_iff]

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

Goal state before:
pp: n : ℕ
x y : Fin (n + 1)
⊢ (∃ z, x.succAbove z = y) → y ≠ x

Tactic:
by rintro ⟨y, rfl⟩; exact succAbove_ne _ _

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

Goal state before:
pp: n : ℕ
⊢ succAbove 1 1 = 2

Tactic:
by
  simpa only [succ_zero_eq_one, val_zero, zero_succAbove, succ_one_eq_two]
    using succ_succAbove_succ (0 : Fin (n + 2)) (0 : Fin (n + 1))

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ (↑s).Subsingleton

Tactic:
by
  rw [card_le_one_iff_subsingleton_coe, ← Set.subsingleton_coe, SetLike.coe_sort_coe]

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ ∀ x ∈ image (fun i ↦ f ↑i) univ, P x

Tactic:
simp [A]

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

Goal state before:
pp: case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}.toFinset ↔ p x

Tactic:
· intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_ofPred]

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

Goal state before:
pp: case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}ᶜ.toFinset ↔ ¬p x

Tactic:
· intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_ofPred]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
⊢ ∃ n < #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s

Tactic:
let g (i : ℕ) : Finset α := s.image f^[i]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
⊢ ∃ n < #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_3
p : Fin (n + 1)
x : α
f : Fin n → α
⊢ range (p.insertNth x f) = Set.insert x (range f)

Tactic:
by
  ext y
  simp [Fin.exists_iff_succAbove p, Set.insert, eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
l : List α
hf : StrictAnti f
⊢ (map f l).SortedLE ↔ l.SortedGE

Tactic:
grind [hf.le_iff_ge]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
l : List α
hf : StrictAnti f
⊢ (map f l).SortedGE ↔ l.SortedLE

Tactic:
grind [hf.le_iff_ge]

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

Goal state before:
pp: case succ
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n) ↔ ∀ (m : ℕ), m < n - 1 → r m m.succ
⊢ IsChain r (range (n + 1)) ↔ ∀ (m : ℕ), m < n + 1 - 1 → r m m.succ

Tactic:
simp only [range_succ, Nat.add_one_sub_one, Nat.lt_sub_iff_add_lt] at hn ⊢

Goal state after:
case succ
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n) ↔ ∀ (m : ℕ), m + 1 < n → r m m.succ
⊢ IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m m.succ
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
p : α → Prop
l : List α
h : IsChain r l
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : ∀ (lne : l ≠ []), p (l.getLast lne)
⊢ ∀ (i : α), i ∈ l → p i

Tactic:
have H : IsChain (flip (flip r)) l := h

Goal state after:
α : Type u_1
r : α → α → Prop
p : α → Prop
l : List α
h : IsChain r l
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : ∀ (lne : l ≠ []), p (l.getLast lne)
H : IsChain (flip (flip r)) l
⊢ ∀ (i : α), i ∈ l → p i
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
⊢ ∀ (a : α) (s : Multiset α), filter p (n • s) = n • filter p s → filter p (n • (a ::ₘ s)) = n • filter p (a ::ₘ s)

Tactic:
· intro a ha ih
    rw [nsmul_cons, filter_add, ih, filter_cons, nsmul_add]
    congr
    split_ifs with hp <;>
      · simp only [filter_eq_self, nsmul_zero, filter_eq_nil]
        intro b hb
        rwa [mem_singleton.mp (mem_of_mem_nsmul hb)]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun b ↦ count a (f b)) S = count a (f x) ::ₘ m'
⊢ count a (f x) ≤ (count a (f x) ::ₘ m').sum

Tactic:
sum_cons

Goal state after:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun b ↦ count a (f b)) S = count a (f x) ::ₘ m'
⊢ count a (f x) ≤ count a (f x) + m'.sum
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
M : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : ExistsAddOfLE M
inst✝³ : AddLeftMono M
inst✝² : AddLeftReflectLE M
inst✝¹ : Sub M
inst✝ : OrderedSub M
l : Multiset ι
f g : ι → M
hfg : ∀ (x : ι), x ∈ l → g x ≤ f x
⊢ (map (fun x ↦ f x - g x) l).sum + (map g l).sum = (map f l).sum

Tactic:
rw [← sum_map_add]
    congr 1
    exact map_congr rfl fun x hx => tsub_add_cancel_of_le <| hfg _ hx

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

Goal state before:
pp: α : Type u_1
l : List α
this : ∀ (x : α × ℕ), x ∈ l.zipIdx → (l.eraseIdx x.snd).length = l.length - 1
⊢ l.offDiag.length = l.length * (l.length - 1)

Tactic:
simp [offDiag, map_congr_left this]

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

Goal state before:
pp: case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!

Tactic:
have h₂ : choose n (succ k) * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n ! := by
        rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]
        simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]

Goal state after:
case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (x, y) ∈ l.offDiag ↔ x ∈ l ∧ y ∈ l ∧ x ≠ y

Tactic:
mem_offDiag_iff_getElem,

Goal state after:
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h j h_1, i ≠ j ∧ l[i] = x ∧ l[j] = y) ↔ x ∈ l ∧ y ∈ l ∧ x ≠ y
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst✝ : DecidableEq α
⊢ (s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty

Tactic:
simp [Finset.Nonempty, Classical.skolem]

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

Goal state before:
pp: case inl
r n : ℕ
b : r ≤ n
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
rcases le_or_gt r (n / 2) with a | h

Goal state after:
case inl.inl
r n : ℕ
b : r ≤ n
a : r ≤ n / 2
⊢ n.choose r ≤ n.choose (n / 2)

case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n.choose r ≤ n.choose (n / 2)
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
hs : Fintype ↑s
ht : Fintype ↑t
⊢ Fintype ↑(image2 f s t)

Tactic:
← image_prod

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
hs : Fintype ↑s
ht : Fintype ↑t
⊢ Fintype ↑((fun x ↦ f x.1 x.2) '' s ×ˢ t)
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
⊢ Finite ↑(image2 f s t)

Tactic:
← image_prod

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
⊢ Finite ↑((fun x ↦ f x.1 x.2) '' s ×ˢ t)
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : DecidablePred fun x ↦ x ∈ s ^ n
⊢ DecidablePred fun x ↦ x ∈ s ^ (n + 1)

Tactic:
pow_succ

Goal state after:
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : DecidablePred fun x ↦ x ∈ s ^ n
⊢ DecidablePred fun x ↦ x ∈ s ^ n * s
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Injective f ∧ Surjective f ↔ ∀ (i : ι), Bijective ((U i).restrictPreimage f)

Tactic:
injective_iff_injective_of_iUnion_eq_univ hU,

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ (∀ (i : ι), Injective ((U i).restrictPreimage f)) ∧ Surjective f ↔ ∀ (i : ι), Bijective ((U i).restrictPreimage f)
Module: Mathlib.Algebra.Group.Submonoid.Defs

Goal state before:
pp: M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
⊢ x ^ (n + 1) ∈ S

Tactic:
pow_succ

Goal state after:
M : Type u_3
A : Type u_4
inst✝² : Monoid M
inst✝¹ : SetLike A M
inst✝ : SubmonoidClass A M
S : A
x : M
hx : x ∈ S
n : ℕ
⊢ x ^ n * x ∈ S
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ (n + 1)).Nonempty

Tactic:
pow_succ

Goal state after:
α : Type u_2
inst✝ : Monoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ n * s).Nonempty
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case refine_1
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : (mulSingle k u * mulSingle l v) k = (mulSingle m u * mulSingle n v) k
hl : (mulSingle k u * mulSingle l v) l = (mulSingle m u * mulSingle n v) l
hm : (mulSingle k u * mulSingle l v) m = (mulSingle m u * mulSingle n v) m
hn : (mulSingle k u * mulSingle l v) n = (mulSingle m u * mulSingle n v) n
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n

Tactic:
grind [mul_one, one_mul, mul_apply]

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i → ∃ i, p i ∧ x ∈ K i

pp: case refine_2
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i✝ : ι
hp : p i✝
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
x✝ : ∃ i, p i ∧ x ∈ K i
i : ι
hi' : p i
hi : x ∈ K i
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i

Tactic:
· suffices x ∈ closure (⋃ i, ⋃ (_ : p i), (K i : Set G)) → ∃ i, p i ∧ x ∈ K i by
      simpa only [closure_iUnion, closure_eq (K _)] using this
    refine fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ ?_ ?_ hx
    · simp
    · exact ⟨i, hp, (K i).one_mem⟩
    · rintro x y _ _ ⟨i, hip, hi⟩ ⟨j, hjp, hj⟩
      rcases hK i hip j hjp with ⟨k, hk, hki, hkj⟩
      exact ⟨k, hk, mul_mem (hki hi) (hkj hj)⟩
    · rintro _ _ ⟨i, hi', hi⟩
      exact ⟨i, hi', inv_mem hi⟩

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i✝ : ι
hp : p i✝
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
x✝ : ∃ i, p i ∧ x ∈ K i
i : ι
hi' : p i
hi : x ∈ K i
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ ↑H ∩ Set.range ⇑f = Set.range ⇑f ∩ ↑H

Tactic:
Set.inter_comm

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ Set.range ⇑f ∩ ↑H = Set.range ⇑f ∩ ↑H
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
ι : Type u_5
f : F
hf : Injective ⇑f
S : Submonoid M
x : M
⊢ x ∈ comap f (map f S) → x ∈ S

Tactic:
simp [mem_comap, mem_map, hf.eq_iff]

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
⊢ (bit b n).testBit m.succ = n.testBit m

Tactic:
by
  have : bodd (((bit b n) >>> 1) >>> m) = bodd (n >>> m) := by
    simp only [shiftRight_eq_div_pow]
    simp [← div2_val, div2_bit]
  rw [← shiftRight_add, Nat.add_comm] at this
  simp only [bodd_eq_one_and_ne_zero] at this
  exact this

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ g (f_inv (x * y) * (f_inv x * f_inv y)⁻¹) = 1

Tactic:
← g.mem_ker

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ f_inv (x * y) * (f_inv x * f_inv y)⁻¹ ∈ g.ker
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ g (f_inv (f x) * x⁻¹) = 1

Tactic:
← g.mem_ker

Goal state after:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f_inv (f x) * x⁻¹ ∈ g.ker
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x : FreeMonoid α
e : α ≃ β
⊢ (map ⇑e.symm) ((map ⇑e) x) = x

Tactic:
simp [map_map]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : FreeMonoid β
e : α ≃ β
⊢ (map ⇑e) ((map ⇑e.symm) x) = x

Tactic:
simp [map_map]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ (x ^ ((m + 1) * (n - 1))) ^ k = x ^ (m.succ % n * ((n - 1) * k))

Tactic:
pow_mul _ (_ % _),

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ (x ^ ((m + 1) * (n - 1))) ^ k = (x ^ (m.succ % n)) ^ ((n - 1) * k)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableLT β
f : α → β
a : α
l : List α
⊢ foldl (argAux fun b c ↦ f c < f b) none (l ++ [a]) =
    Option.casesOn (foldl (argAux fun b c ↦ f c < f b) none l) (some a) fun c ↦ if f c < f a then some a else some c

Tactic:
simp [argAux]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ #u.toLeft + #u.toRight = #u

Tactic:
by
  rw [← card_disjSum, toLeft_disjSum_toRight]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
l tl : List α
hd : α
ih : (a :: tl).maximum = max (↑a) tl.maximum
⊢ max (max (↑a) tl.maximum) ↑hd = max (↑a) (max tl.maximum ↑hd)

Tactic:
max_assoc

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a : α
l tl : List α
hd : α
ih : (a :: tl).maximum = max (↑a) tl.maximum
⊢ max (↑a) (max tl.maximum ↑hd) = max (↑a) (max tl.maximum ↑hd)
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
⊢ f (min a b) = f a ⊓ f b

Tactic:
by
      obtain h | h := le_total a b
      · rw [inf_eq_left.2 h, inf_eq_left.2 (OrderHomClass.mono f h : f a ≤ f b)]
      · rw [inf_eq_right.2 h, inf_eq_right.2 (OrderHomClass.mono f h : f b ≤ f a)]

Goal state after:
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f a \ f b ⊔ f (b \ a) = f a \ f b ⊔ f b \ f a

Tactic:
map_sdiff'

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f a \ f b ⊔ f b \ f a = f a \ f b ⊔ f b \ f a
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
⊢ Pairwise (Lex (Function.swap R)) (a :: l).sublists'

Tactic:
simp only [sublists'_cons, pairwise_append, pairwise_map, mem_sublists', mem_map, exists_imp,
      and_imp]
    refine ⟨H₂.sublists', H₂.sublists'.imp fun l₁ => Lex.cons l₁, ?_⟩
    rintro l₁ sl₁ x l₂ _ rfl
    rcases l₁ with - | ⟨b, l₁⟩; · constructor
    exact Lex.rel (H₁ _ <| sl₁.subset mem_cons_self)

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

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
⊢ powersetCard 1 ⟦l⟧ = map singleton ⟦l⟧

Tactic:
simp [powersetCard_coe, sublistsLen_one, map_reverse, Function.comp_def]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
⊢ ↑(t.sup f) = t.sup fun x ↦ ↑(f x)

Tactic:
apply apply_sup_eq_sup_comp Subtype.val <;> intros

Goal state after:
case g_sup
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
x✝ y✝ : { x // P x }
⊢ ↑(x✝ ⊔ y✝) = ↑x✝ ⊔ ↑y✝

case bot
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := ⋯
this : OrderBot { x // P x } := ⋯
⊢ ↑⊥ = ⊥