mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

Goal state before:
pp: E : Type u_1
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
H : Type u_2
inst✝¹² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → NormedAddCommGroup (V x)
inst✝⁵ : (x : M) → InnerProductSpace ℝ (V x)
inst✝⁴ : FiberBundle F V
σ τ : (x : M) → V x
cov : CovariantDerivative I F V
inst✝³ : VectorBundle ℝ F V
inst✝² : IsContMDiffRiemannianBundle I 1 F V
X : (x : M) → TangentSpace I x
inst✝¹ : ContMDiffVectorBundle 1 F V I
inst✝ : FiniteDimensional ℝ F
x : M
hσ : MDiffAt (T% σ) x
hτ : MDiffAt (T% τ) x
⊢ (((TensorialAt.mkHom₂ (fun x1 x2 ↦ derivMetricTensorAux I cov x1 x2 x) x ⋯ ⋯) (σ x)) (τ x)) (X x) =
    ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) - (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x -
      (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x

Tactic:
TensorialAt.mkHom₂_apply _ _ hσ hτ,

Goal state after:
E : Type u_1
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
H : Type u_2
inst✝¹² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → NormedAddCommGroup (V x)
inst✝⁵ : (x : M) → InnerProductSpace ℝ (V x)
inst✝⁴ : FiberBundle F V
σ τ : (x : M) → V x
cov : CovariantDerivative I F V
inst✝³ : VectorBundle ℝ F V
inst✝² : IsContMDiffRiemannianBundle I 1 F V
X : (x : M) → TangentSpace I x
inst✝¹ : ContMDiffVectorBundle 1 F V I
inst✝ : FiniteDimensional ℝ F
x : M
hσ : MDiffAt (T% σ) x
hτ : MDiffAt (T% τ) x
⊢ (derivMetricTensorAux I cov σ τ x) (X x) =
    ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) - (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x -
      (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank ↥(closureCommutatorRepresentatives G) ≤ 2 * Nat.card ↑(commutatorSet G)

Tactic:
by
  rw [two_mul]
  exact
    (Subgroup.rank_closure_finite_le_nat_card _).trans
      ((Set.card_union_le _ _).trans
        (add_le_add ((Finite.card_image_le _).trans (Finite.card_range_le _))
          ((Finite.card_image_le _).trans (Finite.card_range_le _))))

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

Tactic:
classical
  rcases fintypeOrInfinite G; swap
  · rw [mul_comm, Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_mul]
  simp only [Nat.card_eq_fintype_card]
  calc card { p : G × G // Commute p.1 p.2 }
      _ = card ((a : G) × { b // Commute a b }) :=
            card_congr (Equiv.subtypeProdEquivSigmaSubtype Commute)
      _ = ∑ i, card { b // Commute i b } := card_sigma
      _ = ∑ x, card (MulAction.fixedBy G x) :=
            sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // Commute a b })
              (fun g ↦ card (MulAction.fixedBy G g))
              fun g ↦ card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.eq
      _ = card (Quotient (MulAction.orbitRel (ConjAct G) G)) * card (ConjAct G) :=
             MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group _ _
      _ = card (ConjClasses G) * card G := by
             congr 1; apply card_congr'; congr; ext
             exact (Setoid.comm' _).trans isConj_iff.symm

Goal state after:
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
⊢ inl.range ⊔ inr.range = Subgroup.closure (Set.range ⇑inl ∪ Set.range ⇑inr)

Tactic:
Subgroup.closure_union,

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
⊢ inl.range ⊔ inr.range = Subgroup.closure (Set.range ⇑inl) ⊔ Subgroup.closure (Set.range ⇑inr)
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
f : { f // M.IsLiftable f }
i : B
⊢ ↑((fun ι ↦ ⟨⇑ι ∘ cs.simple, ⋯⟩) ((fun f ↦ (Units.coeHom G).comp (cs.groupLift ⋯)) f)) i = ↑f i

Tactic:
simp only [MonoidHom.comp_apply, comp_apply, groupLift, simple]

Goal state after:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
f : { f // M.IsLiftable f }
i : B
⊢ (Units.coeHom G)
      ((PresentedGroup.toGroup (@CoxeterSystem.relations_liftable B M Gˣ Units.instGroup (restrictUnit ⋯) ⋯))
        (cs.mulEquiv.toMonoidHom (cs.mulEquiv.symm (PresentedGroup.of i)))) =
    ↑f i
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ ∀ (i i' : B), Multiplicative.ofAdd (1 + 1) ^ M.M i i' = 1

Tactic:
(by decide : (1 + 1 : ZMod 2) = 0)

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ ∀ (i i' : B), Multiplicative.ofAdd 0 ^ M.M i i' = 1
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.rightInvSeq ω).getD j 1 =
      (cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)
j' : ℕ
⊢ ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω :: cs.rightInvSeq ω).getD (j' + 1) 1 =
    (cs.wordProd (drop (j' + 1 + 1) (i :: ω)))⁻¹ * (Option.map cs.simple (i :: ω)[j' + 1]?).getD 1 *
      cs.wordProd (drop (j' + 1 + 1) (i :: ω))

Tactic:
simp only [getD_eq_getElem?_getD] at ih
      simp [ih j']

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
α : Type u_2
x : DivisibleHull M
f : M → ℕ+ → α
h : ∀ (m m' : M) (s s' : ℕ+), mk m s = mk m' s' → f m s = f m' s'
p p' : M × ↥(nonZeroDivisors ℕ)
heq : p ≈ p'
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
      obtain ⟨u, hu⟩ := heq
      exact mk_eq_mk.mpr ⟨↑ⁿ.symm u, hu⟩

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a h : G
hh : h ∈ ↑H
k : G
hk : k ∈ ↑K
hb : h * a * k ∈ doubleCoset a ↑H ↑K
⊢ doubleCoset (h * a * k) ↑H ↑K = doubleCoset a ↑H ↑K

Tactic:
rw [doubleCoset, doubleCoset, ← Set.singleton_mul_singleton, ← Set.singleton_mul_singleton,
    mul_assoc, mul_assoc, Subgroup.singleton_mul_subgroup hk, ← mul_assoc, ← mul_assoc,
    Subgroup.subgroup_mul_singleton hh]

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ∃ x ∈ doubleCoset a ↑H ↑K, x ∈ doubleCoset b ↑H ↑K
⊢ b ∈ doubleCoset a ↑H ↑K

Tactic:
simp only [mem_doubleCoset] at *

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ∃ x, (∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * a * y) ∧ ∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * b * y
⊢ ∃ x ∈ ↑H, ∃ y ∈ ↑K, b = x * a * y
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
ι : Type
w✝ : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h₂.some
e' : (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) ≃* ((i : ι) → Multiplicative (ZMod (n i)) →* Mˣ) :=
  Pi.monoidHomMulEquiv (fun i ↦ Multiplicative (ZMod (n i))) Mˣ
this : ∀ (i : ι), NeZero (n i)
⊢ Nonempty ((G →* Mˣ) ≃* G)

Tactic:
have inst i : HasEnoughRootsOfUnity M <| Nat.card <| Multiplicative <| ZMod (n i) := by
    have hdvd : Nat.card (Multiplicative (ZMod (n i))) ∣ Monoid.exponent G := by
      simpa only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, ZMod.card]
        using dvd_exponent e i
    exact HasEnoughRootsOfUnity.of_dvd M hdvd

Goal state after:
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
ι : Type
w✝ : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h₂.some
e' : (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) ≃* ((i : ι) → Multiplicative (ZMod (n i)) →* Mˣ) :=
  Pi.monoidHomMulEquiv (fun i ↦ Multiplicative (ZMod (n i))) Mˣ
this : ∀ (i : ι), NeZero (n i)
inst : ∀ (i : ι), HasEnoughRootsOfUnity M (Nat.card (Multiplicative (ZMod (n i))))
⊢ Nonempty ((G →* Mˣ) ≃* G)
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
rintro ⟨n, H, hH, hn⟩
    refine ⟨n, 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.Goursat

Goal state before:
pp: 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
⊢ I =
    map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype)
      (comap ((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)) e.toMonoidHom.graph)

Tactic:
rw [← he]

Goal state after:
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
⊢ I =
    map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype)
      (comap ((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd))
        (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G

Tactic:
rw [Group.nilpotencyClass_def, Nat.find_eq_zero, upperCentralSeries_zero,
    subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]

Goal state after:
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₁ B₂ : Set X
h₁ : IsBlock G B₁
h₂ : IsBlock G B₂
⊢ IsBlock G (B₁ ∩ B₂)

Tactic:
simp only [isBlock_iff_smul_eq_smul_of_nonempty, smul_set_inter] at h₁ h₂ ⊢

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₁ ∩ g₂ • B₁).Nonempty → g₁ • B₁ = g₂ • B₁
h₂ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₂ ∩ g₂ • B₂).Nonempty → g₁ • B₂ = g₂ • B₂
⊢ ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₁ ∩ g₁ • B₂ ∩ (g₂ • B₁ ∩ g₂ • B₂)).Nonempty → g₁ • B₁ ∩ g₁ • B₂ = g₂ • B₁ ∩ g₂ • B₂
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
a : α
this : Fintype α := Fintype.ofFinite α
⊢ {a}ᶜ.card + {a}.card = Nat.card α

pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
a : α
this : Fintype α := Fintype.ofFinite α
⊢ ∀ (x : α), x ∈ {a}ᶜ ↔ x ∈ ofStabilizer G a

Tactic:
Finset.card_compl_add_card,

Goal state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
a : α
this : Fintype α := Fintype.ofFinite α
⊢ Fintype.card α = Nat.card α

G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
a : α
this : Fintype α := Fintype.ofFinite α
⊢ ∀ (x : α), x ∈ {a}ᶜ ↔ x ∈ ofStabilizer G a
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)
⊢ ∀ x ∈ Finset.univ, (Set.range ⇑f ∩ ↑x).ncard ≤ 1

Tactic:
· rintro ⟨x, ⟨g, rfl⟩⟩ -
    suffices Set.Subsingleton (Set.range f ∩ g • B) by simpa
    -- It suffices to prove that the preimage is subsingleton
    rw [← Set.image_preimage_eq_range_inter]
    apply Set.Subsingleton.image
    -- Since the action of M on α is primitive, it suffices to prove that
    -- the preimage is a block which is not ⊤
    apply Or.resolve_right (isTrivialBlock_of_isBlock ((hB.translate g).preimage f))
    intro h
    simp only [Set.preimage_eq_univ_iff] at h
    -- We will prove that B is large, which will contradict the assumption that it is not ⊤
    apply hB_ne_top
    apply hB.eq_univ_of_card_lt
    -- It remains to show that Nat.card β < Set.ncard B * 2
    apply lt_of_lt_of_le hf'
    rw [mul_comm, mul_le_mul_iff_left₀ Nat.succ_pos']
    apply le_trans (Set.ncard_le_ncard h) (Set.ncard_image_le B.toFinite)

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

Goal state before:
pp: case «2»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
ha : Even 2
h2 : g.cycleType = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ (swap 0 4).Disjoint (swap 1 3)

Tactic:
rw [disjoint_iff_disjoint_support, support_swap h04, support_swap h13]

Goal state after:
case «2»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
ha : Even 2
h2 : g.cycleType = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ _root_.Disjoint {0, 4} {1, 3}
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this : IsPretransitive G α
⊢ Nontrivial α

Tactic:
← ENat.one_lt_card_iff_nontrivial

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this : IsPretransitive G α
⊢ 1 < ENat.card α
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this✝ : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : normalClosure ↑(stabilizer G a) ≤ stabilizer G a
⊢ Nontrivial ↥(ofStabilizer G a)

Tactic:
← ENat.one_lt_card_iff_nontrivial

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this✝ : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : normalClosure ↑(stabilizer G a) ≤ stabilizer G a
⊢ 1 < ENat.card ↥(ofStabilizer G a)
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case mpr.left
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
⊢ IsMultiplyPretransitive M α n.succ

Tactic:
exact ofStabilizer.isMultiplyPretransitive.mpr H.isMultiplyPretransitive

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))
x : α
hx : x ∈ ofFixingSubgroup M s
hx'✝ : ⟨x, hx⟩ ∈ Subtype.val ⁻¹' t
hx' : x ∈ t
⊢ ⟨↑m, ⋯⟩ • x = x

Tactic:
exact (mem_fixingSubgroup_union_iff.mp m.prop).2 ⟨x, hx'⟩

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

Goal state before:
pp: 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
hn1 : 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
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
⊢ t.ncard < n + 1

Tactic:
← hsn

Goal state after:
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
hn1 : 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
ht : t.Finite
htm : t.ncard = t.ncard - 1 + 1
⊢ t.ncard < s.ncard
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
m n : ℕ
inst✝¹ : IsMultiplyPreprimitive M α n
s : Set α
inst✝ : Finite ↑s
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = ↑m
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) t)

Tactic:
let t' : Set α := Subtype.val '' t
    have htt' : t = Subtype.val ⁻¹' t' :=
      (Set.preimage_image_eq _ Subtype.coe_injective).symm
    rw [htt']
    suffices IsPreprimitive (fixingSubgroup M (s ∪ t')) (ofFixingSubgroup M (s ∪ t')) by
      apply IsPreprimitive.of_surjective map_ofFixingSubgroupUnion_bijective.surjective
    apply IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup _ n
    rw [Set.encard_union_eq _]
    · rw [Subtype.coe_injective.encard_image, add_assoc, ht,
        ← hs, Nat.cast_add, Set.Finite.cast_ncard_eq]
      exact Set.toFinite s
    · apply disjoint_val_image

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

Goal state before:
pp: 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
⊢ t.ncard < n + 1

Tactic:
← hsn

Goal state after:
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
⊢ t.ncard < s.ncard
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : 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
⊢ univ.encard = 2

Tactic:
← Set.encard_add_encard_compl s

Goal state after:
α : 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
⊢ s.encard + sᶜ.encard = 2
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
n : ℕ
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
x✝ : Infinite α
⊢ False

Tactic:
simp [Nat.card_eq_zero_of_infinite] at hsn'

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
s : Set α
inst✝¹ : Finite α
inst✝ : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : k ∈ fixingSubgroup M s
hx' : ⟨k, hk⟩ • b ∈ sᶜ
⊢ (⟨k, ?m.152⟩ • B ∩ B).Nonempty

pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
s : Set α
inst✝¹ : Finite α
inst✝ : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : k ∈ fixingSubgroup M s
hx' : ⟨k, hk⟩ • b ∈ sᶜ
⊢ k ∈ G

Tactic:
· refine ⟨a, ?_, ha⟩
      rw [mem_fixingSubgroup_iff] at hk
      rw [← hk a ha']
      exact Set.smul_mem_smul_set ha

Goal state after:
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
s : Set α
inst✝¹ : Finite α
inst✝ : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : k ∈ fixingSubgroup M s
hx' : ⟨k, hk⟩ • b ∈ sᶜ
⊢ k ∈ G