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

Goal state before:
pp: case hf
G : Type u_1
inst✝⁴ : Group G
α : Type u_2
inst✝³ : MulAction G α
inst✝² : DecidableEq α
inst✝¹ : Nontrivial G
inst✝ : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h : (toPermHom G ↑(powersetCard α n)) g = 1
⊢ Function.Injective ⇑(toPermHom G ↑(powersetCard α n))

Tactic:
have := powersetCard.faithfulSMul (G := G) (α := α) hn ?_

Goal state after:
case hf.refine_2
G : Type u_1
inst✝⁴ : Group G
α : Type u_2
inst✝³ : MulAction G α
inst✝² : DecidableEq α
inst✝¹ : Nontrivial G
inst✝ : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h : (toPermHom G ↑(powersetCard α n)) g = 1
this : FaithfulSMul G ↑(powersetCard α n)
⊢ Function.Injective ⇑(toPermHom G ↑(powersetCard α n))

case hf.refine_1
G : Type u_1
inst✝⁴ : Group G
α : Type u_2
inst✝³ : MulAction G α
inst✝² : DecidableEq α
inst✝¹ : Nontrivial G
inst✝ : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h : (toPermHom G ↑(powersetCard α n)) g = 1
⊢ ↑n < ENat.card α
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: case neg
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this✝ :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
this : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α (Nat.card α - n))
hn' : ¬n ≤ Nat.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)

Tactic:
suffices Subsingleton (powersetCard α n) by infer_instance

Goal state after:
case neg
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
this✝ :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_1 : Fintype α],
    3 ≤ Nat.card α → 2 * n ≤ Nat.card α → IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α n)
hn : Nat.card α < 2 * n
this : IsPretransitive ↥(alternatingGroup α) ↑(powersetCard α (Nat.card α - n))
hn' : ¬n ≤ Nat.card α
⊢ Subsingleton ↑(powersetCard α n)
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
u : ℤˣ
a : ↥(toSubgroup A B u)
⊢ ↑((toSubgroupEquiv φ (-u)) ((toSubgroupEquiv φ u) a)) = ↑a

Tactic:
rcases Int.units_eq_one_or u with rfl | rfl

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B 1)
⊢ ↑((toSubgroupEquiv φ (-1)) ((toSubgroupEquiv φ 1) a)) = ↑a

case inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B (-1))
⊢ ↑((toSubgroupEquiv φ (- -1)) ((toSubgroupEquiv φ (-1)) a)) = ↑a
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 : ℤˣ
g : G
⊢ (unitsSMulGroup φ d u g).2 = (⋯.equiv g).2

Tactic:
rcases Int.units_eq_one_or u with rfl | rfl

Goal state after:
case inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
⊢ (unitsSMulGroup φ d 1 g).2 = (⋯.equiv g).2

case inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
⊢ (unitsSMulGroup φ d (-1) g).2 = (⋯.equiv g).2
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
a : M
⊢ (f.noncommCoprod g comm) (a, 1) = f a

Tactic:
noncommCoprod_apply,

Goal state after:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
a : M
⊢ f (a, 1).1 * g (a, 1).2 = f a
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
a : N
⊢ (f.noncommCoprod g comm) (1, a) = g a

Tactic:
noncommCoprod_apply,

Goal state after:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
a : N
⊢ f (1, a).1 * g (1, a).2 = g a
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg.inr
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, toSubgroupEquiv_neg_one, Units.val_neg, Units.val_one,
        Int.reduceNeg, zpow_neg, zpow_one, mul_assoc]
      erw [equiv_symm_eq_conj, (d.compl (-1)).equiv_snd_eq_inv_mul]
      simp [mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case t
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : NormalWord d
⊢ ReducedWord.prod φ (t • w).toReducedWord = t * ReducedWord.prod φ w.toReducedWord

Tactic:
| t =>

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ Function.fixedPoints ⇑g
⊢ x ∈ (↑(↑τ c)).support ↔ x ∈ (↑c).support

Tactic:
suffices ∀ (d : g.cycleFactorsFinset), x ∉ (d : Perm α).support by
      simp only [this]

Goal state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∈ Function.fixedPoints ⇑g
⊢ ∀ (d : ↥g.cycleFactorsFinset), x ∉ (↑d).support
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
⊢ a.ofPermHomFun 1 x = x

Tactic:
rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | ⟨c, hc, m, hm⟩)
  · rw [ofPermHomFun_apply_of_mem_fixedPoints a _ hx]
  · rw [ofPermHomFun_apply_of_cycleOf_mem a _ hc hm, OneMemClass.coe_one, coe_one, id_eq, hm]

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₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
d : TransversalPair G A B
w₁' : NormalWord d
hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁
hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList
hw₂'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂
hw₂'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₂.toList
hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₁.head • ↑(toSubgroup A B (-u))
hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₂.head • ↑(toSubgroup A B (-u))
u : ℤˣ
hu : u ∈ Option.map Prod.fst w₁.toList.head?
⊢ w₁.head • ↑(toSubgroup A B (-u)) = w₂.head • ↑(toSubgroup A B (-u))

Tactic:
rw [← hw₁'3 _ hu, ← hw₂'3 _]

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w₁ w₂ : ReducedWord G A B
hprod : ReducedWord.prod φ w₁ = ReducedWord.prod φ w₂
d : TransversalPair G A B
w₁' : NormalWord d
hw₁'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₁
hw₁'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₁.toList
hw₂'1 : ReducedWord.prod φ w₁'.toReducedWord = ReducedWord.prod φ w₂
hw₂'2 : List.map Prod.fst w₁'.toList = List.map Prod.fst w₂.toList
hw₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₁.head • ↑(toSubgroup A B (-u))
hw₂'3 : ∀ u ∈ Option.map Prod.fst w₂.toList.head?, w₁'.head • ↑(toSubgroup A B (-u)) = w₂.head • ↑(toSubgroup A B (-u))
u : ℤˣ
hu : u ∈ Option.map Prod.fst w₁.toList.head?
⊢ u ∈ Option.map Prod.fst w₂.toList.head?
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : ↥g.cycleFactorsFinset → ℕ := fun c ↦ #(↑c).support
hsc : sc = fun c ↦ #(↑c).support
this : Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
⊢ ∏ i ∈ Finset.image (fun c ↦ #(↑c).support) g.cycleFactorsFinset.attach, (Fintype.card { a // #(↑a).support = i })! =
    ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
simp_rw [← CycleType.count_def]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
sc : ↥g.cycleFactorsFinset → ℕ := fun c ↦ #(↑c).support
hsc : sc = fun c ↦ #(↑c).support
this : Fintype.card ↥(toPermHom g).range = Fintype.card ↑{k | sc ∘ ⇑k = sc}
⊢ ∏ x ∈ Finset.image (fun c ↦ #(↑c).support) g.cycleFactorsFinset.attach, (Multiset.count x g.cycleType)! =
    ∏ x ∈ g.cycleType.toFinset, (Multiset.count x g.cycleType)!
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
hs : sign g = 1
⊢ False

Tactic:
rw [g.sign_of_cycleType, hg, neg_one_pow_eq_one_iff_even (by simp)] at hs

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
hs : Even (m.sum + m.card)
⊢ False
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
x✝ : PushoutI φ →* K
⊢ ∀ (i : ι),
    ((fun f ↦ lift (↑f).1 (↑f).2 ⋯) ((fun f ↦ ⟨(fun i ↦ f.comp (of i), f.comp (base φ)), ⋯⟩) x✝)).comp (of i) =
      x✝.comp (of i)

Tactic:
by simp [DFunLike.ext_iff]

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
x✝ : PushoutI φ →* K
⊢ ((fun f ↦ lift (↑f).1 (↑f).2 ⋯) ((fun f ↦ ⟨(fun i ↦ f.comp (of i), f.comp (base φ)), ⋯⟩) x✝)).comp (base φ) =
    x✝.comp (base φ)

Tactic:
by simp [DFunLike.ext_iff]

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)
⊢ Nonempty (Transversal φ)

Tactic:
choose t ht using fun i => (φ i).range.exists_isComplement_right 1

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)
t : (i : ι) → Set (G i)
ht : ∀ (i : ι), IsComplement (↑(φ i).range) (t i) ∧ 1 ∈ t i
⊢ Nonempty (Transversal φ)
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case pos
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
w : Word G
i : ι
h✝ : H
hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → ↑(⋯.equiv g).2 = g
hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (CoprodI.of ((φ i) h✝) • w).toList → ↑(⋯.equiv g).2 = g
h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = i
⊢ ↑(⋯.equiv (⋯ ▸ (w.toList.head ⋯).snd)).2 = ⋯ ▸ (w.toList.head ⋯).snd

