mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ map f (normalClosure s) = normalClosure (⇑f '' s)

Tactic:
apply le_antisymm

Goal state after:
case a
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ map f (normalClosure s) ≤ normalClosure (⇑f '' s)

case a
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ normalClosure (⇑f '' s) ≤ map f (normalClosure s)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ max (map f l).prod (map g l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod

Tactic:
rw [max_le_iff]
  constructor <;> apply List.prod_le_prod' <;> intros
  · apply le_max_left
  · apply le_max_right

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

Goal state before:
pp: case neg
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : ¬l = []
hla_restrict : ∀ (x : α), x ∈ l → p x
hp_sup : p l.prod
hp_a : p a
⊢ f a * f l.prod ≤ f a * (map f l).prod

Tactic:
← ih hl_empty hla_restrict

Goal state after:
case neg
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : ¬l = []
hla_restrict : ∀ (x : α), x ∈ l → p x
hp_sup : p l.prod
hp_a : p a
⊢ f a * f l.prod ≤ f a * f l.prod
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ toFunAux (ofNat s 0) = 0

Tactic:
toFunAux_eq,

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ #({y ∈ range ↑(ofNat s 0) | y ∈ s}) = 0
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: case H.inl
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : image f s = ∅
⊢ motive s

pp: case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
⊢ motive s

Tactic:
· simp only [image_eq_empty] at hne
    simp only [hne, empty]

Goal state after:
case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
⊢ motive s
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ (powersetCard n.succ u).sup id = u

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ (powersetCard n.succ u).sup id ⊆ u

case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ u ⊆ (powersetCard n.succ u).sup id
Module: Mathlib.Order.Cover

Goal state before:
pp: case inl
α : Type u_1
inst✝ : PartialOrder α
b c : α
h : c ⩿ b
⊢ c ≤ c ∧ c ≤ b

pp: case inr
α : Type u_1
inst✝ : PartialOrder α
a c : α
h : a ⩿ c
⊢ a ≤ c ∧ c ≤ c

Tactic:
exacts [⟨le_rfl, h.le⟩, ⟨h.le, le_rfl⟩]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : (a₁, b) < c
h₂ : c < (a₂, b)
this : c.2 = b
⊢ False

Tactic:
← @Prod.mk.eta _ _ c,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : (a₁, b) < (c.1, c.2)
h₂ : (c.1, c.2) < (a₂, b)
this : c.2 = b
⊢ False
Module: Mathlib.Order.Cover

Goal state before:
pp: case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
i : ι
hab : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
c : (i : ι) → α i
hac : a < c
hcb : c < b
⊢ False

Tactic:
have haci : a i < c i := by
    obtain ⟨hac, j, hj⟩ := Pi.lt_def.1 hac
    exact (eq_or_ne j i).elim (· ▸ hj) fun hj' ↦
      ((lt_of_antisymmRel_of_lt (h j hj').symm hj).not_ge (hcb.le j)).elim

Goal state after:
case mpr
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
i : ι
hab : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
c : (i : ι) → α i
hac : a < c
hcb : c < b
haci : a i < c i
⊢ False
Module: Mathlib.Order.Cover

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

Tactic:
by
  rw [covBy_iff]
  constructor
  · rintro ⟨i, hi, h⟩
    exact ⟨i, a 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.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
inst✝ : LE α
x : Subtype Q
⊢ Minimal (fun x ↦ P ↑x) x ↔ Minimal (P ⊓ Q) ↑x

Tactic:
obtain ⟨x, hx⟩ := x

Goal state after:
α : Type u_2
P Q : α → Prop
inst✝ : LE α
x : α
hx : Q x
⊢ Minimal (fun x ↦ P ↑x) ⟨x, hx⟩ ↔ Minimal (P ⊓ Q) ↑⟨x, hx⟩
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : α → Prop
inst✝ : LE α
x : Subtype P
⊢ Minimal (fun x ↦ True) x ↔ Minimal P ↑x

Tactic:
obtain ⟨x, hx⟩ := x

Goal state after:
α : Type u_2
P : α → Prop
inst✝ : LE α
x : α
hx : P x
⊢ Minimal (fun x ↦ True) ⟨x, hx⟩ ↔ Minimal P ↑⟨x, hx⟩
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α ↪o β
h : Set.range ⇑f = Set.range ⇑g
ef : ↑Set.univ ≃o ↑(⇑f '' Set.univ) := StrictMonoOn.orderIso (⇑f) Set.univ ⋯
eg : ↑Set.univ ≃o ↑(⇑g '' Set.univ) := StrictMonoOn.orderIso (⇑g) Set.univ ⋯
i : ↑(⇑f '' Set.univ) ≃o ↑(⇑g '' Set.univ) :=
  let __spread.0 := Equiv.setCongr ⋯;
  { toEquiv := __spread.0, map_rel_iff' := ⋯ }
⊢ f = g

Tactic:
have : (ef.trans i).trans eg.symm = .refl _ := by
    exact Subsingleton.elim _ _

Goal state after:
α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α ↪o β
h : Set.range ⇑f = Set.range ⇑g
ef : ↑Set.univ ≃o ↑(⇑f '' Set.univ) := StrictMonoOn.orderIso (⇑f) Set.univ ⋯
eg : ↑Set.univ ≃o ↑(⇑g '' Set.univ) := StrictMonoOn.orderIso (⇑g) Set.univ ⋯
i : ↑(⇑f '' Set.univ) ≃o ↑(⇑g '' Set.univ) :=
  let __spread.0 := Equiv.setCongr ⋯;
  { toEquiv := __spread.0, map_rel_iff' := ⋯ }
this : (ef.trans i).trans eg.symm = OrderIso.refl ↑Set.univ
⊢ f = g
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 ↦ x1 > x2) ↪r r
k : ℕ
⊢ Nonempty { f_1 // f k ∈ Set.range ⇑f_1 }

Tactic:
exact ⟨⟨f, k, rfl⟩⟩

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: s : Set ℕ
inst✝ : Infinite ↑s
dP : DecidablePred fun x ↦ x ∈ s
n : ℕ
⊢ ofNat s n = ofNat s n

Tactic:
congr!

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

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

Tactic:
by
  rw [← coe_eq_empty, coe_Icc, Set.Icc_eq_empty_iff]

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : a₁ < a₂
⊢ Set.Ico a₂ b ⊆ ↑(Ioo a₁ b)

Tactic:
coe_Ioo

Goal state after:
α : Type u_2
a₁ a₂ b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : a₁ < a₂
⊢ Set.Ico a₂ b ⊆ Set.Ioo a₁ b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Set.Ioc a b₁ ⊆ ↑(Ioo a b₂)

Tactic:
coe_Ioo

Goal state after:
α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Set.Ioc a b₁ ⊆ Set.Ioo a b₂
Module: Mathlib.Order.Interval.Finset.Defs

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

Tactic:
by
  rw [subtype_Ioc_eq]
  refine Finset.subtype_map_of_mem fun x hx => ?_
  rw [mem_Ioc] at hx
  exact hp hx.1.le hx.2 a.prop b.prop

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ Iio a ⊆ Iic a

Tactic:
simpa [← coe_subset] using Set.Iio_subset_Iic_self

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
⊢ s.Finite

Tactic:
by
  by_contra! hi
  obtain ⟨m, n, hmn, h⟩ := hp (hi.natEmbedding _)
  exact hmn.ne ((hi.natEmbedding _).injective <| Subtype.val_injective <|
    ha.eq (hi.natEmbedding _ m).2 (hi.natEmbedding _ n).2 h)

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ = (closure s)⁻¹

Tactic:
apply le_antisymm

Goal state after:
case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ ≤ (closure s)⁻¹

case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ (closure s)⁻¹ ≤ closure s⁻¹
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
disjoint_iff_inter_eq_empty,

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a₁ a₂ ∩ Ioc b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
r : α → α → Prop
s : Finset ι
f : ι → Set α
⊢ (⋃ i ∈ s, f i).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r

Tactic:
simpa only [Finset.sup_eq_iSup] using! s.partiallyWellOrderedOn_sup

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
s : Set α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ BddBelow s → s.WellFoundedOn fun x1 x2 ↦ x1 < x2

Tactic:
by
  rw [wellFoundedOn_iff_no_descending_seq]
  rintro ⟨a, ha⟩ f hf
  refine infinite_range_of_injective f.injective ?_
  exact (finite_Icc a <| f 0).subset <| range_subset_iff.2 <| fun n =>
    ⟨ha <| hf _,
      antitone_iff_forall_lt.2 (fun a b hab => (f.map_rel_iff.2 hab).le) <| Nat.zero_le _⟩

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
m n : ℕ
mn : m < n
⊢ ¬r (↑(fs n) m) (↑(fs n) n)

Tactic:
exact (fs n).2.1.2 m n mn

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
z : M
h : IsMulCentral z
a c : M
⊢ a * z * c = a * (z * c)

Tactic:
by
  rw [h.comm, ← h.right_assoc, ← h.comm, ← h.left_assoc, h.comm]

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]
  rw [← List.foldr_map]
  simp [List.map_pmap]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
σ : Equiv.Perm ι
s : Finset ι
f : ι → ι → M
hs : {a | σ a ≠ a} ⊆ ↑s
⊢ ∏ x ∈ s, f (σ x) x = ∏ x ∈ s, f x ((Equiv.symm σ) x)

Tactic:
by
  convert! σ.prod_comp s (fun x => f x (σ.symm x)) hs
  rw [Equiv.symm_apply_apply]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ ConjAct.toConjAct g • H = H ↔ g ∈ normalizer ↑H

Tactic:
rw [← (normalizer H : Subgroup G).inv_mem_iff]

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
g : G
⊢ ConjAct.toConjAct g • H = H ↔ g⁻¹ ∈ normalizer ↑H
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case mk.mk
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
f : α → β
val✝¹ : Multiset α
sl : List α
hsl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid α)) sl)
val✝ : Multiset α
tl : List α
htl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid α)) tl)
comm :
  (↑({ val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl } ∪
          { val := Quot.mk (⇑(List.isSetoid α)) tl, nodup := htl })).Pairwise
    (Commute on f)
h : Disjoint ↑sl ↑tl
⊢ ({ val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl } ∪
          { val := Quot.mk (⇑(List.isSetoid α)) tl, nodup := htl }).noncommProd
      f comm =
    { val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl }.noncommProd f ⋯ *
      { val := Quot.mk (⇑(List.isSetoid α)) tl, nodup := htl }.noncommProd f ⋯

Tactic:
simp [noncommProd, ← Multiset.add_eq_union_iff_disjoint.mpr h]

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

Goal state before:
pp: case cons
α : Type u_3
β : Type u_4
inst✝ : Monoid β
f g : α → β
x : α
s : Finset α
hnotMem : x ∉ s
ih :
  ∀ (comm_ff : (↑s).Pairwise (Commute on f)) (comm_gg : (↑s).Pairwise (Commute on g))
    (comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnotMem)).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnotMem)).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnotMem)).Pairwise fun x y ↦ Commute (g x) (f y)
⊢ f x * g x * (s.noncommProd f ⋯ * s.noncommProd g ⋯) = f x * s.noncommProd f ⋯ * (g x * s.noncommProd g ⋯)

Tactic:
(noncommProd_commute _ _ _ _ fun y hy => ?_).mul_mul_mul_comm

Goal state after:
case cons
α : Type u_3
β : Type u_4
inst✝ : Monoid β
f g : α → β
x : α
s : Finset α
hnotMem : x ∉ s
ih :
  ∀ (comm_ff : (↑s).Pairwise (Commute on f)) (comm_gg : (↑s).Pairwise (Commute on g))
    (comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnotMem)).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnotMem)).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnotMem)).Pairwise fun x y ↦ Commute (g x) (f y)
⊢ f x * s.noncommProd f ⋯ * (g x * s.noncommProd g ⋯) = f x * s.noncommProd f ⋯ * (g x * s.noncommProd g ⋯)

α : Type u_3
β : Type u_4
inst✝ : Monoid β
f g : α → β
x : α
s : Finset α
hnotMem : x ∉ s
ih :
  ∀ (comm_ff : (↑s).Pairwise (Commute on f)) (comm_gg : (↑s).Pairwise (Commute on g))
    (comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnotMem)).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnotMem)).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnotMem)).Pairwise fun x y ↦ Commute (g x) (f y)
y : α
hy : y ∈ s
⊢ Commute (g x) (f y)
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
s : Set (Setoid α)
⊢ (EqvGen.setoid fun x y ↦ ∃ r ∈ s, r x y) = EqvGen.setoid (⨆ a ∈ s, ⇑a)

Tactic:
congr with (x y)

Goal state after:
α : Type u_1
s : Set (Setoid α)
x y : α
⊢ (∃ r ∈ s, r x y) ↔ (⨆ a ∈ s, ⇑a) x y
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case mk
M : Type u_1
inst✝ : Mul M
d : Con M
toSetoid✝ : Setoid M
mul'✝ : ∀ {w x y z : M}, toSetoid✝ w x → toSetoid✝ y z → toSetoid✝ (w * y) (x * z)
⊢ { toSetoid := toSetoid✝, mul' := mul'✝ }.toSetoid = d.toSetoid → { toSetoid := toSetoid✝, mul' := mul'✝ } = d

Tactic:
congr!

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

Goal state before:
pp: case mpr
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
s t : { d // c ≤ d }
⊢ s ≤ t →
    { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        s ≤
      { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        t

Tactic:
· exact Relation.map_mono

Goal state after:
Module: Mathlib.GroupTheory.Coset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x ↦ x ∈ s
x y : α
⊢ Decidable ((leftRel s) x y)

Tactic:
rw [leftRel_eq]

Goal state after:
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x ↦ x ∈ s
x y : α
⊢ Decidable ((fun x y ↦ x⁻¹ * y ∈ s) x y)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
x✝ : α
⊢ (fun g ↦ ⇑g ∘ of) ((fun f ↦ MonoidHom.mk' (Quot.lift (Lift.aux f) ⋯) ⋯) f) x✝ = f x✝

Tactic:
simp [of, Lift.aux]

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
g : FreeGroup α →* β
a✝ : α
⊢ ((fun f ↦ MonoidHom.mk' (Quot.lift (Lift.aux f) ⋯) ⋯) ((fun g ↦ ⇑g ∘ of) g)) (of a✝) = g (of a✝)

Tactic:
simp [of, Lift.aux]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
⊢ Subgroup.closure (Set.range f) ≤ (lift f).range

Tactic:
Subgroup.closure_le

Goal state after:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
⊢ Set.range f ⊆ ↑(lift f).range
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Subgroup.closure (Set.range (of ∘ f)) = Subgroup.closure (of '' Set.range f)

Tactic:
Set.range_comp

Goal state after:
α : Type u
β : Type v
f : α → β
⊢ Subgroup.closure (of '' Set.range f) = Subgroup.closure (of '' Set.range f)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
F : Fintype ↥s
h : ∀ (x : ι), x ∈ s ↔ (fun x ↦ x ∈ s) x
⊢ ∏ i, f ↑i = ∏ a, f ↑a

Tactic:
congr!

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

Goal state before:
pp: M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq M
m : List M
s : Finset M
hs : m.toFinset ⊆ s
⊢ m.prod = ∏ i ∈ s, i ^ count i m

Tactic:
prod_list_count

Goal state after:
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq M
m : List M
s : Finset M
hs : m.toFinset ⊆ s
⊢ ∏ m_1 ∈ m.toFinset, m_1 ^ count m_1 m = ∏ i ∈ s, i ^ count i m
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
⊢ FG M ↔ ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ

Tactic:
by
  constructor
  · rw [fg_iff_exists_freeMonoid_hom_surjective]
    intro ⟨S, hS, φ, hφ⟩
    obtain ⟨n, ⟨e⟩⟩ := hS.exists_equiv_fin S
    exact ⟨Fin n, inferInstance, φ.comp (FreeMonoid.freeMonoidCongr e).symm,
      hφ.comp (FreeMonoid.freeMonoidCongr e).symm.surjective⟩
  · intro ⟨α, _, φ, hφ⟩
    exact Monoid.fg_of_surjective _ hφ

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M✝ : Type u_4
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : Monoid M✝
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst✝ : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
⊢ G ⧸ N →* H ⧸ M

Tactic:
refine QuotientGroup.lift N ((mk' M).comp f) ?_
  intro x hx
  refine QuotientGroup.eq.2 ?_
  rw [mul_one, Subgroup.inv_mem_iff]
  exact h hx

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
G' : Type u_5
inst✝ : Group G'
P : Subgroup G
Q : Subgroup G'
hP : P.FG
hQ : Q.FG
⊢ (P.prod Q).FG

Tactic:
rw [fg_iff_submonoid_fg] at *
  exact hP.prod hQ

Goal state after:
Module: Mathlib.GroupTheory.Abelianization.Defs

Goal state before:
pp: G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
⊢ Subgroup.closure (commutatorSet G) ≤ f.ker

Tactic:
Subgroup.closure_le

Goal state after:
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
⊢ commutatorSet G ⊆ ↑f.ker
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
K₁ K₂ : Subgroup G'
⊢ ⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆

Tactic:
apply le_antisymm

Goal state after:
case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁.prod K₁, H₂.prod K₂⁆ ≤ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆

case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ⁅⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆, ⊤⁆ = ⊥

Tactic:
suffices ⁅⁅⊤, centralizer (commutator G : Set G)⁆, centralizer (commutator G : Set G)⁆ = ⊥ by
    refine Subgroup.commutator_commutator_eq_bot_of_rotate ?_ this
    rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
z : N
H : z * f ↑y = f x
⊢ z = f.mk' x y

Tactic:
by rwa [mk', mul_inv_right]

Goal state after:
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
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f).symm (f.mk' x y) = mk x y

Tactic:
by
  rw [mk_eq_monoidOf_mk'_apply]; exact mulEquivOfQuotient_symm_mk' _ _

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a < b
hb : pred b = b
⊢ ∃ n, pred^[n] b = a

Tactic:
cases (min_of_le_pred hb.ge).not_lt hab

Goal state after: