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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
this : IsPretransitive G α
B : Set α
hB : ∀ ⦃g : G⦄ ⦃a : α⦄, a ∈ B → g • a ∈ B → g • B = B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : G
hga : g • a = a
hgb : g • b = c
⊢ g • a ∈ B

Tactic:
hga

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
this : IsPretransitive G α
B : Set α
hB : ∀ ⦃g : G⦄ ⦃a : α⦄, a ∈ B → g • a ∈ B → g • B = B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : G
hga : g • a = a
hgb : g • b = c
⊢ a ∈ B
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
habG : swap a b ∉ G
g✝ g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
⊢ (swap x y ∈ G ↔ g ∈ G) ↔ swap x y * g ∈ alternatingGroup α

Tactic:
mul_mem_iff_of_index_two alternatingGroup.index_eq_two,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index = 2
a✝ : Nontrivial α
a b : α
hab : a ≠ b
habG : swap a b ∉ G
g✝ g : Perm α
x y : α
hxy : x ≠ y
ih : g ∈ G ↔ g ∈ alternatingGroup α
⊢ (swap x y ∈ G ↔ g ∈ G) ↔ (swap x y ∈ alternatingGroup α ↔ g ∈ alternatingGroup α)
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B✝ : Type u_1
inst✝¹⁸ : TopologicalSpace B✝
F✝ : Type u_2
inst✝¹⁷ : NormedAddCommGroup F✝
inst✝¹⁶ : NormedSpace ℝ F✝
E✝ : B✝ → Type u_3
inst✝¹⁵ : TopologicalSpace (TotalSpace F✝ E✝)
inst✝¹⁴ : (x : B✝) → NormedAddCommGroup (E✝ x)
inst✝¹³ : (x : B✝) → InnerProductSpace ℝ (E✝ x)
inst✝¹² : FiberBundle F✝ E✝
inst✝¹¹ : VectorBundle ℝ F✝ E✝
B : Type u_4
inst✝¹⁰ : TopologicalSpace B
F : Type u_5
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
E : B → Type u_6
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (b : B) → TopologicalSpace (E b)
inst✝⁵ : (b : B) → AddCommGroup (E b)
inst✝⁴ : (b : B) → Module ℝ (E b)
inst✝³ : ∀ (b : B), IsTopologicalAddGroup (E b)
inst✝² : ∀ (b : B), ContinuousConstSMul ℝ (E b)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
g : RiemannianMetric E
b : B
v : E b
h : ((g.inner b) v) v = 0
⊢ v = 0

Tactic:
contrapose! h; exact (g.pos b v h).ne'

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j✝.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j = Fintype.card α - 1
⊢ (g • x) i = (k • x) i

Tactic:
· rw [← hxj]
        apply congr_arg
        rw [Fin.ext_iff, hi, hj]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
⊢ ∃ g, g • x = y

Tactic:
rcases Int.units_eq_one_or (Equiv.Perm.sign g) with h | h

Goal state after:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Equiv.Perm.sign g = 1
⊢ ∃ g, g • x = y

case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Equiv.Perm.sign g = -1
⊢ ∃ g, g • x = y
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤

Tactic:
suffices ∃ g, g ∉ stabilizer (alternatingGroup α) s by contrapose! this; simp [this]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
⊢ ∃ g, g ∉ stabilizer (↥(alternatingGroup α)) s
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
⊢ False

Tactic:
by
    rcases lt_or_ge (Nat.card α) (sᶜ.ncard * 2) with hB' | hB'
    · apply h0.ne_empty
      rw [← compl_univ_iff]
      exact hsc.eq_univ_of_card_lt hB'
    · rw [← not_lt] at hB'
      apply hB'
      rwa [← Set.ncard_add_ncard_compl sᶜ, mul_two, add_lt_add_iff_left, compl_compl]

Goal state after:
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 α
this : s.Nonempty
⊢ ∃ a t, a ∈ s ∧ s = insert a (Subtype.val '' t)

Tactic:
obtain ⟨a, ha⟩ := this
      use a, Subtype.val ⁻¹' s, ha
      ext x
      by_cases hx : x = a <;> simp [hx, mem_ofStabilizer_iff, ha]

Goal state after:
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 α := ⋯
f : α →ₑ[⇑φ] α := ⋯
hf : Function.Bijective ⇑f
⊢ Nat.card (Perm α) ≤ Nat.card ↥φ.range

Tactic:
simp only [Nat.card_perm, hα, Nat.factorial_two]

Goal state after:
α : 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
⊢ 2 ≤ Nat.card ↥φ.range
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α✝ : Type u_1
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
h0' : s.Subsingleton
⊢ 3 ≤ Nat.card α

Tactic:
← ncard_add_ncard_compl s

Goal state after:
α✝ : Type u_1
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
h0' : s.Subsingleton
⊢ 3 ≤ s.ncard + sᶜ.ncard
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
H : Type u_2
inst✝ : Group H
f : G →* H
x : H
hx : ∀ (a : ↥A), x * f ↑a = f ↑(φ a) * x
⊢ (lift f x hx) t = x

Tactic:
simp [lift, t]

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

Goal state before:
pp: case inl
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ s * (m₁, s₁).1
⊢ f m ∣ n₁ ∨ f m ∣ n₂

Tactic:
have := map_dvd f dvd

Goal state after:
case inl
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this✝ : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ s * (m₁, s₁).1
this : f m ∣ f (s * (m₁, s₁).1)
⊢ f m ∣ n₁ ∨ f m ∣ n₂
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case inr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ (m₂, s₂).1
⊢ f m ∣ n₁ ∨ f m ∣ n₂

Tactic:
have := map_dvd f dvd

Goal state after:
case inr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this✝ : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ (m₂, s₂).1
this : f m ∣ f (m₂, s₂).1
⊢ f m ∣ n₁ ∨ f m ∣ n₂
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑b.2 * a.1 ≤ ↑a.2 * b.1
hbc : ↑c.2 * b.1 ≤ ↑b.2 * c.1
⊢ ↑c.2 * (↑b.2 * a.1) ≤ ↑b.2 * (↑a.2 * c.1)

Tactic:
hab

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑b.2 * a.1 ≤ ↑a.2 * b.1
hbc : ↑c.2 * b.1 ≤ ↑b.2 * c.1
⊢ ↑c.2 * (↑a.2 * b.1) ≤ ↑b.2 * (↑a.2 * c.1)
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a b : Localization s
x✝¹ x✝ : α × ↥s
⊢ mk x✝¹.1 x✝¹.2 ≤ mk x✝.1 x✝.2 ∨ mk x✝.1 x✝.2 ≤ mk x✝¹.1 x✝¹.2

Tactic:
simp_rw [mk_le_mk]

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a b : Localization s
x✝¹ x✝ : α × ↥s
⊢ ↑x✝.2 * x✝¹.1 ≤ ↑x✝¹.2 * x✝.1 ∨ ↑x✝¹.2 * x✝.1 ≤ ↑x✝.2 * x✝¹.1
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
⊢ Prime (f m)

Tactic:
refine ⟨n0, nu, fun n₁ n₂ dvd ↦ ?_⟩
  have ⟨⟨m₁, s₁⟩, eq₁⟩ := f.surj n₁
  have ⟨⟨m₂, s₂⟩, eq₂⟩ := f.surj n₂
  have := (f.map_units (s₁ * s₂)).dvd_mul_right.mpr dvd
  rw [Submonoid.mul_def, map_mul, mul_mul_mul_comm, eq₁, eq₂, ← map_mul, f.map_dvd_map] at this
  have ⟨s, hs, dvd⟩ := this
  rw [← mul_assoc] at dvd
  obtain dvd | dvd := prime.dvd_or_dvd dvd
  all_goals have := map_dvd f dvd
  · rw [map_mul, (f.map_units ⟨s, hs⟩).dvd_mul_left, ← eq₁, (f.map_units s₁).dvd_mul_right] at this
    exact .inl this
  · rw [← eq₂, (f.map_units s₂).dvd_mul_right] at this; exact .inr this

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
a b : List α
ha : a ∈ p
hb : b ∈ p
⊢ a.Disjoint b → a.formPerm.Disjoint b.formPerm

Tactic:
hab

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hc : m.sum ≤ Fintype.card α
h2c : ∀ a ∈ m, 2 ≤ a
hc' : m.toList.sum ≤ Fintype.card α
p : List (List α)
hp_length : List.map List.length p = m.toList
hp_nodup : ∀ s ∈ p, s.Nodup
hp_disj : List.Pairwise List.Disjoint p
hp2 : ∀ x ∈ p, 2 ≤ x.length
a b : List α
ha : a ∈ p
hb : b ∈ p
hab : a.Disjoint b
⊢ a.formPerm.Disjoint b.formPerm
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ (∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support) ↔ τ ∈ range_toPermHom' g

Tactic:
mem_range_toPermHom'_iff

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
⊢ (∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support) ↔
    ∀ (c : ↥g.cycleFactorsFinset), #(↑(τ c)).support = #(↑c).support
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
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝ : Finite G
P : Sylow (Nat.card ↥N).minFac ↥N
this : Fact (Nat.Prime (Nat.card ↥N).minFac)
⊢ ↑P ≠ ⊥

Tactic:
apply P.ne_bot_of_dvd_card

Goal state after:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝ : Finite G
P : Sylow (Nat.card ↥N).minFac ↥N
this : Fact (Nat.Prime (Nat.card ↥N).minFac)
⊢ (Nat.card ↥N).minFac ∣ Nat.card ↥N
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

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

Tactic:
rw [Nat.card_eq_card_toFinset, Set.toFinset_union, Set.toFinset_singleton, Set.toFinset_ofPred]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
⊢ commutator ↥(alternatingGroup α) ≤ kleinFour α

Tactic:
← Subgroup.Normal.quotient_commutative_iff_commutator_le

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
⊢ IsMulCommutative (↥(alternatingGroup α) ⧸ kleinFour α)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

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

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_xa]
      exact dvd_lcm_right (2 * n) 4

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

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

Tactic:
← commutator_alternatingGroup_eq_top hα

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
hα : 5 ≤ Nat.card α
hα' : Nat.card α ≠ 8
N : Subgroup ↥(alternatingGroup α)
inst✝ : N.Normal
hN : Nontrivial ↥N
this : IsPreprimitive ↥(alternatingGroup α) ↑(Set.powersetCard α 4)
⊢ _root_.commutator ↥(alternatingGroup α) ≤ N
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Simple

Goal state before:
pp: ⊢ normalClosure {⟨finRotate 5, ⋯⟩} = ⊤

Tactic:
have : IsSimpleGroup (alternatingGroup (Fin 5)) := isSimpleGroup (by simp)
  apply normalClosure_normal.eq_bot_or_eq_top.resolve_left
  simp +decide

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

Goal state before:
pp: ⊢ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩} = ⊤

Tactic:
have : IsSimpleGroup (alternatingGroup (Fin 5)) := isSimpleGroup (by simp)
  apply normalClosure_normal.eq_bot_or_eq_top.resolve_left
  simp +decide

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

Goal state before:
pp: case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆

Tactic:
let _ := (hH.mulAutMulEquiv _).toMonoidHom.commGroupOfInjective (hH.mulAutMulEquiv _).injective

Goal state after:
case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
x✝ : CommGroup (MulAut ↥⁅commutator ↥H, commutator ↥H⁆) :=
  (IsCyclic.mulAutMulEquiv ↥⁅commutator ↥H, commutator ↥H⁆).toMonoidHom.commGroupOfInjective ⋯
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
a : α
s : Set β
h : ∫⁻ (b : β), s.indicator (fun x ↦ 1) b ∂κ a = ∫⁻ (b : β), s.indicator (fun x ↦ 1) b ∂η a
hs : MeasurableSet s
⊢ (κ a) s = (η a) s

Tactic:
lintegral_indicator_const hs,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
a : α
s : Set β
hs : MeasurableSet s
h : 1 * (κ a) s = 1 * (η a) s
⊢ (κ a) s = (η a) s
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ 0 = hammingDist x y ↔ x = y

Tactic:
by
  rw [eq_comm, hammingDist_eq_zero]

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 : α
this : ∀ (b : β), Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p | (p.1.2, p.2) ∈ s}}
⊢ MeasurableSet {p | (p.1.2, p.2) ∈ s}

Tactic:
exact (measurable_fst.snd.prodMk measurable_snd) hs

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
r : ℕ
hr : r ≥ 1
⊢ (∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length) ^ r ≤ ↑r * ↑(S.sup List.length)

Tactic:
set maxLen := S.sup List.length
  -- Let `T` be the set of all concatenations of `r` codewords from `S`.
  let T : Finset (List α) := Finset.image concatFn (Finset.univ : Finset (Fin r → S))
  -- Any `x ∈ T` is a concatenation of `r` nonempty codewords, hence `r ≤ |x| ≤ r*maxLen`.
  have hlen_maps (x : List α) (hx : x ∈ T) : x.length ∈ Finset.Icc r (r * maxLen) := by
    rcases Finset.mem_image.mp hx with ⟨_, _, rfl⟩
    exact concatFn_length_mem_Icc
      (fun c hnil => h.epsilon_not_mem (by simpa [hnil] using c.prop))
  let D := (Fintype.card α : ℝ)
  -- Expand the `r`-th power as a sum over `r`-tuples of codewords;
  -- each tuple contributes the weight `(1/D)^{|concatFn w|}`.
  calc (∑ w ∈ S, (1 / (Fintype.card α) : ℝ) ^ w.length) ^ r
    _ = ∑ w : Fin r → S, ∏ i : Fin r, (1 / D) ^ (w i).val.length := by
      simpa [(Finset.sum_coe_sort S _).symm] using
        Fintype.sum_pow (f := fun c : S => (1 / D) ^ c.val.length) r
    -- Each tuple contributes the weight `(1/D)^{|concatFn w|}`.
    _ = ∑ w, (1 / D) ^ (concatFn w).length := by
      apply Fintype.sum_congr
      intro w
      simpa [concatFn_length] using Finset.prod_pow_eq_pow_sum Finset.univ _ _
    -- Unique decodability makes `concatFn` injective, so these concatenations are distinct;
    -- we can reindex the sum by the set `T` of words.
    _ = ∑ x ∈ T, (1 / D) ^ x.length :=
      (Finset.sum_image (f := fun x => (1 / D) ^ x.length)
        (fun _ _ _ _ hEq => concatFn_injective_of_uniquelyDecodable h r hEq)).symm
    -- Group the sum over `T` by the length `s`.
    -- The admissible lengths lie in `[r, r*maxLen]` by `hlen_maps`.
    _ = ∑ s ∈ Finset.Icc r (r * maxLen), ∑ x ∈ T with x.length = s, (1 / D) ^ x.length :=
      (Finset.sum_fiberwise_of_maps_to hlen_maps _).symm
  -- For each length `s`, the `s`-fiber contributes at most `D^s * (1/D)^s`:
  -- there are ≤ `D^s` words of length `s`, and each has weight `(1/D)^s`.
  apply le_trans (Finset.sum_le_sum (fun _ _ => sum_pow_length_filter_eq_le_card_mul))
  -- Summing these bounds over the interval s ∈ [r, r * maxLen] multiplies the term
  -- by the number of lengths. Since r ≥ 1, this count is at most r * maxLen.
  rcases r with (_ | _ | r) <;> rcases maxLen with (_ | _ | maxLen)
    <;> simp at * <;> norm_cast <;> simp

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

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

Tactic:
Kernel.sectR_apply

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 γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((κ ⊗ₖ η) a) (s ×ˢ t) = ∫⁻ (b : β) in s, (η (a, b)) t ∂κ a

Tactic:
compProd_apply (hs.prod ht),

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s ×ˢ t) ∂κ a = ∫⁻ (b : β) in s, (η (a, b)) t ∂κ a
Module: Mathlib.Probability.Kernel.Composition.Prod

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 δ
κ : Kernel α β
inst✝¹ : IsMarkovKernel κ
η : Kernel α γ
inst✝ : IsMarkovKernel η
⊢ IsMarkovKernel (κ ×ₖ η)

Tactic:
rw [Kernel.prod]; infer_instance

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

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 δ
κ : Kernel α β
inst✝¹ : IsFiniteKernel κ
η : Kernel α γ
inst✝ : IsFiniteKernel η
⊢ IsFiniteKernel (κ ×ₖ η)

Tactic:
rw [Kernel.prod]; infer_instance

Goal state after: