mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (↑(List.map f s.toList)).prod = (map f s).prod

Tactic:
← Multiset.map_coe,

Goal state after:
ι : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Multiset ι
f : ι → M
⊢ (map f ↑s.toList).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
⊢ drop n (l ++ [a]) ++ take n (l ++ [a]) = drop n l ++ a :: take n l

Tactic:
drop_append_of_le_length hnl,

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : ¬l.length = 0
⊢ l.rotate n = l.rotate' (n % l.length)

Tactic:
rotate'_eq_drop_append_take (le_of_lt (Nat.mod_lt _ (Nat.pos_of_ne_zero h)))

Goal state after:
α : Type u
l : List α
n : ℕ
h : ¬l.length = 0
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
s : Multiset α
σ : α → Type u_5
t : (a : α) → Multiset (σ a)
l₁ : List α
⊢ Nodup (Quot.mk (⇑(List.isSetoid α)) l₁) →
    (∀ (a : α), (t a).Nodup) → (Multiset.sigma (Quot.mk (⇑(List.isSetoid α)) l₁) t).Nodup

Tactic:
choose f hf using fun a => Quotient.exists_rep (t a)
    simpa [← funext hf] using List.Nodup.sigma

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : z = y
⊢ count (x, y) (map (fun x ↦ (x, y)) l) = count x l

Tactic:
count_map_of_injective l (·, y) (by simp [Function.Injective])

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : z = y
⊢ count x l = count x l
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case succ
n : ℕ
ih : n.choose 2 = n * (n - 1) / 2
⊢ n.choose 1 + n * (n - 1) / 2 = n * (n - 1) / 2 + n

Tactic:
simp [Nat.add_comm]

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ n.choose (n - k) = n ! / (k ! * (n - k)!)

Tactic:
choose_eq_factorial_div_factorial (Nat.sub_le _ _),

Goal state after:
n k : ℕ
hk : k ≤ n
⊢ n ! / ((n - k)! * (n - (n - k))!) = n ! / (k ! * (n - k)!)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p)! * ((p + 1) * (m + 1)) = (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1))

Tactic:
by
      rw [add_choose_mul_factorial_mul_factorial]

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

Goal state before:
pp: case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 1 (k + 1) + (k + 1) = k + 1 + 1

Tactic:
simp [Nat.add_comm]

Goal state after:
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
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ f x ∈ univ

Tactic:
trivial

Goal state after:
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
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
⊢ x ∈ univ

Tactic:
trivial

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
⊢ ⨆ i, p i = ⨆ i, closure ↑(p i)

Tactic:
Subsemigroup.closure_eq

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

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i

pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i

Tactic:
· intro x hz hw
    exact ⟨⟨x, hz⟩, x, hw⟩

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a : α
⊢ (fun x ↦ a⁻¹ * x) '' 1 = {a⁻¹}

Tactic:
image_one,

Goal state after:
α : Type u_2
inst✝ : Group α
a : α
⊢ {a⁻¹ * 1} = {a⁻¹}
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
b : α
⊢ (fun x ↦ x * b⁻¹) '' 1 = {b⁻¹}

Tactic:
image_one,

Goal state after:
α : Type u_2
inst✝ : Group α
b : α
⊢ {1 * b⁻¹} = {b⁻¹}
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ x ^ -[n+1] ∈ K

Tactic:
zpow_negSucc

Goal state after:
M : Type u_3
S : Type u_4
inst✝¹ : DivInvMonoid M
inst✝ : SetLike S M
hSM : SubgroupClass S M
K : S
x : M
hx : x ∈ K
n : ℕ
⊢ (x ^ (n + 1))⁻¹ ∈ K
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
S : Submonoid M
f : M →* N
⊢ mrange (f.domRestrict S) = map f S

Tactic:
simp [SetLike.ext_iff]

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

Goal state before:
pp: case pos
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : a₁ < b
h₂ : a₂ < b
⊢ b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

Tactic:
simp [h₂, h]

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

Goal state before:
pp: case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : ¬a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

Tactic:
simp [h₂, h]

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case inr
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ (subtypeOrLeftEmbedding p q) ((Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯) x) = Sum.inr x

Tactic:
subtypeOrLeftEmbedding_apply_right

Goal state after:
case inr
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ Sum.inr ⟨↑((Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯) x), ⋯⟩ = Sum.inr x

case inr.hx
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ ¬p ↑((Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯) x)
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
a b : Lex (α × β)
this✝¹ : DecidableLT (Lex (α × β))
this✝ : Std.LawfulBEqOrd (Lex (α × β))
this : Std.LawfulLTOrd (Lex (α × β))
⊢ compare a b = compareOfLessAndEq a b

Tactic:
convert! Std.LawfulLTCmp.eq_compareOfLessAndEq (cmp := compare) a b

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
s : Set M
x : M
hx : x ∈ closure s
l : List M
h1 : ∀ y ∈ l, y ∈ s
h2 : l.prod = x
⊢ ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Tactic:
exact ⟨l, h1, (Multiset.prod_coe l).trans h2⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
⊢ (s.disjSum t).card = s.card + t.card

Tactic:
by
  rw [disjSum, card_add, card_map, card_map]

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

Goal state before:
pp: α : Type u_7
R : Type u_8
inst✝ : LinearOrder R
f : α → R
s : Multiset α
hs : s ≠ 0
⊢ ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y

Tactic:
obtain ⟨y, hys, hy⟩ := Finset.exists_max_image s.toFinset f (toFinset_nonempty.mpr hs)

Goal state after:
α : Type u_7
R : Type u_8
inst✝ : LinearOrder R
f : α → R
s : Multiset α
hs : s ≠ 0
y : α
hys : y ∈ s.toFinset
hy : ∀ x' ∈ s.toFinset, f x' ≤ f y
⊢ ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ (map f (a :: l)).sublists' = map (map f) (a :: l).sublists'

Tactic:
simp [map_cons, sublists'_cons, sublists'_map f l, Function.comp]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s₁ : Finset β
f g : β → α
hfg : ∀ a ∈ s₁, f a = g a
⊢ s₁.sup f = s₁.sup g

Tactic:
exact Finset.fold_congr hfg

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

Goal state before:
pp: case refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
j : Finset α
hj : j ⊆ s
hi : insert a j ⊆ s
⊢ insert a j = j

Tactic:
cases Finset.notMem_mono ‹_› ha (Finset.mem_insert_self _ _)

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

Goal state before:
pp: case refine_2
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
hj : insert a i ⊆ s
⊢ i = insert a i

Tactic:
cases Finset.notMem_mono ‹_› ha (Finset.mem_insert_self _ _)

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

Goal state before:
pp: α : Type u_1
s : Finset (Option α)
h : none ∉ s
⊢ #(eraseNone s) = #s

Tactic:
classical rw [card_eraseNone_eq_card_erase, erase_eq_of_notMem h]

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
hs : s.Nonempty
⊢ a ∈ s.sup' hs f ↔ ∃ i ∈ s, a ∈ f i

Tactic:
induction hs using Nonempty.cons_induction

Goal state after:
case singleton
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝ : ι
⊢ a ∈ {a✝}.sup' ⋯ f ↔ ∃ i ∈ {a✝}, a ∈ f i

case cons
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : a ∈ s✝.sup' hs✝ f ↔ ∃ i ∈ s✝, a ∈ f i
⊢ a ∈ (cons a✝¹ s✝ h✝).sup' ⋯ f ↔ ∃ i ∈ cons a✝¹ s✝ h✝, a ∈ f i
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
hs : s.Nonempty
⊢ a ∈ s.inf' hs f ↔ ∀ i ∈ s, a ∈ f i

Tactic:
induction hs using Nonempty.cons_induction

Goal state after:
case singleton
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝ : ι
⊢ a ∈ {a✝}.inf' ⋯ f ↔ ∀ i ∈ {a✝}, a ∈ f i

case cons
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : a ∈ s✝.inf' hs✝ f ↔ ∀ i ∈ s✝, a ∈ f i
⊢ a ∈ (cons a✝¹ s✝ h✝).inf' ⋯ f ↔ ∀ i ∈ cons a✝¹ s✝ h✝, a ∈ f i
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
⊢ a ∈ s.sup f ↔ ∃ i ∈ s, a ∈ f i

Tactic:
by
  induction s using cons_induction <;> simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' Ico a b = Ico ↑a ↑b

Tactic:
← preimage_coe_Ico,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' some ⁻¹' Ico ↑a ↑b = Ico ↑a ↑b
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
⊢ sSup ∅ ≤ ⨆ i, ↑i

Tactic:
convert! h
    rw [← sSup_range, Subtype.range_coe]

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

Goal state before:
pp: case refine_2
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ t, ⨆ i ∈ t, s i ≤ ⨆ i, s i

Tactic:
exact iSup_le fun t => iSup_le fun b => iSup_le fun _ => le_iSup _ _

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
h : a ⋖ b ∨ a ≤ b ∧ b ≤ a
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

Tactic:
obtain h | h := h

Goal state after:
case inl
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
h : a ⋖ b
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)

case inr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
h : a ≤ b ∧ b ≤ a
⊢ ∃ i, ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
⊢ x ∈ sigmaLift f ⟨i, a⟩ ⟨j, b⟩ ↔
    ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨j, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨j, b⟩.snd)

Tactic:
obtain rfl | h := Decidable.eq_or_ne i j

Goal state after:
case inl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ x ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔
    ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨i, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨i, b⟩.snd)

case inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ x ∈ sigmaLift f ⟨i, a⟩ ⟨j, b⟩ ↔
    ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨j, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨j, b⟩.snd)
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (range ⇑coeOrderHom).OrdConnected

Tactic:
simp [WithTop.range_coe, ordConnected_Iio]

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

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ x ∈ sigmaLift f ⟨i, a⟩ ⟨j, b⟩ ↔
    ∃ (ha : ⟨i, a⟩.fst = x.fst) (hb : ⟨j, b⟩.fst = x.fst), x.snd ∈ f (ha ▸ ⟨i, a⟩.snd) (hb ▸ ⟨j, b⟩.snd)

Tactic:
rw [sigmaLift, dif_neg h]
    refine iff_of_false (notMem_empty _) ?_
    rintro ⟨⟨⟩, ⟨⟩, _⟩
    exact h rfl

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: b : ℕ
⊢ #(Iio b) = b

Tactic:
rw [Iio_eq_Ico, card_Ico, Nat.bot_eq_zero, Nat.sub_zero]

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: ⊢ True

Tactic:
trivial

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀ h₁ : LocallyFiniteOrder α
⊢ h₀ = h₁

Tactic:
by
    obtain ⟨h₀_finset_Icc, h₀_finset_Ico, h₀_finset_Ioc, h₀_finset_Ioo,
      h₀_finset_mem_Icc, h₀_finset_mem_Ico, h₀_finset_mem_Ioc, h₀_finset_mem_Ioo⟩ := h₀
    obtain ⟨h₁_finset_Icc, h₁_finset_Ico, h₁_finset_Ioc, h₁_finset_Ioo,
      h₁_finset_mem_Icc, h₁_finset_mem_Ico, h₁_finset_mem_Ioc, h₁_finset_mem_Ioo⟩ := h₁
    have hIcc : h₀_finset_Icc = h₁_finset_Icc := by
      ext a b x
      rw [h₀_finset_mem_Icc, h₁_finset_mem_Icc]
    have hIco : h₀_finset_Ico = h₁_finset_Ico := by
      ext a b x
      rw [h₀_finset_mem_Ico, h₁_finset_mem_Ico]
    have hIoc : h₀_finset_Ioc = h₁_finset_Ioc := by
      ext a b x
      rw [h₀_finset_mem_Ioc, h₁_finset_mem_Ioc]
    have hIoo : h₀_finset_Ioo = h₁_finset_Ioo := by
      ext a b x
      rw [h₀_finset_mem_Ioo, h₁_finset_mem_Ioo]
    simp_rw [hIcc, hIco, hIoc, hIoo]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n : ℕ
h : n + m ∉ bad
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))

Tactic:
simp only [bad, exists_prop, not_not, Set.mem_ofPred_eq, not_forall] at h

Goal state after:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n : ℕ
h : ∃ x, n + m < x ∧ r (f (n + m)) (f x)
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ico a b = ∅ ↔ ¬a < b

Tactic:
by
  rw [← coe_eq_empty, coe_Ico, Set.Ico_eq_empty_iff]

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

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : Set M
m n : ℕ
hmn : m ∣ n
⊢ closure (s ^ n) ≤ closure (s ^ m)

Tactic:
obtain ⟨k, rfl⟩ := hmn

Goal state after:
M : Type u_3
inst✝ : Monoid M
s : Set M
m k : ℕ
⊢ closure (s ^ (m * k)) ≤ closure (s ^ m)
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ MulAction.orbit ↥H ⟦a⟧.out
⊢ ↑b ∈ MulAction.orbit ↥H ↑a

Tactic:
rw [orbitRel.Quotient.mem_subgroup_orbit_iff]

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ MulAction.orbit ↥H ⟦a⟧.out
⊢ b ∈ MulAction.orbit (↥H) a
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
⊢ ¬∃ f,
      IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f ∧
        ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f

Tactic:
rintro ⟨f, hf1, hf2⟩

Goal state after:
case inr
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
⊢ False
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
x y : G
hx : IsConj x g
hy : IsConj y g
⊢ x = y

Tactic:
rw [hx.eq_of_right_mem_center hg, hy.eq_of_right_mem_center hg]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝³ : Monoid M
inst✝² : SMul α M
inst✝¹ : SMulCommClass α M M
inst✝ : IsScalarTower α M M
a : α
um : ConjAct Mˣ
m : M
⊢ a • um • m = um • a • m

Tactic:
units_smul_def,

