mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
hf : IsSubmersionAtOfComplement F I J n f x
hfg : f =ᶠ[𝓝 x] g
⊢ IsSubmersionAtOfComplement F I J n g x

Tactic:
exact LiftSourceTargetPropertyAt.congr_of_eventuallyEq
    isLocalSourceTargetProperty_submmersionAtProp hf.property hfg

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
F : Type u_5
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → Module 𝕜 (V x)
inst✝¹ : (x : M) → TopologicalSpace (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
hs : IsLocalFrameOn I F n s u
hs' : ∀ (i : ι), ∀ x ∈ u, s i x = s' i x
⊢ ∀ {x : M}, x ∈ u → LinearIndependent 𝕜 fun x_1 ↦ s' x_1 x

Tactic:
by
    intro x hx
    have := hs.linearIndependent hx
    simp_all

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
t : (x : M) → V x
inst✝¹ : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F 1 s u
inst✝ : FiniteDimensional 𝕜 F
h : ∀ (i : ι), MDiff[u] ((LinearMap.piApply (hs.coeff i)) t)
x : M
hx : x ∈ u
this✝ : Fintype ι
this : ∀ (i : ι), MDiff[u] fun x ↦ ⟨x, ((LinearMap.piApply (hs.coeff i)) t • s i) x⟩
⊢ MDiff[u] (T% t)

Tactic:
have almost : MDiff[u] (T% (fun x ↦ ∑ i, hs.coeff i x (t x) • s i x)) :=
    .sum_section (fun i _ _ hx ↦ this i _ hx)

Goal state after:
case inr
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
t : (x : M) → V x
inst✝¹ : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F 1 s u
inst✝ : FiniteDimensional 𝕜 F
h : ∀ (i : ι), MDiff[u] ((LinearMap.piApply (hs.coeff i)) t)
x : M
hx : x ∈ u
this✝ : Fintype ι
this : ∀ (i : ι), MDiff[u] fun x ↦ ⟨x, ((LinearMap.piApply (hs.coeff i)) t • s i) x⟩
almost : MDiff[u] fun x ↦ ⟨x, ∑ i, (hs.coeff i x) (t x) • s i x⟩
⊢ MDiff[u] (T% t)
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
cov cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
hcov' : IsCovariantDerivativeOn F cov' s
x : M
hx : x ∈ s
f✝ : M → 𝕜
σ✝ : (x : M) → V x
hf : MDiffAt f✝ x
hσ : MDiffAt (T% σ✝) x
⊢ differenceAux cov cov' (f✝ • σ✝) x = f✝ x • differenceAux cov cov' σ✝ x

Tactic:
by
    simp [differenceAux, hcov.leibniz hσ hf, hcov'.leibniz hσ hf]
    module

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

Goal state before:
pp: n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h : Commute (sr i, r j).1 (sr i, r j).2
⊢ (fun x ↦
        match x with
        | Sum.inl i => ⟨(sr i, r 0), ⋯⟩
        | Sum.inr (Sum.inl j) => ⟨(r 0, sr j), ⋯⟩
        | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)), ⋯⟩
        | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(r i, r j), ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨(sr i, r a), property⟩ => Sum.inl i
          | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j)
          | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j)))
          | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j))))
        ⟨(sr i, r j), h⟩) =
    ⟨(sr i, r j), h⟩

Tactic:
simpa [-r_zero, sub_eq_add_neg, eq_neg_iff_add_eq_zero, hu, eq_comm (a := j) (b := 0)]
          using h.eq

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ MonoidHom.mrange inl ⊔ MonoidHom.mrange inr = Submonoid.closure (Set.range ⇑inl ∪ Set.range ⇑inr)

Tactic:
Submonoid.closure_union,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ MonoidHom.mrange inl ⊔ MonoidHom.mrange inr = Submonoid.closure (Set.range ⇑inl) ⊔ Submonoid.closure (Set.range ⇑inr)
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:

Tactic:
ℓ (π ω') ≤ ω'.length := cs.length_wordProd_le ω'
    _ < (i :: ω').length := by simp

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
t : W
ht : t ∈ cs.rightInvSeq ω
⊢ cs.IsReflection t

Tactic:
induction ω with
  | nil => simp at ht
  | cons i ω ih =>
    dsimp [rightInvSeq] at ht
    rcases ht with _ | ⟨_, mem⟩
    · use (π ω)⁻¹, i
      group
    · exact ih mem

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m m' : M
s s' : ℕ+
⊢ mk m s < mk m' s' ↔ ↑s' • m < ↑s • m'

Tactic:
simp_rw [lt_iff_not_ge, mk_le_mk]

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ
h : b < c
⊢ 0 < c • a - b • a

Tactic:
rw [← sub_smul]

Goal state after:
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ
h : b < c
⊢ 0 < (c - b) • a
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G

Tactic:
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
  rw [← hS1, ← Fintype.card_coe, ← Finset.card_univ, ← Finset.prod_const]
  let f : (∀ g : S, zpowers (g : G)) →* G := noncommPiCoprod fun s t _ x y _ _ => mul_comm x _
  have hf : Function.Surjective f := by
    rw [← MonoidHom.range_eq_top, eq_top_iff, ← hS2, closure_le]
    exact fun g hg => ⟨Pi.mulSingle ⟨g, hg⟩ ⟨g, mem_zpowers g⟩, noncommPiCoprod_mulSingle _ _⟩
  replace hf := card_dvd_of_surjective f hf
  rw [Nat.card_pi] at hf
  refine hf.trans (Finset.prod_dvd_prod_of_dvd _ _ fun g _ => ?_)
  rw [Nat.card_zpowers]
  exact Monoid.order_dvd_exponent (g : G)

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := hR.toRightFun
U : Set G := (fun g ↦ g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u : G
hu : u ∈ ↑(closure U)
r : G
hr : r ∈ R
⊢ f (↑(hR.toRightFun (↑⟨r, hr⟩ * s⁻¹)) * s) = ⟨r, hr⟩

Tactic:
apply (isComplement_iff_existsUnique_mul_inv_mem.mp hR (f (r * s⁻¹) * s)).unique
      (hR.mul_inv_toRightFun_mem (f (r * s⁻¹) * s))

Goal state after:
case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := ⋯
U : Set G := ⋯
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u : G
hu : u ∈ ↑(closure U)
r : G
hr : r ∈ R
⊢ ↑(f (r * s⁻¹)) * s * (↑⟨r, hr⟩)⁻¹ ∈ ↑H
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Finite α
n : ℕ
toFun✝ : α → Fin n
f : Fin n → α
hf_surj : Function.LeftInverse f toFun✝
hf_inj : Function.RightInverse f toFun✝
⊢ (FreeGroup.map f).ker.IsFinitelyNormallyGenerated

Tactic:
· rw [(FreeGroup.map f).ker_eq_bot (FreeGroup.map_injective hf_inj.injective)]
    exact .bot

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
refine ⟨n, fun m => H (n - m), is_descending_rev_series_of_is_ascending G hn hH, ?_⟩

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ (fun m ↦ H (n - m)) n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
n : ℕ
ih : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], nilpotencyClass G = n → P G
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
h : nilpotencyClass G = n + 1
⊢ P G

Tactic:
have hn : Group.nilpotencyClass (G ⧸ center G) = n := by
      simp [nilpotencyClass_quotient_center, h]
    exact hstep _ (ih _ hn)

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G✝ : Type u_1
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
a b c : ℕ
ab✝ : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
ab : a < b
⊢ upperCentralSeries G (a + 1) ≤ upperCentralSeries G a

Tactic:
rw [hn]
    exact upperCentralSeries_mono _ (by grind)

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨h, hy⟩ := hG y

Goal state after:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ ∃ g, g • x = y
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case mpr
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
⊢ IsTrivialBlock B → IsTrivialBlock (g • B)

Tactic:
intro H
    exact IsTrivialBlock.smul H g

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

Goal state before:
pp: case left
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
⊢ Setoid.IsPartition (range fun a ↦ orbit (↥N) a)

Tactic:
apply IsPartition.of_orbits

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

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
⊢ g ∈ H → g ∈ stabilizer G (orbit (↥H) a)

Tactic:
intro hg
    rw [mem_stabilizer_iff, ← Subgroup.coe_mk H g hg, ← Submonoid.smul_def (S := H.toSubmonoid)]
    apply smul_orbit (G := H)

Goal state after:
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:
IsTrivialBlock,

Goal state after:
X : Type u_2
inst✝ : Finite X
hX : Nat.card X ≤ 2
B : Set X
⊢ B.Subsingleton ∨ B = Set.univ
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

Tactic:
by
  let B' := ⋂ (k : G) (_ : a ∈ k • B), k • B
  rcases Set.eq_empty_or_nonempty B with hfB_e | hfB_ne
  · simp [hfB_e]
  have hB'₀ : ∀ (k : G) (_ : a ∈ k • B), B' ≤ k • B := by
    intro k hk
    exact Set.biInter_subset_of_mem hk
  have hfB' : B'.Finite := by
    obtain ⟨b, hb : b ∈ B⟩ := hfB_ne
    obtain ⟨k, hk : k • b = a⟩ := exists_smul_eq G b a
    apply Set.Finite.subset (Set.Finite.map _ hfB) (hB'₀ k ⟨b, hb, hk⟩)
  have hag : ∀ g : G, a ∈ g • B' → B' ≤ g • B' := by
    intro g hg x hx
    -- a = g • b; b ∈ B'; a ∈ k • B → b ∈ k • B
    simp only [B', Set.mem_iInter, Set.mem_smul_set_iff_inv_smul_mem,
      smul_smul, ← mul_inv_rev] at hg hx ⊢
    exact fun _ ↦ hx _ ∘ hg _
  have hag' (g : G) (hg : a ∈ g • B') : B' = g • B' := by
    rw [eq_comm, ← mem_stabilizer_iff, mem_stabilizer_set_iff_subset_smul_set hfB']
    exact hag g hg
  rw [isBlock_iff_smul_eq_of_nonempty]
  rintro g ⟨b : X, hb' : b ∈ g • B', hb : b ∈ B'⟩
  obtain ⟨k : G, hk : k • a = b⟩ := exists_smul_eq G a b
  have hak : a ∈ k⁻¹ • B' := by
    refine ⟨b, hb, ?_⟩
    simp only [← hk, inv_smul_smul]
  have hagk : a ∈ (k⁻¹ * g) • B' := by
    rw [mul_smul, Set.mem_smul_set_iff_inv_smul_mem, inv_inv, hk]
    exact hb'
  have hkB' : B' = k⁻¹ • B' := hag' k⁻¹ hak
  have hgkB' : B' = (k⁻¹ * g) • B' := hag' (k⁻¹ * g) hagk
  rw [mul_smul] at hgkB'
  rw [← smul_eq_iff_eq_inv_smul] at hkB' hgkB'
  rw [← hgkB', hkB']

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

Goal state before:
pp: case inr
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
⊢ IsTrivialBlock B

Tactic:
IsTrivialBlock,

Goal state after:
case inr
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
⊢ B.Subsingleton ∨ B = Set.univ
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)
⊢ ↑(Set.range fun g ↦ g • B).toFinset.card ≤ (orbit H B).ncard

Tactic:
← Set.ncard_eq_toFinset_card',

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)
⊢ ↑(Set.range fun g ↦ g • B).ncard ≤ (orbit H B).ncard
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case inr
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
x : X
hx : x ∈ A
g : G
hg : g • x = a
⊢ ∃ g, a ∈ g • A

Tactic:
use g, x

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Embedding

Goal state before:
pp: α : Type u_1
m n : ℕ
inst✝ : Finite α
hmn : m ≤ n
hn : n ≤ Nat.card α
⊢ Surjective fun x ↦ (castLEEmb hmn).trans x

Tactic:
by
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
  exact Fin.Embedding.restrictSurjective_of_add_le_natCard hn

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

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
a b : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: b :: l, g.IsSwap
hn : (b :: l).length = 2 * n + 1
⊢ (a :: b :: l).prod ∈ closure {σ | σ.IsThreeCycle}

Tactic:
rw [List.prod_cons, List.prod_cons, ← mul_assoc]

Goal state after:
case succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
a b : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: b :: l, g.IsSwap
hn : (b :: l).length = 2 * n + 1
⊢ a * b * l.prod ∈ closure {σ | σ.IsThreeCycle}
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα4 : 4 ≤ Nat.card α
⊢ center ↥(alternatingGroup α) ≤ ⊥

Tactic:
rintro ⟨g, hg⟩ hg'

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ center ↥(alternatingGroup α)
⊢ ⟨g, hg⟩ ∈ ⊥
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Perm α)
hG : G.index ≤ 2
⊢ alternatingGroup α ≤ G

Tactic:
rcases G.index.eq_zero_or_pos with h | h
  · exact (index_ne_zero_of_finite h).elim
  rcases (Nat.succ_le_iff.mpr h).eq_or_lt' with h | h
  · exact index_eq_one.mp h ▸ le_top
  rw [eq_alternatingGroup_of_index_eq_two (hG.antisymm h)]

Goal state after:
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 α
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
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
obtain ⟨g, hg : g • b = a⟩ := exists_smul_eq M b a

Goal state after:
case mpr.right
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
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : ⟨a, ha⟩ ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
⊢ ∃ a_1, (map_ofFixingSubgroupUnion M s t) a_1 = ⟨⟨a, ha⟩, ha'⟩

Tactic:
suffices a ∈ ofFixingSubgroup M (s ∪ t) by
      exact ⟨⟨a, this⟩,  rfl⟩

Goal state after:
case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
a : α
ha : a ∈ ofFixingSubgroup M s
ha' : ⟨a, ha⟩ ∈ ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t)
⊢ a ∈ ofFixingSubgroup M (s ∪ t)
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s : Set α
n : ℕ
inst✝ : Finite ↑s
x : Fin n ↪ ↥(ofFixingSubgroup M s)
this : Nonempty (Fin s.ncard ≃ ↑s)
y : Fin s.ncard ↪ ↑s := (Classical.choice this).toEmbedding
⊢ Fin (s.ncard + n) ↪ α

Tactic:
apply Fin.Embedding.append (x := y.trans (subtype _)) (y := x.trans (subtype _))

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s : Set α
n : ℕ
inst✝ : Finite ↑s
x : Fin n ↪ ↥(ofFixingSubgroup M s)
this : Nonempty (Fin s.ncard ≃ ↑s)
y : Fin s.ncard ↪ ↑s := ⋯
⊢ Disjoint (Set.range ⇑(y.trans (subtype fun x ↦ x ∈ s)))
    (Set.range ⇑(x.trans (subtype fun x ↦ x ∈ ofFixingSubgroup M s)))
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
⊢ b ∈ s

Tactic:
have hg : swap a b ∈ stabilizer (Perm α) s := by simp_all

Goal state after:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : stabilizer (Perm α) s = ⊤
hg : swap a b ∈ stabilizer (Perm α) s
⊢ b ∈ s
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : ∀ ⦃a : α⦄, a ∈ s → a ∉ ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = -1
x : ↑s
⊢ k ↑x = ↑x

Tactic:
← notMem_support

Goal state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : ∀ ⦃a : α⦄, a ∈ s → a ∉ ↑k.support
hks : k • s = s
g : Perm ↑s
hsg : sign g = -1
x : ↑s
⊢ ↑x ∉ k.support
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
⊢ ∃ g, g.IsSwap ∧ g ∈ G

Tactic:
have : ∀ (t : Set α) (_ : 1 < t.encard), ∃ (g : Perm α),
      g.IsSwap ∧ g ∈ stabilizer (Perm α) t := by
    intro t ht
    rw [Set.one_lt_encard_iff] at ht
    obtain ⟨a, b, ha, hb, h⟩ := ht
    use swap a b, Perm.swap_isSwap_iff.mpr h, swap_mem_stabilizer ha hb
  rcases lt_or_ge 1 s.encard with h1 | h1'
  · obtain ⟨g, hg, hg'⟩ := this s h1
    exact ⟨g, hg, hG.le hg'⟩
  rcases lt_or_ge 1 sᶜ.encard with h1c | h1c'
  · obtain ⟨g, hg, hg'⟩ := this sᶜ h1c
    use g, hg
    rw [stabilizer_compl] at hg'
    exact hG.le hg'
  have hα : Set.encard (_root_.Set.univ : Set α) = 2 := by
    rw [← Set.encard_add_encard_compl s]
    have : (1 + 1 : ENat) = 2 := by norm_num
    convert! this <;>
    · apply le_antisymm
      · assumption
      rw [one_le_encard_iff_nonempty, Set.nonempty_iff_ne_empty]
      aesop
  have _ : Finite α := by
    rw [finite_iff_nonempty_fintype]
    refine univ_finite_iff_nonempty_fintype.mp ?_
    exact finite_of_encard_eq_coe hα
  have hα : Nat.card α = 2 := by
    rw [← ENat.card_coe_set_eq, ENat.card_eq_coe_natCard, Nat.card_coe_set_eq, ncard_univ] at hα
    exact ENat.natCast_inj.mp hα
  have hα2 : Fact (Nat.card (Perm α)).Prime := by
    apply Fact.mk
    rw [Nat.card_perm, hα, Nat.factorial_two]
    exact Nat.prime_two
  cases G.eq_bot_or_eq_top_of_prime_card with
  | inl h =>
    exfalso; exact ne_bot_of_gt hG h
  | inr h =>
    rw [h, ← stabilizer_univ_eq_top (Perm α) α]
    apply this
    simp_all

Goal state after: