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

Goal state before:
pp: case hXdisj
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
⊢ Pairwise (Disjoint on X')

pp: case hpp
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
⊢ Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X' j ⊆ X' i

pp: ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
⊢ 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)

Tactic:
· show Pairwise (Disjoint on X')
    intro i j hij
    simp only [X']
    apply Disjoint.union_left <;> apply Disjoint.union_right
    · exact hXdisj hij
    · exact hXYdisj i j
    · exact (hXYdisj j i).symm
    · exact hYdisj hij

Goal state after:
case hpp
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
⊢ Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X' j ⊆ X' i

ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
⊢ 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
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
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < r' ^ 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
⊢ ‖(Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
          Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x)
        v‖ ≤
    r' * ‖v‖

Tactic:
suffices ‖((trivializationAt F E x).symmL ℝ y) w‖ ^ 2 ≤ r' ^ 2 * ‖v‖ ^ 2 from
    le_of_sq_le_sq (by simpa [mul_pow]) (by positivity)

Goal state after:
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
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < r' ^ 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
⊢ ‖(Trivialization.symmL ℝ (trivializationAt F E x) y) w‖ ^ 2 ≤ r' ^ 2 * ‖v‖ ^ 2
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ g ^ ((H.quotientEquivSigmaZMod g) q).snd.cast • Quotient.out ((H.quotientEquivSigmaZMod g) q).fst = q

Tactic:
← quotientEquivSigmaZMod_symm_apply,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ (H.quotientEquivSigmaZMod g).symm ⟨((H.quotientEquivSigmaZMod g) q).fst, ((H.quotientEquivSigmaZMod g) q).snd⟩ = q
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ g ^ ((H.quotientEquivSigmaZMod g) (g ^ k.cast • Quotient.out q)).snd.cast *
      Quotient.out (Quotient.out ((H.quotientEquivSigmaZMod g) (g ^ k.cast • Quotient.out q)).fst) =
    g ^ k.cast * Quotient.out (Quotient.out q)

Tactic:
← quotientEquivSigmaZMod_symm_apply,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ g ^ ((H.quotientEquivSigmaZMod g) ((H.quotientEquivSigmaZMod g).symm ⟨q, k⟩)).snd.cast *
      Quotient.out (Quotient.out ((H.quotientEquivSigmaZMod g) ((H.quotientEquivSigmaZMod g).symm ⟨q, k⟩)).fst) =
    g ^ k.cast * Quotient.out (Quotient.out q)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
⊢ 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)

Tactic:
inhabit ι

Goal state after:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
inhabited_h : Inhabited ι
⊢ 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
N : Subgroup G
hN : N.IsFinitelyNormallyGenerated
f : G →* H
hf : Function.Surjective ⇑f
⊢ (map f N).IsFinitelyNormallyGenerated

Tactic:
obtain ⟨S, hSfinite, hSclosure⟩ := hN

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
N : Subgroup G
f : G →* H
hf : Function.Surjective ⇑f
S : Set G
hSfinite : S.Finite
hSclosure : normalClosure S = N
⊢ (map f N).IsFinitelyNormallyGenerated
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : (Nat.card G).minFac = p
P : Sylow p G
hP : IsCyclic ↥↑P
⊢ normalizer ↑P ≤ centralizer ↑P

Tactic:
subst hp
  by_cases hn : Nat.card G = 1
  · have := (Nat.card_eq_one_iff_unique.mp hn).1
    rw [Subsingleton.elim (normalizer _) (centralizer P)]
  have := Fact.mk (Nat.minFac_prime hn)
  have key := card_dvd_of_injective _ (QuotientGroup.kerLift_injective P.normalizerMonoidHom)
  rw [normalizerMonoidHom_ker, ← index, ← relIndex] at key
  refine relIndex_eq_one.mp (Nat.eq_one_of_dvd_coprimes ?_ dvd_rfl key)
  obtain ⟨k, hk⟩ := P.2.exists_card_eq
  rcases eq_zero_or_pos k with h0 | h0
  · rw [hP.card_mulAut, hk, h0, pow_zero, Nat.totient_one]
    apply Nat.coprime_one_right
  rw [hP.card_mulAut, hk, Nat.totient_prime_pow Fact.out h0]
  refine (Nat.Coprime.pow_right _ ?_).mul_right ?_
  · apply Nat.Coprime.coprime_dvd_left (relIndex_dvd_of_le_left _ P.le_centralizer)
    apply Nat.Coprime.coprime_dvd_left (relIndex_dvd_index_of_le P.le_normalizer)
    rw [Nat.coprime_comm, Nat.Prime.coprime_iff_not_dvd Fact.out]
    exact P.not_dvd_index
  · apply Nat.Coprime.coprime_dvd_left <| relIndex_dvd_card ..
    apply Nat.Coprime.coprime_dvd_left <| card_subgroup_dvd_card _
    have h1 := Nat.gcd_dvd_left (Nat.card G) ((Nat.card G).minFac - 1)
    have h2 := Nat.gcd_le_right (n := (Nat.card G).minFac - 1) (Nat.card G)
      (tsub_pos_iff_lt.mpr (Nat.minFac_prime hn).one_lt)
    contrapose! h2
    refine Nat.sub_one_lt_of_le (Nat.card G).minFac_pos (Nat.minFac_le_of_dvd ?_ h1)
    exact (Nat.two_le_iff _).mpr ⟨ne_zero_of_dvd_ne_zero Nat.card_pos.ne' h1, h2⟩

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x = 1
g : G
hm : n ≤ m
⊢ ⁅x, g⁆ ∈ (fun m ↦ H (n - m)) (m + 1)

Tactic:
subst hx

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
m : ℕ
g : G
hm : n ≤ m
⊢ ⁅1, g⁆ ∈ (fun m ↦ H (n - m)) (m + 1)
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
a : α × Bool
hl : [a] = g.toWord
⊢ (mk [w])⁻¹ • ⟨mk [a], ⋯⟩ • x ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x}

Tactic:
show a = w by simpa [← hl, startsWith] using hg,

Goal state after:
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
a : α × Bool
hl : [a] = g.toWord
⊢ (mk [w])⁻¹ • ⟨mk [w], ⋯⟩ • x ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x}
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H₁ H₂ : Subgroup G
inst✝¹ : H₁.Normal
inst✝ : H₂.Normal
h : H₁ = H₂
⊢ comap (mk' H₁) (center (G ⧸ H₁)) = comap (mk' H₂) (center (G ⧸ H₂))

Tactic:
subst h; rfl

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : ℕ
ab : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
⊢ upperCentralSeries G a = upperCentralSeries G c

Tactic:
by
  wlog ab : a < b
  · grind
  refine eq_ge_of_eq_succ ac (le_antisymm ?_ ?_)
  · exact upperCentralSeries_mono _ <| Nat.le_succ ..
  · rw [hn]
    exact upperCentralSeries_mono _ (by grind)

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

Goal state before:
pp: case inl
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B.Subsingleton
⊢ IsTrivialBlock (⇑f '' B)

Tactic:
apply Or.intro_left

Goal state after:
case inl
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B.Subsingleton
⊢ (⇑f '' B).Subsingleton
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inl
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B.Subsingleton
⊢ IsTrivialBlock (⇑f ⁻¹' B)

Tactic:
apply Or.intro_left

Goal state after:
case inl
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B.Subsingleton
⊢ (⇑f ⁻¹' B).Subsingleton
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
H : IsTrivialBlock (g • B)
⊢ B = g⁻¹ • g • B

Tactic:
simp only [inv_smul_smul]

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

Goal state before:
pp: M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ IwaS.T (g • a) ≤ N ⊔ IwaS.T a

Tactic:
rw [Subgroup.smul_def, IwaS.is_conj g a]

Goal state after:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
g : ↥N
⊢ MulAut.conj ↑g • IwaS.T a ≤ N ⊔ IwaS.T a
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : Nontrivial X
a : X
⊢ Nontrivial (BlockMem G a)

Tactic:
rw [nontrivial_iff]

Goal state after:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : Nontrivial X
a : X
⊢ ∃ x y, x ≠ y
Module: Mathlib.GroupTheory.Perm.ConjAct

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ (k⁻¹ • k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset

Tactic:
simp only [inv_smul_smul]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ g.cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case mp.inl
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
h : IsSimpleOrder (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := eq_bot_or_eq_top
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = ↑⊥
⊢ IsTrivialBlock B

Tactic:
left; rw [hB']; exact Set.subsingleton_singleton

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

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : Nontrivial X
inst✝ : IsPreprimitive G X
a : X
⊢ IsCoatom (stabilizer G a)

Tactic:
rwa [isCoatom_stabilizer_iff_preprimitive]

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype ↑(Set.range fun g ↦ g • B)
⊢ ∑ᶠ (t : ↑(Set.range fun g ↦ g • B)), (Set.range ⇑f ∩ ↑t).ncard ≤ (orbit H B).ncard

Tactic:
finsum_eq_sum_of_fintype

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype ↑(Set.range fun g ↦ g • B)
⊢ ∑ i, (Set.range ⇑f ∩ ↑i).ncard ≤ (orbit H B).ncard
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: case right
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
⊢ Function.Surjective ⇑(conjMap hg)

Tactic:
· intro x
    exact ⟨conjMap _ x, inv_conjMap_comp_apply _ x⟩

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
g : ↥(stabilizer G s)
x : ↑s
⊢ g • ↑x ∈ s

Tactic:
convert! Set.smul_mem_smul_set x.prop

Goal state after:
case e'_4
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
g : ↥(stabilizer G s)
x : ↑s
⊢ s = g • s
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case neg
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
⊢ c ∈ B

Tactic:
rw [← hB (g := g) ha (by rw [hga]; exact ha), ← hgb]

Goal state after:
case neg
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 • b ∈ g • B
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case mpr.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ ∀ {s : Set α}, s.encard + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
simpa using isPreprimitive_of_fixingSubgroup_empty_iff.mpr h

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

Goal state before:
pp: case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsPreprimitive M α → IsMultiplyPreprimitive M α 1

Tactic:
intro h
    rw [isMultiplyPreprimitive_iff]
    constructor
    · exact is_one_pretransitive_iff.mpr h.toIsPretransitive
    · simpa using isPreprimitive_of_fixingSubgroup_empty_iff.mpr h

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
hm : ↑m ∈ fixingSubgroup M (s ∪ t) := Subtype.prop m
⊢ ↑m ∈ fixingSubgroup M s

Tactic:
simp only [fixingSubgroup_union, Subgroup.mem_inf] at hm

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
hm : ↑m ∈ fixingSubgroup M s ∧ ↑m ∈ fixingSubgroup M t
⊢ ↑m ∈ fixingSubgroup M s
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
hm : ↑m ∈ fixingSubgroup M (s ∪ t) := Subtype.prop m
⊢ ⟨↑m, ⋯⟩ ∈ fixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)

Tactic:
simp only [fixingSubgroup_union, Subgroup.mem_inf] at hm

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
m : ↥(fixingSubgroup M (s ∪ t))
hm : ↑m ∈ fixingSubgroup M s ∧ ↑m ∈ fixingSubgroup M t
⊢ ⟨↑m, ⋯⟩ ∈ fixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
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.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ ofFixingSubgroup M s
hg'a : g⁻¹ • a ∈ ofFixingSubgroup M s
⊢ ∃ g_1, g_1 • ⟨a, ha'⟩ = ⟨x, hx✝⟩

Tactic:
obtain ⟨⟨k, hk⟩, hkax⟩ := hs.exists_smul_eq ⟨g⁻¹ • a, hg'a⟩ ⟨g⁻¹ • x, hg'x⟩

Goal state after:
case inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ ofFixingSubgroup M s
hg'a : g⁻¹ • a ∈ ofFixingSubgroup M s
k : M
hk : k ∈ fixingSubgroup M s
hkax : ⟨k, hk⟩ • ⟨g⁻¹ • a, hg'a⟩ = ⟨g⁻¹ • x, hg'x⟩
⊢ ∃ g_1, g_1 • ⟨a, ha'⟩ = ⟨x, hx✝⟩
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case refine_2
α : Type u_2
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
g : Perm ↑s
g' : α
a : g' ∈ s
⊢ ∃ y ∈ s, (ofSubtype g) y = g'

Tactic:
use (g⁻¹ ⟨g', a⟩)
    simp

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

Goal state before:
pp: α : 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
x : α
hx : x ∈ s
⊢ k • x = x

Tactic:
rw [Perm.smul_def, ← Perm.notMem_support]

Goal state after:
α : 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
x : α
hx : x ∈ s
⊢ x ∉ k.support
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective toPerm
⊢ (s ∩ B).Subsingleton

Tactic:
← Subtype.image_preimage_val

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective toPerm
⊢ (Subtype.val '' Subtype.val ⁻¹' B).Subsingleton