Goal state after:
α : Type u_1
M : Type u_2
G : Type u_3
inst✝³ : Monoid M
inst✝² : SMul α M
inst✝¹ : SMulCommClass α M M
inst✝ : IsScalarTower α M M
a : α
um : ConjAct Mˣ
m : M
⊢ a • (↑(ofConjAct um) * m * ↑(ofConjAct um)⁻¹) = um • a • m
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝³ : Monoid M
inst✝² : SMul α M
inst✝¹ : SMulCommClass α M M
inst✝ : IsScalarTower α M M
a : α
um : ConjAct Mˣ
m : M
⊢ a • (↑(ofConjAct um) * m * ↑(ofConjAct um)⁻¹) = um • a • m

Tactic:
units_smul_def,

Goal state after:
α : Type u_1
M : Type u_2
G : Type u_3
inst✝³ : Monoid M
inst✝² : SMul α M
inst✝¹ : SMulCommClass α M M
inst✝ : IsScalarTower α M M
a : α
um : ConjAct Mˣ
m : M
⊢ a • (↑(ofConjAct um) * m * ↑(ofConjAct um)⁻¹) = ↑(ofConjAct um) * a • m * ↑(ofConjAct um)⁻¹
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g k : G
⊢ g * k = k * g ↔ k * g = g * k

Tactic:
exact eq_comm

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
m n : ℕ
hmn : m ∣ n
⊢ closure (s ^ n) ≤ closure (s ^ m)

Tactic:
obtain ⟨k, rfl⟩ := hmn

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
m k : ℕ
⊢ closure (s ^ (m * k)) ≤ closure (s ^ m)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case inv_mem
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H * ↑N
⊢ x⁻¹ ∈ ↑H * ↑N

Tactic:
obtain ⟨x, hx, y, hy, rfl⟩ := hx

Goal state after:
case inv_mem
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
⊢ ((fun x1 x2 ↦ x1 * x2) x y)⁻¹ ∈ ↑H * ↑N
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mul
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x x'✝ x' : G
hx✝ : x'✝ ∈ closure (↑H * ↑N)
hy✝ : x' ∈ closure (↑H * ↑N)
hx : x'✝ ∈ ↑H * ↑N
hx' : x' ∈ ↑H * ↑N
⊢ x'✝ * x' ∈ ↑H * ↑N

Tactic:
obtain ⟨x, hx, y, hy, rfl⟩ := hx

Goal state after:
case mul
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x' : G
hy✝ : x' ∈ closure (↑H * ↑N)
hx' : x' ∈ ↑H * ↑N
x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 ↦ x1 * x2) x y ∈ closure (↑H * ↑N)
⊢ (fun x1 x2 ↦ x1 * x2) x y * x' ∈ ↑H * ↑N
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

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

Tactic:
← Multiset.map_coe,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
⊢ (Multiset.map f ↑s.toList).prod = (Multiset.map f s.val).prod
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
x y : M
hf : ∀ (x : M), ↑(f x) * ↑x = 1
h : ↑x = ↑y
hf' : ∀ (x : M), ↑x * ↑(f x) = 1
this :
  { val := ↑x, inv := ↑(f x), val_inv := ⋯, inv_val := ⋯ } = { val := ↑y, inv := ↑(f y), val_inv := ⋯, inv_val := ⋯ }
⊢ ↑(f x) = ↑(f y)

Tactic:
exact congr_arg Units.inv this

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : ι) → Decidable ¬p x
f : ι → M
this : DecidableEq ι
⊢ ∏ x ∈ filter p s ∪ {a ∈ s | ¬p a}, f x = ∏ x ∈ s, f x

Tactic:
filter_union_filter_not_eq

Goal state after:
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : ι) → Decidable ¬p x
f : ι → M
this : DecidableEq ι
⊢ ∏ x ∈ s, f x = ∏ x ∈ s, f x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : Fintype ι
s t : Finset ι
h : IsCompl s t
f : ι → M
⊢ ∏ x ∈ s.disjUnion t ⋯, f x = ∏ i, f i

Tactic:
by
    classical rw [Finset.disjUnion_eq_union, ← Finset.sup_eq_union, h.sup_eq_top]; rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case e_f
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : ↥s → M
x : ι
hx : x ∈ s
⊢ f ⟨x, hx⟩ = extend Subtype.val f 1 ↑⟨x, hx⟩

Tactic:
Subtype.val_injective.extend_apply

Goal state after:
case e_f
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : ↥s → M
x : ι
hx : x ∈ s
⊢ f ⟨x, hx⟩ = f ⟨x, hx⟩
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
u : ℕ → M
N : ℕ
hu : ∀ n ≥ N, u n = 1
m : ℕ
⊢ ∏ k ∈ range (N + m), u k = ∏ k ∈ range N, u k

Tactic:
induction m with

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n m : ℕ
⊢ ∏ x ∈ range (n + m), f x = (∏ x ∈ range n, f x) * ∏ x ∈ range m, f (n + x)

Tactic:
induction m with

Goal state after: