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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ a.ofPermHomFun τ x ≠ x ↔ ∃ a, ↑τ a ≠ a ∧ ↑a x ≠ x

Tactic:
rw [ofPermHomFun_apply_of_cycleOf_mem a τ hc hm]
    conv_lhs => rw [← hm]
    rw [(g ^ m).injective.ne_iff, a.injective.ne_iff, not_iff_comm]
    by_cases H : (τ : Perm g.cycleFactorsFinset) c = c
    · simp only [H, iff_true]
      push Not
      intro d hd
      rw [← notMem_support]
      have := g.cycleFactorsFinset_pairwise_disjoint c.prop d.prop
      rw [disjoint_iff_disjoint_support, Finset.disjoint_left] at this
      exact this (by lia) hc
    · simpa only [H, iff_false, not_not] using ⟨c, H, mem_support.mp hc⟩

Goal state after:
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ H, g ∉ H

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ H, g ∉ H
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ H, H.FiniteIndex ∧ g ∉ H

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ H, H.FiniteIndex ∧ g ∉ H
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
this : Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
⊢ ∏ i ∈ Finset.image (fun c ↦ #(↑c).support) g.cycleFactorsFinset.attach, (Fintype.card { a // #(↑a).support = i })! =
    ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
[

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
this : Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
⊢ ∏ i ∈ Finset.image (fun c ↦ #(↑c).support) g.cycleFactorsFinset.attach, (Fintype.card { a // #(↑a).support = i })! =
    ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
g : Perm α
⊢ g ∈ map (Embedding.subtype fun x ↦ x ∈ alternatingGroup α) {g | (↑g).cycleType = m} ↔ g ∈ {g | g.cycleType = m}

Tactic:
[

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
g : Perm α
⊢ g ∈ map (Embedding.subtype fun x ↦ x ∈ alternatingGroup α) {g | (↑g).cycleType = m} ↔ g ∈ {g | g.cycleType = m}
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' : x ∉ Function.fixedPoints ⇑g
⊢ ((noncommPiCoprod ⋯) (u, v).2) x = ↑(v ⟨g.cycleOf x, hx⟩) x

Tactic:
noncommPiCoprod_apply,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
u : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
hx' : x ∉ Function.fixedPoints ⇑g
⊢ (Finset.univ.noncommProd (fun i ↦ ↑((u, v).2 i)) ⋯) x = ↑(v ⟨g.cycleOf x, hx⟩) x
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g ∈ map (Embedding.subtype fun x ↦ x ∈ alternatingGroup α) {g | (↑g).cycleType = m}
⊢ False

Tactic:
[

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g ∈ map (Embedding.subtype fun x ↦ x ∈ alternatingGroup α) {g | (↑g).cycleType = m}
⊢ False
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
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ =
    (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ * h

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
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : G ⧸ H
x✝ : q ∈ Finset.univ
⊢ (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ =
    (MonoidHom.id ↥H) ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩ * h
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
f : PushoutI φ →* K
i : ι
⊢ ((fun i ↦ f.comp (of i), f.comp (base φ)).1 i).comp (φ i) = (fun i ↦ f.comp (of i), f.comp (base φ)).2

Tactic:
by rw [MonoidHom.comp_assoc, of_comp_eq_base]

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 φ
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
hg : ⟨i, g⟩ ∈ w'.toList
⊢ g ∈ d.set i

Tactic:
simp only [w', Word.cons, mem_cons, Sigma.mk.inj_iff] at hg

Goal state after:
ι : 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
hg : i = i✝ ∧ g ≍ ↑n.2 ∨ ⟨i, g⟩ ∈ w.toList
⊢ g ∈ d.set i
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ (if Even (n + 1) then #{g | g.cycleType = {n}} else 0) = if Odd n then (n - 1)! * (Fintype.card α).choose n else 0

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ (if Even (n + 1) then #{g | g.cycleType = {n}} else 0) = if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
⊢ sign (ofSubtype ((k, v).1, (k, v).2).1) * sign ((noncommPiCoprod ⋯) ((k, v).1, (k, v).2).2) =
    sign k * ∏ c, sign ↑(v c)

Tactic:
sign_ofSubtype,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
⊢ sign ((k, v).1, (k, v).2).1 * sign ((noncommPiCoprod ⋯) ((k, v).1, (k, v).2).2) = sign k * ∏ c, sign ↑(v c)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : 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
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
hk_cT : (↑k).cycleType = Multiset.replicate (↑k).cycleType.card 2
this : (↑k).cycleType.card * 2 = #(↑k).support
⊢ (↑k).cycleType.card * 2 = #c.support * 2

Tactic:
this

Goal state after:
α : 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
hτ : τ ∈ range_toPermHom' g
k : ↥(Subgroup.centralizer {g}) := a.toCentralizer ⟨τ, hτ⟩
hk : k = a.toCentralizer ⟨τ, hτ⟩
hk_cT : (↑k).cycleType = Multiset.replicate (↑k).cycleType.card 2
this : (↑k).cycleType.card * 2 = #(↑k).support
⊢ #(↑k).support = #c.support * 2
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ #{g_1 | g_1.cycleType = g.cycleType} = Nat.card ↑{h | IsConj g h}

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ #{g_1 | g_1.cycleType = g.cycleType} = Nat.card ↑{h | IsConj g h}
Module: Mathlib.GroupTheory.PushoutI

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

Tactic:
· rw [Word.equivPair_head]
      dsimp
      split_ifs with hep
      · rcases hep with ⟨hnil, rfl⟩
        rw [head?_eq_some_head hnil]
        simp_all
      · push Not at hep
        by_cases hw : w.toList = []
        · simp [hw, Word.fstIdx]
        · simp [head?_eq_some_head hw, Word.fstIdx, hep hw]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
⊢ x ∈ (kerParam g).range

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
⊢ x ∈ (kerParam g).range
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : N = ⊤
hN1 : Nat.card ↥N = 0
⊢ ∃ H, N.IsComplement' H

Tactic:
hN

Goal state after:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : N = ⊤
hN1 : Nat.card ↥N = 0
⊢ ∃ H, ⊤.IsComplement' H
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↑({1} ∪ {g | (↑g).cycleType = {2, 2}}) ≤ Fintype.card ↑↑S

Tactic:
[

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↑({1} ∪ {g | (↑g).cycleType = {2, 2}}) ≤ Fintype.card ↑↑S
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ {1} ∪ {g | (↑g).cycleType = {2, 2}}
⊢ g ^ 2 = 1

Tactic:
rcases hg' with hg' | hg'

Goal state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ {1}
⊢ g ^ 2 = 1

case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ {g | (↑g).cycleType = {2, 2}}
⊢ g ^ 2 = 1
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
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : (↑k).cycleType = {2, 2}
⊢ kleinFour α = commutator ↥(alternatingGroup α)

Tactic:
refine le_antisymm ?_ comm_le

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk22 : (↑k).cycleType = {2, 2}
⊢ kleinFour α ≤ commutator ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs : s.card = 4
k : ↥(alternatingGroup α)
⊢ k ∈ Subgroup.map (ofSubtype s) (kleinFour ↥s) ↔ (↑k).support ⊆ s ∧ (↑k = 1 ∨ (↑k).cycleType = {2, 2})

Tactic:
have hs : Nat.card s = 4 := by simpa

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card ↥s = 4
⊢ k ∈ Subgroup.map (ofSubtype s) (kleinFour ↥s) ↔ (↑k).support ⊆ s ∧ (↑k = 1 ∨ (↑k).cycleType = {2, 2})
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
hs : Nat.card ↥s = 4
σ : ↥(alternatingGroup ↥s)
hk : (↑((ofSubtype s) σ)).support ⊆ s
⊢ (ofSubtype s) σ ∈ Subgroup.map (ofSubtype s) (kleinFour ↥s) ↔
    (↑((ofSubtype s) σ)).support ⊆ s ∧ (↑((ofSubtype s) σ) = 1 ∨ (↑((ofSubtype s) σ)).cycleType = {2, 2})

Tactic:
[

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
hs : Nat.card ↥s = 4
σ : ↥(alternatingGroup ↥s)
hk : (↑((ofSubtype s) σ)).support ⊆ s
⊢ (ofSubtype s) σ ∈ Subgroup.map (ofSubtype s) (kleinFour ↥s) ↔
    (↑((ofSubtype s) σ)).support ⊆ s ∧ (↑((ofSubtype s) σ) = 1 ∨ (↑((ofSubtype s) σ)).cycleType = {2, 2})
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card ↥s = 4
hk : ¬(↑k).support ⊆ s
⊢ k ∈ Subgroup.map (ofSubtype s) (kleinFour ↥s) ↔ (↑k).support ⊆ s ∧ (↑k = 1 ∨ (↑k).cycleType = {2, 2})

Tactic:
[

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs✝ : s.card = 4
k : ↥(alternatingGroup α)
hs : Nat.card ↥s = 4
hk : ¬(↑k).support ⊆ s
⊢ k ∈ Subgroup.map (ofSubtype s) (kleinFour ↥s) ↔ (↑k).support ⊆ s ∧ (↑k = 1 ∨ (↑k).cycleType = {2, 2})
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs : s.card = 4
g : Perm α
hg : g ∈ alternatingGroup α
k : Perm α
hk : k ∈ alternatingGroup α
⊢ ⟨k, hk⟩ ∈ Subgroup.map (ofSubtype (⟨g, hg⟩ • s)) (kleinFour ↥(⟨g, hg⟩ • s)) ↔
    ⟨k, hk⟩ ∈ MulAut.conj ⟨g, hg⟩ • Subgroup.map (ofSubtype s) (kleinFour ↥s)

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs : s.card = 4
g : Perm α
hg : g ∈ alternatingGroup α
k : Perm α
hk : k ∈ alternatingGroup α
⊢ ⟨k, hk⟩ ∈ Subgroup.map (ofSubtype (⟨g, hg⟩ • s)) (kleinFour ↥(⟨g, hg⟩ • s)) ↔
    ⟨k, hk⟩ ∈ MulAut.conj ⟨g, hg⟩ • Subgroup.map (ofSubtype s) (kleinFour ↥s)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case inl
⊢ orderOf (a 1) = 2 * 0

Tactic:
[

Goal state after:
case inl
⊢ orderOf (a 1) = 2 * 0
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
⊢ κ = η ↔ ∀ (a : α) (s : Set β), MeasurableSet s → (κ a) s = (η a) s

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
⊢ κ = η ↔ ∀ (a : α) (s : Set β), MeasurableSet s → (κ a) s = (η a) s
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
a : α
s : Set β
h : ∫⁻ (b : β), s.indicator (fun x ↦ 1) b ∂κ a = ∫⁻ (b : β), s.indicator (fun x ↦ 1) b ∂η a
hs : MeasurableSet s
⊢ (κ a) s = (η a) s

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
a : α
s : Set β
h : ∫⁻ (b : β), s.indicator (fun x ↦ 1) b ∂κ a = ∫⁻ (b : β), s.indicator (fun x ↦ 1) b ∂η a
hs : MeasurableSet s
⊢ (κ a) s = (η a) s
Module: Mathlib.InformationTheory.Hamming

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

Tactic:
[

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = hammingDist y x
Module: Mathlib.Probability.Kernel.Defs

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

Tactic:
by
  ext a
  simp [Measure.eq_zero_of_isEmpty (κ a)]

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

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

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ η : Kernel α β
inst✝ : Countable ι
κ : ι → Kernel α β
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ (Measure.sum fun n ↦ (κ n) b) s
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
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ (Measure.dirac (f b)) s

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ (Measure.dirac (f b)) s
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ (Measure.dirac (f a)) s = s.indicator 1 (f a)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ (Measure.dirac (f a)) s = s.indicator 1 (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.InformationTheory.Hamming

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

Tactic:
[

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Fintype ι
κ : ι → Kernel α β
⊢ Kernel.sum κ = ∑ i, κ i

Tactic:
by
  ext a s hs
  simp only [sum_apply' κ a hs, finsetSum_apply' _ κ a s, tsum_fintype]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsSFiniteKernel κ
a : α
⊢ (Kernel.sum κ.seq) a = κ a

Tactic:
kernel_sum_seq κ

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
h : IsSFiniteKernel κ
a : α
⊢ κ a = κ a
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
h : ∀ i ∈ ∅, IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel (∑ i ∈ ∅, κs i)

Tactic:
Finset.sum_empty

Goal state after:
case empty
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κs : ι → Kernel α β
h : ∀ i ∈ ∅, IsSFiniteKernel (κs i)
⊢ IsSFiniteKernel 0
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
⊢ Kernel.sum κs = Kernel.sum fun n ↦ Kernel.sum (κs n).seq

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
⊢ Kernel.sum κs = Kernel.sum fun n ↦ Kernel.sum (κs n).seq
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → DecidableEq (β i)
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : Zero α
inst✝ : (i : ι) → SMulWithZero α (β i)
k : α
x : (i : ι) → β i
i : ι
⊢ k • 0 = 0

Tactic:
[

Goal state after:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → DecidableEq (β i)
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : Zero α
inst✝ : (i : ι) → SMulWithZero α (β i)
k : α
x : (i : ι) → β i
i : ι
⊢ k • 0 = 0
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n ↦ Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum fun n ↦ Kernel.sum (κs n).seq) a) s = ((Kernel.sum fun n ↦ (κs (e n).1).seq (e n).2) a) s

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Denumerable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
e : ℕ ≃ ι × ℕ := (Denumerable.eqv (ι × ℕ)).symm
hκ_eq : Kernel.sum κs = Kernel.sum fun n ↦ Kernel.sum (κs n).seq
a : α
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum fun n ↦ Kernel.sum (κs n).seq) a) s = ((Kernel.sum fun n ↦ (κs (e n).1).seq (e n).2) a) s