mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i : I
⊢ ∀ ⦃j : I⦄, i ≠ j → (fun i j ↦ ∀ (x : f i) (y : f j), Commute (mulSingle i x) (mulSingle j y)) i j

Tactic:
j

Goal state after:
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
⊢ i ≠ j → (fun i j ↦ ∀ (x : f i) (y : f j), Commute (mulSingle i x) (mulSingle j y)) i j
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
n : ℤ
s t : Set α
⊢ s / t = s * t⁻¹

Tactic:
← image_id (s / t),

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
n : ℤ
s t : Set α
⊢ id '' (s / t) = s * t⁻¹
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case a.one
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
⊢ 1 ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
exact Or.inl <| by simp

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

Goal state before:
pp: S : Type u_4
M : Type u_5
inst✝² : Mul M
inst✝¹ : SetLike S M
inst✝ : MulMemClass S M
s : S
x y : ↥s
⊢ Commute ↑x ↑y ↔ Commute x y

Tactic:
by
  simp [commute_iff_eq, Subtype.ext_iff]

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

Goal state before:
pp: 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⁻¹

Tactic:
rintro _ _ ⟨n, rfl⟩

Goal state after:
case refine_4
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
n : ℤ
hx✝ : x ^ n ∈ closure {x}
⊢ ∃ n_1, x ^ n_1 = (x ^ n)⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : G
i : ι
ha : a ∈ S i
b : G
⊢ ∀ (x : ι), b ∈ S x → a * b = b * a

Tactic:
j

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : G
i : ι
ha : a ∈ S i
b : G
j : ι
⊢ b ∈ S j → a * b = b * a
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (fun g ↦ ↑g.1 * ↑g.2) x = (fun g ↦ ↑g.1 * ↑g.2) y
⊢ x = y

Tactic:
rw [← inv_mul_eq_iff_eq_mul, ← mul_assoc, ← mul_inv_eq_one, mul_assoc] at hxy

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑y.1)⁻¹ * ↑x.1 * (↑x.2 * (↑y.2)⁻¹) = 1
⊢ x = y
Module: Mathlib.Algebra.Group.Subgroup.MulOpposite

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
x : Gᵐᵒᵖ
⊢ x ∈ (normalizer ↑H).op ↔ x ∈ normalizer ↑H.op

Tactic:
rw [mem_op, mem_normalizer_iff', mem_normalizer_iff']

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
x : Gᵐᵒᵖ
⊢ (∀ (n : G), n * MulOpposite.unop x ∈ H ↔ MulOpposite.unop x * n ∈ H) ↔ ∀ (n : Gᵐᵒᵖ), n * x ∈ H.op ↔ x * n ∈ H.op
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: ⊢ unpair 0 = 0

Tactic:
rw [unpair]
  simp

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

Goal state before:
pp: A : Type u_2
inst✝ : AddGroup A
x : A
⊢ ↑(Subgroup.zpowers (Multiplicative.ofAdd x)) = ⇑Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x)

Tactic:
rw [Equiv.eq_image_iff_symm_image_eq]

Goal state after:
A : Type u_2
inst✝ : AddGroup A
x : A
⊢ ⇑Multiplicative.ofAdd.symm '' ↑(Subgroup.zpowers (Multiplicative.ofAdd x)) = ↑(AddSubgroup.zmultiples x)
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
a : α
⊢ (down a).up = a

Tactic:
by
  simp [up, down, Equiv.symm_apply_apply]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H ≤ H

Tactic:
exact characteristic_iff_comap_le.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g h : G
⊢ (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, x = g⁻¹ * h * g) ↔ h ∈ s)

Tactic:
exists_eq_right,

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
⊢ H ≤ normalizer s ↔ ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ s

Tactic:
refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp hg, fun hH h hh k ↦ ⟨fun hk ↦ hH h hh k hk, fun hk ↦ ?_⟩⟩
  simpa [mul_assoc] using hH h⁻¹ (inv_mem hh) _ hk

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ≤ normalizer ↑K ↔ ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K

Tactic:
refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp hg, fun hH h hh k ↦ ⟨fun hk ↦ hH h hh k hk, fun hk ↦ ?_⟩⟩
  simpa [mul_assoc] using hH h⁻¹ (inv_mem hh) _ hk

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A : Set β
a : α
x : β
⊢ x ∈ a⁻¹ • A ↔ a • x ∈ A

Tactic:
by
  simp only [← image_smul, mem_image, inv_smul_eq_iff, exists_eq_right]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective ⇑f
⊢ normalizer ↑(Subgroup.map f H) = ⊤

Tactic:
← top_le_iff,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective ⇑f
⊢ ⊤ ≤ normalizer ↑(Subgroup.map f H)
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (x • s ∩ t).Nonempty → ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

pp: case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x) → (x • s ∩ t).Nonempty

Tactic:
· rintro ⟨a, h, ha⟩
    obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h
    exact ⟨b, x • b, ⟨hb, ha⟩, by simp⟩

Goal state after:
case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x) → (x • s ∩ t).Nonempty
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
⊢ map f (normalClosure s) = normalClosure (⇑f '' s)

Tactic:
by
  have : Normal (map f (normalClosure s)) := Normal.map inferInstance f hf
  apply le_antisymm
  · exact map_normalClosure_le s f
  · exact normalClosure_le_normal (Set.image_mono subset_normalClosure)

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

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : M
i : ι
ha : a ∈ S i
b : M
⊢ ∀ (x : ι), b ∈ S x → a * b = b * a

Tactic:
j

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : M
i : ι
ha : a ∈ S i
b : M
j : ι
⊢ b ∈ S j → a * b = b * a
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
N : Type u_4
F : Type u_5
inst✝² : Monoid N
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
m : M
⊢ map f (powers m) = powers (f m)

Tactic:
by
  simp only [powers_eq_closure, map_mclosure f, Set.image_singleton]

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

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoid A
x : A
⊢ ↑(Submonoid.powers (Multiplicative.ofAdd x)) = ⇑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x)

Tactic:
rw [Equiv.eq_image_iff_symm_image_eq]

Goal state after:
A : Type u_2
inst✝ : AddMonoid A
x : A
⊢ ⇑Multiplicative.ofAdd.symm '' ↑(Submonoid.powers (Multiplicative.ofAdd x)) = ↑(AddSubmonoid.multiples x)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen l₁.length l₂
⊢ l₁ ∈ sublistsLen l₁.length (a :: l₂)

Tactic:
| @cons l₁ l₂ a s IH =>

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

Goal state before:
pp: case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
⊢ ∀ ⦃y : α⦄, y ∈ ⋃ n, f n → i ≠ y → r i y

Tactic:
j

Goal state after:
case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
⊢ j ∈ ⋃ n, f n → i ≠ j → r i j
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ {x ∈ s.powerset ∪ image (insert x) s.powerset | #x = n.succ} =
    powersetCard n.succ s ∪ image (insert x) (powersetCard n s)

Tactic:
filter_union,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ {x ∈ s.powerset | #x = n.succ} ∪ {x ∈ image (insert x) s.powerset | #x = n.succ} =
    powersetCard n.succ s ∪ image (insert x) (powersetCard n s)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs✝ : s✝.Nonempty
ih : (s✝.inf fun b ↦ a \ f b) = a \ s✝.sup f
⊢ ((cons a✝ s✝ h✝).inf fun b ↦ a \ f b) = a \ (cons a✝ s✝ h✝).sup f

Tactic:
rw [sup_cons, inf_cons, ih, sdiff_sup]

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
⊢ ⨆ p, f p ≤ c ↔ ⨆ b, ⨆ c, f (b, c) ≤ c

Tactic:
ciSup_le_iff (bddAbove_iff_subset_Iic.mpr hf),

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
⊢ (∀ (i : β × γ), f i ≤ c) ↔ ⨆ b, ⨆ c, f (b, c) ≤ c
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

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

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

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝ : i ∈ ↑s
⊢ ∀ ⦃y : ι⦄, y ∈ ↑s → i ≠ y → (Disjoint on fun i ↦ map (Embedding.sigmaMk i) (t i)) i y

Tactic:
j

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝ : i ∈ ↑s
j : ι
⊢ j ∈ ↑s → i ≠ j → (Disjoint on fun i ↦ map (Embedding.sigmaMk i) (t i)) i j
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ (∃ a_1 ∈ f (⋯ ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd, (Embedding.sigmaMk ⟨i, b⟩.fst) a_1 = ⟨i, x⟩) → x ∈ f a b

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

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
hx : x ∈ f (⋯ ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd
⊢ x ∈ f a b
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 : Sigma α
b : Sigma β
x : Sigma γ
h : a.fst ≠ x.fst
⊢ ¬∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)

Tactic:
exact fun H => h H.fst

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s : Set ι
h : (f '' s).Finite
hs : s.Nonempty
⊢ ∃ i, MaximalFor (fun x ↦ x ∈ s) f i

Tactic:
obtain ⟨_, ⟨a, ha, rfl⟩, hmax⟩ := Finite.exists_maximalFor id (f '' s) h (hs.image f)
  exact ⟨a, ha, fun a' ha' hf ↦ hmax (mem_image_of_mem f ha') hf⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ {x ∈ finsetIcc a b | a ≠ x ∧ x ≠ b} ↔ a < x ∧ x < b

Tactic:
by
    rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_and_ne, lt_iff_le_and_ne]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
h : WellFoundedGT α
a : ℕ →o α
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

Tactic:
obtain ⟨x, ⟨n, rfl⟩, H⟩ := h.wf.has_min _ (Set.range_nonempty a)
    exact ⟨n, fun m _ => H _ (Set.mem_range_self _)⟩

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_6
r : α → α → Prop
a : α
h : Acc r a
b : { x // x ∈ {b | ReflTransGen r b a} }
⊢ Acc r ↑b

Tactic:
← acc_transGen_iff

Goal state after:
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : { x // x ∈ {b | ReflTransGen r b a} }
⊢ Acc (TransGen r) ↑b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_6
r : α → α → Prop
a : α
h : Acc r a
b : { x // x ∈ {b | ReflTransGen r b a} }
⊢ Acc r ↑b

Tactic:
rw [← acc_transGen_iff] at h ⊢

Goal state after:
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : { x // x ∈ {b | ReflTransGen r b a} }
⊢ Acc (TransGen r) ↑b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_2.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m ≠ f n
h : n < m
⊢ rᶜ (f m) (f n)

Tactic:
· exact mt symm (H _ _ h)

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

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

Tactic:
by
  rw [isConj_comm, isConj_iff, mem_orbit_iff]; rfl

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
hs : closure s = ⊤
⊢ ⨅ g ∈ s, centralizer {g} = ⨅ g, centralizer {↑g}

Tactic:
← iInf_subtype''

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
hs : closure s = ⊤
⊢ ⨅ i, centralizer {↑i} = ⨅ g, centralizer {↑g}
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c ↦ (f c, g c)) c c'
h' :
  ((fun c ↦ (f c, g c)) c).1 = ((fun c ↦ (f c, g c)) c').1 ∧ rβ ((fun c ↦ (f c, g c)) c).2 ((fun c ↦ (f c, g c)) c').2
⊢ ((PSigma.Lex (Subrel rα fun x ↦ x ∈ range f) fun a ↦ Subrel (rβ on g) fun x ↦ x ∈ f ⁻¹' {↑a}) on fun c ↦
      ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩)
    c c'

Tactic:
dsimp only [InvImage, (· on ·)] at h' ⊢

Goal state after:
case inr
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c ↦ (f c, g c)) c c'
h' : f c = f c' ∧ rβ (g c) (g c')
⊢ PSigma.Lex (Subrel rα fun x ↦ x ∈ range f) (fun a ↦ Subrel (rβ on g) fun x ↦ x ∈ f ⁻¹' {↑a}) ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩
    ⟨⟨f c', ⋯⟩, ⟨c', ⋯⟩⟩
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : ((fun c ↦ ⟨f c, g (f c) c⟩) c).fst = ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ ((PSigma.Lex (Subrel rι fun x ↦ x ∈ range f) fun a ↦ Subrel (rπ ↑a on g ↑a) fun x ↦ x ∈ f ⁻¹' {↑a}) on fun c ↦
      ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩)
    c c'

Tactic:
dsimp only [InvImage, (· on ·)] at h' ⊢

Goal state after:
case inr
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ PSigma.Lex (Subrel rι fun x ↦ x ∈ range f) (fun a ↦ Subrel (rπ ↑a on g ↑a) fun x ↦ x ∈ f ⁻¹' {↑a}) ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩
    ⟨⟨f c', ⋯⟩, ⟨c', ⋯⟩⟩
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mem
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' : G
hg' : g' ∈ s
x : X
hx : x ∈ t
⊢ g' • x ∈ t

Tactic:
| mem g' hg' =>

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

Goal state before:
pp: ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i✝ i : ι
a✝ : i ∈ ↑univ
⊢ ∀ ⦃y : ι⦄, y ∈ ↑univ → i ≠ y → (Commute on fun i ↦ (MonoidHom.mulSingle M i) (x i)) i y

Tactic:
j

Goal state after:
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i✝ i : ι
a✝ : i ∈ ↑univ
j : ι
⊢ j ∈ ↑univ → i ≠ j → (Commute on fun i ↦ (MonoidHom.mulSingle M i) (x i)) i j
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hf : ker f ≤ r
⊢ ⇑(r.map f) = Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2

Tactic:
refine le_antisymm ?_ (sup_le Relation.EqvGen.rel (by rintro _ _ rfl; exact .refl _))

Goal state after:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hf : ker f ≤ r
⊢ ⇑(r.map f) ≤ Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2
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
⊢ ∀ {a b : { N // N.Normal }},
    { toFun := fun N ↦ QuotientGroup.con ↑N, invFun := fun c ↦ ⟨c.subgroup, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun N ↦ QuotientGroup.con ↑N, invFun := fun c ↦ ⟨c.subgroup, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by
    simp only [QuotientGroup.con, Equiv.coe_fn_mk, Con.le_def, Con.rel_mk, leftRel_apply]
    refine ⟨fun h x _ ↦ ?_, fun hle _ _ h ↦ hle h⟩
    specialize @h 1 x
    simp_all

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:
by
  rw [prod_list_count]
  refine prod_subset hs fun x _ hx => ?_
  rw [mem_toFinset] at hx
  rw [count_eq_zero_of_not_mem hx, pow_zero]

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
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
i : κ
hi : i ∈ ↑s
⊢ ∀ ⦃y : κ⦄, y ∈ ↑s → i ≠ y → (_root_.Disjoint on t') i y

Tactic:
j

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
i : κ
hi : i ∈ ↑s
j : κ
⊢ j ∈ ↑s → i ≠ j → (_root_.Disjoint on t') i j
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ : R
s : ↥⊥
h : x✝¹ * ↑s = x✝ * ↑s
⊢ ↑s * x✝¹ = ↑s * x✝

Tactic:
rcases s with ⟨s, hs⟩

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝¹ x✝ s : R
hs : s ∈ ⊥
h : x✝¹ * ↑⟨s, hs⟩ = x✝ * ↑⟨s, hs⟩
⊢ ↑⟨s, hs⟩ * x✝¹ = ↑⟨s, hs⟩ * x✝
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ : R
s : ↥⊥
⊢ ↑s * x✝ = x✝ * ↑s

Tactic:
rcases s with ⟨s, hs⟩

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ s : R
hs : s ∈ ⊥
⊢ ↑⟨s, hs⟩ * x✝ = x✝ * ↑⟨s, hs⟩
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ x + y >>= f >>= g = x + y >>= fun x ↦ f x >>= g

Tactic:
iterate 3 rw [add_bind] <;> try rw [ihx, ihy]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ (lift (g ∘ f)) x = (lift g) ((map f) x)

Tactic:
by
  induction x using FreeAbelianGroup.induction_on with
  | zero => simp only [map_zero]
  | of => simp only [lift_apply_of, map, Function.comp]
  | neg _ h => simp only [h, map_neg]
  | add _ _ h₁ h₂ => simp only [h₁, h₂, map_add]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 : α
x₁ x₂ : FreeAbelianGroup α
ih₁ : x₁ * of L2 * of L3 = x₁ * (of L2 * of L3)
ih₂ : x₂ * of L2 * of L3 = x₂ * (of L2 * of L3)
⊢ (x₁ + x₂) * of L2 * of L3 = (x₁ + x₂) * (of L2 * of L3)

Tactic:
| add x₁ x₂ ih₁ ih₂ =>

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ H₁ ≤ normalizer ↑⁅H₁, H₂⁆

Tactic:
apply le_normalizer_closure_iff.mpr
  rintro g hg _ ⟨g₁, hg₁, g₂, hg₂, rfl⟩
  apply (mul_mem_cancel_right <| commutator_mem_commutator hg hg₂).mp
  rw [← commutatorElement_mul_left_eq_conj_mul g g₁ g₂]
  exact commutator_mem_commutator (mul_mem hg hg₁) hg₂

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

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

Tactic:
refine Subgroup.commutator_commutator_eq_bot_of_rotate ?_ this
    rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]

Goal state after:
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_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
⊢ r₃ * (↑u * r₁) = ↑s₃ * (↑u₀ * r₁)

Tactic:
rw [← mul_assoc, ← mul_assoc, h₃]

Goal state after: