mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
⊢ a ∈ sᶜ ∪ (g • s)ᶜ

Tactic:
exact Set.mem_union_left _ ha.1

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

Goal state before:
pp: case inr
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
B : Set α
G : Subgroup M
hB : IsBlock (↥G) B
inst✝ : IsPreprimitive ↥(stabilizer (↥G) B) ↑B
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Subtype.val ⁻¹' B = Set.univ
g' : M
hg' : g' ∈ G
hg's : g' ∉ stabilizer M B
h : _root_.Disjoint (⟨g', hg'⟩ • B) B
⊢ (g' • B).Subsingleton

Tactic:
apply hB_not_le_sc (⟨g', hg'⟩ • B) (hB.translate _)

Goal state after:
case inr
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
B : Set α
G : Subgroup M
hB : IsBlock (↥G) B
inst✝ : IsPreprimitive ↥(stabilizer (↥G) B) ↑B
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Subtype.val ⁻¹' B = Set.univ
g' : M
hg' : g' ∈ G
hg's : g' ∉ stabilizer M B
h : _root_.Disjoint (⟨g', hg'⟩ • B) B
⊢ ⟨g', hg'⟩ • B ⊆ Bᶜ
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s B : Set α
G : Subgroup ↥(alternatingGroup α)
hs : s.Nontrivial
hB_ss_sc : B ⊂ sᶜ
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
hB : IsBlock (↥G) B
⊢ B.Subsingleton

Tactic:
apply hB.subsingleton_of_ssubset_of_stabilizer_le hB_ss_sc
  intro g
  obtain ⟨⟨k, hk⟩, rfl⟩ := alternatingGroup.stabilizer.surjective_toPerm (by rwa [compl_compl]) g
  rw [stabilizer_compl] at hk
  exact ⟨⟨⟨k, hG hk⟩, by aesop⟩, rfl⟩

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

Goal state before:
pp: α✝ : Type u_1
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)

Tactic:
· by_cases h0' : s.Nontrivial
    · apply isCoatom_stabilizer_of_ncard_lt_ncard_compl h0' hs'
    · simp only [not_nontrivial_iff] at h0'
      apply isCoatom_stabilizer_singleton _ h0 h0'
      rw [← ncard_add_ncard_compl s]
      rw [← ncard_pos] at h0 h1
      grind

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

Goal state before:
pp: α✝ : Type u_2
n✝ : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)

Tactic:
apply isPretransitive_of_isMultiplyPretransitive

Goal state after:
α✝ : Type u_2
n✝ : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n
Module: Mathlib.GroupTheory.MonoidLocalization.DivPairs

Goal state before:
pp: M : Type u_1
G : Type u_2
H : Type u_3
inst✝² : CommMonoid M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : ⊤.LocalizationMap G
g : ⊤.LocalizationMap H
s : Submonoid G
⊢ divPairs g (comap (g.mulEquivOfLocalizations f).toMonoidHom s) = divPairs f s

Tactic:
ext; simp

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: case f.H
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
b : Localization s
a✝¹ : α
b✝¹ : ↥s
a✝ c✝ : α
b✝ d✝ : ↥s
h✝ : (r s) (a✝, b✝) (c✝, d✝)
⊢ ⋯ = ⋯

pp: case H
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a b : Localization s
a✝ c✝ : α
b✝ d✝ : ↥s
h✝ : (r s) (a✝, b✝) (c✝, d✝)
⊢ ⋯ = ⋯

Tactic:
all_goals rfl

Goal state after:
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 α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
l : List ℕ
hl : l ∈ c.ranges
n : ℕ
hn : n ∈ l
⊢ n < c.sum

Tactic:
rw [← mem_mem_ranges_iff_lt_sum]

Goal state after:
α : 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
l : List ℕ
hl : l ∈ c.ranges
n : ℕ
hn : n ∈ l
⊢ ∃ s ∈ c.ranges, n ∈ s
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝¹ : Group D
inst✝ : Group Q
⊢ rightHom.comp inl = MonoidHom.id Q

Tactic:
ext; simp

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
g : G
hg : of g = ReducedWord.prod φ w
w' : ReducedWord G A B :=
  let __src := ReducedWord.empty G A B;
  { head := g, toList := __src.toList, chain := ⋯ }
this : ReducedWord.prod φ w = ReducedWord.prod φ w'
⊢ w.toList = []

Tactic:
simpa [w'] using (map_fst_eq_and_of_prod_eq φ this).1

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

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

Tactic:
rw [mem_range_toPermHom_iff', Set.mem_ofPred_eq]

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
x : H
⊢ (of i) ((φ i) x) = (base φ) x

Tactic:
by
  rw [← MonoidHom.comp_apply, of_comp_eq_base]

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

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

Tactic:
ite_and,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
⊢ (if Even (m.sum + m.card) then
      #{g | g.cycleType = m} * ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    if Even (m.sum + m.card) then if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0 else 0
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
⊢ #{g | g.cycleType = m} = 0

Tactic:
Equiv.Perm.card_of_cycleType,

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
⊢ (if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    0
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
hK : K ⊔ N = ⊤
⊢ K = ⊤

Tactic:
contrapose! h3
  have h4 : (N.comap K.subtype).index = N.index := by
    rw [← N.relIndex_top_right, ← hK]
    exact (relIndex_sup_right K N).symm
  have h5 : Nat.card K < Nat.card G := by
    rw [← K.index_mul_card]
    exact lt_mul_of_one_lt_left Nat.card_pos (one_lt_index_of_ne_top h3)
  have h6 : Nat.Coprime (Nat.card (N.comap K.subtype)) (N.comap K.subtype).index := by
    rw [h4]
    exact h1.coprime_dvd_left (card_comap_dvd_of_injective N K.subtype Subtype.coe_injective)
  obtain ⟨H, hH⟩ := h2 K h5 h6
  replace hH : Nat.card (H.map K.subtype) = N.index := by
    rw [← relIndex_bot_left, ← relIndex_comap, MonoidHom.comap_bot, Subgroup.ker_subtype,
      relIndex_bot_left, ← IsComplement'.index_eq_card (IsComplement'.symm hH), index_comap,
      range_subtype, ← relIndex_sup_right, hK, relIndex_top_right]
  have h7 : Nat.card N * Nat.card (H.map K.subtype) = Nat.card G := by
    rw [hH, ← N.index_mul_card, mul_comm]
  have h8 : (Nat.card N).Coprime (Nat.card (H.map K.subtype)) := by
    rwa [hH]
  exact ⟨H.map K.subtype, isComplement'_of_coprime h7 h8⟩

Goal state after:
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, 1) * (1, (k, v).2)).1 * (noncommPiCoprod ⋯) (((k, v).1, 1) * (1, (k, v).2)).2) =
    sign k * ∏ c, sign ↑(v c)

Tactic:
Prod.mk_mul_mk,

Goal state after:
α : 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 * 1, 1 * (k, v).2).1 * (noncommPiCoprod ⋯) ((k, v).1 * 1, 1 * (k, v).2).2) =
    sign k * ∏ c, sign ↑(v c)
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)
U : Set ↥g.cycleFactorsFinset := ↑Finset.univ
hU : U.Pairwise fun i j ↦ (↑(v i)).Disjoint ↑(v j)
⊢ (ofSubtype (((k, v).1, 1) * (1, (k, v).2)).1 * (noncommPiCoprod ⋯) (((k, v).1, 1) * (1, (k, v).2)).2).cycleType =
    k.cycleType + ∑ c, (↑(v c)).cycleType

Tactic:
Prod.mk_mul_mk,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers ↑c)
U : Set ↥g.cycleFactorsFinset := ↑Finset.univ
hU : U.Pairwise fun i j ↦ (↑(v i)).Disjoint ↑(v j)
⊢ (ofSubtype ((k, v).1 * 1, 1 * (k, v).2).1 * (noncommPiCoprod ⋯) ((k, v).1 * 1, 1 * (k, v).2).2).cycleType =
    k.cycleType + ∑ c, (↑(v c)).cycleType
Module: Mathlib.GroupTheory.Perm.Centralizer

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

Tactic:
(Term.byTactic
 "by"
 (Tactic.tacticSeq
  (Tactic.tacticSeq1Indented
   [(Tactic.tacticHave__
     "have"
     (Term.letConfig [])
     (Term.letDecl
      (Term.letIdDecl
       (Term.letId `hn₀)
       []
       [(Term.typeSpec ":" («term_≠_» `n "≠" (num "0")))]
       ":="
       (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.lia "lia" (Tactic.optConfig []))]))))))
    []
    (Tactic.tacticHave__
     "have"
     (Term.letConfig [])
     (Term.letDecl
      (Term.letIdDecl
       (Term.letId `aux)
       []
       [(Term.typeSpec
         ":"
         («term_=_»
          (Nat.term_! `n "!")
          "="
          («term_*_»
           (Nat.term_!
            (Term.paren (Term.hygienicLParen "(" (hygieneInfo `[anonymous])) («term_-_» `n "-" (num "1")) ")")
            "!")
           "*"
           `n)))]
       ":="
       (Term.byTactic
        "by"
        (Tactic.tacticSeq
         (Tactic.tacticSeq1Indented
          [(Tactic.rwSeq
            "rw"
            (Tactic.optConfig [])
            (Tactic.rwRuleSeq
             "["
             [(Tactic.rwRule [] `mul_comm) "," (Tactic.rwRule [] (Term.app `mul_factorial_pred [`hn₀]))]
             "]")
            [])]))))))
    []
    (Tactic.rwSeq
     "rw"
     (Tactic.optConfig [])
     (Tactic.rwRuleSeq
      "["
      [(Tactic.rwRule [] `mul_comm)
       ","
       (Tactic.rwRule ["←"] (Term.app `Nat.mul_left_inj [`hn₀]))
       ","
       (Tactic.rwRule [] `mul_assoc)
       ","
       (Tactic.rwRule ["←"] `aux)
       ","
       (Tactic.rwRule
        ["←"]
        (Term.app
         `Nat.mul_left_inj
         [(Term.paren
           (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
           (Term.app `factorial_ne_zero [(Term.hole "_")])
           ")")]))
       ","
       (Tactic.rwRule [] (Term.app `Nat.choose_mul_factorial_mul_factorial [`hα]))
       ","
       (Tactic.rwRule [] `mul_assoc)]
      "]")
     [])
    []
    (Tactic.simpa
     "simpa"
     []
     []
     (Tactic.simpaArgsRest
      (Tactic.optConfig [])
      []
      []
      [(Tactic.simpArgs
        "["
        [(Tactic.simpLemma [] [] `ite_and)
         ","
         (Tactic.simpLemma [] [] (Term.app `if_pos [`hα]))
         ","
         (Tactic.simpLemma [] [] (Term.app `if_pos [`hn']))
         ","
         (Tactic.simpLemma [] [] (Term.app `mul_comm [(Term.hole "_") `n]))
         ","
         (Tactic.simpLemma [] [] `mul_assoc)]
        "]")]
      ["using"
       (Term.app
        `card_of_cycleType_mul_eq
        [`α
         (choice
          («term{_}» "{" [`n] "}")
          (Term.structInst
           "{"
           []
           (Term.structInstFields [(Term.structInstField (Term.structInstLVal `n []) [])])
           (Term.optEllipsis [])
           []
           "}"))])]))])))

Goal state after:
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:
← Nat.card_eq_fintype_card

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
⊢ ⨆ s, Subgroup.map (ofSubtype ↑s) (kleinFour ↥↑s) = ⊤

Tactic:
rw [eq_top_iff, ← closure_cycleType_eq_two_two_eq_top h5, Subgroup.closure_le]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h5 : 5 ≤ Nat.card α
⊢ {g | (↑g).cycleType = {2, 2}} ⊆ ↑(⨆ s, Subgroup.map (ofSubtype ↑s) (kleinFour ↥↑s))
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 ⋯
h : ¬f.ker < ⊤
⊢ ↑P = ⊥

Tactic:
← Subgroup.isComplement'_top_left,

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 : ¬f.ker < ⊤
⊢ ⊤.IsComplement' ↑P
Module: Mathlib.GroupTheory.Subgroup.Saturated

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

Tactic:
simpa using h (by simpa using hgn)

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Saturated

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

Tactic:
simpa using h (by simpa using hgn)

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : Group G''
f : G →* G'
f' : G' →* G''
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : Nontrivial ↥H
⊢ ⁅Subgroup.map H.subtype ⊤, Subgroup.map H.subtype ⊤⁆ < Subgroup.map H.subtype ⊤

Tactic:
← Subgroup.map_commutator,

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : Group G''
f : G →* G'
f' : G' →* G''
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : Nontrivial ↥H
⊢ Subgroup.map H.subtype ⁅⊤, ⊤⁆ < Subgroup.map H.subtype ⊤
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
x : PushoutI φ
g₁ : G i
hg₁ : (of i) g₁ = x
g₂ : G j
hg₂ : (of j) g₂ = x
hx : ¬x ∈ (base φ).range
⊢ False

Tactic:
have hx1 : x ≠ 1 := by rintro rfl; simp_all only [ne_eq, one_mem, not_true_eq_false]

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
x : PushoutI φ
g₁ : G i
hg₁ : (of i) g₁ = x
g₂ : G j
hg₂ : (of j) g₂ = x
hx : ¬x ∈ (base φ).range
hx1 : x ≠ 1
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case neg.inr
G : Type u_1
inst✝⁴ : Group G
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : IsCyclic 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
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
k : K
hk : ¬ϕ k = 1
u v : ZMod (Nat.card G)
hvu : v.cast * u.cast ≡ 1 [ZMOD ↑(Nat.card G)]
hu : ↑u.cast = ϕ k - 1
p : G
⊢ k • p ^ v.cast * (p ^ v.cast)⁻¹ = p ^ 1

Tactic:
h (p ^ v.cast) k u.cast hu.symm,

Goal state after:
case neg.inr
G : Type u_1
inst✝⁴ : Group G
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : IsCyclic 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
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
k : K
hk : ¬ϕ k = 1
u v : ZMod (Nat.card G)
hvu : v.cast * u.cast ≡ 1 [ZMOD ↑(Nat.card G)]
hu : ↑u.cast = ϕ k - 1
p : G
⊢ (p ^ v.cast) ^ u.cast = p ^ 1
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
inst✝ : (↑P).Normal
K : Subgroup G
hK : K.IsComplement' ↑P
h : K ⊔ ↑P ≤ Subgroup.centralizer ↑↑P
⊢ ↑P ≤ Subgroup.center G

Tactic:
rwa [hK.sup_eq_top, top_le_iff, Subgroup.centralizer_eq_top_iff_subset] at h

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 β
inst✝ : Countable ι
κ : ι → ι → Kernel α β
a : α
s : Set β
a✝ : MeasurableSet s
⊢ (Measure.sum fun n ↦ Measure.sum fun n_1 ↦ (κ n n_1) a) s = (Measure.sum fun n ↦ Measure.sum fun n_1 ↦ (κ n_1 n) a) s

Tactic:
rw [Measure.sum_comm]

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

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

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
f : β ≃ᵐ γ
η : Kernel α γ
⊢ κ.map ⇑f = η ↔ κ = η.map ⇑f.symm

Tactic:
by
  simp_rw [Kernel.ext_iff, map_apply _ f.measurable, map_apply _ f.symm.measurable,
    f.map_apply_eq_iff_map_symm_apply_eq]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set (α × α)
hs : MeasurableSet s
h_meas : ∀ (a : α), MeasurableSet (Prod.mk a ⁻¹' s)
⊢ ∫⁻ (a : α), (Function.diag ⁻¹' s).indicator 1 a ∂μ = μ (Function.diag ⁻¹' s)

Tactic:
rw [lintegral_indicator_one]
    exact (measurable_id.prod measurable_id) hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
hg : Measurable g
⊢ comap 0 g hg = 0

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ κ.comap id ⋯ = κ

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
g : γ → α
κ : Kernel α β
f : δ → γ
hf : Measurable f
hg : Measurable g
⊢ κ.comap (g ∘ f) ⋯ = (κ.comap g hg).comap f hf

Tactic:
ext; simp

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 α β
⊢ prodMkLeft γ (κ + η) = prodMkLeft γ κ + prodMkLeft γ η

Tactic:
ext; simp

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 α β
⊢ prodMkRight γ (κ + η) = prodMkRight γ κ + prodMkRight γ η

Tactic:
ext; simp

Goal state after: