mathlib-initiative/mathlib-tactics huggingface dataset:
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
hgx : ((g x) v) v = ((g' x) w) w
⊢ ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) = ((g' y) w) w

Tactic:
rw [inCoordinates_apply_eq₂ h'y h'y (Set.mem_univ _)]

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
hgx : ((g x) v) v = ((g' x) w) w
⊢ ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) =
    (Trivialization.linearMapAt ℝ (trivializationAt ℝ (fun x ↦ ℝ) x) y)
      (((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w))
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg.inr.refine_2
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
h1 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ∣ Nat.card G
h2 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ≠ 1
⊢ 2 ≤ (Nat.card G).gcd ((Nat.card G).minFac - 1)

Tactic:
exact (Nat.two_le_iff _).mpr ⟨ne_zero_of_dvd_ne_zero Nat.card_pos.ne' h1, h2⟩

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
this : Subsingleton G
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P

Tactic:
Subsingleton.elim (MonoidHom.transferSylow P (hP.normalizer_le_centralizer rfl)).ker ⊥,

Goal state after:
case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
this : Subsingleton G
⊢ ⊥.IsComplement' ↑P
Module: Mathlib.GroupTheory.Frattini

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
⊢ (frattini G).Characteristic

Tactic:
rw [characteristic_iff_comap_eq]

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
⊢ ∀ (ϕ : G ≃* G), comap ϕ.toMonoidHom (frattini G) = frattini G
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
L : List (α × Bool)
⊢ conjugator L ++ reduceCyclically L ++ invRev (conjugator L) = L

Tactic:
by
  induction L using List.bidirectionalRec
  case nil => simp
  case singleton => simp
  case cons_append a l b eq =>
    rw [reduceCyclically.cons_append, conjugator.cons_append]
    split
    case isTrue h =>
      nth_rw 4 [← eq]
      simp [invRev, h.1.symm, h.2.symm]
    case isFalse => simp

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ
⊢ ⁅upperCentralSeries G (n + 1), ⊤⁆ ≤ upperCentralSeries G n

Tactic:
apply closure_le _ |>.mpr

Goal state after:
G : Type u_1
inst✝ : Group G
n : ℕ
⊢ {g | ∃ g₁ ∈ upperCentralSeries G (n + 1), ∃ g₂ ∈ ⊤, ⁅g₁, g₂⁆ = g} ⊆ ↑(upperCentralSeries G n)
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
hc : conjugator x.toWord = conjugator y.toWord
n : ℕ
hn : n + 1 ≠ 0
heq : g x (n + 1) = g y (n + 1)
heq₂ : g x (2 * (n + 1)) = g y (2 * (n + 1))
leq : f x (n + 1) = f y (n + 1)
leq₂ : f x (2 * (n + 1)) = f y (2 * (n + 1))
heq' :
  (replicate (n + 1) (reduceCyclically x.toWord)).flatten ++ invRev (conjugator x.toWord) =
    (replicate (n + 1) (reduceCyclically y.toWord)).flatten ++ invRev (conjugator y.toWord)
hm : reduceCyclically x.toWord = reduceCyclically y.toWord
this : mk x.toWord = mk y.toWord
⊢ x = y

Tactic:
mk_toWord,

Goal state after:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
hc : conjugator x.toWord = conjugator y.toWord
n : ℕ
hn : n + 1 ≠ 0
heq : g x (n + 1) = g y (n + 1)
heq₂ : g x (2 * (n + 1)) = g y (2 * (n + 1))
leq : f x (n + 1) = f y (n + 1)
leq₂ : f x (2 * (n + 1)) = f y (2 * (n + 1))
heq' :
  (replicate (n + 1) (reduceCyclically x.toWord)).flatten ++ invRev (conjugator x.toWord) =
    (replicate (n + 1) (reduceCyclically y.toWord)).flatten ++ invRev (conjugator y.toWord)
hm : reduceCyclically x.toWord = reduceCyclically y.toWord
this : x = mk y.toWord
⊢ x = y
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) → ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
rintro ⟨n, H, hH, hn⟩
    refine ⟨n, fun m => H (n - m), is_descending_rev_series_of_is_ascending G hn hH, ?_⟩
    dsimp only
    rw [tsub_self]
    exact hH.1

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Characteristic
d : ℕ
a✝ : (S.lowerCentralSeries d).Characteristic
⊢ (S.lowerCentralSeries (d + 1)).Characteristic

Tactic:
rw [lowerCentralSeries_succ]

Goal state after:
case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Characteristic
d : ℕ
a✝ : (S.lowerCentralSeries d).Characteristic
⊢ ⁅S.lowerCentralSeries d, S⁆.Characteristic
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
⊢ S ≤ normalizer ↑(S.lowerCentralSeries (n + 1))

Tactic:
rw [lowerCentralSeries_succ]

Goal state after:
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
⊢ S ≤ normalizer ↑⁅S.lowerCentralSeries n, S⁆
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
· rintro n ⟨H, ⟨hH, hn⟩⟩
    refine ⟨fun m => H (n - m), is_ascending_rev_series_of_is_descending G hn hH, ?_⟩
    dsimp only
    rw [tsub_self]
    exact hH.1

Goal state after:
Module: Mathlib.GroupTheory.Generators

Goal state before:
pp: G : Type u_1
H : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Group G
inst✝ : Group H
P : Generators G ι
f : G →* H
hf : Function.Surjective ⇑f
⊢ Subgroup.map f ⊤ = ⊤

Tactic:
Subgroup.map_top_of_surjective f hf

Goal state after:
G : Type u_1
H : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Group G
inst✝ : Group H
P : Generators G ι
f : G →* H
hf : Function.Surjective ⇑f
⊢ ⊤ = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Normal
n : ℕ
a✝ : (S.lowerCentralSeries n).Normal
⊢ (S.lowerCentralSeries (n + 1)).Normal

Tactic:
rw [lowerCentralSeries_succ]

Goal state after:
case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Normal
n : ℕ
a✝ : (S.lowerCentralSeries n).Normal
⊢ ⁅S.lowerCentralSeries n, S⁆.Normal
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: case mpr
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
x y : G × H
hx : x ∈ I
hy : y ∈ I
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
h : (1, x.2 / y.2) ∈ I
⊢ (y.1 / x.1, 1) ∈ I

Tactic:
· simpa [Prod.mul_def, Prod.div_def] using div_mem (mul_mem h hy) hx

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : IsNilpotent (G ⧸ center G)
⊢ IsNilpotent G

Tactic:
by
  obtain ⟨n, hn⟩ := h.nilpotent
  use n.succ
  simp [← comap_upperCentralSeries_quotient_center, hn]

Goal state after:
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: case mp
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : G
h : H
hgh : (g, h) ∈ I
⊢ (g, h) ∈ map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype) (P.prod Q).range

Tactic:
simpa only [G', H', mem_map, MonoidHom.mem_range, MonoidHom.prod_apply, Subtype.exists,
        Prod.exists, MonoidHom.coe_prodMap, coe_subtype, Prod.mk.injEq, Prod.map_apply,
        MonoidHom.coe_snd, exists_eq_right, exists_and_right, exists_eq_right_right,
        MonoidHom.coe_fst]
        using ⟨⟨h, hgh⟩, ⟨g, hgh⟩, g, h, hgh, ⟨rfl, rfl⟩⟩

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ _root_.StrictMonoOn (upperCentralSeries G) (Set.Iic (nilpotencyClass G))

Tactic:
by
  by_cases hG : IsNilpotent G
  · intros a ha b hb ab
    simp only [Set.mem_Iic] at ha hb
    apply lt_of_le_of_ne
    · exact upperCentralSeries_mono _ ab.le
    · grind only [IsNilpotent.nilpotent', IsNilpotent.nilpotent, eq_top,
        upperCentralSeries_eq_top_iff_nilpotencyClass_le]
  · rw [nilpotencyClass_of_not_nilpotent hG, ← Nat.bot_eq_zero, Set.Iic_bot]
    apply Set.strictMonoOn_singleton

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

Goal state before:
pp: M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
x' y' : α
⊢ ∃ g, g • f x' = f y'

Tactic:
obtain ⟨g, rfl⟩ := h.exists_smul_eq x' y'

Goal state after:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
x' : α
g : M
⊢ ∃ g_1, g_1 • f x' = f (g • x')
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: X : Type u_2
inst✝ : Finite X
hX : Nat.card X ≤ 2
B : Set X
⊢ IsTrivialBlock B

Tactic:
rw [IsTrivialBlock, ← B.ncard_le_one_iff_subsingleton, B.eq_univ_iff_ncard]

Goal state after:
X : Type u_2
inst✝ : Finite X
hX : Nat.card X ≤ 2
B : Set X
⊢ B.ncard ≤ 1 ∨ B.ncard = Nat.card X
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: g : Perm (Fin 5)
h : 3 ∈ g.cycleType
⊢ (g * g).IsThreeCycle

Tactic:
by
  obtain ⟨c, g', rfl, hd, _, h3⟩ := mem_cycleType_iff.1 h
  simp only [mul_assoc]
  rw [hd.commute.eq, ← mul_assoc g']
  suffices hg' : orderOf g' ∣ 2 by
    rw [← pow_two, orderOf_dvd_iff_pow_eq_one.1 hg', one_mul]
    exact (card_support_eq_three_iff.1 h3).isThreeCycle_sq
  rw [← lcm_cycleType, Multiset.lcm_dvd]
  intro n hn
  rw [le_antisymm (two_le_of_mem_cycleType hn) (le_trans (le_card_support_of_mem_cycleType hn) _)]
  apply le_of_add_le_add_left
  rw [← hd.card_support_mul, h3]
  exact (c * g').support.card_le_univ

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ Nat.card α
⊢ 1 < Nat.card α

Tactic:
refine lt_of_lt_of_le (by decide) h3

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

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
g : G
hgxy : g • snoc x = snoc y
hg : g ∈ stabilizer G a
i : Fin n
⊢ g • ↑(x i) = ↑(y i)

Tactic:
rw [← ofStabilizer.snoc_castSucc x, ← smul_apply, hgxy, ofStabilizer.snoc_castSucc]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
⊢ IsMultiplyPretransitive G α (s.ncard + m)

Tactic:
hmn

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
⊢ IsMultiplyPretransitive G α n
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case zero
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α 0
s : Set α
hs : s.ncard = 0
⊢ (fixingSubgroup G s).index * (Nat.card α - 0)! = (Nat.card α)!

Tactic:
rw [Set.ncard_eq_zero] at hs
    simp [hs]

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

Goal state before:
pp: case neg
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = ↑n.succ
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) := Subtype.val ⁻¹' s'
x : α
hxs : x ∈ s'
hxa : ¬x = a
⊢ x ∈ insert a (Subtype.val '' t)

Tactic:
· exact Set.mem_insert_of_mem _
              ⟨⟨x, hxa⟩, by simp only [t, Set.mem_preimage]; exact hxs, rfl⟩

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

Goal state before:
pp: case succ.inl
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : IsMultiplyPreprimitive M α n → m ≤ n → ↑n ≤ ENat.card α → IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn✝ : m ≤ n + 1
hα : ↑(n + 1) ≤ ENat.card α
hmn : m = n + 1
⊢ IsMultiplyPreprimitive M α m

Tactic:
hmn

Goal state after:
case succ.inl
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : IsMultiplyPreprimitive M α n → m ≤ n → ↑n ≤ ENat.card α → IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn✝ : m ≤ n + 1
hα : ↑(n + 1) ≤ ENat.card α
hmn : m = n + 1
⊢ IsMultiplyPreprimitive M α (n + 1)
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy✝ : y ∈ t
hy : y ∈ ⇑f '' s
⊢ φ m • ↑⟨y, hy✝⟩ = ↑⟨y, hy✝⟩

Tactic:
Set.mem_image

Goal state after:
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
x✝¹ : ↥(fixingSubgroup M s)
m : M
hm : m ∈ fixingSubgroup M s
x✝ : ↑t
y : β
hy✝ : y ∈ t
hy : ∃ x ∈ s, f x = y
⊢ φ m • ↑⟨y, hy✝⟩ = ↑⟨y, hy✝⟩
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case w
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h✝ : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨m, hm⟩ => ⟨φ m, ⋯⟩
f' : ↥(ofFixingSubgroup M s) →ₑ[φ'] ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun x ↦
      match x with
      | ⟨x, hx⟩ => ⟨f.toFun x, ⋯⟩,
    map_smul' := ⋯ }
y : β
hy : y ∈ ofFixingSubgroup N t
x : α
hx : f x = y
h : x ∈ s
⊢ y ∈ ⇑f '' s

Tactic:
exact ⟨x, h, hx⟩

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

Goal state before:
pp: case inr
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
⊢ ∃ g, g.IsSwap ∧ g ∈ G

Tactic:
rcases lt_or_ge 1 sᶜ.encard with h1c | h1c'

Goal state after:
case inr.inl
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c : 1 < sᶜ.encard
⊢ ∃ g, g.IsSwap ∧ g ∈ G

case inr.inr
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
⊢ ∃ g, g.IsSwap ∧ g ∈ G
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case pos.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
c : α
hct : c ∈ t
hc : ¬c = a ∧ c ∉ {b}
⊢ ⟨swap c a * swap a b, ⋯⟩ • a = b

Tactic:
· simp only [Subgroup.mk_smul, Perm.smul_def, coe_mul]
      grind

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 α
a : α
t : Set ↥(ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
h : a ∈ Subtype.val '' t
⊢ False

Tactic:
Set.mem_image

Goal state after:
n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        s.ncard = n + 1 →
          n + 2 < Nat.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → Finite α → IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
a : α
t : Set ↥(ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
h : ∃ x ∈ t, ↑x = a
⊢ False
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
this : sᶜ ⊆ B
⊢ Nat.card α < B.ncard * 2

Tactic:
have : sᶜ.ncard ≤ B.ncard := ncard_le_ncard this

Goal state after:
α : 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
this✝ : sᶜ ⊆ B
this : sᶜ.ncard ≤ B.ncard
⊢ Nat.card α < B.ncard * 2
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case inl
α : 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ᶜ
hB' : Nat.card α < sᶜ.ncard * 2
⊢ False

pp: case inr
α : 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ᶜ
hB' : sᶜ.ncard * 2 ≤ Nat.card α
⊢ False

Tactic:
· apply h0.ne_empty
      rw [← compl_univ_iff]
      exact hsc.eq_univ_of_card_lt hB'

Goal state after:
case inr
α : 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ᶜ
hB' : sᶜ.ncard * 2 ≤ Nat.card α
⊢ False