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

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
H : Type u_3
β : Type u_4
inst✝² : Group H
inst✝¹ : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective ⇑f
inst✝ : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (n ↪ β) → n ↪ α := fun x ↦ x.trans (Function.Embedding.ofSurjective (⇑f) hf)
aux_apply : ∀ (x : n ↪ β) (i : n), f.toFun ((aux x) i) = x i
g : G
hg : ∀ (x_1 : n), (g • aux x) x_1 = (aux y) x_1
i : n
⊢ (σ g • x) i = y i

Tactic:
smul_apply

Goal state after:
case h
G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
H : Type u_3
β : Type u_4
inst✝² : Group H
inst✝¹ : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective ⇑f
inst✝ : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (n ↪ β) → n ↪ α := fun x ↦ x.trans (Function.Embedding.ofSurjective (⇑f) hf)
aux_apply : ∀ (x : n ↪ β) (i : n), f.toFun ((aux x) i) = x i
g : G
hg : ∀ (x_1 : n), (g • aux x) x_1 = (aux y) x_1
i : n
⊢ σ g • x i = y i
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
g✝ g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
habG : swap x y ∈ G
⊢ ⋯.choose * swap x y * ⋯.choose⁻¹ ∈ G

Tactic:
exact (normal_of_index_eq_two hG).conj_mem _ habG _

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := append x
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := append y
hy : y' = append y
g : G
hg : g • x' = y'
a : ↑s
i : Fin s.ncard := (Classical.choice Hs).symm a
⊢ (Classical.choice Hs) i = a

Tactic:
simp [i]

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

Goal state before:
pp: case h.left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
hk : k ∈ fixingSubgroup M s
⊢ (MulAut.conj g⁻¹) k ∈ fixingSubgroup M t

Tactic:
apply Set.conj_mem_fixingSubgroup _ hk

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
hk : k ∈ fixingSubgroup M s
⊢ g⁻¹ • s = t
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : ⟨a, ha⟩ ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
this : a ∈ ofFixingSubgroup M (s ∪ t)
⊢ ∃ a_1, (map_ofFixingSubgroupUnion M s t) a_1 = ⟨⟨a, ha⟩, ha'⟩

Tactic:
exact ⟨⟨a, this⟩,  rfl⟩

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

Goal state before:
pp: case inl
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
n : ℕ
hα : ↑n.succ ≤ ENat.card α
inst✝ : IsMultiplyPretransitive M α n.succ
hn : n = 0
⊢ IsMultiplyPreprimitive M α 0

Tactic:
exact is_zero_preprimitive M α

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : Nat.card α ≤ 2
⊢ IsTrivialBlock B

pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
⊢ IsTrivialBlock B

Tactic:
· exact isTrivialBlock_of_card_le_two h2 B

Goal state after:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
⊢ IsTrivialBlock B
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this✝ : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha✝ : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
htm : t.ncard = t.ncard - 1 + 1
hmn : t.ncard - 1 < n
htm' : t.ncard - 1 + 2 < Nat.card α
hsgs_ne_top : s ∪ g • s ≠ ⊤
this : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
⊢ (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)

Tactic:
refine ⟨this, fun hs_prim ↦ ?_⟩
      apply (hrec _ hmn hG htm htm').2
      exact IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
          hs_prim hsgs_ne_top

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
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
⊢ ⇑S.rightHom = ⇑S'.rightHom ∘ ⇑equiv.toMulEquiv

Tactic:
← equiv.rightHom_comm

Goal state after:
N : Type u_1
E : Type u_2
G : Type u_3
inst✝³ : Group N
inst✝² : Group E
inst✝¹ : Group G
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
equiv : S.Equiv S'
⊢ ⇑S'.rightHom ∘ ⇑equiv.toMulEquiv = ⇑S'.rightHom ∘ ⇑equiv.toMulEquiv
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: α : 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 α
φ : K →* Perm α := toPermHom K α
f : α →ₑ[⇑φ] α := { toFun := id, map_smul' := ⋯ }
hf : Function.Bijective ⇑f
this : Function.Surjective ⇑φ
⊢ IsPretransitive (Perm α) (Fin (Nat.card α) ↪ α)

Tactic:
apply Perm.isMultiplyPretransitive

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ⁅⊤, ⊤⁆ = ⊤ ↔ _root_.commutator G = ⊤

Tactic:
commutator_def

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ ⁅⊤, ⊤⁆ = ⊤ ↔ ⁅⊤, ⊤⁆ = ⊤
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ IsPerfect ↥⊤ ↔ IsPerfect G

Tactic:
by
  rw [isPerfect_def, isPerfect_def, ← map_subtype_inj,
    map_subtype_commutator, ← MonoidHom.range_eq_map, subtype_range, commutator_def]

Goal state after:
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
⊢ ⁅_root_.commutator G, Subgroup.upperCentralSeries G 2⁆ = ⊥

Tactic:
commutator_def

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsPerfect G
n : ℕ
hn : n ≠ 0
⊢ ⁅⁅⊤, ⊤⁆, Subgroup.upperCentralSeries G 2⁆ = ⊥
Module: Mathlib.GroupTheory.HNNExtension

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

Tactic:
dif_neg hcan

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
⊢ (let g' := unitsSMulGroup φ d 1 (↑g • w).head;
    cons (↑g'.1) 1 ((↑g'.2 * (↑g • w).head⁻¹) • ↑g • w) ⋯ ⋯) =
    ↑(φ g) •
      let g' := unitsSMulGroup φ d 1 w.head;
      cons (↑g'.1) 1 ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
g : Perm α
⊢ f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ

Tactic:
simp only [funext_iff]

Goal state after:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
g : Perm α
⊢ (∀ (x : α), (f ∘ ⇑g) x = f x) ↔ ∀ (x : α), (φ ∘ ⇑g) x = φ x
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
w : ReducedWord G A B
g : G
l : List (ℤˣ × G)
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l
hw1 : { head := g, toList := l, chain := chain }.head = 1
⊢ ∃ w',
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := g, toList := l, chain := chain } ∧
      List.map Prod.fst w'.toList = List.map Prod.fst { head := g, toList := l, chain := chain }.toList ∧
        ∀ u ∈ Option.map Prod.fst { head := g, toList := l, chain := chain }.toList.head?, w'.head ∈ toSubgroup A B (-u)

Tactic:
dsimp at hw1

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
g : G
l : List (ℤˣ × G)
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) l
hw1 : g = 1
⊢ ∃ w',
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := g, toList := l, chain := chain } ∧
      List.map Prod.fst w'.toList = List.map Prod.fst { head := g, toList := l, chain := chain }.toList ∧
        ∀ u ∈ Option.map Prod.fst { head := g, toList := l, chain := chain }.toList.head?, w'.head ∈ toSubgroup A B (-u)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : ↥g.cycleFactorsFinset
a✝¹ : c ∈ ↑(↑τ).support
d : ↥g.cycleFactorsFinset
a✝ : d ∈ ↑(↑τ).support
h : c ≠ d
⊢ Function.onFun _root_.Disjoint (fun c ↦ (↑c).support) c d

Tactic:
apply Equiv.Perm.Disjoint.disjoint_support

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : ↥g.cycleFactorsFinset
a✝¹ : c ∈ ↑(↑τ).support
d : ↥g.cycleFactorsFinset
a✝ : d ∈ ↑(↑τ).support
h : c ≠ d
⊢ (↑c).Disjoint ↑d
Module: Mathlib.GroupTheory.RegularWreathProduct

Goal state before:
pp: D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
G✝ : Type u
n✝ : ℕ
inst✝³ : Group G✝
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst✝² : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst✝¹ : Group G
inst✝ : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
e1 : α ≃ (Fin n → G) := (Finite.equivFinOfCardEq hα).trans (Finite.equivFinOfCardEq ⋯).symm
f : IteratedWreathProduct G n →* Equiv.Perm α := e1.symm.permCongrHom.toMonoidHom.comp (iteratedWreathToPermHom G n)
hf : Function.Injective ⇑f
g : ↥f.range ≃* IteratedWreathProduct G n := (MonoidHom.ofInjective hf).symm
⊢ p ^ ∑ i ∈ Finset.range n, p ^ i = p ^ (p ^ n).factorial.factorization p

Tactic:
← Nat.multiplicity_eq_factorization hp.out (p ^ n).factorial_ne_zero,

Goal state after:
D : Type u_1
Q : Type u_2
inst✝⁵ : Group D
inst✝⁴ : Group Q
G✝ : Type u
n✝ : ℕ
inst✝³ : Group G✝
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst✝² : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst✝¹ : Group G
inst✝ : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
e1 : α ≃ (Fin n → G) := (Finite.equivFinOfCardEq hα).trans (Finite.equivFinOfCardEq ⋯).symm
f : IteratedWreathProduct G n →* Equiv.Perm α := e1.symm.permCongrHom.toMonoidHom.comp (iteratedWreathToPermHom G n)
hf : Function.Injective ⇑f
g : ↥f.range ≃* IteratedWreathProduct G n := (MonoidHom.ofInjective hf).symm
⊢ p ^ ∑ i ∈ Finset.range n, p ^ i = p ^ multiplicity p (p ^ n).factorial
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : ∀ (g : G), g ≠ 1 → ∃ H x, ∃ (_ : Finite H), ∃ f, f g ≠ 1
g : G
hg : g ≠ 1
w✝² : Type u
w✝¹ : Group w✝²
w✝ : Finite w✝²
f : G →* w✝²
hf : f g ≠ 1
⊢ g ∉ f.ker

Tactic:
simpa using hf

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
⊢ Odd ((card ∘ support) c)

Tactic:
suffices sign c = 1 by
    rw [IsCycle.sign _, neg_eq_iff_eq_neg, ← Int.units_ne_iff_eq_neg] at this
    · rw [← Nat.not_even_iff_odd, comp_apply]
      exact fun h ↦ this h.neg_one_pow
    · rw [mem_cycleFactorsFinset_iff] at hc
      exact hc.left

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ sign c = 1
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 ↥N
inst✝ : (map N.subtype K).Normal
key : map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = map N.subtype ⊤
⊢ K = ⊥ ∨ K = ⊤

Tactic:
rwa [map_subtype_inj, map_subtype_inj] at key

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 : ↥(kleinFour α)), orderOf g ∣ 2

Tactic:
rintro ⟨⟨g, hg⟩, hg'⟩

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ kleinFour α
⊢ orderOf ⟨⟨g, hg⟩, hg'⟩ ∣ 2
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
this : IsPreprimitive ↥(alternatingGroup α) ↑(Set.powersetCard α 3)
⊢ _root_.commutator ↥(alternatingGroup α) ≤ N

Tactic:
apply iwasawaStructure_three.commutator_le

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 6
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
this : IsPreprimitive ↥(alternatingGroup α) ↑(Set.powersetCard α 3)
⊢ fixedPoints ↥N ↑(Set.powersetCard α 3) ≠ Set.univ
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

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

Tactic:
mul_zero,

Goal state after:
case inl
⊢ orderOf (a 1) = 0
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hG' : IsCyclic ↥↑Q
hQ : Subgroup.comap f ↑Q = ↑P
h : Subgroup.map f ↑P ≤ ↑Q
this : IsCyclic ↥(Subgroup.map f ↑P)
⊢ IsCyclic ↥↑P

Tactic:
exact isCyclic_of_surjective _ (Subgroup.equivMapOfInjective P f hf).symm.surjective

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ IsCyclic ↥(commutator G)

Tactic:
commutator_def

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ IsCyclic ↥⁅⊤, ⊤⁆
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case ind.inl
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
hH : ∀ y < ⊥, IsCyclic ↥⁅y, y⁆
⊢ IsCyclic ↥⁅⊥, ⊥⁆

pp: case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
hH : ∀ y < H, IsCyclic ↥⁅y, y⁆
h : H ≠ ⊥
⊢ IsCyclic ↥⁅H, H⁆

Tactic:
· rw [Subgroup.commutator_bot_left]
    infer_instance

Goal state after:
case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
hH : ∀ y < H, IsCyclic ↥⁅y, y⁆
h : H ≠ ⊥
⊢ IsCyclic ↥⁅H, H⁆
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
hx1 : x ≠ 1
hg₁1 : g₁ ≠ 1
hg₂1 : g₂ ≠ 1
hg₁r : g₁ ∉ (φ i).range
hg₂r : g₂ ∉ (φ j).range
w : Word G := { toList := [⟨i, g₁⟩, ⟨j, g₂⁻¹⟩], ne_one := ⋯, chain_ne := ⋯ }
hw : Reduced φ w
⊢ ofCoprodI w.prod ∈ (base φ).range

Tactic:
simp only [w, Word.prod, List.map_cons, List.prod_cons, List.prod_nil,
          List.map_nil, map_mul, ofCoprodI_of, hg₁, hg₂, map_inv, mul_one,
          mul_inv_cancel, one_mem]

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)
inst✝² : Finite G
P : Sylow p G
inst✝¹ : IsCyclic ↥↑P
inst✝ : (↑P).Normal
K : Subgroup G
hK : K.IsComplement' ↑P
h : ⁅K, ↑P⁆ = ↑P
⊢ ⁅K, ↑P⁆ ≤ commutator G

Tactic:
commutator_def

Goal state after:
case refine_2
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⁆ = ↑P
⊢ ⁅K, ↑P⁆ ≤ ⁅⊤, ⊤⁆
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)
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 : ↑P ≤ ⁅Subgroup.normalizer ↑↑P, Subgroup.normalizer ↑↑P⁆
⊢ ↑P ≤ commutator G

Tactic:
exact h.trans (Subgroup.commutator_mono le_top le_top)

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✝ : IsZeroOrMarkovKernel κ
a : α
⊢ IsZeroOrProbabilityMeasure (κ a)

Tactic:
rcases eq_zero_or_isMarkovKernel κ with rfl | h'
  · simp only [zero_apply]
    infer_instance
  · infer_instance

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 α β
f : α → β
hf : Measurable f
⊢ Measurable fun a ↦ Measure.dirac (f a)

Tactic:
by
    refine Measure.measurable_of_measurable_coe _ fun s hs => ?_
    simp_rw [Measure.dirac_apply' _ hs]
    exact measurable_one.indicator (hf hs)

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 α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
i : ℕ
⊢ ((if i = 0 then κ else 0) a) s = if i = 0 then (κ a) s else 0

Tactic:
split_ifs <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
t : Set β
⊢ (if a ∈ s then κ a else η a) t = if a ∈ s then (κ a) t else (η a) t

Tactic:
split_ifs <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → ℝ≥0∞
⊢ (∫⁻ (b : β), g b ∂if a ∈ s then κ a else η a) = if a ∈ s then ∫⁻ (b : β), g b ∂κ a else ∫⁻ (b : β), g b ∂η a

Tactic:
split_ifs <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
g : β → ℝ≥0∞
t : Set β
⊢ (∫⁻ (b : β) in t, g b ∂if a ∈ s then κ a else η a) =
    if a ∈ s then ∫⁻ (b : β) in t, g b ∂κ a else ∫⁻ (b : β) in t, g b ∂η a

Tactic:
split_ifs <;> rfl

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
a : α
s : Set (α × α)
hs : MeasurableSet s
⊢ (((copy α) a).bind ⇑(swap α α)) s = ((copy α) a) s

Tactic:
copy_apply,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
a : α
s : Set (α × α)
hs : MeasurableSet s
⊢ ((Measure.dirac (a, a)).bind ⇑(swap α α)) s = (Measure.dirac (a, a)) s
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 : β), ((copy β) b) (s ×ˢ t) ∂κ a = (κ a) (s ∩ t)

Tactic:
copy_apply,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β), (Measure.dirac (b, b)) (s ×ˢ t) ∂κ a = (κ a) (s ∩ t)
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: case inr
α : 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 δ
f : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
hg : Measurable g
h : IsMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap g hg)

Tactic:
have := IsMarkovKernel.comap κ hg; 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 α β
a : ℝ≥0∞
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
⊢ (a • μ) ⊗ₘ κ = a • μ ⊗ₘ κ

Tactic:
ext s hs
  simp only [compProd_apply hs, lintegral_smul_measure, smul_apply, smul_eq_mul]

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 (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
⊢ (((copy α) a).bind
        ⇑(swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β) ∘ₖ
            (Kernel.id ∥ₖ κ)))
      s =
    ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂κ a

Tactic:
copy_apply,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
⊢ ((Measure.dirac (a, a)).bind
        ⇑(swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β) ∘ₖ
            (Kernel.id ∥ₖ κ)))
      s =
    ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂κ a