mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case one
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : M → Prop
hs : closure s = ⊤
x : M
one : motive 1
mul_left : ∀ x ∈ s, ∀ (y : M), motive y → motive (x * y)
⊢ motive 1

Tactic:
| one =>

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

Goal state before:
pp: case one
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : M → Prop
hs : closure s = ⊤
x : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
⊢ motive 1

Tactic:
| one =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a
⊢ argmax f (a :: (hd ++ [tl])) =
    Option.casesOn (argmax f (hd ++ [tl])) (some a) fun c ↦ if f a < f c then some c else some a

Tactic:
← cons_append,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a
⊢ argmax f (a :: hd ++ [tl]) =
    Option.casesOn (argmax f (hd ++ [tl])) (some a) fun c ↦ if f a < f c then some c else some a
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁.ndunion s₂).sup = s₁.sup ⊔ s₂.sup

Tactic:
rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]; simp

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

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).sup = s₁.sup ⊔ s₂.sup

Tactic:
rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]; simp

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
⊢ (a :: (tl ++ [hd])).maximum = max (↑a) (tl ++ [hd]).maximum

Tactic:
← cons_append,

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

Goal state before:
pp: case inl
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 : α
h : a ≤ b
⊢ f (min a b) = f a ⊓ f b

Tactic:
rw [inf_eq_left.2 h, inf_eq_left.2 (OrderHomClass.mono f h : f a ≤ f b)]

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

Goal state before:
pp: α : Type u
l : List α
⊢ (map l.get (finRange l.length)).sublists ~ (map l.get (finRange l.length)).sublists'

Tactic:
sublists_map,

Goal state after:
α : Type u
l : List α
⊢ map (map l.get) (finRange l.length).sublists ~ (map l.get (finRange l.length)).sublists'
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup γ
inst✝ : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
⊢ g (f c ⊔ t.sup f) = (g ∘ f) c ⊔ t.sup (g ∘ f)

Tactic:
g_sup,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup γ
inst✝ : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
⊢ g (f c) ⊔ g (t.sup f) = (g ∘ f) c ⊔ t.sup (g ∘ f)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
⊢ WithBot.recBotCoe True p ↑(s.sup' H f)

Tactic:
rw [coe_sup']

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
⊢ WithBot.recBotCoe True p (s.sup (WithBot.some ∘ f))
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ (a ∈ s.sup fun b ↦ {f b}) ↔ a ∈ image f s

Tactic:
rw [mem_sup, mem_image]

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
s : Finset β
f : β → α
a : α
⊢ (∃ i ∈ s, a ∈ {f i}) ↔ ∃ a_1 ∈ s, f a_1 = a
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Unique ι
s : ι → α
⊢ ⨆ i, s i = s default

Tactic:
have : ∀ i, s i = s default := fun i => congr_arg s (Unique.eq_default i)

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Unique ι
s : ι → α
this : ∀ (i : ι), s i = s default
⊢ ⨆ i, s i = s default
Module: Mathlib.Data.Set.Sigma

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
j : ι
x : α j
y : β (f i)
hys : y ∈ s
hxy : ⟨f i, y⟩ = Sigma.map f g ⟨j, x⟩
⊢ ⟨j, x⟩ ∈ Sigma.mk i '' g i ⁻¹' s

Tactic:
simp only [hf.eq_iff, Sigma.map, Sigma.ext_iff] at hxy

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
j : ι
x : α j
y : β (f i)
hys : y ∈ s
hxy : i = j ∧ y ≍ g j x
⊢ ⟨j, x⟩ ∈ Sigma.mk i '' g i ⁻¹' s
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
i : ι
x : α i
h : a i ⩿ x
⊢ a i ⩿ Function.update a i x i ∧ ∀ (j : ι), j ≠ i → a j = Function.update a i x j

Tactic:
simpa +contextual

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ a ⩿ b ↔ ∃ i x, a i ⩿ x ∧ b = Function.update a i x

Tactic:
rw [wcovBy_iff]
  constructor
  · rintro ⟨i, hi, h⟩
    exact ⟨i, b i, hi, by simpa [Function.eq_update_iff, eq_comm] using h⟩
  · rintro ⟨i, x, h, rfl⟩
    exact ⟨i, by simpa +contextual⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
x : α i
h : a i ⋖ x
⊢ a i ⋖ Function.update a i x i ∧ ∀ (j : ι), j ≠ i → a j = Function.update a i x j

Tactic:
simpa +contextual

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
i : ι
x : α i
h : x ⩿ b i
⊢ Function.update b i x i ⩿ b i ∧ ∀ (j : ι), j ≠ i → Function.update b i x j = b j

Tactic:
simpa +contextual

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
b : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
x : α i
h : x ⋖ b i
⊢ Function.update b i x i ⋖ b i ∧ ∀ (j : ι), j ≠ i → Function.update b i x j = b j

Tactic:
simpa +contextual

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

Goal state before:
pp: α : Type u
β : Type v
f : α ↪ β
s : Finset β
t : Finset α
⊢ s ⊆ map f t ↔ ∃ u ⊆ t, s = map f u

Tactic:
classical
  simp_rw [map_eq_image, subset_image_iff, eq_comm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ filter (fun x ↦ x < c) (Ico a b) = Ico a (min b c)

Tactic:
by
  rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_lt]

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Preorder α
inst✝ : WellQuasiOrderedLE α
⊢ WellFoundedLT α

Tactic:
WellFoundedLT,

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Preorder α
inst✝ : WellQuasiOrderedLE α
⊢ IsWellFounded α fun x1 x2 ↦ x1 < x2
Module: Mathlib.Order.Interval.Finset.Basic

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

Tactic:
rw [← coe_inj, coe_insert, coe_Ioc, coe_Icc, Set.insert_eq, Set.union_comm, Set.Ioc_union_left h]

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

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

Tactic:
simp [pow_mul]

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

Goal state before:
pp: case one
M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x : N
⊢ ∃ n, r ^ n • 1 ∈ closure (r • s)

Tactic:
| one =>

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
g h : M
H : IsConj g h
Hg : g ∈ Set.center M
⊢ g = h

Tactic:
by
  rcases H with ⟨u, hu⟩; rwa [← u.mul_left_inj, Hg.comm u]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g h : G
⊢ h ∈ orbit (ConjAct G) g ↔ h ∈ (ConjClasses.mk g).carrier

Tactic:
rw [ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj, mem_orbit_conjAct]

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

Goal state before:
pp: case refine_2.refine_1
G : Type u_1
inst✝ : Group G
h g : G
hh : h ∈ centralizer {g}
⊢ h * g * h⁻¹ ∈ {g}

Tactic:
exact (eq_mul_inv_of_mul_eq <| hh g rfl).symm

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : {x | x ∈ ↑l}.Pairwise fun x y ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ noncommFoldr f (↑l) comm b = List.foldr f b l

Tactic:
simp only [noncommFoldr, coe_foldr, coe_attach, List.attach, List.attachWith, Function.comp_def]

Goal state after:
α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : {x | x ∈ ↑l}.Pairwise fun x y ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ List.foldr (fun x ↦ f ↑x) b (List.pmap Subtype.mk l ⋯) = List.foldr f b l
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case one
G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
x : G
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x * y) ⋯
inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x⁻¹ * y) ⋯
⊢ p 1 ⋯

Tactic:
| one =>

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

Goal state before:
pp: case one
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
⊢ C 1

Tactic:
| one =>

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

Goal state before:
pp: case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a * hd * tl.prod = hd * a * tl.prod

Tactic:
congr 1

Goal state after:
case h.cons.e_a
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a * hd = hd * a
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

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

Tactic:
simp [pow_mul]

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

Goal state before:
pp: case one
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x : G
⊢ 1 ∈ ↑H * ↑N

Tactic:
| one =>

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

Goal state before:
pp: case one
G : Type u_2
inst✝¹ : Group G
X : Type u_5
inst✝ : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g : G
x : X
hx : x ∈ t
⊢ 1 • x ∈ t

Tactic:
| one =>

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t
hfg : ∀ i ∈ s, f i = g (e i)
⊢ ∏ i ∈ s, f i = ∏ i ∈ t, g i

Tactic:
by refine prod_nbij' e e.symm ?_ ?_ ?_ ?_ hfg <;> simp [hst]

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

Goal state before:
pp: case one
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
⊢ ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = 1

Tactic:
| one =>

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

Goal state before:
pp: case mul
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ (∏ x ∈ t ∪ u, x ^ f x) * ∏ x ∈ t ∪ u, x ^ g x = (∏ x ∈ t, x ^ f x) * ∏ x ∈ u, x ^ g x

Tactic:
congr 1

Goal state after:
case mul.e_a
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∏ x ∈ t ∪ u, x ^ f x = ∏ x ∈ t, x ^ f x

case mul.e_a
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∏ x ∈ t ∪ u, x ^ g x = ∏ x ∈ u, x ^ g x
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c d : Con M
H : ∀ (x y : M), c x y ↔ d x y
⊢ ⇑c = ⇑d

Tactic:
by ext; apply H

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι → κ
he : Set.InjOn e ↑s
hest : Set.MapsTo e ↑s ↑t
h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ ∀ x ∈ t, x ∉ image e s → g x = 1

Tactic:
by simpa using h'

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f g : c.Quotient →* P
h : f.comp c.mk' = g.comp c.mk'
⊢ c.lift (f.comp c.mk') ⋯ = c.lift (g.comp c.mk') ⋯

Tactic:
congr 1

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

Goal state before:
pp: case add
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x y : FreeAddGroup α
hx : (fun x ↦ x • FreeAddGroup.of default) ((fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) x) = x
hy : (fun x ↦ x • FreeAddGroup.of default) ((fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) y) = y
⊢ (fun x ↦ x • FreeAddGroup.of default) ((fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) (x + y)) = x + y

Tactic:
| add x y hx hy =>

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
h : P.FG
e : M →* M'
⊢ (Submonoid.map e P).FG

Tactic:
classical
    obtain ⟨s, rfl⟩ := h
    exact ⟨s.image e, by rw [Finset.coe_image, MonoidHom.map_mclosure]⟩

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x s =
    f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s)

Tactic:
congr 1

Goal state after:
case pos.e_a
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ ∏ x ∈ s.toFinset.erase a, f x ^ count x s = ∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s)
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
⊢ Injective ⇑(lift N φ HN) ↔ N = φ.ker

Tactic:
rw [← MonoidHom.ker_eq_bot_iff, QuotientGroup.ker_lift, Subgroup.map_eq_bot_iff]
  grind [QuotientGroup.ker_mk']

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
inst✝ : AddCommGroup G
f g : α → G
x y : FreeAbelianGroup α
hx : (lift (f + g)) x = (lift f) x + (lift g) x
hy : (lift (f + g)) y = (lift f) y + (lift g) y
⊢ (lift (f + g)) (x + y) = (lift f) (x + y) + (lift g) (x + y)

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : Fintype κ
inst✝ : CommMonoid M
e : ι → κ
he : Injective e
f : ι → M
g : κ → M
h' : ∀ i ∉ Set.range e, g i = 1
h : ∀ (i : ι), f i = g (e i)
⊢ ∀ i ∈ univ, i ∉ e '' ↑univ → g i = 1

Tactic:
by simpa using h'

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case zero
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
⊢ Prod.mk <$> 0 <*> y = (fun b a ↦ (a, b)) <$> y <*> 0

Tactic:
FreeAbelianGroup.map_zero,

Goal state after:
case zero
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
⊢ 0 <*> y = (fun b a ↦ (a, b)) <$> y <*> 0
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.zero
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
⊢ Prod.mk p <$> 0 = (fun b a ↦ (a, b)) <$> 0 <*> pure p

Tactic:
FreeAbelianGroup.map_zero,

Goal state after:
case pure.zero
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
⊢ 0 = (fun b a ↦ (a, b)) <$> 0 <*> pure p
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.zero
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
⊢ 0 = (fun b a ↦ (a, b)) <$> 0 <*> pure p

Tactic:
FreeAbelianGroup.map_zero,

Goal state after:
case pure.zero
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
⊢ 0 = 0 <*> pure p
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆

Tactic:
simp_rw [le_antisymm_iff, map_le_iff_le_comap, commutator_le, mem_comap, map_commutatorElement]
  constructor
  · intro p hp q hq
    exact commutator_mem_commutator (mem_map_of_mem _ hp) (mem_map_of_mem _ hq)
  · rintro _ ⟨p, hp, rfl⟩ _ ⟨q, hq, rfl⟩
    rw [← map_commutatorElement]
    exact mem_map_of_mem _ (commutator_mem_commutator hp hq)

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G) = commutatorSet G

Tactic:
by
  apply Set.Subset.antisymm
  · rintro - ⟨-, ⟨g₁, g₂, rfl⟩, rfl⟩
    exact ⟨g₁, g₂, rfl⟩
  · exact fun g hg ↦
      ⟨_, ⟨⟨_, subset_closure <| .inl ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩⟩,
          ⟨_, subset_closure <| .inr ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩⟩, rfl⟩,
        hg.choose_spec.choose_spec⟩

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
L2 L1 : α
ih : (lift ⇑f) (of L1 * of L2) = (lift ⇑f) (of L1) * (lift ⇑f) (of L2)
⊢ -(lift ⇑f) (of L1 * of L2) = -((lift ⇑f) (of L1) * (lift ⇑f) (of L2))

Tactic:
exact congr_arg Neg.neg ih

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case zero
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
y : FreeAbelianGroup α
⊢ 0 * y = y * 0

Tactic:
exact zero_mul y

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
⊢ of (Mul.mul s t) = of (Mul.mul t s)

Tactic:
congr 1

Goal state after:
case of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s t : α
⊢ Mul.mul s t = Mul.mul t s
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ t' • (r₁ * r * r₂) /ₒ (t' * s) = t' • (r₁ * r' * r₂) /ₒ (t' * s)

Tactic:
congr 1

Goal state after:
case e_r
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ t' • (r₁ * r * r₂) = t' • (r₁ * r' * r₂)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : N
⊢ g (f.sec (x * y)).1 * g ↑(f.sec y).2 =
    g (f.sec y).1 * (g ↑(f.sec (x * y)).2 * (g (f.sec x).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec x).2)⁻¹))

Tactic:
←
      mul_assoc,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : N
⊢ g (f.sec (x * y)).1 * g ↑(f.sec y).2 =
    g (f.sec y).1 * g ↑(f.sec (x * y)).2 * (g (f.sec x).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec x).2)⁻¹)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this✝ : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
this : ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S
⊢ (↑s₄' * (r₃' * (r₂' * r₂))) • r₁ /ₒ (s₄' * (s₃' * (s₁' * s))) =
    (↑s₄' * (r₃' * (r₂' * r₂))) • r₁ /ₒ ⟨↑s₄' * (r₃' * (↑s₂' * ↑s)), ⋯⟩

Tactic:
congr 1

Goal state after:
case e_s
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this✝ : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
this : ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S
⊢ s₄' * (s₃' * (s₁' * s)) = ⟨↑s₄' * (r₃' * (↑s₂' * ↑s)), ⋯⟩