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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
⊢ count a (orderedInsert r b L) = count a L + if b = a then 1 else 0

Tactic:
(L.perm_orderedInsert r b).count_eq,

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
⊢ count a (b :: L) = count a L + if b = a then 1 else 0
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl : ∀ (a : α), a ∈ x :: xs → ∀ (b : α), b ∈ x :: xs → (r a b ↔ s (f a) (f b))
⊢ map f (insertionSort r (x :: xs)) = insertionSort s (map f (x :: xs))

Tactic:
simp_rw [List.forall_mem_cons, forall_and] at hl

Goal state after:
case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ map f (insertionSort r (x :: xs)) = insertionSort s (map f (x :: xs))
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
simp [rev_succAbove]

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

Goal state before:
pp: case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b s = op a (fold op b s)

Tactic:
rw [← cons_erase h, fold_cons_left, ← ha.assoc, hi.idempotent]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
head✝ : α
tail✝ : List α
ih : ∀ {c : List α}, Pairwise r c → c <+ tail✝ → c <+ insertionSort r tail✝
c : List α
hr : Pairwise r c
hc : c <+ head✝ :: tail✝
⊢ c <+ insertionSort r (head✝ :: tail✝)

Tactic:
cases hc with

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.SortedLT ↔ Pairwise (fun x1 x2 ↦ x1 < x2) l

Tactic:
simp only [sortedLT_iff_strictMono_get, StrictMono, Fin.forall_iff]

Goal state after:
α : Type u_1
l : List α
inst✝ : Preorder α
⊢ (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
      ⟨i, h⟩ < ⟨i_1, h_1⟩ → l.get ⟨i, h⟩ < l.get ⟨i_1, h_1⟩) ↔
    Pairwise (fun x1 x2 ↦ x1 < x2) l
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun b a ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ R a (l.getLast ⋯)

Tactic:
getLast_eq_head_reverse

Goal state after:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun b a ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ R a (l.reverse.head ⋯)
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
h : Pairwise R l
⊢ Pairwise (fun a b ↦ Decidable.decide (R a b) = true) l

Tactic:
by
  refine h.imp fun {a b} h => by simpa using h

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
⊢ map Prod.swap (s ×ˢ t) = t ×ˢ s

Tactic:
by
  induction s using Multiset.induction <;> simp_all

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

Goal state before:
pp: α : Type u_1
β : Type v
M : Type u_4
inst✝ : CommMonoid M
s : Multiset α
t : Multiset β
f : α × β → M
⊢ (map f (s ×ˢ t)).prod = (map (fun i ↦ (map (fun j ↦ f (i, j)) t).prod) s).prod

Tactic:
by
  induction s using Multiset.induction <;> simp_all

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin (n + 1) → Set α
⊢ ⋃ i, f i = iUnion (f ∘ Fin.castSucc) ∪ f (Fin.last n)

Tactic:
by
  cases f using Fin.snocCases
  simp [Function.comp_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (f '' sᶜ ∩ tᶜ)ᶜ = (f '' sᶜ)ᶜ ∪ t

Tactic:
compl_inter,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (f '' sᶜ)ᶜ ∪ tᶜᶜ = (f '' sᶜ)ᶜ ∪ t
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 : β
i : ι
hi : x ∈ U i
⊢ ∃ a, f a = x

Tactic:
exact ⟨_, congr_arg Subtype.val (H i ⟨x, hi⟩).choose_spec⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → α
g : α → Set β
⊢ ⋂ x, ⋂ y, ⋂ (_ : f y = x), g x = ⋂ y, g (f y)

Tactic:
by simpa using biInter_range

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : InvolutiveInv α
s : Set α
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = g x
⊢ f '' s⁻¹ = g '' s

Tactic:
by
  rw [← Set.image_inv_eq_inv, Set.image_image]; exact Set.image_congr H

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (Prod.mk '' s).seq t = ((fun b a ↦ (a, b)) '' t).seq s

Tactic:
rw [← prod_eq_seq, ← image_swap_prod, prod_eq_seq, image_seq, ← image_comp]; rfl

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
p₁ p₂ : Submonoid M
⊢ Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1

Tactic:
disjoint_iff_inf_le,

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
p₁ p₂ : Submonoid M
⊢ p₁ ⊓ p₂ ≤ ⊥ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x a b : M
ha : ∀ (y : M), f (a * y) = f a * f y
hb : ∀ (y : M), f (b * y) = f b * f y
y : M
⊢ f (a * b * y) = f (a * b) * f y

Tactic:
by rw [mul_assoc, ha, ha, hb, mul_assoc]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
g : G
⊢ g⁻¹ ∈ normalizer S ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S

Tactic:
mem_set_normalizer_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
S : Set G
g : G
⊢ (∀ (h : G), h ∈ S ↔ g⁻¹ * h * g⁻¹⁻¹ ∈ S) ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x y : G
⊢ y ∈ closure {x} ↔ ∃ n, x ^ n = y

Tactic:
refine
    ⟨fun hy => closure_induction ?_ ?_ ?_ ?_ hy, fun ⟨n, hn⟩ =>
      hn ▸ zpow_mem (subset_closure <| mem_singleton x) n⟩

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ {x}, ∃ n, x ^ n = x_1

case refine_2
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∃ n, x ^ n = 1

case refine_3
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 y : G), x_1 ∈ closure {x} → y ∈ closure {x} → (∃ n, x ^ n = x_1) → (∃ n, x ^ n = y) → ∃ n, x ^ n = x_1 * y

case refine_4
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ closure {x}, (∃ n, x ^ n = x_1) → ∃ n, x ^ n = x_1⁻¹
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
M' : Submonoid M
⊢ Surjective ⇑(f.submonoidMap M')

Tactic:
rintro ⟨_, x, hx, rfl⟩
  exact ⟨⟨x, hx⟩, rfl⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : ⇑(MulAut.conj g) '' s = s
⊢ g ∈ normalizer ↑(closure s)

Tactic:
mem_normalizer_iff_map_conj_eq,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : ⇑(MulAut.conj g) '' s = s
⊢ map (↑(MulAut.conj g)) (closure s) = closure s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
⊢ h ∈ normalizer ↑(closure s)

Tactic:
mem_normalizer_iff_map_conj_eq,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
⊢ map (↑(MulAut.conj h)) (closure s) = closure s
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ ⋃ g, g⁻¹ • s = ⋃ i, {x | i • x ∈ s}

Tactic:
← preimage_smul,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ ⋃ g, (fun x ↦ g • x) ⁻¹' s = ⋃ i, {x | i • x ∈ s}
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a • s ∩ b • t ⊆ z • s⁻¹ * s ∩ (z • t⁻¹ * t)

Tactic:
gcongr <;> apply smul_set_subset_mul

Goal state after:
case h₁
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ a ∈ z • s⁻¹

case h₂
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ b ∈ z • t⁻¹
Module: Mathlib.Data.Sigma.Lex

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

Tactic:
· exact Lex.right _ _ (symm hab)

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithTop.map (⇑ofDual) s.min = (image (⇑ofDual) s).sup WithBot.some

Tactic:
sup_image

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithTop.map (⇑ofDual) s.min = s.sup (WithBot.some ∘ ⇑ofDual)
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithTop.map (⇑toDual) s.min = (image (⇑toDual) s).sup WithBot.some

Tactic:
sup_image

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithTop.map (⇑toDual) s.min = s.sup (WithBot.some ∘ ⇑toDual)
Module: Mathlib.Data.List.Zip

Goal state before:
pp: α : Type u
β : Type u_1
a : α
l₁ : List α
b : β
l₂ : List β
⊢ map Prod.swap ((a :: l₁).zip (b :: l₂)) = (b :: l₂).zip (a :: l₁)

Tactic:
by
    simp only [zip_cons_cons, map_cons, zip_swap l₁ l₂, Prod.swap_prod_mk]

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

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α
⊢ (powersetAux l).revzip ~ (powersetAux' l).revzip

Tactic:
rw [revzip_powersetAux_lemma l revzip_powersetAux, revzip_powersetAux_lemma l revzip_powersetAux']

Goal state after:
α : Type u_1
l : List α
this : DecidableEq α
⊢ List.map (fun x ↦ (x, ↑l - x)) (powersetAux l) ~ List.map (fun x ↦ (x, ↑l - x)) (powersetAux' l)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ l₁✝.sublists' <+ l₂✝.sublists' ++ map (List.cons a) l₂✝.sublists'

Tactic:
exact ih.trans (List.sublist_append_left ..)

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.powerset = ∅.powerset ↔ s = ∅

Tactic:
powerset_inj

Goal state after:
α : Type u_1
s : Finset α
⊢ s = ∅ ↔ s = ∅
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddAbove (⋃ i, range (f i))
a : α
h : a ∈ upperBounds (⋃ i, range (f i))
⊢ BddAbove (range fun i ↦ ⨆ j, f i j)

Tactic:
refine ⟨a ⊔ (sSup ∅), fun x ⟨i, hx⟩ ↦ hx ▸ ?_⟩

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddAbove (⋃ i, range (f i))
a : α
h : a ∈ upperBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨆ j, f i j
i : ι
hx : (fun i ↦ ⨆ j, f i j) i = x
⊢ (fun i ↦ ⨆ j, f i j) i ≤ a ⊔ sSup ∅
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ Ico a b ⊆ {a}

Tactic:
by
  rw [← Icc_sdiff_right, h.Icc_eq, sdiff_singleton_subset_iff, pair_comm]

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
h : a ⩿ b
i : ι
ci : α i
h₁ : a i < ci
h₂ : ci < b i
hcb : Function.update a i ci ≤ b
⊢ False

Tactic:
refine h.2 (by simpa) (lt_of_le_not_ge hcb ?_)

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
ci : α i
h₁ : a i < ci
h₂ : ci < b i
hcb : Function.update a i ci ≤ b
⊢ ¬b ≤ Function.update a i ci
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
⊢ Minimal P x ↔ Minimal Q x

Tactic:
refine ⟨fun h' ↦ ⟨?_, fun y hy hyx ↦ h'.le_of_le (hPQ hy) hyx⟩,
    fun h' ↦ ⟨hPQ h'.prop, fun y hy hyx ↦ ?_⟩⟩
  · obtain ⟨y, hyx, hy⟩ := h h'.prop
    rwa [((h'.le_of_le (hPQ hy)) hyx).antisymm hyx]
  obtain ⟨z, hzy, hz⟩ := h hy
  exact (h'.le_of_le hz (hzy.trans hyx)).trans hzy

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ↪o β
t : Set β
hts : t ⊆ ⇑f '' s
⊢ x ∈ s ∧ x ∈ {a | Minimal (fun x ↦ x ∈ t) (f a)} ↔ Minimal (fun x ↦ x ∈ s ∧ x ∈ ⇑f ⁻¹' t) x

Tactic:
mem_ofPred_eq,

Goal state after:
α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ↪o β
t : Set β
hts : t ⊆ ⇑f '' s
⊢ x ∈ s ∧ Minimal (fun x ↦ x ∈ t) (f x) ↔ Minimal (fun x ↦ x ∈ s ∧ x ∈ ⇑f ⁻¹' t) x
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioo a b ↔ a < x ∧ x < b

Tactic:
by rw [Ioo, ← Finset.mem_def, Finset.mem_Ioo]

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Ici a ↔ a ≤ x

Tactic:
rw [Ici, ← Finset.mem_def, Finset.mem_Ici]

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

Goal state before:
pp: s : Set ℕ
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅

Tactic:
cases eq_empty_or_nonempty s with
  | inl h => subst h
             simp only [or_true, InfSet.sInf,
                        mem_empty_iff_false, exists_false, dif_neg, not_false_iff]
  | inr h => simp only [h.ne_empty, or_false, Nat.sInf_def, h, Nat.find_eq_zero]

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

Goal state before:
pp: a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)
l : ℕ
hl : l ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)
hkl : k % a = l % a
⊢ a ≠ 0

Tactic:
by rintro rfl; simp at hk

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

Goal state before:
pp: case inr.mpr.inl.refine_1
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + a * (1 + n / a)

Tactic:
Nat.mul_add,

Goal state after:
case inr.mpr.inl.refine_1
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n ≤ i + (a * 1 + a * (n / a))
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr.mpr.inl.refine_2
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a + a * (n / a + 1) ≤ n + a

Tactic:
Nat.mul_add,

Goal state after:
case inr.mpr.inl.refine_2
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a + (a * (n / a) + a * 1) ≤ n + a
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
by
  rw [← coe_eq_empty, coe_Ioo, Set.Ioo_eq_empty_iff]

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Set.Icc a₁ b₁ ⊆ Set.Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
Set.Icc_subset_Icc_iff h₁

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂

Tactic:
← coe_ssubset,

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ ↑(Icc a₁ b₁) ⊂ ↑(Icc a₂ b₂)
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ Finset.subtype p (Ioc ↑a ↑b) ↔ a < x ∧ x ≤ b

Tactic:
simp_rw [Finset.mem_subtype, mem_Ioc, Subtype.coe_le_coe, Subtype.coe_lt_coe]

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂

Tactic:
← coe_ssubset,

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ ↑(Icc a₁ b₁) ⊂ ↑(Icc a₂ b₂)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (Icc a b).erase a = Ioc a b

Tactic:
by simp [← coe_inj]

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (Icc a b).erase b = Ico a b

Tactic:
by simp [← coe_inj]

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (Ico a b).erase a = Ioo a b

Tactic:
by simp [← coe_inj]

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (Ioc a b).erase b = Ioo a b

Tactic:
by simp [← coe_inj]

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ Icc a b \ {a, b} = Ioo a b

Tactic:
by simp [← coe_inj]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Ici a) = Ici ↑a

Tactic:
by
  rw [subtype_Ici_eq]
  exact Finset.subtype_map_of_mem fun x hx => hp (mem_Ici.1 hx) a.prop

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

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : Set M
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ closure s ≤ closure (s ^ n)

Tactic:
grw [← subset_pow hs hn]

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ #(Ico a b) = #(cons b (Ico a b) ⋯) - 1

Tactic:
card_cons

Goal state after:
case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ #(Ico a b) = #(Ico a b) + 1 - 1
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ #(Ioo a b) = #(cons a (Ioo a b) ⋯) - 1

Tactic:
card_cons

Goal state after:
case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ #(Ioo a b) = #(Ioo a b) + 1 - 1
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ center G
__src✝ : Group G := inst✝
x y : G
⊢ x * y = y * x

Tactic:
apply Subgroup.mem_center_iff.mp _ x

Goal state after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x ∈ center G
__src✝ : Group G := inst✝
x y : G
⊢ y ∈ center G
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝³ : Group G
inst✝² : SMul α G
inst✝¹ : SMulCommClass α G G
inst✝ : IsScalarTower α G G
a : α
ug : ConjAct G
g : G
⊢ a • ug • g = ug • a • g

Tactic:
rw [smul_def, smul_def, mul_smul_comm, smul_mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : g * h * g⁻¹ ∈ s
⊢ h ∈ s

Tactic:
convert! hh
    simpa using hg _ hh

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ closure s ≤ closure (s ^ n)

Tactic:
grw [← subset_pow hs hn]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
g : G
hg : g ∈ normalizer ↑H ∧ g ∈ normalizer ↑K
⊢ g ∈ normalizer ↑(H ⊔ K)

Tactic:
mem_normalizer_iff_map_conj_eq,

Goal state after:
G : Type u_2
inst✝ : Group G
H K : Subgroup G
g : G
hg : map (↑(MulAut.conj g)) H = H ∧ map (↑(MulAut.conj g)) K = K
⊢ map (↑(MulAut.conj g)) (H ⊔ K) = H ⊔ K
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Sort u_5
H : ι → Subgroup G
g : G
hg : ∀ (i : ι), g ∈ normalizer ↑(H i)
⊢ g ∈ normalizer ↑(⨆ i, H i)

Tactic:
mem_normalizer_iff_map_conj_eq,

Goal state after:
G : Type u_2
inst✝ : Group G
ι : Sort u_5
H : ι → Subgroup G
g : G
hg : ∀ (i : ι), map (↑(MulAut.conj g)) (H i) = H i
⊢ map (↑(MulAut.conj g)) (⨆ i, H i) = ⨆ i, H i
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_2
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ H ≤ MulAut.conj h • H

Tactic:
rw [subset_pointwise_smul_iff, ← map_inv]
    exact conj_smul_le_of_le (le_refl H) ⟨h⁻¹, H.inv_mem hh⟩

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
⊢ (map g) ((map f) x) = (map (g ∘ f)) x

Tactic:
rcases x with ⟨L⟩; simp [Function.comp_def]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ P.FG

Tactic:
use s.preimage e he.injOn

Goal state after:
case h
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ closure ↑(s.preimage ⇑e ⋯) = P
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
g : G
hg : g ∈ H₁
g₁ : G
hg₁ : g₁ ∈ H₁
g₂ : G
hg₂ : g₂ ∈ H₂
⊢ g * ⁅g₁, g₂⁆ * g⁻¹ * ⁅g, g₂⁆ ∈ ⁅H₁, H₂⁆

Tactic:
rw [← commutatorElement_mul_left_eq_conj_mul g g₁ g₂]

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
g : G
hg : g ∈ H₁
g₁ : G
hg₁ : g₁ ∈ H₁
g₂ : G
hg₂ : g₂ ∈ H₂
⊢ ⁅g * g₁, g₂⁆ ∈ ⁅H₁, H₂⁆