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
⊢ ∃ C > 0, ∀ᶠ (y : B) in 𝓝 x, ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ < C

Tactic:
refine ⟨(1 + ‖(trivializationAt F E x).continuousLinearMapAt ℝ  x‖) * 2, by positivity, ?_⟩
  filter_upwards [eventually_norm_symmL_trivializationAt_self_comp_lt F E x one_lt_two] with y hy
  have A : ((trivializationAt F E x).continuousLinearMapAt ℝ x) ∘L
      ((trivializationAt F E x).symmL ℝ x) = ContinuousLinearMap.id _ _ := by
    ext v
    have h'x : x ∈ (trivializationAt F E x).baseSet := FiberBundle.mem_baseSet_trivializationAt' x
    simp only [Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply,
      mem_baseSet_trivializationAt, comp_apply, id_apply]
    convert! ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v
    simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]
  have : (trivializationAt F E x).continuousLinearMapAt ℝ y =
    (ContinuousLinearMap.id _ _) ∘L ((trivializationAt F E x).continuousLinearMapAt ℝ y) := by simp
  grw [this, ← A, comp_assoc, opNorm_comp_le]
  gcongr
  linarith

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case cons.refine_1
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
motive : Word M → Sort u_4
empty : motive Word.empty
cons :
  (i : ι) → (m : M i) → (w : Word M) → (h1 : w.fstIdx ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Word.cons m w h1 h2)
m : (i : ι) × M i
w : List ((i : ι) × M i)
ih :
  (h1 : ∀ l ∈ w, l.snd ≠ 1) →
    (h2 : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) w) → motive { toList := w, ne_one := h1, chain_ne := h2 }
h1 : ∀ l ∈ m :: w, l.snd ≠ 1
h2 : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (m :: w)
⊢ { toList := w, ne_one := ⋯, chain_ne := ⋯ }.fstIdx ≠ some m.fst

Tactic:
List.isChain_cons

Goal state after:
case cons.refine_1
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
motive : Word M → Sort u_4
empty : motive Word.empty
cons :
  (i : ι) → (m : M i) → (w : Word M) → (h1 : w.fstIdx ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Word.cons m w h1 h2)
m : (i : ι) × M i
w : List ((i : ι) × M i)
ih :
  (h1 : ∀ l ∈ w, l.snd ≠ 1) →
    (h2 : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) w) → motive { toList := w, ne_one := h1, chain_ne := h2 }
h1 : ∀ l ∈ m :: w, l.snd ≠ 1
h2✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (m :: w)
h2 : (∀ y ∈ w.head?, m.fst ≠ y.fst) ∧ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) w
⊢ { toList := w, ne_one := ⋯, chain_ne := ⋯ }.fstIdx ≠ some m.fst
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case succ
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
⊢ cs.wordProd (alternatingWord i i' (m + 1)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)

Tactic:
rw [alternatingWord_succ', wordProd_cons, ih]

Goal state after:
case succ
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
ih :
  cs.wordProd (alternatingWord i i' m) = (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
⊢ cs.simple (if Even m then i' else i) *
      ((if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)) =
    (if Even (m + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((m + 1) / 2)
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case h₂
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ 1 ≤ cs.length (cs.simple i)

Tactic:
· by_contra! length_lt_one
    have : cs.lengthParity (s i) = Multiplicative.ofAdd 0 := by
      rw [lengthParity_eq_ofAdd_length, Nat.lt_one_iff.mp length_lt_one, Nat.cast_zero]
    have : Multiplicative.ofAdd (0 : ZMod 2) = Multiplicative.ofAdd 1 :=
      this.symm.trans (cs.lengthParity_simple i)
    contradiction

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

Goal state before:
pp: case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) < cs.length w → cs.length (w * cs.simple i) + 1 = cs.length w

pp: case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) + 1 = cs.length w → cs.length (w * cs.simple i) < cs.length w

Tactic:
· intro _
    exact (cs.length_mul_simple w i).resolve_left (by lia)

Goal state after:
case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) + 1 = cs.length w → cs.length (w * cs.simple i) < cs.length w
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ∀ l ∈ _w₁✝.toList, l.snd ≠ 1
_w₂_ih✝ : ∀ l ∈ _w₂✝.toList, l.snd ≠ 1
l : (i : ι) × M i
h : l ∈ (_w₁✝.append _hne✝ _w₂✝).toList
⊢ l.snd ≠ 1

Tactic:
simp only [toList, List.mem_append] at h

Goal state after:
case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ∀ l ∈ _w₁✝.toList, l.snd ≠ 1
_w₂_ih✝ : ∀ l ∈ _w₂✝.toList, l.snd ≠ 1
l : (i : ι) × M i
h : l ∈ _w₁✝.toList ∨ l ∈ _w₂✝.toList
⊢ l.snd ≠ 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 ω ++ ω[j]?.toList ++ drop (j + 1) ω) *
      ((cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)

Tactic:
obtain lt | le := lt_or_ge j ω.length

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 : ℕ
lt : j < ω.length
⊢ cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) *
      ((cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)) =
    cs.wordProd (take j ω ++ drop (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 : ℕ
le : ω.length ≤ j
⊢ cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) *
      ((cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)) =
    cs.wordProd (take j ω ++ drop (j + 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 ω ++ ω[j]?.toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)

Tactic:
obtain lt | le := lt_or_ge j ω.length

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 : ℕ
lt : j < ω.length
⊢ cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (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 : ℕ
le : ω.length ≤ j
⊢ cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : mk m s = mk m' s'
h' : mk n t = mk n' t'
⊢ (↑t • m ≤ ↑s • n) = (↑t' • m' ≤ ↑s' • n')

Tactic:
rw [mk_eq_mk_iff_smul_eq_smul] at h h'
  rw [propext_iff, ← nsmul_le_nsmul_iff_right (mul_ne_zero s'.ne_zero t'.ne_zero)]
  convert! (nsmul_le_nsmul_iff_right (M := M) (mul_ne_zero s.ne_zero t.ne_zero)) using 2
  · simp_rw [smul_smul, mul_rotate s'.val, ← smul_smul, h, smul_smul]
    ring_nf
  · simp_rw [smul_smul, ← mul_rotate s'.val, ← smul_smul, ← h', smul_smul]
    ring_nf

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: ι : Type u_1
G : Type u_2
inst✝ : Monoid G
n : ι → ℕ
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i)))
i : ι
⊢ n i ∣ Monoid.exponent G

Tactic:
have : n i = orderOf (e.symm <| Pi.mulSingle i <| .ofAdd 1) := by
    simpa only [MulEquiv.orderOf_eq, orderOf_piMulSingle, orderOf_ofAdd_eq_addOrderOf]
      using (ZMod.addOrderOf_one (n i)).symm

Goal state after:
ι : Type u_1
G : Type u_2
inst✝ : Monoid G
n : ι → ℕ
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i)))
i : ι
this : n i = orderOf (e.symm (Pi.mulSingle i (Multiplicative.ofAdd 1)))
⊢ n i ∣ Monoid.exponent G
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case hpp.inl
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hlt : 0 < n
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i

pp: case hpp.inr
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i

Tactic:
· have h1n : 1 ≤ n := hlt
      calc
        a i ^ n • X' j ⊆ a i ^ n • (Y i)ᶜ :=
          smul_set_mono ((hXYdisj j i).union_left <| hYdisj hij.symm).subset_compl_right
        _ ⊆ X i := by
          clear hnne0 hlt
          induction n, h1n using Int.leInduction with
          | base => rw [zpow_one]; exact hX i
          | succ n _hle hi =>
            calc
              a i ^ (n + 1) • (Y i)ᶜ = (a i ^ n * a i) • (Y i)ᶜ := by rw [zpow_add, zpow_one]
              _ = a i ^ n • a i • (Y i)ᶜ := mul_smul _ _ _
              _ ⊆ a i ^ n • X i := smul_set_mono <| hX i
              _ ⊆ a i ^ n • (Y i)ᶜ := smul_set_mono (hXYdisj i i).subset_compl_right
              _ ⊆ X i := hi
        _ ⊆ X' i := Set.subset_union_left

Goal state after:
case hpp.inr
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n✝ n : ℤ
hle : n ≤ -1
hi : a i ^ n • (X i)ᶜ ⊆ Y i
⊢ a i ^ (n - 1) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ

Tactic:
rw [zpow_sub, zpow_one]

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ ∏ q, ϕ ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x ↦ g • x) q.out * Quotient.out q.out, ⋯⟩ =
    ϕ ⟨g ^ H.index, ⋯⟩

Tactic:
← Finset.prod_map_toList,

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ (List.map
        (fun q ↦ ϕ ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x ↦ g • x) q.out * Quotient.out q.out, ⋯⟩)
        Finset.univ.toList).prod =
    ϕ ⟨g ^ H.index, ⋯⟩
Module: Mathlib.GroupTheory.FixedPointFree

Goal state before:
pp: F : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : FunLike F G G
inst✝ : MonoidHomClass F G G
φ : F
hφ : FixedPointFree ⇑φ
⊢ Function.Injective (commutatorMap ⇑φ)

Tactic:
refine fun x y h ↦ inv_mul_eq_one.mp <| hφ _ ?_

Goal state after:
F : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : FunLike F G G
inst✝ : MonoidHomClass F G G
φ : F
hφ : FixedPointFree ⇑φ
x y : G
h : commutatorMap (⇑φ) x = commutatorMap (⇑φ) y
⊢ φ (x⁻¹ * y) = x⁻¹ * y
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
x : ↥H
this : Fintype (Quotient (MulAction.orbitRel (↥(zpowers ↑x)) (G ⧸ H)))
⊢ H.transferFocal ↑x = ↑x ^ H.index

Tactic:
rw [transferFocal, index_eq_sum_minimalPeriod H x, ← Finset.prod_pow_eq_pow_sum,
    MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot]

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
x : ↥H
this : Fintype (Quotient (MulAction.orbitRel (↥(zpowers ↑x)) (G ⧸ H)))
⊢ ∏ q,
      (QuotientGroup.mk' H.focalSubgroupOf)
        ⟨(Quotient.out q.out)⁻¹ * ↑x ^ minimalPeriod (fun x_1 ↦ ↑x • x_1) q.out * Quotient.out q.out, ⋯⟩ =
    ∏ i, ↑x ^ minimalPeriod (fun x_1 ↦ ↑x • x_1) i.out
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
ih : IsReduced l → IsCyclicallyReduced (reduceCyclically l)
h : IsReduced (a :: (l ++ [b]))
h✝ : b.1 = a.1 ∧ (!b.2) = a.2
⊢ IsCyclicallyReduced (reduceCyclically l)

Tactic:
exact ih (h.infix ⟨[a], [b], rfl⟩)

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
rintro n ⟨H, ⟨hH, hn⟩⟩
    rw [← top_le_iff, ← hn]
    exact ascending_central_series_le_upper H hH n

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type ?u.18
inst✝ : Monoid X
f : End (root' T) →* X
X✝ Y✝ Z✝ : G
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ f (loopOfHom T (f✝ ≫ g✝)) = f (loopOfHom T g✝ * loopOfHom T f✝)

Tactic:
simp only [IsIso.inv_hom_id_assoc, loopOfHom, End.mul_def, Category.assoc]

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 : Set X
H : Type u_3
Y : Type u_4
inst✝ : SMul H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
hB : IsBlock G B
⊢ ∀ (x x_1 : G), ⇑j '' (x • B) ≠ ⇑j '' (x_1 • B) → Disjoint (⇑j '' (x • B)) (⇑j '' (x_1 • B))

Tactic:
exact fun g₁ g₂ hg ↦ disjoint_image_of_injective hj <| hB <| ne_of_apply_ne _ hg

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 : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ ⦃B_1 : Set X⦄, (B_1 ∈ range fun g ↦ g • B) → IsBlock G B_1

Tactic:
rintro B' ⟨g, rfl⟩

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
g : G
⊢ IsBlock G ((fun g ↦ g • B) g)
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.index = 2
x : G
hxH : x ∈ H
g : G
⊢ (g ∈ H ↔ x ∈ H) ↔ g⁻¹ ∈ H

Tactic:
hxH,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.index = 2
x : G
hxH : x ∈ H
g : G
⊢ (g ∈ H ↔ True) ↔ g⁻¹ ∈ H
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:
by
    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
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)
g : H
h : Set.range ⇑f ⊆ g • B
⊢ (Set.range ⇑f).ncard * 2 ≤ B.ncard * 2

Tactic:
mul_le_mul_iff_left₀ Nat.succ_pos'

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)
g : H
h : Set.range ⇑f ⊆ g • B
⊢ (Set.range ⇑f).ncard ≤ B.ncard
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ closure {σ | σ.IsThreeCycle} = alternatingGroup α

Tactic:
refine closure_eq_of_le _ (fun _ ↦ IsThreeCycle.mem_alternatingGroup) fun σ hσ ↦ ?_

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
⊢ σ ∈ closure {σ | σ.IsThreeCycle}
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).cycleType + (swap 1 3).cycleType = Multiset.replicate 2 2

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:
(isCycle_swap h04).cycleType,

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
⊢ {(swap 0 4).support.card} + (swap 1 3).cycleType = Multiset.replicate 2 2

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)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

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

Tactic:
rw [← not_nontrivial_iff_subsingleton] at this

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

Goal state before:
pp: case mpr
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 α := ⋯
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) := ⋯
x : α
⊢ x ∈ insert a (Subtype.val '' t) → x ∈ s'

Tactic:
rw [Set.mem_insert_iff]

Goal state after:
case mpr
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 : α
⊢ x = a ∨ x ∈ Subtype.val '' t → x ∈ s'
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
s : Set α
hMk : IsMultiplyPretransitive G α s.ncard
⊢ s.ncard ≤ Nat.card α

Tactic:
rw [← ncard_univ]

Goal state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
s : Set α
hMk : IsMultiplyPretransitive G α s.ncard
⊢ s.ncard ≤ univ.ncard
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ IsMultiplyPretransitive (Perm α) α n

Tactic:
rw [isMultiplyPretransitive_iff]

Goal state after:
α : Type u_1
n : ℕ
⊢ ∀ (x y : Fin n ↪ α), ∃ g, g • x = y
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : (t \ {a, b}).Nonempty
⊢ ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b

Tactic:
obtain ⟨c, hct, hc⟩ := ht

Goal state after:
case pos
α : 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, b}
⊢ ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b
Module: Mathlib.GroupTheory.GroupExtension.Defs

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
⊢ (MonoidHom.ofInjective ⋯).trans (MulEquiv.trans (MulAut.conjNormal 1) (MonoidHom.ofInjective ⋯).symm) = 1

Tactic:
ext _

Goal state after:
N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
x✝ : N
⊢ ((MonoidHom.ofInjective ⋯).trans (MulEquiv.trans (MulAut.conjNormal 1) (MonoidHom.ofInjective ⋯).symm)) x✝ = 1 x✝