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

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x y : D₁ ≀ᵣ Q₁
⊢ { left := ⇑f ∘ (x * y).left ∘ ⇑g.symm, right := g (x * y).right } =
    { left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right } * { left := ⇑f ∘ y.left ∘ ⇑g.symm, right := g y.right }

Tactic:
ext

Goal state after:
case left
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x y : D₁ ≀ᵣ Q₁
x✝ : Q₂
⊢ { left := ⇑f ∘ (x * y).left ∘ ⇑g.symm, right := g (x * y).right }.left x✝ =
    ({ left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right } * { left := ⇑f ∘ y.left ∘ ⇑g.symm, right := g y.right }).left
      x✝

case right
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
D₁ : Type u_3
Q₁ : Type u_4
D₂ : Type u_5
Q₂ : Type u_6
inst✝³ : Group D₁
inst✝² : Group Q₁
inst✝¹ : Group D₂
inst✝ : Group Q₂
f : D₁ ≃* D₂
g : Q₁ ≃* Q₂
x y : D₁ ≀ᵣ Q₁
⊢ { left := ⇑f ∘ (x * y).left ∘ ⇑g.symm, right := g (x * y).right }.right =
    ({ left := ⇑f ∘ x.left ∘ ⇑g.symm, right := g x.right } *
        { left := ⇑f ∘ y.left ∘ ⇑g.symm, right := g y.right }).right
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ τ ∈ (toPermHom g).range ↔ ∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ τ ∈ (toPermHom g).range → ∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ (∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support) → τ ∈ (toPermHom g).range
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : ResiduallyFinite G
H : Subgroup G
g : ↥H
hg : ∀ (H_1 : FiniteIndexNormalSubgroup ↥H), g ∈ H_1
⊢ g = 1

Tactic:
ext

Goal state after:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : ResiduallyFinite G
H : Subgroup G
g : ↥H
hg : ∀ (H_1 : FiniteIndexNormalSubgroup ↥H), g ∈ H_1
⊢ ↑g = ↑1
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : ResiduallyFinite G
inst✝ : ResiduallyFinite G'
g : G × G'
hg : ∀ (H : FiniteIndexNormalSubgroup (G × G')), g ∈ H
⊢ g = 1

Tactic:
ext

Goal state after:
case fst
G : Type u_1
G' : Type u_2
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : ResiduallyFinite G
inst✝ : ResiduallyFinite G'
g : G × G'
hg : ∀ (H : FiniteIndexNormalSubgroup (G × G')), g ∈ H
⊢ g.1 = 1.1

case snd
G : Type u_1
G' : Type u_2
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : ResiduallyFinite G
inst✝ : ResiduallyFinite G'
g : G × G'
hg : ∀ (H : FiniteIndexNormalSubgroup (G × G')), g ∈ H
⊢ g.2 = 1.2
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:
rw [mul_inv_rev]; exact mul_smul (op g₁⁻¹) (op g₂⁻¹) T

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : ↥g.cycleFactorsFinset → ℕ := fun c ↦ #(↑c).support
hsc : sc = fun c ↦ #(↑c).support
⊢ (fun x ↦ x ∈ (toPermHom g).range) = fun x ↦ x ∈ {k | sc ∘ ⇑k = sc}

Tactic:
ext

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : ↥g.cycleFactorsFinset → ℕ := ⋯
hsc : sc = fun c ↦ #(↑c).support
x✝ : Perm ↥g.cycleFactorsFinset
⊢ x✝ ∈ (toPermHom g).range ↔ x✝ ∈ {k | sc ∘ ⇑k = sc}
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case intro
ι : 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
f g : PushoutI φ →* K
h : ∀ (i : ι), f.comp (of i) = g.comp (of i)
i : ι
⊢ f.comp (base φ) = g.comp (base φ)

Tactic:
ext

Goal state after:
case intro
ι : 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
f g : PushoutI φ →* K
h : ∀ (i : ι), f.comp (of i) = g.comp (of i)
i : ι
x✝ : H
⊢ (f.comp (base φ)) x✝ = (g.comp (base φ)) x✝
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case inr
ι : 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 φ
i✝ : ι
g✝ : G i✝
w : NormalWord d
hmw : w.fstIdx ≠ some i✝
hgr : g✝ ∉ (φ i✝).range
n : ↑↑(φ i✝).range × ↑(d.set i✝) := ⋯.equiv (g✝ * (φ i✝) w.head)
w' : Word G := Word.cons (↑n.2) w.toWord hmw ⋯
i : ι
g : G i
h✝ : ⟨i, g⟩ ∈ w.toList
⊢ g ∈ d.set i

Tactic:
exact w.normalized _ _ (by assumption)

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card)
⊢ #{g | (↑g).cycleType = m} =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))

Tactic:
rw [← Finset.card_map, map_subtype_of_cycleType, if_pos hm.2,
      Equiv.Perm.card_of_cycleType α m, if_pos hm.1, mul_assoc]

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

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ofSubtype.range ≤ map (centralizer {g}).subtype (toPermHom g).ker ∧
    ∀ (i : ↥g.cycleFactorsFinset), ↑i ∈ map (centralizer {g}).subtype (toPermHom g).ker

Tactic:
constructor

Goal state after:
case a.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ofSubtype.range ≤ map (centralizer {g}).subtype (toPermHom g).ker

case a.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ∀ (i : ↥g.cycleFactorsFinset), ↑i ∈ map (centralizer {g}).subtype (toPermHom g).ker
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case refine_2
ι : 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 : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
this : ↑(⋯.equiv ((φ i) h * ((Word.equivPair i) w).head)).2 = (φ i) h * ((Word.equivPair i) w).head
⊢ h = 1

Tactic:
equiv_mul_left_of_mem (d.compl i) ⟨_, rfl⟩,

Goal state after:
case refine_2
ι : 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 : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
this :
  ↑(⟨(φ i) h, ⋯⟩ * (⋯.equiv ((Word.equivPair i) w).head).1, (⋯.equiv ((Word.equivPair i) w).head).2).2 =
    (φ i) h * ((Word.equivPair i) w).head
⊢ h = 1
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case refine_1
ι : 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 : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
⊢ ¬(φ i) h * ((Word.equivPair i) w).head = 1 ∧
    (⟨i, (φ i) h * ((Word.equivPair i) w).head⟩ ∈ w.toList.tail ∨
      w.toList.head? = some ⟨i, ((Word.equivPair i) w).head⟩ ∨ ¬w.fstIdx = some i ∧ ((Word.equivPair i) w).head = 1)

Tactic:
constructor

Goal state after:
case refine_1.left
ι : 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 : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
⊢ ¬(φ i) h * ((Word.equivPair i) w).head = 1

case refine_1.right
ι : 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 : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
⊢ ⟨i, (φ i) h * ((Word.equivPair i) w).head⟩ ∈ w.toList.tail ∨
    w.toList.head? = some ⟨i, ((Word.equivPair i) w).head⟩ ∨ ¬w.fstIdx = some i ∧ ((Word.equivPair i) w).head = 1
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case refine_1.left
ι : 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 : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
h₁ : ↑⟨(φ i) h, ⋯⟩ * ↑(⋯.equiv 1).1 = 1
h₂ : ((Word.equivPair i) w).head = 1
⊢ False

Tactic:
((d.compl i).coe_equiv_fst_eq_one_iff_mem (one_mem _)).mpr (d.one_mem _),

Goal state after:
case refine_1.left
ι : 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 : Word G
i : ι
h : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h) • w).toList → ↑(⋯.equiv g).2 = g
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
h₁ : ↑⟨(φ i) h, ⋯⟩ * 1 = 1
h₂ : ((Word.equivPair i) w).head = 1
⊢ False
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : Subsingleton ↥N ∧ Nonempty ↥N
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
this : Subsingleton ↥N
⊢ ∃ H, N.IsComplement' H

Tactic:
rw [N.eq_bot_of_subsingleton]

Goal state after:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : Subsingleton ↥N ∧ Nonempty ↥N
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
this : Subsingleton ↥N
⊢ ∃ H, ⊥.IsComplement' H
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
⊢ (∀ ⦃x : Perm α⦄, x ∈ Subgroup.centralizer {g} → x ∈ alternatingGroup α) ↔
    (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
⊢ (∀ ⦃x : Perm α⦄, x ∈ Subgroup.centralizer {g} → x ∈ alternatingGroup α) →
    (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1

case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
⊢ ((∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1) →
    ∀ ⦃x : Perm α⦄, x ∈ Subgroup.centralizer {g} → x ∈ alternatingGroup α
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
⊢ Nat.card ↥(alternatingGroup α) = 3 * Nat.card ↥(kleinFour α)

Tactic:
rw [card_of_card_eq_four hα4, kleinFour_card_of_card_eq_four hα4]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ ⁅alternatingGroup α, alternatingGroup α⁆ = alternatingGroup α

Tactic:
← Subgroup.map_subtype_commutator,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ Subgroup.map (alternatingGroup α).subtype (_root_.commutator ↥(alternatingGroup α)) = alternatingGroup α
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 : ι
d : Transversal φ
⊢ Injective ⇑(of i)

Tactic:
let _ := Classical.decEq ι

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 : ι
d : Transversal φ
x✝ : DecidableEq ι := Classical.decEq ι
⊢ Injective ⇑(of i)
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)
d : Transversal φ
⊢ Injective ⇑(base φ)

Tactic:
let _ := Classical.decEq ι

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)
d : Transversal φ
x✝ : DecidableEq ι := Classical.decEq ι
⊢ Injective ⇑(base φ)
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)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
h : H
heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod
this✝ : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
this : w'.toWord = Word.empty
hw'map : w.toList = []
⊢ w = Word.empty

Tactic:
ext

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)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
h : H
heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod
this✝ : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
this : w'.toWord = Word.empty
hw'map : w.toList = []
i✝ : ℕ
a✝ : (i : ι) × G i
⊢ w.toList[i✝]? = some a✝ ↔ Word.empty.toList[i✝]? = some a✝
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_1
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P K : Subgroup G
inst✝ : IsCyclic ↥P
hP : IsPGroup p ↥P
hKP : K ≤ Subgroup.normalizer ↑P
hPK : (Nat.card ↥P).Coprime (Nat.card ↥K)
x✝ : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P) (k : ↥K), k • g * g⁻¹ = 1
⊢ ⁅K, P⁆ ≤ ⊥

Tactic:
Subgroup.commutator_le

Goal state after:
case refine_1
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P K : Subgroup G
inst✝ : IsCyclic ↥P
hP : IsPGroup p ↥P
hKP : K ≤ Subgroup.normalizer ↑P
hPK : (Nat.card ↥P).Coprime (Nat.card ↥K)
x✝ : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P) (k : ↥K), k • g * g⁻¹ = 1
⊢ ∀ g₁ ∈ K, ∀ g₂ ∈ P, ⁅g₁, g₂⁆ ∈ ⊥
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_2
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P K : Subgroup G
inst✝ : IsCyclic ↥P
hP : IsPGroup p ↥P
hKP : K ≤ Subgroup.normalizer ↑P
hPK : (Nat.card ↥P).Coprime (Nat.card ↥K)
x✝ : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P), ∃ k q, k • q * q⁻¹ = g
⊢ ⁅K, P⁆ ≤ P ∧ P ≤ ⁅K, P⁆

Tactic:
Subgroup.commutator_le

Goal state after:
case refine_2
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P K : Subgroup G
inst✝ : IsCyclic ↥P
hP : IsPGroup p ↥P
hKP : K ≤ Subgroup.normalizer ↑P
hPK : (Nat.card ↥P).Coprime (Nat.card ↥K)
x✝ : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P), ∃ k q, k • q * q⁻¹ = g
⊢ (∀ g₁ ∈ K, ∀ g₂ ∈ P, ⁅g₁, g₂⁆ ∈ P) ∧ P ≤ ⁅K, P⁆
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ swap hammingDist x y = hammingDist x y

Tactic:
exact hammingDist_comm _ _

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
⊢ ∫⁻ (a : α), f a ∂Measure.dirac a = f a

Tactic:
lintegral_dirac

Goal state after:
α : Type u_1
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
⊢ f a = f a
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
β : Type u_4
inst✝ : MeasurableSpace β
μ ν : Measure α
⊢ const β (μ + ν) = const β μ + const β ν

Tactic:
ext

Goal state after:
α : Type u_1
mα : MeasurableSpace α
β : Type u_4
inst✝ : MeasurableSpace β
μ ν : Measure α
a✝¹ : β
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ((const β (μ + ν)) a✝¹) s✝ = ((const β μ + const β ν) a✝¹) s✝
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ s ∈ uniformity (Hamming β) ↔ ∃ ε > 0, ∀ {a b : Hamming β}, ↑(hammingDist (ofHamming a) (ofHamming b)) < ε → (a, b) ∈ s

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ s ∈ uniformity (Hamming β) → ∃ ε > 0, ∀ {a b : Hamming β}, ↑(hammingDist (ofHamming a) (ofHamming b)) < ε → (a, b) ∈ s

case mpr
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ (∃ ε > 0, ∀ {a b : Hamming β}, ↑(hammingDist (ofHamming a) (ofHamming b)) < ε → (a, b) ∈ s) →
    s ∈ uniformity (Hamming β)
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ (Bornology.cobounded (Hamming β)).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}

Tactic:
ext

Goal state after:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x✝ : Set (Hamming β)
⊢ x✝ ∈ (Bornology.cobounded (Hamming β)).sets ↔ x✝ ∈ {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
⊢ 0 ∘ₖ κ = 0

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((0 ∘ₖ κ) a✝¹) s✝ = (0 a✝¹) s✝
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel β γ
⊢ κ ∘ₖ 0 = 0

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel β γ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((κ ∘ₖ 0) a✝¹) s✝ = (0 a✝¹) s✝
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), ↑c ≠ []
⊢ r ≤ ∑ i, (↑(w i)).length ∧ ∑ i, (↑(w i)).length ≤ r * S.sup List.length

Tactic:
constructor

Goal state after:
case left
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), ↑c ≠ []
⊢ r ≤ ∑ i, (↑(w i)).length

case right
α : Type u_1
S : Finset (List α)
r : ℕ
w : Fin r → ↥S
h0 : ∀ (c : ↥S), ↑c ≠ []
⊢ ∑ i, (↑(w i)).length ≤ r * S.sup List.length
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
p : γ → Prop
hp : MeasurableSet {z | p z}
h : ∀ᵐ (y : β) ∂κ a, ∀ᵐ (z : γ) ∂η y, p z
⊢ ∀ᵐ (z : γ) ∂(η ∘ₖ κ) a, p z

Tactic:
rwa [ae_iff, comp_null] at *

Goal state after:
case hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
a : α
p : γ → Prop
hp : MeasurableSet {z | p z}
h : (κ a) {a | ¬∀ᵐ (z : γ) ∂η a, p z} = 0
⊢ MeasurableSet {a | ¬p a}
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ discard β ∘ₖ κ = discard α

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a✝¹ : α
s✝ : Set PUnit.{u_4 + 1}
a✝ : MeasurableSet s✝
⊢ ((discard β ∘ₖ κ) a✝¹) s✝ = ((discard α) a✝¹) s✝
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ const β μ ∘ₖ κ = const α μ

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure γ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((const β μ ∘ₖ κ) a✝¹) s✝ = ((const α μ) a✝¹) s✝
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsMarkovKernel η
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a : α
⊢ IsProbabilityMeasure ((κ a).bind ⇑η)

Tactic:
constructor

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsMarkovKernel η
κ : Kernel α β
inst✝ : IsMarkovKernel κ
a : α
⊢ ((κ a).bind ⇑η) Set.univ = 1
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsSFiniteKernel η
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (η ∘ₖ Kernel.sum κ.seq)

Tactic:
← kernel_sum_seq η,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsSFiniteKernel η
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (Kernel.sum η.seq ∘ₖ Kernel.sum κ.seq)