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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
⊢ alternatingGroup α ≤ G

Tactic:
by
  rcases Nat.lt_or_ge (Nat.card α) 2 with hα1 | hα
  · -- Nat.card α  < 2
    rw [eq_bot_of_card_le_two hα1.le]
    exact bot_le
  -- 2 ≤ Nat.card α
  apply Equiv.Perm.alternatingGroup_le_of_index_le_two
  -- one picks up a set of cardinality (card α - 2)
  obtain ⟨s, _, hs⟩ :=
    Set.exists_subset_card_eq (s := (Set.univ : Set α)) (n := Nat.card α - 2)
      (by rw [Set.ncard_univ]; exact sub_le (Nat.card α) 2)
  rw [← hs] at hmt
  -- The index of (fixingSubgroup G s) is (card α)!/2
  have := hmt.index_of_fixingSubgroup_mul rfl
  rw [hs, Nat.sub_sub_self hα, factorial_two] at this
  -- conclude
  rw [← mul_le_mul_iff_of_pos_left (a := Nat.card G) card_pos,
    Subgroup.card_mul_index, ← (fixingSubgroup G s).index_mul_card,
    mul_assoc, mul_comm _ 2, ← mul_assoc]
  rw [this, Nat.card_perm]
  refine Nat.le_mul_of_pos_right (Nat.card α)! card_pos

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

Goal state before:
pp: case h.inr.inr
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 ≠ ⊤
hs_trans : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ IsMultiplyPretransitive G α 2

Tactic:
apply (hrec _ hmn hG htm htm').1

Goal state after:
case h.inr.inr
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 α := ⋯
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 ≠ ⊤
hs_trans : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
⊢ IsPretransitive ↥(fixingSubgroup G t) ↥(ofFixingSubgroup G t)
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
σ σ' : S.Section
g✝ g₁ g₂ : G
equiv : S.Equiv S'
g : G
⊢ S.rightHom (σ g) = g

Tactic:
rightHom_section

Goal state after:
N : Type u_1
G : Type u_2
inst✝³ : Group N
inst✝² : Group G
E : Type u_3
inst✝¹ : Group E
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
σ σ' : S.Section
g✝ g₁ g₂ : G
equiv : S.Equiv S'
g : G
⊢ g = g
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
s t : ↑(powersetCard α n)
inst✝ : DecidableEq α
g : G
f : Fin n ↪ α
⊢ ofFinEmb n α (g • f) = id g • ofFinEmb n α f

Tactic:
rw [← Subtype.coe_inj, coe_smul, f.smul_def, val_ofFinEmb, val_ofFinEmb,
      smul_finset_def, ← map_map, map_eq_image]
    simp [toPerm]

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

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

Tactic:
apply isCoatom_stabilizer

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

case hsc_nonempty
α : Type u_2
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this✝² : Finite α
this✝¹ : Fintype α
this✝ : IsPretransitive (Perm α) ↑(powersetCard α n)
this : Nontrivial ↑(powersetCard α n)
s : ↑(powersetCard α n)
⊢ (↑s)ᶜ.Nonempty

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

Goal state before:
pp: case top
G : Type u_1
inst✝ : Group G
H : Subgroup G
ne_top : ⊤ ≠ ⊤
⊢ ∃ K, K.Normal ∧ ⊤ ≤ K ∧ K < ⊤

Tactic:
contradiction

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
⊢ (fun g i ↦ (mk.symm ↑(MulOpposite.unop g)).subtypePerm ⋯)
      ((fun g ↦ { unop' := ⟨mk (stabilizerEquiv_invFun_aux g), ⋯⟩ }) g) =
    g

Tactic:
ext i a

Goal state after:
α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
i : ι
a : { x // f x = i }
⊢ ↑(((fun g i ↦ (mk.symm ↑(MulOpposite.unop g)).subtypePerm ⋯)
          ((fun g ↦ { unop' := ⟨mk (stabilizerEquiv_invFun_aux g), ⋯⟩ }) g) i)
        a) =
    ↑((g i) a)
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ Nat.card { b // ?m.28 b }ᵐᵒᵖ = ∏ i, (Fintype.card { a // f a = i })!

pp: α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ (Perm α)ᵈᵐᵃ → Prop

pp: α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : Perm α
⊢ f ∘ ⇑x✝ = f ↔ ?m.28 (mk x✝)

Tactic:
Nat.card_congr (DomMulAct.stabilizerMulEquiv f).toEquiv,

Goal state after:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ Nat.card ((i : ι) → Perm { a // f a = i }) = ∏ i, (Fintype.card { a // f a = i })!

α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : Perm α
⊢ f ∘ ⇑x✝ = f ↔ mk x✝ ∈ stabilizer (Perm α)ᵈᵐᵃ f
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₁'3 : ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁'.head⁻¹ * w₁.head ∈ toSubgroup A B (-u)
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⁻¹ * w₂.head ∈ toSubgroup A B (-u)
⊢ ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁.head⁻¹ * w₂.head ∈ toSubgroup A B (-u)

Tactic:
simp only [← leftCoset_eq_iff] at *

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 ∈ Option.map Prod.fst w₁.toList.head?, w₁.head • ↑(toSubgroup A B (-u)) = w₂.head • ↑(toSubgroup A B (-u))
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 : Even (m.sum + m.card)
⊢ False

Tactic:
contradiction

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

Goal state before:
pp: case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a b : ↥g.cycleFactorsFinset
h : ¬b = a
⊢ _root_.Disjoint (↑a).support (↑b).support

Tactic:
rw [← disjoint_iff_disjoint_support]

Goal state after:
case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a b : ↥g.cycleFactorsFinset
h : ¬b = a
⊢ (↑a).Disjoint ↑b
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ _root_.Disjoint ofSubtype.range (noncommPiCoprod ⋯).range

Tactic:
noncommPiCoprod_range,

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ _root_.Disjoint ofSubtype.range (⨆ i, zpowers ↑i)
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ofSubtype.range ≤ map (centralizer {g}).subtype (toPermHom g).ker ∧
    (noncommPiCoprod ⋯).range ≤ map (centralizer {g}).subtype (toPermHom g).ker

Tactic:
noncommPiCoprod_range,

Goal state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ofSubtype.range ≤ map (centralizer {g}).subtype (toPermHom g).ker ∧
    ⨆ i, zpowers ↑i ≤ map (centralizer {g}).subtype (toPermHom g).ker
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: case pos.hnc.inr
α : 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)
hm : ¬Even (m.sum + m.card)
⊢ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

Tactic:
contradiction

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case refine_1.left
ι : 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
hhead : ↑(⋯.equiv ((Word.equivPair i) w).head).2 = ((Word.equivPair i) w).head
hh1 : ¬h = 1
h₁ : h = 1
h₂ : ((Word.equivPair i) w).head = 1
⊢ False

Tactic:
contradiction

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)
U : Set ↥g.cycleFactorsFinset := ↑Finset.univ
hU : U.Pairwise fun i j ↦ (↑(v i)).Disjoint ↑(v j)
⊢ (ofSubtype k).cycleType + ∑ i, (↑(v i)).cycleType =
    k.cycleType + ∑ c ∈ g.cycleFactorsFinset.attach, (↑(v c)).cycleType

Tactic:
Finset.univ_eq_attach

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).cycleType + ∑ i ∈ g.cycleFactorsFinset.attach, (↑(v i)).cycleType =
    k.cycleType + ∑ c ∈ g.cycleFactorsFinset.attach, (↑(v c)).cycleType
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ ↑S
⊢ k ∈ {1} ∪ {g | (↑g).cycleType = {2, 2}}

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:
· -- inclusion S ⊆ {1} ∪ {g |  cycleType g = { 2, 2 }}
    obtain ⟨n, hn⟩ := (IsPGroup.iff_orderOf.mp S.isPGroup') ⟨k, hk⟩
    replace hn : (orderOf (k : Perm α)) = 2 ^ n := by simpa using hn
    convert! mem_kleinFour_of_order_two_pow hα4 k.2 hn.dvd
    simp

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ Fintype.card (QuaternionGroup n) = 4 * n

Tactic:
by
  rw [← Fintype.card_eq.mpr ⟨fintypeHelper⟩, Fintype.card_sum, ZMod.card, two_mul]
  ring

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case mul
ι : 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)
x y : PushoutI φ
ihx : ∀ (w : NormalWord d), (x • w).prod = x * w.prod
ihy : ∀ (w : NormalWord d), (y • w).prod = y * w.prod
w : NormalWord d
⊢ (x • y • w).prod = x * y * w.prod

Tactic:
ihx,

Goal state after:
case mul
ι : 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)
x y : PushoutI φ
ihx : ∀ (w : NormalWord d), (x • w).prod = x * w.prod
ihy : ∀ (w : NormalWord d), (y • w).prod = y * w.prod
w : NormalWord d
⊢ x * (y • w).prod = x * y * w.prod
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case inr
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
inst✝ : IsZGroup G''
h_le : f'.ker ≤ f.range
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this✝ : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker ↑P
this : IsCyclic ↥(Subgroup.map f' ↑P)
⊢ IsCyclic ↥↑P

Tactic:
apply isCyclic_of_injective (f'.subgroupMap P)

Goal state after:
case inr
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
inst✝ : IsZGroup G''
h_le : f'.ker ≤ f.range
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this✝ : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker ↑P
this : IsCyclic ↥(Subgroup.map f' ↑P)
⊢ Function.Injective ⇑(f'.subgroupMap ↑P)
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ {i | x i ≠ z i} ⊆ {i | x i ≠ y i} ∪ {i | y i ≠ z i}

Tactic:
rw [← filter_or]

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ {i | x i ≠ z i} ⊆ {a | x a ≠ y a ∨ y a ≠ z a}
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ (∀ ⦃x_1 : ι⦄, x x_1 = y x_1) → ∀ ⦃x_1 : ι⦄, x x_1 = y x_1

Tactic:
imp_self

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
ξ : Kernel γ δ
η : Kernel β γ
κ : Kernel α β
a : α
f : δ → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : δ), f b ∂(ξ ∘ₖ η ∘ₖ κ) a = ∫⁻ (b : δ), f b ∂(ξ ∘ₖ (η ∘ₖ κ)) a

Tactic:
lintegral_comp _ _ _ hf,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
ξ : Kernel γ δ
η : Kernel β γ
κ : Kernel α β
a : α
f : δ → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : β), ∫⁻ (b : γ), ∫⁻ (b : δ), f b ∂ξ b ∂η b ∂κ a = ∫⁻ (b : γ), ∫⁻ (b : δ), f b ∂ξ b ∂(η ∘ₖ κ) a
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 μ
inst✝ : SFinite ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
⊢ (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ

Tactic:
Measure.compProd,

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SFinite ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
⊢ (Kernel.const Unit (μ + ν) ⊗ₖ Kernel.prodMkLeft Unit κ) () =
    (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) () + (Kernel.const Unit ν ⊗ₖ Kernel.prodMkLeft Unit κ) ()
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.1) Set.univ ≤ κ.bound

Tactic:
exact measure_le_bound κ a.1 Set.univ

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 α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η

Tactic:
Measure.compProd,

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit (κ + η)) () =
    (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ) () + (Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit η) ()
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 γ
f : α → β
hf : Measurable f
g : β → γ
hg : Measurable g
⊢ (deterministic f hf).map g = deterministic (g ∘ f) ⋯

Tactic:
by
  rw [← id_map, ← map_comp_right _ hf hg, id_map]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (Kernel.prodMkRight γ κ)

Tactic:
Kernel.prodMkRight

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
⊢ IsMarkovKernel (κ.comap Prod.fst ⋯)
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
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (Kernel.prodMkRight γ κ)

Tactic:
Kernel.prodMkRight

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsZeroOrMarkovKernel κ
⊢ IsZeroOrMarkovKernel (κ.comap Prod.fst ⋯)
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
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (Kernel.prodMkRight γ κ)

Tactic:
Kernel.prodMkRight

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsFiniteKernel κ
⊢ IsFiniteKernel (κ.comap Prod.fst ⋯)
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
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (Kernel.prodMkRight γ κ)

Tactic:
Kernel.prodMkRight

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ IsSFiniteKernel (κ.comap Prod.fst ⋯)
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

Tactic:
by_cases hη : IsSFiniteKernel η

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
γ : Type u_3
mγ : MeasurableSpace γ
η : Kernel (α × β) γ
hμ : SFinite μ
hκ : IsSFiniteKernel κ
hη : ¬IsSFiniteKernel η
⊢ map (⇑MeasurableEquiv.prodAssoc.symm) (μ ⊗ₘ (κ ⊗ₖ η)) = μ ⊗ₘ κ ⊗ₘ η
Module: Mathlib.Probability.Kernel.Composition.CompMap

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β (γ × δ)
⊢ (η ∘ₖ κ).snd = η.snd ∘ₖ κ

Tactic:
simp_rw [snd_eq, map_comp κ η _]

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 α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
⊢ (ν ⊗ₘ η) (s ×ˢ univ) = 0

Tactic:
by_cases hη : IsSFiniteKernel η

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
hη : IsSFiniteKernel η
⊢ (ν ⊗ₘ η) (s ×ˢ univ) = 0

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
h_zero : ∀ (a : α), NeZero (κ a)
h : μ ⊗ₘ κ ≪ ν ⊗ₘ η
s : Set α
hs : MeasurableSet s
hs0 : ν s = 0
hν : SFinite ν
hη : ¬IsSFiniteKernel η
⊢ (ν ⊗ₘ η) (s ×ˢ univ) = 0