mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝⁴ : VectorBundle 𝕜 F V
inst✝³ : ContMDiffVectorBundle 1 F V I
e : Trivialization F TotalSpace.proj
inst✝² : MemTrivializationAtlas e
ι : Type u_7
b : Basis ι 𝕜 F
s : (x : M) → V x
x : M
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : CompleteSpace 𝕜
hxe : x ∈ e.baseSet
hs : MDiffAt (T% s) x
i : ι
aux : M → 𝕜 := fun x ↦ (b.repr (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) i
⊢ MDiffAt ((LinearMap.piApply (Trivialization.localFrameCoeff I e b i)) s) x

Tactic:
suffices MDiffAt aux x by
    apply this.congr_of_eventuallyEq
    apply eventuallyEq_of_mem (s := e.baseSet) (by simp [e.open_baseSet.mem_nhds hxe])
    intro y hy
    simp [aux, e.localFrameCoeff_eq_coeff hy]

Goal state after:
𝕜 : 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
inst✝⁴ : VectorBundle 𝕜 F V
inst✝³ : ContMDiffVectorBundle 1 F V I
e : Trivialization F TotalSpace.proj
inst✝² : MemTrivializationAtlas e
ι : Type u_7
b : Basis ι 𝕜 F
s : (x : M) → V x
x : M
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : CompleteSpace 𝕜
hxe : x ∈ e.baseSet
hs : MDiffAt (T% s) x
i : ι
aux : M → 𝕜 := fun x ↦ (b.repr (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) i
⊢ MDiffAt aux x
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
inst✝⁴ : VectorBundle 𝕜 F V
inst✝³ : ContMDiffVectorBundle 1 F V I
e : Trivialization F TotalSpace.proj
inst✝² : MemTrivializationAtlas e
ι : Type u_7
b : Basis ι 𝕜 F
s : (x : M) → V x
x : M
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : CompleteSpace 𝕜
hxe : x ∈ e.baseSet
hs : MDiffAt (T% s) x
i : ι
aux : M → 𝕜 := fun x ↦ (b.repr (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) i
⊢ (MDiffAt fun x ↦ (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) x

Tactic:
simpa using (e.mdifferentiableAt_section_iff I s hxe).1 hs

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

Goal state before:
pp: case r.r.r
n : ℕ
a b c : ZMod n
⊢ r a * r b * r c = r a * (r b * r c)

Tactic:
simp only [(· * ·), mul]

Goal state after:
case r.r.r
n : ℕ
a b c : ZMod n
⊢ r (a + b + c) = r (a + (b + c))
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case r.r.sr
n : ℕ
a b c : ZMod n
⊢ r a * r b * sr c = r a * (r b * sr c)

Tactic:
simp only [(· * ·), mul]

Goal state after:
case r.r.sr
n : ℕ
a b c : ZMod n
⊢ sr (c - (a + b)) = sr (c - b - a)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case r.sr.r
n : ℕ
a b c : ZMod n
⊢ r a * sr b * r c = r a * (sr b * r c)

Tactic:
simp only [(· * ·), mul]

Goal state after:
case r.sr.r
n : ℕ
a b c : ZMod n
⊢ sr (b - a + c) = sr (b + c - a)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case r.sr.sr
n : ℕ
a b c : ZMod n
⊢ r a * sr b * sr c = r a * (sr b * sr c)

Tactic:
simp only [(· * ·), mul]

Goal state after:
case r.sr.sr
n : ℕ
a b c : ZMod n
⊢ r (c - (b - a)) = r (a + (c - b))
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case sr.r.r
n : ℕ
a b c : ZMod n
⊢ sr a * r b * r c = sr a * (r b * r c)

Tactic:
simp only [(· * ·), mul]

Goal state after:
case sr.r.r
n : ℕ
a b c : ZMod n
⊢ sr (a + b + c) = sr (a + (b + c))
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case sr.r.sr
n : ℕ
a b c : ZMod n
⊢ sr a * r b * sr c = sr a * (r b * sr c)

Tactic:
simp only [(· * ·), mul]

Goal state after:
case sr.r.sr
n : ℕ
a b c : ZMod n
⊢ r (c - (a + b)) = r (c - b - a)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case sr.sr.r
n : ℕ
a b c : ZMod n
⊢ sr a * sr b * r c = sr a * (sr b * r c)

Tactic:
simp only [(· * ·), mul]

Goal state after:
case sr.sr.r
n : ℕ
a b c : ZMod n
⊢ r (b - a + c) = r (b + c - a)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case sr.sr.sr
n : ℕ
a b c : ZMod n
⊢ sr a * sr b * sr c = sr a * (sr b * sr c)

Tactic:
simp only [(· * ·), mul]

Goal state after:
case sr.sr.sr
n : ℕ
a b c : ZMod n
⊢ sr (c - (b - a)) = sr (a + (c - b))
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, sr j).1 (sr i, sr 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, sr j), h⟩) =
    ⟨(sr i, sr j), h⟩

Tactic:
by
        replace h := r.inj h
        rw [← neg_sub, neg_eq_iff_add_eq_zero, hu, sub_eq_zero] at h
        rw [Subtype.ext_iff, Prod.ext_iff, sr.injEq, sr.injEq, h, and_self, ← two_mul]
        exact u.inv_mul_cancel_left j

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 = MonoidHom.mrange inl ⊔ Submonoid.closure ↑(MonoidHom.mrange inr)

Tactic:
Submonoid.closure_eq

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ MonoidHom.mrange inl ⊔ MonoidHom.mrange inr = MonoidHom.mrange inl ⊔ MonoidHom.mrange inr
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ uncurry M.relation (i, i) = FreeGroup.of i * FreeGroup.of i

Tactic:
simp [relation]

Goal state after:
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
w : W
⊢ ∃ n ω, n = ω.length ∧ cs.wordProd ω = w

Tactic:
rcases cs.wordProd_surjective w with ⟨ω, rfl⟩

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ ∃ n ω_1, n = ω_1.length ∧ cs.wordProd ω_1 = cs.wordProd ω
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
j : ℕ
⊢ (cs.wordProd (drop (j + 1) ω))⁻¹ *
      ((Option.map cs.simple ω[j]?).getD 1 *
        (cs.wordProd (drop (j + 1) ω) *
          ((cs.wordProd (drop (j + 1) ω))⁻¹ * ((Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω))))) =
    1

Tactic:
rcases em (j < ω.length) with hj | nhj

Goal state after:
case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
hj : j < ω.length
⊢ (cs.wordProd (drop (j + 1) ω))⁻¹ *
      ((Option.map cs.simple ω[j]?).getD 1 *
        (cs.wordProd (drop (j + 1) ω) *
          ((cs.wordProd (drop (j + 1) ω))⁻¹ * ((Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω))))) =
    1

case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
nhj : ¬j < ω.length
⊢ (cs.wordProd (drop (j + 1) ω))⁻¹ *
      ((Option.map cs.simple ω[j]?).getD 1 *
        (cs.wordProd (drop (j + 1) ω) *
          ((cs.wordProd (drop (j + 1) ω))⁻¹ * ((Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω))))) =
    1
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
j : ℕ
⊢ cs.wordProd (take j ω) *
      ((Option.map cs.simple ω[j]?).getD 1 *
        ((cs.wordProd (take j ω))⁻¹ *
          (cs.wordProd (take j ω) * ((Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹)))) =
    1

Tactic:
rcases em (j < ω.length) with hj | nhj

Goal state after:
case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
hj : j < ω.length
⊢ cs.wordProd (take j ω) *
      ((Option.map cs.simple ω[j]?).getD 1 *
        ((cs.wordProd (take j ω))⁻¹ *
          (cs.wordProd (take j ω) * ((Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹)))) =
    1

case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
nhj : ¬j < ω.length
⊢ cs.wordProd (take j ω) *
      ((Option.map cs.simple ω[j]?).getD 1 *
        ((cs.wordProd (take j ω))⁻¹ *
          (cs.wordProd (take j ω) * ((Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹)))) =
    1
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case succ.cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
k : B
ω : List B
tail_ih✝ : cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)
⊢ drop j (cs.rightInvSeq ω) = drop (j + 1) ((cs.wordProd ω)⁻¹ * cs.simple k * cs.wordProd ω :: cs.rightInvSeq ω)

Tactic:
drop_succ_cons

Goal state after:
case succ.cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
k : B
ω : List B
tail_ih✝ : cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)
⊢ drop j (cs.rightInvSeq ω) = drop j (cs.rightInvSeq ω)
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
n : ℕ
h : M → ℝ
b c₀ : ℝ
hb : 1 < b
H : ∀ (x : M), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
t : M
ht : t ∈ {x | IsOfFinOrder x}
⊢ t ∈ {a | h a ≤ c₀ / (b - 1)}

Tactic:
have : Finite ↥(Submonoid.powers t) := ht.finite_powers

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
n : ℕ
h : M → ℝ
b c₀ : ℝ
hb : 1 < b
H : ∀ (x : M), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
t : M
ht : t ∈ {x | IsOfFinOrder x}
this : Finite ↥(Submonoid.powers t)
⊢ t ∈ {a | h a ≤ c₀ / (b - 1)}
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H j)
hh : i ≠ j
this : (lift f) w.inv.prod ≠ 1
heq : (lift f) w.prod = 1
⊢ False

Tactic:
apply this

Goal state after:
case pos
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H j)
hh : i ≠ j
this : (lift f) w.inv.prod ≠ 1
heq : (lift f) w.prod = 1
⊢ (lift f) w.inv.prod = 1
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: case h
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
ι : Type
w✝ : Fintype ι
n : ι → ℕ
left✝ : ∀ (i : ι), 1 < n i
h : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := ⋯
i : ι
hi : e a i ≠ 1
φi : Multiplicative (ZMod (n i)) →* M
hφi : φi (Multiplicative.ofAdd (Multiplicative.toAdd (e a i))) ≠ 1
⊢ ((φi.comp (Pi.evalMonoidHom (fun i ↦ Multiplicative (ZMod (n i))) i)).comp ↑e) a ≠ 1

Tactic:
simpa only [coe_comp, coe_coe, Function.comp_apply, Pi.evalMonoidHom_apply, ne_eq] using! hφi

Goal state after:
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)
⊢ HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))

Tactic:
rwa [Monoid.exponent_eq_of_mulEquiv (monoidHom_mulEquiv_of_hasEnoughRootsOfUnity G M).some]

Goal state after:
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)
Φ : (Subgroup (G →* Mˣ))ᵒᵈ
⊢ HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))

Tactic:
rwa [Monoid.exponent_eq_of_mulEquiv (monoidHom_mulEquiv_of_hasEnoughRootsOfUnity G M).some]

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.focalSubgroupOf.Normal

Tactic:
focalSubgroupOf_def,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (H.focalSubgroup.subgroupOf H).Normal
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
⊢ ⟨g⁻¹ * h * g, hconj⟩⁻¹ * ⟨h, hh⟩ ∈ H.focalSubgroupOf

Tactic:
focalSubgroupOf_def,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
g : G
hconj : g⁻¹ * h * g ∈ H
⊢ ⟨g⁻¹ * h * g, hconj⟩⁻¹ * ⟨h, hh⟩ ∈ H.focalSubgroup.subgroupOf H
Module: Mathlib.Order.Radical

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
w : ∃ a_1, IsCoatom a_1 ∧ a ≤ a_1
⊢ a = ⊤

Tactic:
obtain ⟨m, c, le⟩ := w
    have q : a ⊔ radical α ≤ m := sup_le le (radical_le_coatom c)
    -- Now note that `a ⊔ radical α ≤ m` since both `a ≤ m` and `radical α ≤ m`.
    rw [h, top_le_iff] at q
    simpa using c.1 q

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 ∈ H (n - m)
g : G
hm : n ≤ m
⊢ ⁅x, g⁆ ∈ (fun m ↦ H (n - m)) (m + 1)

pp: case neg
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 ∈ H (n - m)
g : G
hm : m < n
⊢ ⁅x, g⁆ ∈ (fun m ↦ H (n - m)) (m + 1)

Tactic:
· rw [tsub_eq_zero_of_le hm, h0, Subgroup.mem_bot] at hx
    subst hx
    rw [commutatorElement_one_left]
    exact Subgroup.one_mem _

Goal state after:
case neg
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 ∈ H (n - m)
g : G
hm : m < n
⊢ ⁅x, g⁆ ∈ (fun m ↦ H (n - m)) (m + 1)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
g : G
⊢ g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)

Tactic:
rw [smul_orbit_eq_orbit_smul]

Goal state after:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
g : G
⊢ orbit (↥N) (g • a) = orbit (↥N) a ∨ Disjoint (orbit (↥N) (g • a)) (orbit (↥N) 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
a : X
⊢ ∀ (a_1 : BlockMem G a), ⟨{a}, ⋯⟩ ≤ a_1

Tactic:
rintro ⟨B, ha, hB⟩
    simp only [Subtype.mk_le_mk, Set.singleton_subset_iff]
    exact ha

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
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
⊢ ¬b = a

Tactic:
exact Ne.symm h

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
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
⊢ b ∉ B

Tactic:
rw [this]; rw [Set.mem_singleton_iff]; exact Ne.symm h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ center ↥(alternatingGroup α)
a : α
ha : a ∈ g.support
hab : g a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ g a
hd : d ≠ a ∧ d ≠ g a
k : Perm α := swap (g a) d * swap (g a) c
hka : k • a = a
hkga : k • g a = c
this : k • ⟨g, hg⟩ • a ≠ c
⊢ False

Tactic:
apply this

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 α)
a : α
ha : a ∈ g.support
hab : g a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ g a
hd : d ≠ a ∧ d ≠ g a
k : Perm α := ⋯
hka : k • a = a
hkga : k • g a = c
this : k • ⟨g, hg⟩ • a ≠ c
⊢ k • ⟨g, hg⟩ • a = c
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : IsMulCommutative ↥(alternatingGroup α)
h : 3 < Nat.card α
this : ¬Nontrivial ↥(alternatingGroup α)
⊢ False

Tactic:
apply this

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : IsMulCommutative ↥(alternatingGroup α)
h : 3 < Nat.card α
this : ¬Nontrivial ↥(alternatingGroup α)
⊢ Nontrivial ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case succ
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
⊢ (fixingSubgroup (↥(stabilizer G a)) t ⊔ (stabilizer G a).subtype.ker).index * (stabilizer G a).subtype.range.index *
      (Nat.card α - (k + 1))! =
    (Nat.card α)!

Tactic:
MonoidHom.ker_eq_bot (stabilizer G a).subtype
        (by simp only [Subgroup.coe_subtype, Subtype.coe_injective])

Goal state after:
case succ
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
⊢ (fixingSubgroup (↥(stabilizer G a)) t ⊔ ⊥).index * (stabilizer G a).subtype.range.index * (Nat.card α - (k + 1))! =
    (Nat.card α)!
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
hk : ∀ y ∈ t, k • y = y
y : α
hy : y ∈ s
⊢ (MulAut.conj g) k • y = y

Tactic:
rw [MulAut.conj_apply, eq_comm, mul_smul, mul_smul, ← inv_smul_eq_iff, eq_comm]

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
hk : ∀ y ∈ t, k • y = y
y : α
hy : y ∈ s
⊢ k • g⁻¹ • y = g⁻¹ • y
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' : n + 2 < Nat.card α
this✝ : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn✝ : n + 1 < 2
hn : n = 0
a : α
hsa : s = {a}
this : IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
⊢ (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
    (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)

Tactic:
refine ⟨this, fun hs_prim ↦ ?_⟩
      rw [hsa] at hs_prim
      rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G α le_rfl (a := a),
        is_one_preprimitive_iff]
      exact IsPreprimitive.of_surjective
          ofFixingSubgroup_of_singleton_bijective.surjective

Goal state after:
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 α
g : M
hst : g • s = t
⊢ Surjective ⇑(conjMap_ofFixingSubgroup hst)

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ ∃ a, (conjMap_ofFixingSubgroup hst) a = ⟨x, hx⟩
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 α
⊢ 1 < s.ncard

Tactic:
rwa [hsn]

Goal state after: