mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
w' : NormalWord d
hS : a.2 ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
this : w'.head ∈ toSubgroup A B a.1
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) [a]
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := [], chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := [], chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := [], chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
hx' : Option.map Prod.fst { head := 1, toList := [], chain := ⋯ }.toList.head? = some (-a.1, x).1
⊢ False

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
w' : NormalWord d
hS : a.2 ∈ toSubgroup A B a.1
x : G
hx : w'.toList.head? = some (-a.1, x)
this : w'.head ∈ toSubgroup A B a.1
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) [a]
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := [], chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := [], chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := [], chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
hx' : Option.map Prod.fst { head := 1, toList := [], chain := ⋯ }.toList.head? = some (-a.1, x).1
⊢ False
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case pos
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
h1 : ¬f b = f a
h2 : f b = a
⊢ f a ∈ orbit (↥(closure S)) a

Tactic:
;

Goal state after:
case pos
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
h1 : ¬f b = f a
h2 : f b = a
⊢ f a ∈ orbit (↥(closure S)) a
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case pos
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : f b = b
⊢ (if b = a then a else if b = a then f a else b) = b

Tactic:
;

Goal state after:
case pos
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : f b = b
⊢ (if b = a then a else if b = a then f a else b) = b
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
d : TransversalPair G A B
w₁' : NormalWord d
hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁
hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList
hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head⁻¹ * w₁.head ∈ toSubgroup A B (-u)
w₂' : NormalWord d
hw₂'1 : ReducedWord.prod φ w₂'.toReducedWord = ReducedWord.prod φ w₂
hw₂'2 : List.map Prod.fst w₂'.toList = List.map Prod.fst w₂.toList
hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₂'.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)
⊢ ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂'.toReducedWord

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
d : TransversalPair G A B
w₁' : NormalWord d
hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁
hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList
hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head⁻¹ * w₁.head ∈ toSubgroup A B (-u)
w₂' : NormalWord d
hw₂'1 : ReducedWord.prod φ w₂'.toReducedWord = ReducedWord.prod φ w₂
hw₂'2 : List.map Prod.fst w₂'.toList = List.map Prod.fst w₂.toList
hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₂'.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)
⊢ ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂'.toReducedWord
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
x✝ : Q
⊢ (rightHom.comp inl) x✝ = (MonoidHom.id Q) x✝

Tactic:
;

Goal state after:
D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
x✝ : Q
⊢ (rightHom.comp inl) x✝ = (MonoidHom.id Q) x✝
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case left
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
Λ : Type u_3
inst✝³ : MulAction D Λ
inst✝² : FaithfulSMul D Λ
inst✝¹ : Nonempty Q
inst✝ : Nonempty Λ
m₁ m₂ : D ≀ᵣ Q
h : ∀ (a : Λ) (b : Q), m₁.left (m₁.right * b) • a = m₂.left (m₂.right * b) • a ∧ m₁.right = m₂.right
a : Λ
b q : Q
hh : ∀ (a : Λ), m₁.left q • a = m₂.left q • a
⊢ m₁.left q = m₂.left q

Tactic:
exact FaithfulSMul.eq_of_smul_eq_smul hh

Goal state after:
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case zero
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n : ℕ
inst✝ : Finite G
⊢ Finite PUnit.{u + 1}

Tactic:
;

Goal state after:
case zero
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n : ℕ
inst✝ : Finite G
⊢ Finite PUnit.{u + 1}
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case succ
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n✝ : ℕ
inst✝ : Finite G
n : ℕ
h : Finite (IteratedWreathProduct G n)
⊢ Finite (IteratedWreathProduct G n ≀ᵣ G)

Tactic:
;

Goal state after:
case succ
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n✝ : ℕ
inst✝ : Finite G
n : ℕ
h : Finite (IteratedWreathProduct G n)
⊢ Finite (IteratedWreathProduct G n ≀ᵣ G)
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case zero
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n : ℕ
inst✝ : Group G
⊢ Group PUnit.{u + 1}

Tactic:
;

Goal state after:
case zero
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n : ℕ
inst✝ : Group G
⊢ Group PUnit.{u + 1}
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: case succ
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n✝ : ℕ
inst✝ : Group G
n : ℕ
ih : Group (IteratedWreathProduct G n)
⊢ Group (IteratedWreathProduct G n ≀ᵣ G)

Tactic:
;

Goal state after:
case succ
D : Type u_1
Q : Type u_2
inst✝² : Group D
inst✝¹ : Group Q
G : Type u
n✝ : ℕ
inst✝ : Group G
n : ℕ
ih : Group (IteratedWreathProduct G n)
⊢ Group (IteratedWreathProduct G n ≀ᵣ G)
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
g₁ g₂ : G
q : H.QuotientDiff
T : H.LeftTransversal
⊢ (fun α ↦ op (g₂⁻¹ * g₁⁻¹) • α) T = (fun α ↦ op g₁⁻¹ • α) ((fun α ↦ op g₂⁻¹ • α) T)

Tactic:
;

Goal state after:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
g₁ g₂ : G
q : H.QuotientDiff
T : H.LeftTransversal
⊢ (fun α ↦ op (g₂⁻¹ * g₁⁻¹) • α) T = (fun α ↦ op g₁⁻¹ • α) ((fun α ↦ op g₂⁻¹ • α) T)
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
q : H.QuotientDiff
T : H.LeftTransversal
⊢ (fun α ↦ op 1 • α) T = T

Tactic:
;

Goal state after:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : IsMulCommutative ↥H
inst✝¹ : H.FiniteIndex
α β : H.LeftTransversal
inst✝ : H.Normal
q : H.QuotientDiff
T : H.LeftTransversal
⊢ (fun α ↦ op 1 • α) T = T
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
⊢ Mul (con φ).Quotient

Tactic:
;

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
⊢ Mul (con φ).Quotient
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
⊢ One (con φ).Quotient

Tactic:
;

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
⊢ One (con φ).Quotient
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
x : ↥g.cycleFactorsFinset
hx : x = ⟨c, hc⟩
⊢ #(↑⟨d, hd⟩).support = #(↑⟨c, hc⟩).support

Tactic:
;

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
x : ↥g.cycleFactorsFinset
hx : x = ⟨c, hc⟩
⊢ #(↑⟨d, hd⟩).support = #(↑⟨c, hc⟩).support
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
x : ↥g.cycleFactorsFinset
hx : ¬x = ⟨c, hc⟩
hx' : x = ⟨d, hd⟩
⊢ #(↑⟨c, hc⟩).support = #(↑⟨d, hd⟩).support

Tactic:
;

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset := swap ⟨c, hc⟩ ⟨d, hd⟩
a : g.Basis
x : ↥g.cycleFactorsFinset
hx : ¬x = ⟨c, hc⟩
hx' : x = ⟨d, hd⟩
⊢ #(↑⟨c, hc⟩).support = #(↑⟨d, hd⟩).support
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
aux : n ! = (n - 1)! * n
⊢ #{g | g.cycleType = {n}} * n * ?m.83! = (card α).choose n * n ! * ?m.83!

pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
aux : n ! = (n - 1)! * n
⊢ ℕ

Tactic:
Nat.choose_mul_factorial_mul_factorial hα,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
aux : n ! = (n - 1)! * n
⊢ #{g | g.cycleType = {n}} * n * (card α - n)! = (card α)!
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝² : Group G
inst✝¹ : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
G' : Type u
x✝¹ : Group G'
x✝ : Finite G'
hG' : Nat.card G' < Nat.card G
⊢ Nat.card G' = Nat.card G'

Tactic:
;

Goal state after:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
G' : Type u
x✝¹ : Group G'
x✝ : Finite G'
hG' : Nat.card G' < Nat.card G
⊢ Nat.card G' = Nat.card G'
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
h₁ : H
w₂ : Word G
h₂ : H
hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i
hw₁✝ :
  ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂).toList → g ∈ d.set i_1
hw₁ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (CoprodI.of ((φ i) (h₁⁻¹ * h₂)) • w₂).toList → g ∈ d.set i_1
this : h₁ = h₂
⊢ { toWord := ((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂, head := h₁, normalized := hw₁✝ } =
    { toWord := w₂, head := h₂, normalized := hw₂ }

Tactic:
;

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
h₁ : H
w₂ : Word G
h₂ : H
hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i
hw₁✝ :
  ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂).toList → g ∈ d.set i_1
hw₁ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (CoprodI.of ((φ i) (h₁⁻¹ * h₂)) • w₂).toList → g ∈ d.set i_1
this : h₁ = h₂
⊢ { toWord := ((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂, head := h₁, normalized := hw₁✝ } =
    { toWord := w₂, head := h₂, normalized := hw₂ }
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w₁ w₂ : NormalWord d
i : ι
h : CoprodI.of ((φ i) w₁.head) • w₁.toWord = CoprodI.of ((φ i) w₂.head) • w₂.toWord
⊢ w₁ = w₂

Tactic:
by
  rcases w₁ with ⟨w₁, h₁, hw₁⟩
  rcases w₂ with ⟨w₂, h₂, hw₂⟩
  dsimp at *
  rw [smul_eq_iff_eq_inv_smul, ← mul_smul] at h
  subst h
  simp only [← map_inv, ← map_mul] at hw₁
  have : h₁⁻¹ * h₂ = 1 := eq_one_of_smul_normalized w₂ (h₁⁻¹ * h₂) hw₂ hw₁
  rw [inv_mul_eq_one] at this; subst this
  simp

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
x✝² x✝¹ : G i
x✝ : NormalWord d
⊢ (equivPair i).symm
      { head := x✝² * x✝¹ * ((equivPair i) x✝).head, tail := ((equivPair i) x✝).tail, fstIdx_ne := ⋯,
        normalized := ⋯ } =
    (equivPair i).symm
      {
        head :=
          x✝² *
            ((equivPair i)
                ((equivPair i).symm
                  { head := x✝¹ * ((equivPair i) x✝).head, tail := ((equivPair i) x✝).tail, fstIdx_ne := ⋯,
                    normalized := ⋯ })).head,
        tail :=
          ((equivPair i)
              ((equivPair i).symm
                { head := x✝¹ * ((equivPair i) x✝).head, tail := ((equivPair i) x✝).tail, fstIdx_ne := ⋯,
                  normalized := ⋯ })).tail,
        fstIdx_ne := ⋯, normalized := ⋯ }

Tactic:
simp [mul_assoc, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
⊢ 4 ≠ 0

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
⊢ 4 ≠ 0
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n : ℕ
i j k : ZMod (2 * n)
⊢ ↑(2 * n) = 0

Tactic:
;

Goal state after:
n : ℕ
i j k : ZMod (2 * n)
⊢ ↑(2 * n) = 0
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case zero
n : ℕ
⊢ a 1 ^ 0 = a 0

Tactic:
;

Goal state after:
case zero
n : ℕ
⊢ a 1 ^ 0 = a 0
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case inl
n : ℕ
h : 0 < n
this : CharZero (ZMod (2 * 0))
⊢ ¬↑n = 0

Tactic:
simpa using h.ne'

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : Nontrivial G
p : ℕ := (Nat.card G).minFac
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
hP : IsCyclic ↥↑P
f : G →* ↥↑P := MonoidHom.transferSylow P ⋯
⊢ commutator G < ⊤

Tactic:
refine lt_of_le_of_lt (Abelianization.commutator_subset_ker f) ?_

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : Nontrivial G
p : ℕ := (Nat.card G).minFac
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
hP : IsCyclic ↥↑P
f : G →* ↥↑P := MonoidHom.transferSylow P ⋯
⊢ f.ker < ⊤
Module: Mathlib.GroupTheory.Subgroup.Saturated

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.PowSaturated
n : ℤ
g : G
hgn : g ^ n ∈ H
⊢ n = 0 ∨ g ∈ H

Tactic:
obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg <;> simpa using h (by simpa using hgn)

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case cons
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
hmw✝ : w.fstIdx ≠ some i
_hgn✝ : g ∈ d.set i
hgr✝ : g ∉ (φ i).range
_hw1✝ : w.head = 1
ih : w.prod • empty = w
⊢ (cons g w hmw✝ hgr✝).prod • empty = cons g w hmw✝ hgr✝

Tactic:
prod_cons,

Goal state after:
case cons
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
hmw✝ : w.fstIdx ≠ some i
_hgn✝ : g ∈ d.set i
hgr✝ : g ∉ (φ i).range
_hw1✝ : w.head = 1
ih : w.prod • empty = w
⊢ ((of i) g * w.prod) • empty = cons g w hmw✝ hgr✝
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
g₁ : G i
g₂ : G j
hg₁ : (of i) g₁ = 1
hg₂ : (of j) g₂ = 1
hx : ¬1 ∈ (base φ).range
⊢ False

Tactic:
;

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
g₁ : G i
g₂ : G j
hg₁ : (of i) g₁ = 1
hg₂ : (of j) g₂ = 1
hx : ¬1 ∈ (base φ).range
⊢ False
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
g : Kernel α β
toFun✝ : α → Measure β
measurable'✝ : Measurable toFun✝
h : { toFun := toFun✝, measurable' := measurable'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, measurable' := measurable'✝ } = g

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
g : Kernel α β
toFun✝ : α → Measure β
measurable'✝ : Measurable toFun✝
h : { toFun := toFun✝, measurable' := measurable'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, measurable' := measurable'✝ } = g
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
toFun✝¹ : α → Measure β
measurable'✝¹ : Measurable toFun✝¹
toFun✝ : α → Measure β
measurable'✝ : Measurable toFun✝
h : { toFun := toFun✝¹, measurable' := measurable'✝¹ }.toFun = { toFun := toFun✝, measurable' := measurable'✝ }.toFun
⊢ { toFun := toFun✝¹, measurable' := measurable'✝¹ } = { toFun := toFun✝, measurable' := measurable'✝ }

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
toFun✝¹ : α → Measure β
measurable'✝¹ : Measurable toFun✝¹
toFun✝ : α → Measure β
measurable'✝ : Measurable toFun✝
h : { toFun := toFun✝¹, measurable' := measurable'✝¹ }.toFun = { toFun := toFun✝, measurable' := measurable'✝ }.toFun
⊢ { toFun := toFun✝¹, measurable' := measurable'✝¹ } = { toFun := toFun✝, measurable' := measurable'✝ }
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ η✝ : Kernel α β
inst✝ : IsEmpty β
κ η : Kernel α β
a : α
s : Set β
a✝ : MeasurableSet s
⊢ (κ a) s = (η a) s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ η✝ : Kernel α β
inst✝ : IsEmpty β
κ η : Kernel α β
a : α
s : Set β
a✝ : MeasurableSet s
⊢ (κ a) s = (η a) s
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ η✝ : Kernel α β
inst✝ : IsEmpty β
κ η : Kernel α β
⊢ κ = η

Tactic:
ext a s; simp [Set.eq_empty_of_isEmpty s]

Goal state after:
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
f : α → β
hf : Measurable f
a : α
⊢ IsProbabilityMeasure (Measure.dirac (f a))

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
f : α → β
hf : Measurable f
a : α
⊢ IsProbabilityMeasure (Measure.dirac (f a))
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ : ι → ι → Kernel α β
a : α
s : Set β
a✝ : MeasurableSet s
⊢ ((Kernel.sum fun n ↦ Kernel.sum (κ n)) a) s = ((Kernel.sum fun m ↦ Kernel.sum fun n ↦ κ n m) a) s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ : ι → ι → Kernel α β
a : α
s : Set β
a✝ : MeasurableSet s
⊢ ((Kernel.sum fun n ↦ Kernel.sum (κ n)) a) s = ((Kernel.sum fun m ↦ Kernel.sum fun n ↦ κ n m) a) s
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ : ι → ι → Kernel α β
a : α
s : Set β
a✝ : MeasurableSet s
⊢ (Measure.sum fun n ↦ Measure.sum fun n_1 ↦ (κ n n_1) a) s = (Measure.sum fun n ↦ Measure.sum fun n_1 ↦ (κ n_1 n) a) s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ : ι → ι → Kernel α β
a : α
s : Set β
a✝ : MeasurableSet s
⊢ (Measure.sum fun n ↦ Measure.sum fun n_1 ↦ (κ n n_1) a) s = (Measure.sum fun n ↦ Measure.sum fun n_1 ↦ (κ n_1 n) a) s
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
n : ℕ
⊢ IsFiniteKernel (if n = 0 then κ else 0)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
n : ℕ
⊢ IsFiniteKernel (if n = 0 then κ else 0)