Tactic:
rcases h with ⟨_, rfl⟩
      exact hw _ _ (List.head_mem _)

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
w : NormalWord d
p : Word.Pair G i := (Word.equivPair i) (CoprodI.of ((φ i) w.head) • w.toWord)
j : ι
g : G j
hg :
  ⟨j, g⟩ ∈
    ((Word.equivPair i)
          (Word.rcons
            (have __src := (Word.equivPair i) w.toWord;
            { head := (φ i) w.head * ((Word.equivPair i) w.toWord).head, tail := __src.tail,
              fstIdx_ne := ⋯ }))).tail.toList
⊢ g ∈ d.set j

Tactic:
← Word.equivPair_symm,

Goal state after:
ι : 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 : ι
w : NormalWord d
p : Word.Pair G i := (Word.equivPair i) (CoprodI.of ((φ i) w.head) • w.toWord)
j : ι
g : G j
hg :
  ⟨j, g⟩ ∈
    ((Word.equivPair i)
          ((Word.equivPair i).symm
            (have __src := (Word.equivPair i) w.toWord;
            { head := (φ i) w.head * ((Word.equivPair i) w.toWord).head, tail := __src.tail,
              fstIdx_ne := ⋯ }))).tail.toList
⊢ g ∈ d.set j
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case e'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x ↦ ↑⟨c, hc⟩ ^ x) k = ↑(uv ⟨c, hc⟩)
⊢ Odd #(↑⟨c, hc⟩).support

Tactic:
apply h_odd

Goal state after:
case e'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm ↑(Function.fixedPoints ⇑g)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers ↑c)
hx : (kerParam g) (y, uv) ∈ (kerParam g).range
c : Perm α
hc : c ∈ g.cycleFactorsFinset
a✝ : ⟨c, hc⟩ ∈ univ
k : ℤ
hk : (fun x ↦ ↑⟨c, hc⟩ ^ x) k = ↑(uv ⟨c, hc⟩)
⊢ #(↑⟨c, hc⟩).support ∈ g.cycleType
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs : s.card = 4
g : Perm α
hg : g ∈ alternatingGroup α
k : Perm α
hk : k ∈ alternatingGroup α
⊢ ⟨k, hk⟩ ∈ Subgroup.map (ofSubtype (⟨g, hg⟩ • s)) (kleinFour ↥(⟨g, hg⟩ • s)) ↔
    ⟨k, hk⟩ ∈ MulAut.conj ⟨g, hg⟩ • Subgroup.map (ofSubtype s) (kleinFour ↥s)

Tactic:
Subgroup.mem_pointwise_smul_iff_inv_smul_mem,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
hs : s.card = 4
g : Perm α
hg : g ∈ alternatingGroup α
k : Perm α
hk : k ∈ alternatingGroup α
⊢ ⟨k, hk⟩ ∈ Subgroup.map (ofSubtype (⟨g, hg⟩ • s)) (kleinFour ↥(⟨g, hg⟩ • s)) ↔
    (MulAut.conj ⟨g, hg⟩)⁻¹ • ⟨k, hk⟩ ∈ Subgroup.map (ofSubtype s) (kleinFour ↥s)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: n k : ℕ
⊢ a 1 ^ k = a ↑k

Tactic:
by
  induction k with
  | zero => rw [Nat.cast_zero]; rfl
  | succ k IH =>
    rw [pow_succ, IH, a_mul_a]
    congr 1
    norm_cast

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 ≠ ⊥ → ⁅H, H⁆ < H

Tactic:
intro H h

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 : H ≠ ⊥
⊢ ⁅H, H⁆ < H
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
hG : Group.IsNilpotent G
this : ∀ (p : ↥(Nat.card G).primeFactors), Fact (Nat.Prime ↑p)
ϕ : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
g h : G
⊢ g * h = h * g

Tactic:
rw [← ϕ.symm.injective.eq_iff, map_mul, mul_comm, ← map_mul]

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 : ↑Q ≤ Subgroup.center ↥(Subgroup.normalizer ↑P)
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P

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 : ↑Q ≤ commutator ↥(Subgroup.normalizer ↑P)
⊢ ↑P ≤ commutator G

Tactic:
· rw [← SetLike.coe_subset_coe, ← Subgroup.centralizer_eq_top_iff_subset, eq_top_iff,
      ← Subgroup.map_subtype_le_map_subtype, ← MonoidHom.range_eq_map,
      (Subgroup.normalizer (P : Set G)).range_subtype] at h
    replace h := h.trans (Subgroup.map_centralizer_le_centralizer_image _ _)
    rwa [← Subgroup.coe_map, P.coe_subtype, ← P.coe_coe,
      Subgroup.map_subgroupOf_eq_of_le P.le_normalizer] at h

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
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : ↑Q ≤ commutator ↥(Subgroup.normalizer ↑P)
⊢ ↑P ≤ commutator G
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
x : α
s : Set β
a✝ : MeasurableSet s
⊢ ((const α 0) x) s = (0 x) s

Tactic:
simp [const_apply]

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 α β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
⊢ Measurable fun a ↦ Measure.comap f (κ a)

Tactic:
refine Measure.measurable_measure.mpr fun t ht => ?_
    have : (fun a => Measure.comap f (κ a) t) = fun a => κ a (f '' t) := by
      ext1 a
      rw [Measure.comap_apply _ hf.injective _ _ ht]
      exact fun s' hs' ↦ hf.measurableSet_image.mpr hs'
    rw [this]
    exact Kernel.measurable_coe _ (hf.measurableSet_image.mpr ht)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
s : Set (β × γ)
hs : MeasurableSet s
a : α
⊢ Measurable fun b ↦ (η (a, b)) (Prod.mk b ⁻¹' s)

Tactic:
by
  have (b : _) : Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p : (α × β) × γ | (p.1.2, p.2) ∈ s}} := rfl
  simp_rw [this]
  refine (measurable_kernel_prodMk_left ?_).comp measurable_prodMk_left
  exact (measurable_fst.snd.prodMk measurable_snd) hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
⊢ Measurable fun a ↦ ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a

Tactic:
refine .iSup fun n => ?_

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
n : ℕ
⊢ Measurable fun a ↦ ∫⁻ (b : β), (F n) (a, b) ∂κ a
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✝ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ ⊗ₘ κ) s = ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' s) ∂μ

Tactic:
by
  simp_rw [compProd, Kernel.compProd_apply hs, Kernel.const_apply, Kernel.prodMkLeft_apply']

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

Goal state before:
pp: case pos
α : 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 κ
f : β → γ
hf : Measurable f
⊢ IsZeroOrMarkovKernel (κ.map f)

pp: case neg
α : 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 κ
f : β → γ
hf : ¬Measurable f
⊢ IsZeroOrMarkovKernel (κ.map f)

Tactic:
· rcases eq_zero_or_isMarkovKernel κ with rfl | h
    · simp only [map_zero]; infer_instance
    · have := IsMarkovKernel.map κ hf; infer_instance

Goal state after:
case neg
α : 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 κ
f : β → γ
hf : ¬Measurable f
⊢ IsZeroOrMarkovKernel (κ.map f)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : IsZeroOrProbabilityMeasure μ
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrProbabilityMeasure (μ ⊗ₘ κ)

Tactic:
by
  rw [compProd]
  exact IsZeroOrMarkovKernel.isZeroOrProbabilityMeasure ()

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ

Tactic:
· have : SFinite μ := sFinite_of_absolutelyContinuous hμν
    refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_
    rw [Measure.compProd_apply hs, lintegral_eq_zero_iff (Kernel.measurable_kernel_prodMk_left hs)]
      at hs_zero ⊢
    exact hμν.ae_eq hs_zero

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case e_f
α : 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 : α
b : β
⊢ ∫⁻ (a : γ × β), ((swap γ β) a) s ∂(η ((a, b), b).1).prod (Measure.dirac ((a, b), b).2) = (η (a, b)) (Prod.mk b ⁻¹' s)

Tactic:
lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable

Goal state after:
case e_f
α : 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 : α
b : β
⊢ ∫⁻ (x : γ), ∫⁻ (y : β), ((swap γ β) (x, y)) s ∂Measure.dirac ((a, b), b).2 ∂η ((a, b), b).1 =
    (η (a, b)) (Prod.mk b ⁻¹' s)
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
h : ∀ (a : α), ∀ᵐ (b : β) ∂κ a, η (a, b) = 0
⊢ κ ⊗ₖ η = 0

Tactic:
· rw [← Kernel.compProd_zero_right κ]
    exact Kernel.compProd_congr h

Goal state after: