mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Powerset

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

Tactic:
simp_rw [Finset.sup_le_iff, mem_powersetCard]

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ ∀ (b : Finset α), b ⊆ u ∧ #b = n.succ → id b ⊆ u
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case insert
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs : (insert a s).Nonempty
⊢ (insert a s).sup f ∈ f '' ↑(insert a s)

Tactic:
| insert a s _ h =>

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ s.sup' H f < a ↔ ∀ i ∈ s, f i < a

Tactic:
rw [← WithBot.coe_lt_coe, coe_sup', Finset.sup_lt_iff (WithBot.bot_lt_coe a)]

Goal state after:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∀ b ∈ s, (WithBot.some ∘ f) b < ↑a) ↔ ∀ i ∈ s, f i < a
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : ¬p
⊢ sSup (range fun h ↦ f h) = sSup ∅

Tactic:
congr

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompletePartialOrderSup α
p : Prop
f : p → α
hp : ¬p
⊢ (range fun h ↦ f h) = ∅
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ sSup (range fun i ↦ f ⟨i, ⋯⟩) = sSup (range f)

Tactic:
congr

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ (range fun i ↦ f ⟨i, ⋯⟩) = range f
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : ConditionallyCompletePartialOrderSup α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
⊢ ⨆ n, f n ∈ ⋂ n, Icc (f n) (g n)

Tactic:
by
  refine mem_iInter.2 fun n => ?_
  have : Nonempty β := ⟨n⟩
  have h₁ : ∀ m, f m ≤ g n := fun m => hf.forall_le_of_antitone hg h m n
  have h₂ : Directed (· ≤ ·) f := hf.directed_le
  exact ⟨h₂.le_ciSup ⟨g <| n, forall_mem_range.2 h₁⟩ _, h₂.ciSup_le h₁⟩

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
⊢ (image (fun i ↦ OrderDual.toDual (f i)) s).max' ⋯ = (image (⇑OrderDual.toDual ∘ f) s).max' ⋯

Tactic:
congr

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

Goal state before:
pp: α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝⁴ : CompleteLattice α
inst✝³ : CompleteLattice β
inst✝² : FunLike F α β
inst✝¹ : SupBotHomClass F α β
inst✝ : Finite ι
f : F
g : ι → α
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
← iSup_univ (f := g),

Goal state after:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝⁴ : CompleteLattice α
inst✝³ : CompleteLattice β
inst✝² : FunLike F α β
inst✝¹ : SupBotHomClass F α β
inst✝ : Finite ι
f : F
g : ι → α
⊢ f (⨆ x ∈ univ, g x) = ⨆ i, f (g i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, f x ≤ sInf ∅
⊢ ⨅ x ∈ l, f x ∈ map f l

Tactic:
simpa using l.toFinset.ciInf_mem_image f (by simpa using h)

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case mpr
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
n : α
this : OrderBot α
⊢ ((∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i) → ⨅ i, f i = n

Tactic:
· rintro ⟨⟨i, rfl⟩, h⟩
    exact le_antisymm (ciInf_le (OrderBot.bddBelow ..) _) (le_ciInf h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Nonempty α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' ↑s) ↑s
hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' ↑s)) x = id x
⊢ (s.preimage f ⋯).sup f = (image (invFunOn f (f ⁻¹' ↑s)) s).sup f

Tactic:
congr

Goal state after:
case e_s
α : Type u_1
β : Type u_2
inst✝² : Nonempty α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
s : Finset β
f : α → β
hf : BijOn f (f ⁻¹' ↑s) ↑s
hfinvs : ∀ x ∈ s, (f ∘ invFunOn f (f ⁻¹' ↑s)) x = id x
⊢ s.preimage f ⋯ = image (invFunOn f (f ⁻¹' ↑s)) s
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)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ sigmaLift f a b = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅

Tactic:
simp_rw [sigmaLift]
  split_ifs with h
  · simp [h]
  · simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ {x ∈ Finset.Ico a b | c ≤ x}.val = (Finset.Ico (max a c) b).val

Tactic:
Finset.Ico_filter_le

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ (Finset.Ico (max a c) b).val = (Finset.Ico (max a c) b).val
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
hIoi : h₀_finset_Ioi = h₁_finset_Ioi
⊢ { finsetIoi := h₀_finset_Ioi, finsetIci := h₀_finset_Ici, finset_mem_Ici := h₀_finset_mem_Ici,
      finset_mem_Ioi := h₀_finset_mem_Ioi } =
    { finsetIoi := h₁_finset_Ioi, finsetIci := h₁_finset_Ici, finset_mem_Ici := h₁_finset_mem_Ici,
      finset_mem_Ioi := h₁_finset_mem_Ioi }

Tactic:
hIci,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
hIoi : h₀_finset_Ioi = h₁_finset_Ioi
⊢ { finsetIoi := h₀_finset_Ioi, finsetIci := h₁_finset_Ici, finset_mem_Ici := ⋯, finset_mem_Ioi := h₀_finset_mem_Ioi } =
    { finsetIoi := h₁_finset_Ioi, finsetIci := h₁_finset_Ici, finset_mem_Ici := h₁_finset_mem_Ici,
      finset_mem_Ioi := h₁_finset_mem_Ioi }
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
⊢ ∀ {x y z : α}, x ∈ orbit G y → y ∈ orbit G z → x ∈ orbit G z

Tactic:
grind [orbit_eq_iff]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
⊢ Quotient.mk' ⁻¹' Quotient.mk' '' U = ⋃ g, (fun x ↦ g • x) '' U

Tactic:
let := orbitRel G α
  set f : α → Quotient (MulAction.orbitRel G α) := Quotient.mk'
  ext a
  constructor
  · rintro ⟨b, hb, hab⟩
    obtain ⟨g, rfl⟩ := Quotient.exact hab
    rw [Set.mem_iUnion]
    exact ⟨g⁻¹, g • a, hb, inv_smul_smul g a⟩
  · intro hx
    rw [Set.mem_iUnion] at hx
    obtain ⟨g, u, hu₁, hu₂⟩ := hx
    rw [Set.mem_preimage, Set.mem_image]
    refine ⟨g⁻¹ • a, ?_, by simp +instances [f, orbitRel, Quotient.eq']⟩
    rw [← hu₂]
    convert! hu₁
    simp only [inv_smul_smul]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
⊢ ∀ ⦃a₂ : Quotient G α⦄, x.orbit = a₂.orbit → x = a₂

Tactic:
y

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x y : Quotient G α
⊢ x.orbit = y.orbit → x = y
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
G' : Type u_4
inst✝³ : Group G'
inst✝² : SMul α β
inst✝¹ : MulAction G' β
inst✝ : SMulCommClass G' α β
a : α
b : β
⊢ stabilizer G' b ≤ stabilizer G' (a • b)

Tactic:
by
  simp_rw [SetLike.le_def, mem_stabilizer_iff, smul_comm]; rintro a h; rw [h]

Goal state after:
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 : G
⊢ ∀ (b : G), x * b = b * x

Tactic:
y

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
x : G
hx : x ∈ center G
⊢ x ∈ normalizer s

Tactic:
y

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
x : G
hx : x ∈ center G
y : G
⊢ y ∈ s ↔ x * y * x⁻¹ ∈ s
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 : G
hx : x ∈ (ConjClasses.mk g).carrier
⊢ ∀ ⦃y : G⦄, y ∈ (ConjClasses.mk g).carrier → x = y

Tactic:
y

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
x : G
hx : x ∈ (ConjClasses.mk g).carrier
y : G
⊢ y ∈ (ConjClasses.mk g).carrier → x = y
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g h : G
⊢ (orbitRel (ConjAct G) G) g h = IsConj g h

Tactic:
by rw [orbitRel_apply, mem_orbit_conjAct]

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

Goal state before:
pp: case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 ↦ x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
x : α
hx : x ∈ {x | x ∈ ↑tl}
⊢ ∀ ⦃y : α⦄, y ∈ {x | x ∈ ↑tl} → x ≠ y → Commute x y

Tactic:
y

Goal state after:
case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 ↦ x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
x : α
hx : x ∈ {x | x ∈ ↑tl}
y : α
⊢ y ∈ {x | x ∈ ↑tl} → x ≠ y → Commute x y
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
x : α
hx : x ∈ {x | x ∈ a ::ₘ ⟦tl⟧}
⊢ ∀ ⦃y : α⦄, y ∈ {x | x ∈ a ::ₘ ⟦tl⟧} → x ≠ y → Commute x y

Tactic:
y

Goal state after:
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
x : α
hx : x ∈ {x | x ∈ a ::ₘ ⟦tl⟧}
y : α
⊢ y ∈ {x | x ∈ a ::ₘ ⟦tl⟧} → x ≠ y → Commute x y
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mp
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hyA : y ∈ ↑A
hyB : y ∈ ↑B
z : G
hz : z ∈ ↑C
⊢ ∃ x ∈ ↑B, ∃ y_1 ∈ ↑C, x * y_1 = y * z

Tactic:
exact ⟨y, hyB, z, hz, rfl⟩

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

Goal state before:
pp: case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm' : ∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
x : α
hx : x ∈ l
⊢ ∀ y ∈ l, x * y = y * x

Tactic:
y

Goal state after:
case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm' : ∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
x : α
hx : x ∈ l
y : α
⊢ y ∈ l → x * y = y * x
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
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)
x : α
hx : x ∈ ↑s
⊢ ∀ ⦃y : α⦄, y ∈ ↑s → x ≠ y → (fun x y ↦ Commute ((f * g) x) ((f * g) y)) x y

Tactic:
y

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
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)
x : α
hx : x ∈ ↑s
y : α
⊢ y ∈ ↑s → x ≠ y → (fun x y ↦ Commute ((f * g) x) ((f * g) y)) x y
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)
⊢ (cons x s hnotMem).noncommProd (f * g) ⋯ =
    (cons x s hnotMem).noncommProd f comm_ff * (cons x s hnotMem).noncommProd g comm_gg

Tactic:
Finset.noncommProd_cons,

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 * g) x * s.noncommProd (f * g) ⋯ =
    (cons x s hnotMem).noncommProd f comm_ff * (cons x s hnotMem).noncommProd g comm_gg
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 * g) x * s.noncommProd (f * g) ⋯ =
    (cons x s hnotMem).noncommProd f comm_ff * (cons x s hnotMem).noncommProd g comm_gg

Tactic:
Finset.noncommProd_cons,

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 * g) x * s.noncommProd (f * g) ⋯ = f x * s.noncommProd f ⋯ * (cons x s hnotMem).noncommProd g comm_gg
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 * g) x * s.noncommProd (f * g) ⋯ = f x * s.noncommProd f ⋯ * (cons x s hnotMem).noncommProd g comm_gg

Tactic:
Finset.noncommProd_cons,

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 * g) x * s.noncommProd (f * g) ⋯ = f x * s.noncommProd f ⋯ * (g x * s.noncommProd g ⋯)
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
q : Quotient (r.prod s)
x y : α × β
hxy : (r.prod s) x y
⊢ (Quotient.mk'' x.1, Quotient.mk'' x.2).1 = (Quotient.mk'' y.1, Quotient.mk'' y.2).1

Tactic:
by simpa [Quotient.eq] using hxy.1

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x✝ : Quotient r
x : α
⊢ (g ∘ Quotient.mk'') x = g ⟦x⟧

Tactic:
Function.comp_apply,

Goal state after:
case mk
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
x✝ : Quotient r
x : α
⊢ g (Quotient.mk'' x) = g ⟦x⟧
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : a ∉ s → f a = 1
⊢ ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x

Tactic:
by_cases a ∈ s <;> grind

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
f : ι → M
s : Finset κ
t : κ → Finset ι
h : (↑s).PairwiseDisjoint t
⊢ Multiset.foldr (fun x1 x2 ↦ x1 * x2) 1 (Multiset.map (fun x ↦ f x) (s.val.bind fun a ↦ (t a).val)) =
    Multiset.foldr (fun x1 x2 ↦ x1 * x2) (Multiset.foldr (fun x1 x2 ↦ x1 * x2) 1 (Multiset.map (fun i ↦ 1) s.val))
      (Multiset.map (fun x ↦ f x) (s.val.bind fun a ↦ (t a).val))

Tactic:
congr

Goal state after:
case e_b
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
f : ι → M
s : Finset κ
t : κ → Finset ι
h : (↑s).PairwiseDisjoint t
⊢ 1 = Multiset.foldr (fun x1 x2 ↦ x1 * x2) 1 (Multiset.map (fun i ↦ 1) s.val)
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: case mp
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 }
h :
  { 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
x : M
⊢ ∀ ⦃y : M⦄, ↑s x y → ↑t x y

Tactic:
y

Goal state after:
case mp
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 }
h :
  { 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
x y : M
⊢ ↑s x y → ↑t x y
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ι → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∏ a with a ∈ s, f a = ∏ i ∈ s, f i

Tactic:
congr

Goal state after:
case e_s
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ι → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ {a | a ∈ s} = s
Module: Mathlib.GroupTheory.FreeGroup.Basic

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

Tactic:
map_eq_lift,

Goal state after:
α : Type u
β : Type v
f : α → β
⊢ (lift (of ∘ f)).range = Subgroup.closure (of '' Set.range f)
Module: Mathlib.GroupTheory.FreeGroup.Basic

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

Tactic:
by induction x <;> simp

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

Goal state before:
pp: G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
f : G →* M
x✝ y✝ : G
⊢ (leftRel f.ker) x✝ y✝ ↔ (Con.ker f) x✝ y✝

Tactic:
Setoid.comm',

Goal state after:
G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
f : G →* M
x✝ y✝ : G
⊢ (leftRel f.ker) y✝ x✝ ↔ (Con.ker f) x✝ y✝
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ ↑x = ↑y ↔ x / y ∈ N

Tactic:
refine eq_comm.trans (QuotientGroup.eq.trans ?_)

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ y⁻¹ * x ∈ N ↔ x / y ∈ N
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: 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 (⇑e '' ⇑e ⁻¹' ↑s) = closure ↑s

Tactic:
congr

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
⊢ ⇑e '' ⇑e ⁻¹' ↑s = ↑s
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: 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
⊢ ⇑e '' ⇑e ⁻¹' ↑s = ↑s

Tactic:
Set.image_preimage_eq_iff,

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
⊢ ↑s ⊆ Set.range ⇑e
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mp
G : Type u_3
inst✝ : Group G
⊢ FG G → ∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ

pp: case mpr
G : Type u_3
inst✝ : Group G
⊢ (∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ) → FG G

Tactic:
· rw [fg_iff_exists_freeGroup_hom_surjective]
    intro ⟨S, hS, φ, hφ⟩
    obtain ⟨n, ⟨e⟩⟩ := hS.exists_equiv_fin S
    exact ⟨Fin n, inferInstance, φ.comp (FreeGroup.freeGroupCongr e).symm,
      hφ.comp (FreeGroup.freeGroupCongr e).symm.surjective⟩

Goal state after:
case mpr
G : Type u_3
inst✝ : Group G
⊢ (∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ) → FG G
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ⁅g₁, g₂⁆ ∈ centralizer ↑H₁
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ⁅g₁, g₂⁆ ∈ centralizer ↑H₂
⊢ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ centralizer ↑H₃

Tactic:
mem_centralizer_iff_commutator_eq_one

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
⊢ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ∀ h ∈ ↑H₃, ⁅h, ⁅g₁, g₂⁆⁆ = 1