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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)

Tactic:
by
  have := ncard_add_ncard_compl s
  have h1 : sᶜ.Nontrivial := by
    rw [← one_lt_ncard_iff_nontrivial]
    exact lt_of_le_of_lt h0.nonempty.ncard_pos hs
  have hα : 4 < Nat.card α := by
    rw [← Set.one_lt_ncard_iff_nontrivial] at h0
    grind
  -- To prove that `stabilizer (alternatingGroup α) s` is maximal,
  -- we need to prove that it is `≠ ⊤`
  use stabilizer_ne_top h0.nonempty h1
  -- … and that every strict over-subgroup `G` is equal to `⊤`
  intro G hG
  suffices IsPreprimitive G α from subgroup_eq_top_of_isPreprimitive hα G hG.le
  -- G acts transitively
  have := G.isPretransitive_of_stabilizer_lt hG
    (exists_mem_stabilizer_smul_eq (Nat.le_of_succ_le hα))
  apply IsPreprimitive.mk
  -- We reduce to proving that a block which is not a subsingleton is `univ`.
  intro B hB
  rw [IsTrivialBlock, or_iff_not_imp_left]
  intro hB'
  suffices sᶜ ⊆ B by
    apply hB.eq_univ_of_card_lt
    have : sᶜ.ncard ≤ B.ncard := ncard_le_ncard this
    grind
  -- The proof needs 4 steps
  /- Step 1 : `sᶜ` is not a block.
       This uses that `s.ncard  < sᶜ.ncard`.
       In the equality case, it is possible that `B = sᶜ` is a block:
       in that case, `G` would be a wreath product,
       this is case (b) of the O'Nan-Scott classification
       of maximal subgroups of the alternating group. -/
  have not_isBlock_sc : ¬ IsBlock G sᶜ := fun hsc ↦ by
    apply compl_ne_univ.mpr h0.nonempty -- `sᶜ ≠ univ`
    apply hsc.eq_univ_of_card_lt
    grind
  -- Step 2 : A block contained in `sᶜ` is a subsingleton
  have hB_not_le_sc (B : Set α) (hB : IsBlock G B) (hBsc : B ⊆ sᶜ) :
      B.Subsingleton :=
    IsBlock.subsingleton_of_ssubset_compl_of_stabilizer_alternatingGroup_le h0
      (hBsc.ssubset_of_ne (by aesop)) -- uses Step 1
      hG.le hB
  -- Step 3 : A block contained in `s` is a subsingleton
  have hB_not_le_s (B : Set α) (hB : IsBlock G B) (hBs : B ⊆ s) :
      B.Subsingleton :=
    have : IsPreprimitive (stabilizer G s) s :=
      stabilizer_subgroup_isPreprimitive h1 hG.le
    hB.subsingleton_of_stabilizer_lt_of_subset hB_not_le_sc hG hBs
  -- Step 4 : sᶜ ⊆ B : A block which is not a subsingleton contains `sᶜ`.
  suffices IsMultiplyPretransitive (↥(alternatingGroup α)) α (s.ncard + 1) by
    have : ¬ B ⊆ s := fun h ↦ hB' (hB_not_le_s B hB h)
    have : ¬ B ⊆ sᶜ := fun h ↦ hB' (hB_not_le_sc B hB h)
    apply hB.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl
      hG.le <;> grind
  have := isMultiplyPretransitive α
  apply isMultiplyPretransitive_of_le (n := Nat.card α - 2) _ (Nat.sub_le _ _)
  grind

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
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:
by congr

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case refine_2
α : Type u_2
inst✝² : DecidableEq α
G : Type u_3
inst✝¹ : AddGroup G
inst✝ : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
h : AddAction.toPerm g = 1
⊢ AddAction.toPerm g = 1

Tactic:
simp only [Equiv.ext_iff, AddAction.toPerm_apply] at h ⊢
    simp [Subtype.ext_iff, Finset.ext_iff, mem_vadd_finset, h]

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

Goal state before:
pp: case neg
α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝ : Finite α
this : Fintype α
h2 : IsMultiplyPretransitive K α 2
hn : ¬n ≤ 2
⊢ IsMultiplyPretransitive K α n

Tactic:
suffices (IsEmpty (Fin n ↪ α)) by infer_instance

Goal state after:
case neg
α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝ : Finite α
this : Fintype α
h2 : IsMultiplyPretransitive K α 2
hn : ¬n ≤ 2
⊢ IsEmpty (Fin n ↪ α)
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
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e : E
⊢ (Function.surjInv ⋯ (S'.rightHom (f e)))⁻¹ * e ∈ S.inl.range

Tactic:
by
      rw [S.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv, ← MonoidHom.comp_apply,
        rightHom_comp]
      simpa only [Function.surjInv_eq] using inv_mul_cancel (S.rightHom e)

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝² : Finite α
this✝¹ : Fintype α
this✝ : IsPretransitive (Perm α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ IsPreprimitive (Perm α) ↑(powersetCard α n)

Tactic:
rw [← isCoatom_stabilizer_iff_preprimitive _ s]

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝² : Finite α
this✝¹ : Fintype α
this✝ : IsPretransitive (Perm α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ IsCoatom (stabilizer (Perm α) s)
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
⊢ (if h : Cancels (-u) (unitsSMul φ u w) then unitsSMulWithCancel φ (-u) (unitsSMul φ u w) h
    else
      let g' := unitsSMulGroup φ d (-u) (unitsSMul φ u w).head;
      cons (↑g'.1) (-u) ((↑g'.2 * (unitsSMul φ u w).head⁻¹) • unitsSMul φ u w) ⋯ ⋯) =
    w

Tactic:
split_ifs with hcan

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : Cancels (-u) (unitsSMul φ u w)
⊢ unitsSMulWithCancel φ (-u) (unitsSMul φ u w) hcan = w

case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : ¬Cancels (-u) (unitsSMul φ u w)
⊢ (let g' := unitsSMulGroup φ d (-u) (unitsSMul φ u w).head;
    cons (↑g'.1) (-u) ((↑g'.2 * (unitsSMul φ u w).head⁻¹) • unitsSMul φ u w) ⋯ ⋯) =
    w
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
⊢ ReducedWord.prod φ
      (if h : Cancels u w then unitsSMulWithCancel φ u w h
        else
          let g' := unitsSMulGroup φ d u w.head;
          cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯).toReducedWord =
    t ^ ↑u * ReducedWord.prod φ w.toReducedWord

Tactic:
split_ifs with hcan

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : Cancels u w
⊢ ReducedWord.prod φ (unitsSMulWithCancel φ u w hcan).toReducedWord = t ^ ↑u * ReducedWord.prod φ w.toReducedWord

case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
u : ℤˣ
w : NormalWord d
hcan : ¬Cancels u w
⊢ ReducedWord.prod φ
      (let g' := unitsSMulGroup φ d u w.head;
        cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯).toReducedWord =
    t ^ ↑u * ReducedWord.prod φ w.toReducedWord
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case pos
α : Type u_2
inst✝ : DecidableEq α
f : Equiv.Perm α
x : α
h : x = f x
⊢ Equiv.swap x (f x) ∈ closure fun x ↦ ∃ x_1 y, x_1 ≠ y ∧ x = Equiv.swap x_1 y

Tactic:
rw [← h, Equiv.swap_self]
    apply Subgroup.one_mem

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)
⊢ (a.ofPermHom τ).support = (↑τ).support.biUnion fun c ↦ (↑c).support

Tactic:
by
  ext x
  simp only [mem_support, Finset.mem_biUnion, ofPermHom_apply]
  rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | ⟨c, hc, m, hm⟩)
  · simp only [ofPermHomFun_apply_of_mem_fixedPoints a τ hx, ne_eq, not_true_eq_false, false_iff,
      ← mem_support]
    rintro ⟨c, -, hc⟩
    rw [Function.mem_fixedPoints_iff] at hx
    exact mem_support.mp ((mem_cycleFactorsFinset_support_le c.prop) hc) hx
  · 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.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ a.ofPermHom τ ∈ centralizer {g}

Tactic:
rw [mem_centralizer_singleton_iff]
  ext x
  simp only [mul_apply]
  exact ofPermHomFun_commute_zpow_apply a τ x 1

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝³ : Group G
N : Subgroup G
inst✝² : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup G
inst✝ : K.Normal
hK : K ≤ N
this : Function.Surjective ⇑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Nat.card (G ⧸ K) < Nat.card G
index_map : (map (QuotientGroup.mk' K) N).index = N.index
index_pos : 0 < N.index
⊢ (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime (map (QuotientGroup.mk' K) N).index

Tactic:
rw [index_map]

Goal state after:
G : Type u
inst✝³ : Group G
N : Subgroup G
inst✝² : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝¹ : Finite G
K : Subgroup G
inst✝ : K.Normal
hK : K ≤ N
this : Function.Surjective ⇑(QuotientGroup.mk' K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Nat.card (G ⧸ K) < Nat.card G
index_map : (map (QuotientGroup.mk' K) N).index = N.index
index_pos : 0 < N.index
⊢ (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime N.index
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)
⊢ ((kerParam g) (k, v)).cycleType = k.cycleType + ∑ c, (↑(v c)).cycleType

Tactic:
by
  let U := SetLike.coe (Finset.univ : Finset { x // x ∈ g.cycleFactorsFinset })
  have hU : U.Pairwise fun i j ↦ (v i).val.Disjoint (v j).val := fun c _ d _ h ↦ by
    obtain ⟨m, hm⟩ := (v c).prop
    obtain ⟨n, hn⟩ := (v d).prop
    simp only [← hm, ← hn]
    apply Disjoint.zpow_disjoint_zpow
    apply cycleFactorsFinset_pairwise_disjoint g c.prop d.prop
    exact Subtype.coe_ne_coe.mpr h
  rw [kerParam, MonoidHom.noncommCoprod_apply, ← Prod.fst_mul_snd ⟨k, v⟩, Prod.mk_mul_mk, mul_one,
    one_mul, Finset.univ_eq_attach,
    Disjoint.cycleType_mul (disjoint_ofSubtype_noncommPiCoprod g k v),
    Subgroup.noncommPiCoprod_apply, Disjoint.cycleType_noncommProd hU, Finset.univ_eq_attach]
  exact congr_arg₂ _ cycleType_ofSubtype rfl

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

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

Tactic:
Nat.coprime_zero_right,

Goal state after:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : Nat.card ↥N = 1
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
⊢ ∃ H, N.IsComplement' 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 : ι) → 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 := ⋯ })
i : ι
g : G i
hg :
  ⟨i, g⟩ ∈ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.tail.toList ∨
    g ≠ 1 ∧ ∃ (h : i✝ = i), g = h ▸ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.head
⊢ g ∈ d.set i

Tactic:
rcases hg with hg | ⟨_, rfl, rfl⟩

Goal state after:
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 φ
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 := ⋯ })
i : ι
g : G i
hg : ⟨i, g⟩ ∈ { head := ↑n.2, tail := p.tail, fstIdx_ne := ⋯ }.tail.toList
⊢ g ∈ d.set i

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
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case refine_1
α : 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}}

Tactic:
convert! mem_kleinFour_of_order_two_pow hα4 k.2 hn.dvd

Goal state after:
α : 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}
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

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

Tactic:
have h := P.ne_bot_of_dvd_card (Nat.card G).minFac_dvd

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

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

Tactic:
obtain ⟨n, rfl | rfl⟩ := n.eq_nat_or_neg

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : g ^ ↑n ∈ H
⊢ ↑n = 0 ∨ g ∈ H

case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.PowSaturated
g : G
n : ℕ
hgn : g ^ (-↑n) ∈ H
⊢ -↑n = 0 ∨ g ∈ H
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case pos
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : Nat.card G = 0
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g

Tactic:
rw [hc, Nat.coprime_zero_left, Nat.card_eq_one_iff_unique] at hGK
    simp [← hGK.1.elim 1]

Goal state after:
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)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h :
  Subgroup.normalizer ↑↑P ≤
    Subgroup.centralizer ↑(Subgroup.map (Subgroup.normalizer ↑↑P).subtype ((↑P).subgroupOf (Subgroup.normalizer ↑↑P)))
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P

Tactic:
Subgroup.map_subgroupOf_eq_of_le P.le_normalizer

Goal state after:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : Subgroup.normalizer ↑↑P ≤ Subgroup.centralizer ↑↑P
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑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
⊢ (∀ ⦃x_1 : ι⦄, x_1 ∈ univ → ¬x x_1 ≠ y x_1) → x = y

Tactic:
Classical.not_not,

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ (∀ ⦃x_1 : ι⦄, x_1 ∈ univ → x x_1 = y x_1) → x = y
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
a : α
t : Set γ
ht : MeasurableSet t
⊢ ((κ.comapRight hf) a) t = (κ a) (f '' t)

Tactic:
comapRight_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
a : α
t : Set γ
ht : MeasurableSet t
⊢ (Measure.comap f (κ a)) t = (κ a) (f '' t)
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf : MeasurableEmbedding f
⊢ IsFiniteKernel (κ.comapRight hf)

Tactic:
refine ⟨⟨κ.bound, κ.bound_lt_top, fun a => ?_⟩⟩
  rw [comapRight_apply' κ hf a .univ]
  exact measure_le_bound κ a _

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

Goal state before:
pp: case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
t : Set (α × β)
hκs : ∀ (a : α), IsFiniteMeasure (κ a)
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : ∀ (i : ℕ), Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' f i)
this : ∀ (a : α), (κ a) (Prod.mk a ⁻¹' ⋃ i, f i) = ∑' (i : ℕ), (κ a) (Prod.mk a ⁻¹' f i)
⊢ Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' ⋃ i, f i)

Tactic:
simpa only [this] using Measurable.tsum hf

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✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
b : Bool
⊢ IsProbabilityMeasure ((boolKernel μ ν) b)

Tactic:
cases b
      <;> simp only [boolKernel_apply, Bool.false_eq_true, ↓reduceIte]
      <;> infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsMarkovKernel κ
⊢ (μ ⊗ₘ κ) univ = μ univ

Tactic:
by
  simp [compProd]

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

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

Tactic:
simp_rw [sum_apply, prodMkRight_apply, sum_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
a : β × α
g : γ → ℝ≥0∞
⊢ ∫⁻ (c : γ), g c ∂κ.swapLeft a = ∫⁻ (c : γ), g c ∂κ a.swap

Tactic:
swapLeft_apply

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel (α × β) γ
a : β × α
g : γ → ℝ≥0∞
⊢ ∫⁻ (c : γ), g c ∂κ a.swap = ∫⁻ (c : γ), g c ∂κ a.swap
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
⊢ κ.swapRight = κ.map Prod.swap

Tactic:
by
  simp [swapRight]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ✝ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ✝ : MeasurableSpace γ✝
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel (α × β) γ
a : α
b : β
inst✝ : NeZero (κ (a, b))
⊢ NeZero ((κ.sectR a) b)

Tactic:
rw [sectR_apply]; infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ∞
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ∞

Tactic:
by
  let t := toMeasurable ((κ ⊗ₖ η) a) s
  have : ∀ b : β, η (a, b) (Prod.mk b ⁻¹' s) ≤ η (a, b) (Prod.mk b ⁻¹' t) := fun b =>
    measure_mono (Set.preimage_mono (subset_toMeasurable _ _))
  have ht : MeasurableSet t := measurableSet_toMeasurable _ _
  have h2t : (κ ⊗ₖ η) a t ≠ ∞ := by rwa [measure_toMeasurable]
  have ht_lt_top : ∀ᵐ b ∂κ a, η (a, b) (Prod.mk b ⁻¹' t) < ∞ := by
    rw [Kernel.compProd_apply ht] at h2t
    exact ae_lt_top (Kernel.measurable_kernel_prodMk_left' ht a) h2t
  filter_upwards [ht_lt_top] with b hb
  exact (this b).trans_lt hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel β γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
⊢ ⇑(Kernel.prodMkLeft α η) ∘ₘ μ ⊗ₘ κ = ⇑η ∘ₘ (μ ⊗ₘ κ).snd

Tactic:
Kernel.prodMkLeft,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
η : Kernel β γ
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
⊢ ⇑(η.comap Prod.snd ⋯) ∘ₘ μ ⊗ₘ κ = ⇑η ∘ₘ (μ ⊗ₘ κ).snd