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

Goal state before:
pp: case inl
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s B : Set α
G : Subgroup M
inst✝ : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
hB : IsBlock (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : (Subtype.val ⁻¹' B).Subsingleton
⊢ B.Subsingleton

Tactic:
rw [← inter_eq_self_of_subset_right hBs, ← Subtype.image_preimage_val]
      apply Set.Subsingleton.image hB'

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

Goal state before:
pp: case a
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Group H
inst✝⁵ : SMul G α
inst✝⁴ : SMul G β
inst✝³ : MulAction H α
inst✝² : SMul H β
inst✝¹ : SMulCommClass G H β
inst✝ : SMulCommClass G H α
s : Set α
b : β
g : H
h : Supports G s b
g' : G
hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
⊢ ∀ ⦃a : α⦄, a ∈ s → g' • a = a

Tactic:
rintro a ha

Goal state after:
case a
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Group H
inst✝⁵ : SMul G α
inst✝⁴ : SMul G β
inst✝³ : MulAction H α
inst✝² : SMul H β
inst✝¹ : SMulCommClass G H β
inst✝ : SMulCommClass G H α
s : Set α
b : β
g : H
h : Supports G s b
g' : G
hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
a : α
ha : a ∈ s
⊢ g' • a = a
Module: Mathlib.GroupTheory.GroupExtension.Defs

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝³ : Group N
inst✝² : Group E
inst✝¹ : Group G
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
x✝² x✝¹ : S.Equiv S'
toMulEquiv✝¹ : E ≃* E'
inl_comm✝¹ : ⇑toMulEquiv✝¹ ∘ ⇑S.inl = ⇑S'.inl
rightHom_comm✝¹ : ⇑S'.rightHom ∘ ⇑toMulEquiv✝¹ = ⇑S.rightHom
toMulEquiv✝ : E ≃* E'
inl_comm✝ : ⇑toMulEquiv✝ ∘ ⇑S.inl = ⇑S'.inl
rightHom_comm✝ : ⇑S'.rightHom ∘ ⇑toMulEquiv✝ = ⇑S.rightHom
h :
  ⇑{ toMulEquiv := toMulEquiv✝¹, inl_comm := inl_comm✝¹, rightHom_comm := rightHom_comm✝¹ }.toMulEquiv =
    ⇑{ toMulEquiv := toMulEquiv✝, inl_comm := inl_comm✝, rightHom_comm := rightHom_comm✝ }.toMulEquiv
x✝ :
  ⇑{ toMulEquiv := toMulEquiv✝¹, inl_comm := inl_comm✝¹, rightHom_comm := rightHom_comm✝¹ }.symm =
    ⇑{ toMulEquiv := toMulEquiv✝, inl_comm := inl_comm✝, rightHom_comm := rightHom_comm✝ }.symm
⊢ { toMulEquiv := toMulEquiv✝¹, inl_comm := inl_comm✝¹, rightHom_comm := rightHom_comm✝¹ } =
    { toMulEquiv := toMulEquiv✝, inl_comm := inl_comm✝, rightHom_comm := rightHom_comm✝ }

Tactic:
congr

Goal state after:
N : Type u_1
E : Type u_2
G : Type u_3
inst✝³ : Group N
inst✝² : Group E
inst✝¹ : Group G
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
x✝² x✝¹ : S.Equiv S'
toMulEquiv✝¹ : E ≃* E'
inl_comm✝¹ : ⇑toMulEquiv✝¹ ∘ ⇑S.inl = ⇑S'.inl
rightHom_comm✝¹ : ⇑S'.rightHom ∘ ⇑toMulEquiv✝¹ = ⇑S.rightHom
toMulEquiv✝ : E ≃* E'
inl_comm✝ : ⇑toMulEquiv✝ ∘ ⇑S.inl = ⇑S'.inl
rightHom_comm✝ : ⇑S'.rightHom ∘ ⇑toMulEquiv✝ = ⇑S.rightHom
h :
  ⇑{ toMulEquiv := toMulEquiv✝¹, inl_comm := inl_comm✝¹, rightHom_comm := rightHom_comm✝¹ }.toMulEquiv =
    ⇑{ toMulEquiv := toMulEquiv✝, inl_comm := inl_comm✝, rightHom_comm := rightHom_comm✝ }.toMulEquiv
x✝ :
  ⇑{ toMulEquiv := toMulEquiv✝¹, inl_comm := inl_comm✝¹, rightHom_comm := rightHom_comm✝¹ }.symm =
    ⇑{ toMulEquiv := toMulEquiv✝, inl_comm := inl_comm✝, rightHom_comm := rightHom_comm✝ }.symm
⊢ toMulEquiv✝¹ = toMulEquiv✝
Module: Mathlib.GroupTheory.GroupExtension.Defs

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
x✝² x✝¹ : S.Section
toFun✝¹ : G → E
rightInverse_rightHom✝¹ : Function.RightInverse toFun✝¹ ⇑S.rightHom
toFun✝ : G → E
rightInverse_rightHom✝ : Function.RightInverse toFun✝ ⇑S.rightHom
x✝ :
  { toFun := toFun✝¹, rightInverse_rightHom := rightInverse_rightHom✝¹ }.toFun =
    { toFun := toFun✝, rightInverse_rightHom := rightInverse_rightHom✝ }.toFun
⊢ { toFun := toFun✝¹, rightInverse_rightHom := rightInverse_rightHom✝¹ } =
    { toFun := toFun✝, rightInverse_rightHom := rightInverse_rightHom✝ }

Tactic:
congr

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

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
toMonoidHom✝¹ : G →* E
rightInverse_rightHom✝¹ : Function.RightInverse (↑toMonoidHom✝¹).toFun ⇑S.rightHom
toMonoidHom✝ : G →* E
rightInverse_rightHom✝ : Function.RightInverse (↑toMonoidHom✝).toFun ⇑S.rightHom
h :
  (fun s ↦ (↑s.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝¹, rightInverse_rightHom := rightInverse_rightHom✝¹ } =
    (fun s ↦ (↑s.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, rightInverse_rightHom := rightInverse_rightHom✝ }
⊢ { toMonoidHom := toMonoidHom✝¹, rightInverse_rightHom := rightInverse_rightHom✝¹ } =
    { toMonoidHom := toMonoidHom✝, rightInverse_rightHom := rightInverse_rightHom✝ }

Tactic:
congr

Goal state after:
N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
toMonoidHom✝¹ : G →* E
rightInverse_rightHom✝¹ : Function.RightInverse (↑toMonoidHom✝¹).toFun ⇑S.rightHom
toMonoidHom✝ : G →* E
rightInverse_rightHom✝ : Function.RightInverse (↑toMonoidHom✝).toFun ⇑S.rightHom
h :
  (fun s ↦ (↑s.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝¹, rightInverse_rightHom := rightInverse_rightHom✝¹ } =
    (fun s ↦ (↑s.toMonoidHom).toFun) { toMonoidHom := toMonoidHom✝, rightInverse_rightHom := rightInverse_rightHom✝ }
⊢ toMonoidHom✝¹ = toMonoidHom✝
Module: Mathlib.GroupTheory.GroupExtension.Defs

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
⊢ Function.Injective fun s ↦ (↑s.toMonoidHom).toFun

Tactic:
intro ⟨_, _⟩ ⟨_, _⟩ h
    congr
    exact DFunLike.coe_injective h

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

Goal state before:
pp: case inr.h1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
this :
  ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Set α},
    s.Nonempty →
      sᶜ.Nonempty → ¬sᶜ.ncard = s.ncard → s.ncard < sᶜ.ncard → IsCoatom (stabilizer (↥(alternatingGroup α)) s)
hs' : ¬s.ncard < sᶜ.ncard
⊢ sᶜᶜ.Nonempty

Tactic:
rw [compl_compl]

Goal state after:
case inr.h1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
this :
  ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Set α},
    s.Nonempty →
      sᶜ.Nonempty → ¬sᶜ.ncard = s.ncard → s.ncard < sᶜ.ncard → IsCoatom (stabilizer (↥(alternatingGroup α)) s)
hs' : ¬s.ncard < sᶜ.ncard
⊢ s.Nonempty
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case inr.hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
this :
  ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Set α},
    s.Nonempty →
      sᶜ.Nonempty → ¬sᶜ.ncard = s.ncard → s.ncard < sᶜ.ncard → IsCoatom (stabilizer (↥(alternatingGroup α)) s)
hs' : ¬s.ncard < sᶜ.ncard
⊢ ¬sᶜᶜ.ncard = sᶜ.ncard

Tactic:
rw [compl_compl]

Goal state after:
case inr.hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
this :
  ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Set α},
    s.Nonempty →
      sᶜ.Nonempty → ¬sᶜ.ncard = s.ncard → s.ncard < sᶜ.ncard → IsCoatom (stabilizer (↥(alternatingGroup α)) s)
hs' : ¬s.ncard < sᶜ.ncard
⊢ ¬s.ncard = sᶜ.ncard
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case inr.hs'
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
this :
  ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Set α},
    s.Nonempty →
      sᶜ.Nonempty → ¬sᶜ.ncard = s.ncard → s.ncard < sᶜ.ncard → IsCoatom (stabilizer (↥(alternatingGroup α)) s)
hs' : ¬s.ncard < sᶜ.ncard
⊢ sᶜ.ncard < sᶜᶜ.ncard

Tactic:
rw [compl_compl]

Goal state after:
case inr.hs'
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
this :
  ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Set α},
    s.Nonempty →
      sᶜ.Nonempty → ¬sᶜ.ncard = s.ncard → s.ncard < sᶜ.ncard → IsCoatom (stabilizer (↥(alternatingGroup α)) s)
hs' : ¬s.ncard < sᶜ.ncard
⊢ sᶜ.ncard < s.ncard
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
σ σ' : S.Section
g✝ g₁ g₂ : G
equiv : S.Equiv S'
g : G
⊢ S'.rightHom ((⇑equiv ∘ ⇑σ) g) = g

Tactic:
Function.comp_apply,

Goal state after:
N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
σ σ' : S.Section
g✝ g₁ g₂ : G
equiv : S.Equiv S'
g : G
⊢ S'.rightHom (equiv (σ g)) = g
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s : S.Splitting
e : E
⊢ S.rightHom e * (S.rightHom (s (S.rightHom e)))⁻¹ = 1

Tactic:
rightHom_splitting,

Goal state after:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s : S.Splitting
e : E
⊢ S.rightHom e * (S.rightHom e)⁻¹ = 1
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
a : List ℕ
ha : a ∈ c.ranges
⊢ pmap (fun a h ↦ Fin.valEmbedding (klift a h)) a ⋯ = map id a

Tactic:
simp [klift, Fin.valEmbedding_apply, List.pmap_eq_map, List.map_id']

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
a : α
⊢ (mk (stabilizerEquiv_invFun_aux g) • f) a = f a

Tactic:
rw [smul_apply, symm_apply_apply, Perm.smul_def]

Goal state after:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
a : α
⊢ f ((stabilizerEquiv_invFun_aux g) a) = f a
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: case hi
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ a ∈ Finset.univ, ↑a ∈ Finset.image f Finset.univ

Tactic:
exact fun g _ => Finset.coe_mem g

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

Goal state before:
pp: case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Perm α
toFun✝¹ : ↥g.cycleFactorsFinset → α
mem_support_self'✝¹ : ∀ (c : ↥g.cycleFactorsFinset), toFun✝¹ c ∈ (↑c).support
toFun✝ : ↥g.cycleFactorsFinset → α
mem_support_self'✝ : ∀ (c : ↥g.cycleFactorsFinset), toFun✝ c ∈ (↑c).support
x✝ :
  (fun a ↦ a.toFun) { toFun := toFun✝¹, mem_support_self' := mem_support_self'✝¹ } =
    (fun a ↦ a.toFun) { toFun := toFun✝, mem_support_self' := mem_support_self'✝ }
⊢ { toFun := toFun✝¹, mem_support_self' := mem_support_self'✝¹ } =
    { toFun := toFun✝, mem_support_self' := mem_support_self'✝ }

Tactic:
congr

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
⊢ (g ^ n) (a c) = (g ^ Nat.find ⋯) (a ⟨g.cycleOf x, hx''⟩)

Tactic:
congr

Goal state after:
case e_6.e_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := ⋯
⊢ c = ⟨g.cycleOf x, hx''⟩
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
⊢ (g ^ Nat.find ⋯) (a (↑τ ⟨g.cycleOf x, hx''⟩)) = (g ^ ↑n) (a (↑τ c))

Tactic:
congr

Goal state after:
case e_6.e_6.e_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
⊢ g.cycleOf x = ↑c
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
⊢ False

Tactic:
rw [Function.mem_fixedPoints_iff] at hx

Goal state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : g x = x
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
⊢ False
Module: Mathlib.GroupTheory.RegularWreathProduct

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

Tactic:
induction n with
  | zero => rw [IteratedWreathProduct_zero]; infer_instance
  | succ n ih => rw [IteratedWreathProduct_succ]; infer_instance

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
c : ↥g.cycleFactorsFinset
⊢ #(↑k * ↑c * (↑k)⁻¹).support = #(↑c).support

Tactic:
Equiv.Perm.support_conj

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
c : ↥g.cycleFactorsFinset
⊢ #(Finset.map (Equiv.toEmbedding ↑k) (↑c).support) = #(↑c).support
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
⊢ Nat.card ↥(toPermHom g).range = Nat.card ↑{k | sc ∘ ⇑k = sc}

Tactic:
congr

Goal state after:
α : 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}
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
⊢ False

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, (φ i) h * ((Word.equivPair i) w).head⟩ ∈ (CoprodI.of ((φ i) h) • w).toList

Tactic:
· apply hh1
    rw [equiv_mul_left_of_mem (d.compl i) ⟨_, rfl⟩, hhead] at this
    simpa [((injective_iff_map_eq_one' _).1 (d.injective i))] using this

Goal state after:
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, (φ i) h * ((Word.equivPair i) w).head⟩ ∈ (CoprodI.of ((φ i) h) • w).toList
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nat.card ↥(centralizer {g}) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
rw [← (toPermHom g).ker.card_mul_index, index_ker, nat_card_range_toPermHom,
    ← kerParam_range_card, ← Nat.card_eq_fintype_card, kerParam_range_eq, card_subtype]

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
⊢ Nat.card ↥(alternatingGroup α) = 12

Tactic:
have : Nontrivial α := by
    rw [← Finite.one_lt_card_iff_nontrivial, hα4]
    simp

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
this : Nontrivial α
⊢ Nat.card ↥(alternatingGroup α) = 12
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:
congr

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
η : Kernel α β
a : α
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrProbabilityMeasure (0 a)

Tactic:
simp only [zero_apply]

Goal state after:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
η : Kernel α β
a : α
inst✝ : IsZeroOrMarkovKernel 0
⊢ IsZeroOrProbabilityMeasure 0
Module: Mathlib.InformationTheory.Hamming

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

Tactic:
rw [eq_comm, hammingDist_eq_zero]

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → Zero (β i)
x : (i : ι) → β i
⊢ hammingDist 0 x = hammingNorm x

Tactic:
hammingDist_comm,

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
inst✝ : (i : ι) → Zero (β i)
x : (i : ι) → β i
⊢ hammingDist x 0 = hammingNorm x
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μβ : Measure β
inst✝ : SFinite μβ
⊢ const α μβ = Kernel.sum fun n ↦ const α (sfiniteSeq μβ n)

Tactic:
by rw [sum_const, sum_sfiniteSeq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ : ∀ (a : α), (κ a) (Set.range f) = 1
a : α
⊢ ((κ.comapRight hf) a) Set.univ = 1

Tactic:
rw [comapRight_apply' κ hf a MeasurableSet.univ]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ : ∀ (a : α), (κ a) (Set.range f) = 1
a : α
⊢ (κ a) (f '' Set.univ) = 1
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
a : α
s : Set (α × α)
hs : MeasurableSet s
⊢ s.indicator 1 (a, a).swap = s.indicator 1 (a, a)

Tactic:
congr

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
⊢ ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length ≤ 1

Tactic:
have h_kraft := kraft_mcmillan_inequality_aux h

Goal state after:
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
h_kraft : ∀ r ≥ 1, (∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length) ^ r ≤ ↑r * ↑(S.sup List.length)
⊢ ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length ≤ 1
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

Tactic:
· simp [hη]

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case pos.e_f
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
s : Set ((α × β) × γ)
hs : MeasurableSet s
a : α
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' Prod.mk a ⁻¹' ⇑MeasurableEquiv.prodAssoc.symm ⁻¹' s) ∂κ a =
    ∫⁻ (b : β), (η (a, b)) (Prod.mk (a, b) ⁻¹' s) ∂κ a

Tactic:
congr

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
f : β → γ
g : β → δ
hf : Measurable f
hg : ¬Measurable g
⊢ (κ.map fun x ↦ (f x, g x)).snd = κ.map g

Tactic:
· have : ¬ Measurable (fun x ↦ (f x, g x)) := by
      contrapose hg; exact hg.snd
    simp [map_of_not_measurable _ hg, map_of_not_measurable _ this]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
hf : Measurable f
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (p : β × γ), g p ∂(deterministic f hf ×ₖ κ) a = ∫⁻ (c : γ), g (f a, c) ∂κ a

Tactic:
rw [lintegral_prod _ _ _ hg, lintegral_deterministic' _ hg.lintegral_prod_right']

Goal state after: