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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : MulAction G A
H : Subgroup G
inst✝ : H.Normal
g : G
hg : g ∈ H
⊢ g ∈ toEndHom.ker

Tactic:
funext a; ext; exact a.2 ⟨g, hg⟩

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

Goal state before:
pp: case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = 1
⊢ ⟨Perm.ofSubtype g, ⋯⟩ ∈ stabilizer (↥(alternatingGroup α)) s

Tactic:
rw [mem_stabilizer_iff, Submonoid.mk_smul]
      exact ofSubtype_mem_stabilizer g

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = -1
x : ↑s
⊢ k ↑x = ↑x

Tactic:
rw [Set.disjoint_left] at hk_support

Goal state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : ∀ ⦃a : α⦄, a ∈ s → a ∉ ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = -1
x : ↑s
⊢ k ↑x = ↑x
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα✝ : univ.encard = 2
x✝ : Finite α
hα : Nat.card α = 2
⊢ Nat.Prime (Nat.factorial 2)

Tactic:
Nat.factorial_two

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα✝ : univ.encard = 2
x✝ : Finite α
hα : Nat.card α = 2
⊢ Nat.Prime 2
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case hM
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
⊢ stabilizer (↥G) s ≠ ⊤

Tactic:
contrapose hG

Goal state after:
case hM
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ stabilizer M s, g • a = b
hG : stabilizer (↥G) s = ⊤
⊢ ¬stabilizer M s < G
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        s.ncard = n + 1 →
          n + 2 < Nat.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → Finite α → IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
⊢ IsPreprimitive ↥(stabilizer G a) ↥(ofStabilizer G a)

Tactic:
rw [← is_one_preprimitive_iff]

Goal state after:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        s.ncard = n + 1 →
          n + 2 < Nat.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → Finite α → IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
⊢ IsMultiplyPreprimitive (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝ : Finite α
s : Set α
hs_nonempty : s.Nonempty
hsc_nonempty : sᶜ.Nonempty
hα : Nat.card α ≠ 2 * s.ncard
h : sᶜ.ncard < s.ncard
⊢ IsCoatom (stabilizer (Perm α) s)

Tactic:
rw [← stabilizer_compl]
    apply isCoatom_stabilizer_of_ncard_lt_ncard_compl hsc_nonempty
    rwa [compl_compl]

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

Goal state before:
pp: case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≤ 2
⊢ Nat.factorial 2 ≤ Fintype.card ↥G

Tactic:
Nat.factorial_two

Goal state after:
case inl
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≤ 2
⊢ 2 ≤ Fintype.card ↥G
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg.inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
hcan : ¬Cancels 1 w
⊢ of ↑((toSubgroupEquiv φ 1) (⋯.equiv w.head).1) *
      (t ^ ↑1 * (of ↑(⋯.equiv w.head).2 * (of w.head)⁻¹ * ReducedWord.prod φ w.toReducedWord)) =
    t ^ ↑1 * ReducedWord.prod φ w.toReducedWord

Tactic:
simp only [toSubgroup_neg_one, toSubgroup_one, toSubgroupEquiv_one, equiv_eq_conj, mul_assoc,
        Units.val_one, zpow_one, inv_mul_cancel_left, mul_right_inj]
      erw [(d.compl 1).equiv_snd_eq_inv_mul]
      simp [mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case cons.refine_1
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
⊢ ReducedWord.prod φ ((t ^ ↑a.1 * of a.2) • w').toReducedWord =
    ReducedWord.prod φ { head := 1, toList := a :: l, chain := chain }

pp: case cons.refine_2
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
a : ℤˣ × G
l : List (ℤˣ × G)
chain : List.IsChain (fun a b ↦ a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) (a :: l)
w' : NormalWord d
hw'1 : ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := l, chain := ⋯ }
hw'2 : List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList
hw'3 : ∀ u ∈ Option.map Prod.fst { head := 1, toList := l, chain := ⋯ }.toList.head?, w'.head ∈ toSubgroup A B (-u)
⊢ List.map Prod.fst ((t ^ ↑a.1 * of a.2) • w').toList =
      List.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList ∧
    ∀ u ∈ Option.map Prod.fst { head := 1, toList := a :: l, chain := chain }.toList.head?,
      ((t ^ ↑a.1 * of a.2) • w').head ∈ toSubgroup A B (-u)

Tactic:
· rw [prod_smul, hw'1]
      simp [ReducedWord.prod]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
c : ↥g.cycleFactorsFinset
⊢ #(↑(((toPermHom g) k) c)).support = #(↑c).support

Tactic:
coe_toPermHom,

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : ↥(centralizer {g})
c : ↥g.cycleFactorsFinset
⊢ #(↑k * ↑c * (↑k)⁻¹).support = #(↑c).support
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : IsMulCommutative ↥H
inst✝ : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ ⟨(unop g)⁻¹ * ↑1 * unop g, ⋯⟩ = 1

Tactic:
rw [Subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_cancel]

Goal state after:
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: case refine_1
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
h6 : (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime (map (QuotientGroup.mk' K) N).index
H : Subgroup (G ⧸ K)
hH : (map (QuotientGroup.mk' K) N).IsComplement' H
key : comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = N
⊢ comap (QuotientGroup.mk' K) ⊤ = ⊤

pp: case refine_1.hf
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
h6 : (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime (map (QuotientGroup.mk' K) N).index
H : Subgroup (G ⧸ K)
hH : (map (QuotientGroup.mk' K) N).IsComplement' H
key : comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = N
⊢ Function.Surjective ⇑(QuotientGroup.mk' K)

Tactic:
comap_top

Goal state after:
case refine_1
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
h6 : (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime (map (QuotientGroup.mk' K) N).index
H : Subgroup (G ⧸ K)
hH : (map (QuotientGroup.mk' K) N).IsComplement' H
key : comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = N
⊢ ⊤ = ⊤

case refine_1.hf
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
h6 : (Nat.card ↥(map (QuotientGroup.mk' K) N)).Coprime (map (QuotientGroup.mk' K) N).index
H : Subgroup (G ⧸ K)
hH : (map (QuotientGroup.mk' K) N).IsComplement' H
key : comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = N
⊢ Function.Surjective ⇑(QuotientGroup.mk' K)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
n : ℕ
hg : orderOf g ∣ 2 ^ n
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : 4 ≤ 4
hk1 : 1 < 4
hg0 : 4 ≠ 2
t : Multiset ℕ
h1 : t = Multiset.replicate t.card 0
ht : g.cycleType = 4 ::ₘ t
h : 0 ∉ g.cycleType
⊢ t = 0

Tactic:
simpa [h1 ▸ ht, Multiset.mem_replicate] using h

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

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
N : Subgroup (Perm α)
inst✝ : N.Normal
ntN : Nontrivial ↥N
this : IsPreprimitive (Perm α) ↑(Set.powersetCard α 2)
⊢ _root_.commutator (Perm α) ≤ N

Tactic:
classical
  apply iwasawaStructure_two.commutator_le
  exact fixedPoints_ne_univ_of_faithfulSMul (by norm_num) (by grind)

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

Goal state before:
pp: ⊢ IsCyclic (QuaternionGroup 1)

Tactic:
by
  apply isCyclic_of_orderOf_eq_card
  · rw [Nat.card_eq_fintype_card, card, mul_one]
    exact orderOf_xa 0

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

Goal state before:
pp: case inl
⊢ Monoid.exponent (QuaternionGroup 0) = 0

Tactic:
exact Monoid.exponent_eq_zero_of_order_zero orderOf_a_one

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

Goal state before:
pp: case inr.a.a
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ a m ^ lcm (2 * n) 4 = 1

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_a]

Goal state after:
case inr.a.a
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 2 * n / (2 * n).gcd m.val ∣ lcm (2 * n) 4
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
⊢ Nat.card ↥↑P ∣ Monoid.exponent G

Tactic:
← (isZGroup p hp P).exponent_eq_card

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
⊢ Monoid.exponent ↥↑P ∣ Monoid.exponent G
Module: Mathlib.InformationTheory.Coding.UniquelyDecodable

Goal state before:
pp: α : Type u_1
S : Set (List α)
h : UniquelyDecodable S
L₁ L₂ : { L // ∀ (x : List α), x ∈ L → x ∈ S }
hflat : (fun L ↦ (↑L).flatten) L₁ = (fun L ↦ (↑L).flatten) L₂
⊢ ↑L₁ = ↑L₂

Tactic:
exact h L₁.val L₂.val L₁.prop L₂.prop hflat

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
⊢ { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h

Tactic:
simp [NormalWord.prod]

Goal state after:
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
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g

Tactic:
· obtain ⟨⟨u, v, -, hvu⟩, hu : u = ϕ k - 1⟩ := (hG k).resolve_left hk
    rw [← u.intCast_zmod_cast] at hu hvu
    rw [← v.intCast_zmod_cast, ← Int.cast_mul, ← Int.cast_one, ZMod.intCast_eq_intCast_iff] at hvu
    refine Or.inr fun p ↦ zpow_one p ▸ ⟨k, p ^ (v.cast : ℤ), ?_⟩
    rw [h (p ^ v.cast) k u.cast hu.symm, ← zpow_mul, zpow_eq_zpow_iff_modEq]
    exact hvu.of_dvd (Int.natCast_dvd_natCast.mpr (orderOf_dvd_natCard p))

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 ∂(piecewise hs κ η) a = if a ∈ s then ∫⁻ (b : β), g b ∂κ a else ∫⁻ (b : β), g b ∂η a

Tactic:
simp_rw [piecewise_apply]

Goal state after:
α : 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
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 ∂(piecewise hs κ η) a = if a ∈ s then ∫⁻ (b : β) in t, g b ∂κ a else ∫⁻ (b : β) in t, g b ∂η a

Tactic:
simp_rw [piecewise_apply]

Goal state after:
α : 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
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
⊢ Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)

Tactic:
← Kernel.kernel_sum_seq κ

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
⊢ Measurable fun a ↦ ((Kernel.sum κ.seq) a) (Prod.mk a ⁻¹' t)
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 δ
f : β → γ
g : γ → α
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
hg : Measurable g
⊢ IsZeroOrMarkovKernel (κ.comap g hg)

Tactic:
by
  rcases eq_zero_or_isMarkovKernel κ with rfl | h
  · simp only [comap_zero]; infer_instance
  · have := IsMarkovKernel.comap κ hg; infer_instance

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

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α × γ
⊢ (η a.2) Set.univ ≤ η.bound

Tactic:
· exact measure_le_bound η a.2 Set.univ

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 α β
⊢ (Kernel.sum fun i ↦ prodMkRight γ (κ i)) = prodMkRight γ (Kernel.sum κ)

Tactic:
ext
  simp_rw [sum_apply, prodMkRight_apply, sum_apply]

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

Goal state before:
pp: case pos.e_f.e_f
X : Type u_1
Y : Type u_2
Z : Type u_3
T : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
mT : MeasurableSpace T
κ : Kernel X Y
X' : Type u_5
mX' : MeasurableSpace X'
η : Kernel X' Z
inst✝¹ : IsSFiniteKernel η
ξ : Kernel Z T
inst✝ : IsSFiniteKernel ξ
hκ : IsSFiniteKernel κ
a : X × X'
s : Set (Y × T)
hs : MeasurableSet s
x : Y
y : Z
⊢ ((Kernel.id ∥ₖ ξ) (x, y)) s = (ξ y) (Prod.mk x ⁻¹' s)

Tactic:
rw [parallelComp_apply' hs, Kernel.id_apply,
    lintegral_dirac' _ (measurable_measure_prodMk_left hs)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ (μ ⊗ₘ κ).snd s = ∫⁻ (a : α), (κ a) s ∂μ

Tactic:
snd_apply hs,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
inst✝¹ : SFinite μ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
s : Set β
hs : MeasurableSet s
⊢ (μ ⊗ₘ κ) (Prod.snd ⁻¹' s) = ∫⁻ (a : α), (κ a) s ∂μ
Module: Mathlib.Probability.Kernel.MeasurableIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun x ↦ ∫ (y : β), f y ∂κ x

Tactic:
by
  by_cases hE : CompleteSpace E; swap
  · simp [integral, hE, stronglyMeasurable_const]
  borelize E
  have : TopologicalSpace.SeparableSpace (range f ∪ {0} : Set E) :=
    hf.separableSpace_range_union_singleton
  let s : ℕ → SimpleFunc β E := SimpleFunc.approxOn _ hf.measurable (range f ∪ {0}) 0 (by simp)
  let f' n : α → E := {x | Integrable f (κ x)}.indicator fun x ↦ (s n).integral (κ x)
  refine stronglyMeasurable_of_tendsto (f := f') atTop (fun n ↦ ?_) ?_
  · refine StronglyMeasurable.indicator ?_ (measurableSet_integrable hf)
    simp_rw [SimpleFunc.integral_eq]
    refine Finset.stronglyMeasurable_fun_sum _ fun _ _ ↦ ?_
    refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _
    exact κ.measurable_coe ((s n).measurableSet_fiber _)
  · rw [tendsto_pi_nhds]; intro x
    by_cases hfx : Integrable f (κ x)
    · simp only [mem_ofPred_eq, hfx, indicator_of_mem, f']
      apply tendsto_integral_approxOn_of_measurable_of_range_subset _ hfx
      exact subset_rfl
    · simp [f', hfx, integral_undef]

Goal state after: