mathlib-initiative/mathlib-tactics huggingface dataset:
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 : (i : ι) → G i →* K
k : H →* K
hf : ∀ (i : ι), (f i).comp (φ i) = k
i : ι
g : G i
⊢ (lift f k hf) ((of i) g) = (f i) g

Tactic:
by
  delta PushoutI lift of
  simp only [MonoidHom.coe_comp, Con.coe_mk', comp_apply, Con.lift_coe,
    lift_apply_inl, CoprodI.lift_of]

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)
⊢ (φ i) w.head ∈ (φ i).range

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case inl
ι : 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 φ
w : NormalWord d
i : ι
g : G i
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 ⋯
β : Type u_2
⊢ ↑n.2 ∈ d.set i

Tactic:
simp

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), ↑p x ∈ c.support ↔ x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c) := fun c ↦ ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
x : α
⊢ ((kerParam g) (u, v)) x = ↑p x

Tactic:
kerParam_apply

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), ↑p x ∈ c.support ↔ x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c) := fun c ↦ ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
x : α
⊢ (if hx : g.cycleOf x ∈ g.cycleFactorsFinset then ↑(v ⟨g.cycleOf x, hx⟩) x else (ofSubtype u) x) = ↑p x
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)
⊢ ∏ i ∈ g.cycleFactorsFinset.attach, (sign.comp (zpowers ↑i).subtype) (((k, v).1, (k, v).2).2 i) =
    ∏ c ∈ g.cycleFactorsFinset.attach, sign ↑(v c)

Tactic:
simp

Goal state after:
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
⊢ (Multiset.replicate (↑k).cycleType.card 2).card * 2 = (Multiset.replicate (↑k).cycleType.card 2).sum

Tactic:
simp

Goal state after:
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
⊢ 2 ≠ 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (∀ ⦃x : Perm α⦄, x ∈ Finset.univ → ¬x.cycleType = m) ↔ ∀ (x : Perm α), ¬x.cycleType = m

Tactic:
simp

Goal state after:
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
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
⊢ { toWord := ((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₁)) • w₂, head := h₁, normalized := hw₁✝ } =
    { toWord := w₂, head := h₁, normalized := hw₂ }

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count :
  ∀ x ∈ g.cycleFactorsFinset.val, ∀ y ∈ g.cycleFactorsFinset.val, (card ∘ support) x = (card ∘ support) y → x = y
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
c : ↥g.cycleFactorsFinset
⊢ ↑(((toPermHom g) ⟨x, ⋯⟩) c) ∈ g.cycleFactorsFinset.val

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_count :
  ∀ x ∈ g.cycleFactorsFinset.val, ∀ y ∈ g.cycleFactorsFinset.val, (card ∘ support) x = (card ∘ support) y → x = y
x : Perm α
hx : x ∈ Subgroup.centralizer {g}
c : ↥g.cycleFactorsFinset
⊢ (toPermHom g) ⟨x, ⋯⟩ ∈ (toPermHom g).range

Tactic:
simp

Goal state after:
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 φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
p : Pair d i
n : ↑↑(φ i).range × ↑(d.set i) := ⋯.equiv p.head
w : Word G :=
  (Word.equivPair i).symm
    (let __src := p.toPair;
    { head := ↑n.2, tail := __src.tail, fstIdx_ne := ⋯ })
left✝ : ⋯ ▸ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.head ≠ 1
⊢ ⋯ ▸ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.head ∈ d.set i

Tactic:
simp

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
⊢ 1 < 4

Tactic:
simp

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
S : Sylow 2 ↥(alternatingGroup α)
⊢ 12 = 2 ^ 2 * 3

Tactic:
simp

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
S : Sylow 2 ↥(alternatingGroup α)
this : 12 = 2 ^ 2 * 3
⊢ 2 ^ (2 * 1 + 0) = 4

Tactic:
simp

Goal state after:
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 : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i
normalized✝¹ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1
head₂ : G i
h₁ : ↑(⋯.equiv head₁).2 = ↑(⋯.equiv head₂).2
fstIdx_ne✝ : tail₁.fstIdx ≠ some i
normalized✝ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₁, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1
h₃ : (⋯.equiv head₁).1 = (⋯.equiv head₂).1
⊢ ↑(⋯.equiv head₂).1 * ↑(⋯.equiv head₂).2 = ↑(⋯.equiv head₂).1 * ↑(⋯.equiv head₂).2 ∧ tail₁ = tail₁

Tactic:
simp

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
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ ↑S
n : ℕ
hn : orderOf ↑k = 2 ^ n
⊢ k ∈ {1} ∪ {g | (↑g).cycleType = {2, 2}} ↔ (↑k).cycleType = ∅ ∨ (↑k).cycleType = {2, 2}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Finite α
inst✝¹ : DecidableEq α
inst✝ : (s : Set α) → DecidablePred fun x ↦ x ∈ s
s : ↑(Set.powersetCard α 2)
⊢ Nat.card ↥↑s ≤ 2

Tactic:
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✝ : NormalWord d
⊢ (equivPair i).symm
      { head := ((equivPair i) x✝).head, tail := ((equivPair i) x✝).tail, fstIdx_ne := ⋯, normalized := ⋯ } =
    x✝

Tactic:
exact (equivPair i).symm_apply_apply _

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

Goal state before:
pp: α : Type u_1
inst✝² : Finite α
inst✝¹ : DecidableEq α
inst✝ : (s : Set α) → DecidablePred fun x ↦ x ∈ s
a b : α
hab : a ≠ b
⊢ a ∈ ↑⟨{a, b}, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Finite α
inst✝¹ : DecidableEq α
inst✝ : (s : Set α) → DecidablePred fun x ↦ x ∈ s
a b : α
hab : a ≠ b
⊢ b ∈ ↑⟨{a, b}, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : ↑(Set.powersetCard α 3)
⊢ Nat.card ↥↑s ≤ 3

Tactic:
simp

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
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ {g | (↑g).cycleType = {2, 2}}
⊢ 2 = {2, 2}.lcm

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ _root_.commutator (Perm α) ≤ alternatingGroup α

Tactic:
by
  simp only [commutator_eq_closure, closure_le, Set.subset_def, mem_commutatorSet_iff,
    SetLike.mem_coe, mem_alternatingGroup, forall_exists_index]
  rintro _ p q rfl
  simp [map_commutatorElement, commutatorElement_eq_one_iff_commute, Commute.all]

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:
simp

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
⊢ kleinFour α = commutator ↥(alternatingGroup α)

Tactic:
have : Nat.card (alternatingGroup α ⧸ kleinFour α) = 3 := by
    rw [← Nat.mul_left_inj (a := Nat.card (kleinFour α))]
    · rw [← Subgroup.card_eq_card_quotient_mul_card_subgroup]
      rw [card_of_card_eq_four hα4, kleinFour_card_of_card_eq_four hα4]
    rw [kleinFour_card_of_card_eq_four hα4]; simp

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
⊢ kleinFour α = commutator ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

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

Tactic:
simp

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
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
⊢ 1 < 12

Tactic:
simp

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

Goal state before:
pp: case a.a
n : ℕ
k l : ZMod (2 * 0)
⊢ (match a k * a l with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j) =
    (match a k with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j) *
      match a l with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j

Tactic:
simp

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

Goal state before:
pp: case a.xa
n : ℕ
k l : ZMod (2 * 0)
⊢ (match a k * xa l with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j) =
    (match a k with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j) *
      match xa l with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j

Tactic:
simp

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

Goal state before:
pp: case xa.a
n : ℕ
k l : ZMod (2 * 0)
⊢ (match xa k * a l with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j) =
    (match xa k with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j) *
      match a l with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j

Tactic:
simp

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

Goal state before:
pp: case xa.xa
n : ℕ
k l : ZMod (2 * 0)
⊢ (match xa k * xa l with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j) =
    (match xa k with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j) *
      match xa l with
      | a j => DihedralGroup.r j
      | xa j => DihedralGroup.sr j

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ a 1 ^ (2 * n) = 1

Tactic:
simp

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

Goal state before:
pp: n : ℕ
i : ZMod (2 * n)
⊢ a ↑(2 * n) = 1

Tactic:
simp

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

Goal state before:
pp: case hfin
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ xa i ^ 2 ^ (1 + 1) = 1

Tactic:
simp

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

Goal state before:
pp: case inr
α : 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
g : ↥(alternatingGroup α)
hg : (↑g).cycleType = {2, 2}
c : Perm α
hc : (MulAut.conjNormal c) k = g
fc : MulAut ↥(alternatingGroup α) := MulAut.conjNormal c
⊢ ⊤ = Subgroup.map (MulEquiv.toMonoidHom fc) ⊤

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
s : ↑(Set.powersetCard α 4)
⊢ Nat.card ↥↑s = 4

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case empty
ι : 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)
⊢ empty.prod • empty = empty

Tactic:
simp

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

Goal state before:
pp: ⊢ 5 ≤ Nat.card (Fin 5)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ 5 ≤ Nat.card (Fin 5)

Tactic:
simp

Goal state after:
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 φ
hw : Reduced φ Word.empty
⊢ empty.prod = ofCoprodI Word.empty.prod

Tactic:
simp

Goal state after:
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
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
h : H
heq : (base φ) h = ofCoprodI w.prod
⊢ ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ Word.empty.toList → g ∈ d.set i

Tactic:
simp

Goal state after:
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
⊢ (∀ g₁ ∈ K, ∀ g₂ ∈ P, ⁅g₁, g₂⁆ ∈ P) ∧ P ≤ ⁅K, P⁆

Tactic:
refine ⟨fun k hk g hg ↦ P.mul_mem ((hKP hk g).mp hg) (P.inv_mem hg), fun g hg ↦ ?_⟩

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 : G
hg : g ∈ P
⊢ g ∈ ⁅K, P⁆
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
mα : MeasurableSpace α✝
mβ : MeasurableSpace β✝
α : Type u_4
β : Type u_5
x✝² : MeasurableSpace α
x✝¹ : MeasurableSpace β
x✝ : α
⊢ (0 x✝) Set.univ ≤ 0

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
h✝ : IsEmpty α
⊢ κ.bound ≤ 1

Tactic:
simp

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
h✝ : Nonempty α
inst✝ : IsZeroOrMarkovKernel 0
⊢ bound 0 ≤ 1

Tactic:
simp

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
h✝¹ : Nonempty α
h✝ : IsMarkovKernel κ
⊢ κ.bound ≤ 1

Tactic:
simp

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✝ : IsEmpty α
κ : Kernel α β
⊢ ∀ (a : α), IsProbabilityMeasure (κ a)

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x : Hamming β), dist x x = 0

Tactic:
by
    push_cast
    exact mod_cast hammingDist_self

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a✝ : α
s✝ : Set β
hs : MeasurableSet s✝
⊢ (κ a✝) (id '' s✝) = (κ a✝) s✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
S : Finset (List α)
h : UniquelyDecodable ↑S
r : ℕ
w₁ w₂ : Fin r → ↥S
hflat : concatFn w₁ = concatFn w₂
i : Fin r
⊢ ∀ w ∈ List.ofFn fun i ↦ ↑(w₁ i), w ∈ ↑S

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
S : Finset (List α)
h : UniquelyDecodable ↑S
r : ℕ
w₁ w₂ : Fin r → ↥S
hflat : concatFn w₁ = concatFn w₂
i : Fin r
⊢ ∀ w ∈ List.ofFn fun i ↦ ↑(w₂ i), w ∈ ↑S

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case false
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ ((boolKernel μ ν) false) Set.univ ≤ max (μ Set.univ) (ν Set.univ)

Tactic:
simp

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

Goal state before:
pp: case true
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ ((boolKernel μ ν) true) Set.univ ≤ max (μ Set.univ) (ν Set.univ)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β), s.indicator 1 b * t.indicator 1 b ∂κ a = (κ a) (s ∩ t)

Tactic:
calc
  _ = ∫⁻ b, (s ∩ t).indicator 1 b ∂κ a := by
    congr with b
    simp [Set.inter_indicator_one]
  _ = κ a (s ∩ t) := lintegral_indicator_one <| hs.inter ht

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((copy β ∘ₖ κ) a) (s ×ˢ t) = (κ a) (s ∩ t)

Tactic:
by
  rw [comp_apply' _ _ _ <| hs.prod ht]
  simp_rw [copy_apply, Measure.dirac_apply' _ <| hs.prod ht, Set.indicator_prod_one]
  calc
  _ = ∫⁻ b, (s ∩ t).indicator 1 b ∂κ a := by
    congr with b
    simp [Set.inter_indicator_one]
  _ = κ a (s ∩ t) := lintegral_indicator_one <| hs.inter ht

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 α β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ boolKernel μ ν = Kernel.sum fun n ↦ boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n)

Tactic:
ext b

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
b : Bool
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ((boolKernel μ ν) b) s✝ = ((Kernel.sum fun n ↦ boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n)) b) s✝
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: case false
α : Type u_1
mα : MeasurableSpace α
κ : Kernel Bool α
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ (κ false) s✝ = ((boolKernel (κ false) (κ true)) false) s✝

Tactic:
simp

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

Goal state before:
pp: case true
α : Type u_1
mα : MeasurableSpace α
κ : Kernel Bool α
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ (κ true) s✝ = ((boolKernel (κ false) (κ true)) true) s✝

Tactic:
simp

Goal state after:
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 : α
⊢ ∫⁻ (a : β), (η a) Set.univ ∂κ a = 1

Tactic:
simp

Goal state after: