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

Goal state before:
pp: case e_f
𝕜 : 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
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ✝ σ'✝ : (x : M) → V x
x✝¹ : M
hσ : MDiffAt (T% σ✝) x✝¹
hσ' : MDiffAt (T% σ'✝) x✝¹
hx : x✝¹ ∈ u
i : ι
x✝ : TangentSpace I x✝¹
⊢ (f i x✝¹ • cov i (σ✝ + σ'✝) x✝¹) x✝ = (f i x✝¹ • cov i σ✝ x✝¹ + f i x✝¹ • cov i σ'✝ x✝¹) x✝

Tactic:
← smul_add,

Goal state after:
case e_f
𝕜 : 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
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ✝ σ'✝ : (x : M) → V x
x✝¹ : M
hσ : MDiffAt (T% σ✝) x✝¹
hσ' : MDiffAt (T% σ'✝) x✝¹
hx : x✝¹ ∈ u
i : ι
x✝ : TangentSpace I x✝¹
⊢ (f i x✝¹ • cov i (σ✝ + σ'✝) x✝¹) x✝ = (f i x✝¹ • (cov i σ✝ x✝¹ + cov i σ'✝ x✝¹)) x✝
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
inst✝¹ : IsManifold I 1 M
n : ℕ∞ω
inst✝ : VectorBundle 𝕜 F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov : ∀ i ∈ s, ContMDiffCovariantDerivativeOn F n (cov i) u
f : ι → M → 𝕜
hf : ∀ i ∈ s, ContMDiffOn I 𝓘(𝕜, 𝕜) n (f i) u
σ : (x : M) → V x
hσ : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (n + 1) (fun x ↦ ⟨x, σ x⟩) u
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, E →L[𝕜] F)) n (fun x ↦ ⟨x, ∑ i ∈ s, f i x • cov i σ x⟩) u

Tactic:
by
    simpa using ContMDiffOn.sum_section
      (fun i hi ↦ (hf i hi).smul_section <| (hcov i hi).contMDiff hσ)

Goal state after:
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:
simp [differenceAux, hcov.leibniz hσ hf, hcov'.leibniz hσ hf]
    module

Goal state after:
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
⊢ (center G).index ≤ Nat.card ↑(commutatorSet G) ^ Fintype.card ↥S

Tactic:
← Nat.card_eq_fintype_card,

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite ↑(commutatorSet G)
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
⊢ (center G).index ≤ Nat.card ↑(commutatorSet G) ^ Nat.card ↥S
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: case neg
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
hy : ¬y = 1
hxy : ¬x = y
⊢ e (x * y) = e x * e y

Tactic:
have univ₂ : {e (x * y), e x, e y, (1 : G₂)} = Finset.univ := by
        simpa [map_univ_equiv e, map_insert, he]
          using congr(Finset.map e.toEmbedding $(eq_finset_univ hx hy hxy))
      rw [← Ne, ← e.injective.ne_iff] at hx hy hxy
      rw [he] at hx hy
      symm
      apply eq_of_mem_insert_of_notMem <| univ₂.symm ▸ mem_univ _
      simpa using mul_notMem_of_exponent_two h hx hy hxy

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ Fintype.card (DihedralGroup n) = 2 * n

Tactic:
← Fintype.card_eq.mpr ⟨equivSum.symm⟩,

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ Fintype.card (ZMod n ⊕ ZMod n) = 2 * n
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case pos
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ take (k + 1) (alternatingWord i j (2 * p)) = alternatingWord j i (k + 1)

Tactic:
rw [← List.take_concat_get (by simp; lia), alternatingWord_succ, ← hk]

Goal state after:
case pos
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ (take k (alternatingWord i j (2 * p))).concat (alternatingWord i j (2 * p))[k] =
    (take k (alternatingWord i j (2 * p))).concat i
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 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)
hm : Even m
h₁ : ¬Even (m + 1)
⊢ ¬2 ∣ m + 1

Tactic:
← even_iff_two_dvd

Goal state after:
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)
hm : Even m
h₁ : ¬Even (m + 1)
⊢ ¬Even (m + 1)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
⊢ ⟨i, m⟩ ∈ ((equivPair j) w).tail.toList → ⟨i, m⟩ ∈ w.toList

Tactic:
rw [mem_equivPair_tail_iff]
  rintro (h | h)
  · exact List.mem_of_mem_tail h
  · revert h; cases w.toList <;> simp +contextual

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

Goal state before:
pp: case inl
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ 1 * (cs.simple i * cs.simple i') ^ (2 * k / 2) = 1 * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - 2 * k) / 2)

Tactic:
mul_comm 2 k,

Goal state after:
case inl
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ 1 * (cs.simple i * cs.simple i') ^ (k * 2 / 2) = 1 * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - k * 2) / 2)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : ⟨j, m₁⟩ ∈ w.toList.tail
⊢ (⟨j, m₁⟩ ∈ w.toList.tail ∨
      ¬m₁ = 1 ∧
        m₁ = m₂ * if h : ∃ (h : ¬w.toList = []), (w.toList.head h).fst = j then ⋯ ▸ (w.toList.head ⋯).snd else 1) ↔
    ¬m₁ = 1 ∧ (⟨j, m₁⟩ ∈ w.toList.tail ∨ (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = m₂ * m') ∨ ¬w.fstIdx = some j ∧ m₁ = m₂)

Tactic:
simp [hw, show m₁ ≠ 1 from w.ne_one _ (List.mem_of_mem_tail hw)]

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

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

Tactic:
simpa using cs.length_le_length_mul_add_right w (s i)

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
w : Word M
⊢ rcons ((equivPair i) w) = w

Tactic:
← equivPair_symm,

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
w : Word M
⊢ (equivPair i).symm ((equivPair i) w) = w
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case of
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i✝ : ι
m✝ : M i✝
w✝ : Word M
⊢ of m✝ * (rcons ((equivPair i✝) w✝)).prod = of m✝ * w✝.prod

Tactic:
← equivPair_symm,

Goal state after:
case of
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i✝ : ι
m✝ : M i✝
w✝ : Word M
⊢ of m✝ * ((equivPair i✝).symm ((equivPair i✝) w✝)).prod = of m✝ * w✝.prod
Module: Mathlib.GroupTheory.Coxeter.Inversion

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

Tactic:
simp at ht

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

Goal state before:
pp: case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.rightInvSeq ω).length
ht : (cs.rightInvSeq ω)[j] ∈ cs.rightInvSeq ω
⊢ cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)

Tactic:
rw [cs.length_rightInvSeq] at hj

Goal state after:
case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj✝ : j < (cs.rightInvSeq ω).length
hj : j < ω.length
ht : (cs.rightInvSeq ω)[j] ∈ cs.rightInvSeq ω
⊢ cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case inl
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : 0 ≤ a
⊢ a • mk m s = mk (a.num • m) (⟨a.den, ⋯⟩ * s)

Tactic:
rw [qsmul_of_nonneg h, nnqsmul_mk, ← natCast_zsmul]

Goal state after:
case inl
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : 0 ≤ a
⊢ mk
      (↑(have this := ⟨a, h⟩;
            this).num •
        m)
      (⟨(have this := ⟨a, h⟩;
            this).den,
          ⋯⟩ *
        s) =
    mk (a.num • m) (⟨a.den, ⋯⟩ * s)
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ (a * b) • mk m s = a • b • mk m s

Tactic:
| mk m s
     => 

Goal state after:
case mk
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ (a * b) • mk m s = a • b • mk m s
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
m : M
s : ℕ+
⊢ 1 • mk m s = mk m s

Tactic:
| mk m s
     => 

Goal state after:
case mk
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
m : M
s : ℕ+
⊢ 1 • mk m s = mk m s
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ (a + b) • mk m s = a • mk m s + b • mk m s

Tactic:
| mk m s
     => 

Goal state after:
case mk
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ (a + b) • mk m s = a • mk m s + b • mk m s
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m : M
s : ℕ+
⊢ mk m s ≤ mk m s

Tactic:
| mk m s
     => 

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m : M
s : ℕ+
⊢ mk m s ≤ mk m s
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
x : Quot ⇑(leftRel K)
⊢ ∃ i, x ∈ Quot.mk ⇑(leftRel K) '' doubleCoset (out i) ↑H ↑K

Tactic:
obtain ⟨y, hy⟩ := exists_rep x

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
x : Quot ⇑(leftRel K)
y : G
hy : ⟦y⟧ = x
⊢ ∃ i, x ∈ Quot.mk ⇑(leftRel K) '' doubleCoset (out i) ↑H ↑K
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : 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 ι
w : Word H
h : (lift f) w.prod = 1
⊢ w = Word.empty

Tactic:
by_contra hnotempty

Goal state after:
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : 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 ι
w : Word H
h : (lift f) w.prod = 1
hnotempty : ¬w = Word.empty
⊢ False
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : 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 ι
⊢ ∀ (b : Word H), (lift f) (Word.equiv.symm b) = 1 → Word.equiv.symm b = 1

Tactic:
intro w Heq

Goal state after:
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : 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 ι
w : Word H
Heq : (lift f) (Word.equiv.symm w) = 1
⊢ Word.equiv.symm w = 1
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
x : Quot ⇑(rightRel H)
⊢ ∃ i, x ∈ Quot.mk ⇑(rightRel H) '' doubleCoset (out i) ↑H ↑K

Tactic:
obtain ⟨y, hy⟩ := exists_rep x

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
x : Quot ⇑(rightRel H)
y : G
hy : ⟦y⟧ = x
⊢ ∃ i, x ∈ Quot.mk ⇑(rightRel H) '' doubleCoset (out i) ↑H ↑K
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : 0 < mk m s
⊢ b • mk m s < c • mk m s

Tactic:
| mk m s
     => 

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : 0 < mk m s
⊢ b • mk m s < c • mk m s
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case h₁.mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s : ℕ+
⊢ ((archimedeanClassOrderHom M).comp (archimedeanClassOrderHomInv M)) (ArchimedeanClass.mk (mk m s)) =
    OrderHom.id (ArchimedeanClass.mk (mk m s))

Tactic:
| mk m s
     => 

Goal state after:
case h₁.mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s : ℕ+
⊢ ((archimedeanClassOrderHom M).comp (archimedeanClassOrderHomInv M)) (ArchimedeanClass.mk (mk m s)) =
    OrderHom.id (ArchimedeanClass.mk (mk m s))
Module: Mathlib.GroupTheory.CoprodI

Goal state before:

Tactic:
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

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case h
ι : 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
inhabited_h : Inhabited ι
⊢ 3 ≤ #(FreeGroup Unit)

Tactic:
rw [FreeGroup.freeGroupUnitEquivInt.cardinal_eq, Cardinal.mk_denumerable]

Goal state after:
case h
ι : 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
inhabited_h : Inhabited ι
⊢ 3 ≤ ℵ₀
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : ¬H.index = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
⊢ g ^ H.index ∈ H

Tactic:
replace key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H := fun k g₀ hk =>
      (congr_arg (· ∈ H) (key k g₀ hk)).mp hk
    replace key : ∀ q : G ⧸ H, g ^ Function.minimalPeriod (g • ·) q ∈ H := fun q =>
      key (Function.minimalPeriod (g • ·) q) q.out
        (QuotientGroup.out_conj_pow_minimalPeriod_mem H g q)
    let f : Quotient (orbitRel (zpowers g) (G ⧸ H)) → zpowers g := fun q =>
      (⟨g, mem_zpowers g⟩ : zpowers g) ^ Function.minimalPeriod (g • ·) q.out
    have hf : ∀ q, f q ∈ H.subgroupOf (zpowers g) := fun q => key q.out
    replace key :=
      Subgroup.prod_mem (H.subgroupOf (zpowers g)) fun q (_ : q ∈ Finset.univ) => hf q
    simpa only [f, Finset.prod_pow_eq_pow_sum, index_eq_sum_minimalPeriod H g] using! key

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : (center G).FiniteIndex
g : G
k : ℕ
x✝ : G
hk : x✝⁻¹ * g ^ k * x✝ ∈ center G
⊢ ?a * (x✝⁻¹ * g ^ k * x✝) = ?a * g ^ k

pp: case a
G : Type u_1
inst✝¹ : Group G
inst✝ : (center G).FiniteIndex
g : G
k : ℕ
x✝ : G
hk : x✝⁻¹ * g ^ k * x✝ ∈ center G
⊢ G

Tactic:
← hk.comm,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : (center G).FiniteIndex
g : G
k : ℕ
x✝ : G
hk : x✝⁻¹ * g ^ k * x✝ ∈ center G
⊢ x✝⁻¹ * g ^ k * x✝ * ?m.57 = ?m.57 * g ^ k

G : Type u_1
inst✝¹ : Group G
inst✝ : (center G).FiniteIndex
g : G
k : ℕ
x✝ : G
hk : x✝⁻¹ * g ^ k * x✝ ∈ center G
⊢ G
Module: Mathlib.GroupTheory.Transfer

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

Tactic:
have := (Nat.card_eq_one_iff_unique.mp hn).1
    rw [Subsingleton.elim (MonoidHom.transferSylow P (hP.normalizer_le_centralizer rfl)).ker ⊥,
      Subsingleton.elim P.1 ⊤]
    exact isComplement'_bot_top

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ = Nat.find ⋯

Tactic:
refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)

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

case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsAscendingCentralSeries H ∧ H n = ⊤) → upperCentralSeries G n = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ = Nat.find ⋯

Tactic:
refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)

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

case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ = Nat.find ⋯

Tactic:
refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)

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

case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), ⊤.lowerCentralSeries n = ⊥ → ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : IsNilpotent G
⊢ NormalizerCondition G

Tactic:
normalizerCondition_iff_only_full_group_self_normalizing

Goal state after:
G : Type u_1
inst✝ : Group G
h : IsNilpotent G
⊢ ∀ (H : Subgroup G), normalizer ↑H = H → H = ⊤
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
hfB : IsFixedBlock G B
⊢ IsBlock G B

Tactic:
by simp [IsBlock, hfB _]

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:
by
  rw [IsTrivialBlock, ← B.ncard_le_one_iff_subsingleton, B.eq_univ_iff_ncard]
  have := B.ncard_le_card
  grind

Goal state after: