mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∀ x ∈ s, σ x = σ' x
hxs' : x ∈ s
ψ : M → 𝕜 := fun x' ↦ if x' ∈ s then 1 else 0
hψx : ψ x = 1
x' : M
⊢ (if x' ∈ s then 1 else 0) • σ x' = (if x' ∈ s then 1 else 0) • σ' x'

Tactic:
split_ifs with hx's

Goal state after:
case pos
𝕜 : 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 : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∀ x ∈ s, σ x = σ' x
hxs' : x ∈ s
ψ : M → 𝕜 := fun x' ↦ if x' ∈ s then 1 else 0
hψx : ψ x = 1
x' : M
hx's : x' ∈ s
⊢ 1 • σ x' = 1 • σ' x'

case neg
𝕜 : 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 : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∀ x ∈ s, σ x = σ' x
hxs' : x ∈ s
ψ : M → 𝕜 := fun x' ↦ if x' ∈ s then 1 else 0
hψx : ψ x = 1
x' : M
hx's : x' ∉ s
⊢ 0 • σ x' = 0 • σ' x'
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G

Tactic:
cases nonempty_fintype G

Goal state after:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G), x.carrier.ncard = Nat.card G
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ Nat.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier = Nat.card G

Tactic:
cases nonempty_fintype G

Goal state after:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nat.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier = Nat.card G
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

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

pp: case sr
n : ℕ
a : ZMod n
⊢ (sr a).inv * sr a = 1

Tactic:
· exact congr_arg r (neg_add_cancel a)

Goal state after:
case sr
n : ℕ
a : ZMod n
⊢ (sr a).inv * sr a = 1
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ orderOf (r i) = n / n.gcd i.val

Tactic:
by
  conv_lhs => rw [← ZMod.natCast_zmod_val i]
  rw [← r_one_pow, orderOf_pow, orderOf_r_one]

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) ≤
    ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card G) ^ 2 * ↑H.index ^ 2 * ↑(Nat.card ↥H) ^ 2

pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ 0 < ↑(Nat.card ↥H) ^ 2

Tactic:
mul_assoc,

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) ≤
    ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card G) ^ 2 * (↑H.index ^ 2 * ↑(Nat.card ↥H) ^ 2)

G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ 0 < ↑(Nat.card ↥H) ^ 2
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ ↑(Nat.card (ConjClasses (G ⧸ H))) ≤ ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G) * ↑(Nat.card ↥H) * ↑(Nat.card (G ⧸ H))

pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ 0 < ↑(Nat.card (G ⧸ H))

Tactic:
mul_assoc,

Goal state after:
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ ↑(Nat.card (ConjClasses (G ⧸ H))) ≤
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G) * (↑(Nat.card ↥H) * ↑(Nat.card (G ⧸ H)))

G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ 0 < ↑(Nat.card (G ⧸ H))
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: case of_mul
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
x : G ⊕ H
xs : FreeMonoid (G ⊕ H)
ihx : mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList xs)).reverse) * mk xs = 1
⊢ mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList xs)).reverse) * mk (of (Sum.map Inv.inv Inv.inv x)) *
      (mk (of x) * mk xs) =
    1

Tactic:
mul_assoc,

Goal state after:
case of_mul
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
x : G ⊕ H
xs : FreeMonoid (G ⊕ H)
ihx : mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList xs)).reverse) * mk xs = 1
⊢ mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList xs)).reverse) *
      (mk (of (Sum.map Inv.inv Inv.inv x)) * (mk (of x) * mk xs)) =
    1
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: α : Type u_1
rels : Set (FreeGroup α)
this : of = ⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) ∘ FreeGroup.of
⊢ Subgroup.closure (⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) '' Set.range FreeGroup.of) = ⊤

Tactic:
← MonoidHom.map_closure (QuotientGroup.mk' _),

Goal state after:
α : Type u_1
rels : Set (FreeGroup α)
this : of = ⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) ∘ FreeGroup.of
⊢ Subgroup.map (QuotientGroup.mk' (Subgroup.normalClosure rels)) (Subgroup.closure (Set.range FreeGroup.of)) = ⊤
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case mul
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
N : Type u_3
inst✝¹ : Monoid N
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
x y : CoprodI G
ihx : MulOpposite.unop ((lift fun i ↦ (MonoidHom.op of).comp (MulEquiv.inv' (G i)).toMonoidHom) x) * x = 1
ihy : MulOpposite.unop ((lift fun i ↦ (MonoidHom.op of).comp (MulEquiv.inv' (G i)).toMonoidHom) y) * y = 1
⊢ MulOpposite.unop ((lift fun i ↦ (MonoidHom.op of).comp (MulEquiv.inv' (G i)).toMonoidHom) y) *
        MulOpposite.unop ((lift fun i ↦ (MonoidHom.op of).comp (MulEquiv.inv' (G i)).toMonoidHom) x) *
      (x * y) =
    1

Tactic:
mul_assoc,

Goal state after:
case mul
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
N : Type u_3
inst✝¹ : Monoid N
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
x y : CoprodI G
ihx : MulOpposite.unop ((lift fun i ↦ (MonoidHom.op of).comp (MulEquiv.inv' (G i)).toMonoidHom) x) * x = 1
ihy : MulOpposite.unop ((lift fun i ↦ (MonoidHom.op of).comp (MulEquiv.inv' (G i)).toMonoidHom) y) * y = 1
⊢ MulOpposite.unop ((lift fun i ↦ (MonoidHom.op of).comp (MulEquiv.inv' (G i)).toMonoidHom) y) *
      (MulOpposite.unop ((lift fun i ↦ (MonoidHom.op of).comp (MulEquiv.inv' (G i)).toMonoidHom) x) * (x * y)) =
    1
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
w✝ : Word M
j : ι
m : M j
w : Word M
h1 : w.fstIdx ≠ some j
h2 : m ≠ 1
x✝ : { p // rcons p = w }
ij : i = j
⊢ rcons { head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ } = cons m w h1 h2

Tactic:
subst ij; simp [rcons, h2]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case inr
ι : 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
h : i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m⟩
⊢ ⟨i, m⟩ ∈ w.toList

Tactic:
revert h; cases w.toList <;> simp +contextual

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m m' : M i
w : Word M
⊢ (m * m') • w = m • m' • w

Tactic:
dsimp +instances [instHSMul]
    simp [mul_assoc, ← equivPair_symm, Equiv.apply_symm_apply]

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
w u : W
i : B
⊢ cs.IsReflection (w * (u * cs.simple i * u⁻¹) * w⁻¹)

Tactic:
use w * u, i

Goal state after:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w u : W
i : B
⊢ w * (u * cs.simple i * u⁻¹) * w⁻¹ = w * u * cs.simple i * (w * u)⁻¹
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
ω : List B
hω : cs.IsReduced ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length
⊢ cs.IsReduced (take j ω) ∧ cs.IsReduced (drop j ω)

Tactic:
have h₃ := calc
    (ω.take j).length + (ω.drop j).length
    _ = ω.length := by rw [← List.length_append, ω.take_append_drop j]
    _ = ℓ (π ω) := hω.symm
    _ = ℓ (π (ω.take j) * π (ω.drop j)) := by rw [← cs.wordProd_append, ω.take_append_drop j]
    _ ≤ ℓ (π (ω.take j)) + ℓ (π (ω.drop j)) := cs.length_mul_le _ _

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length
h₃ : (take j ω).length + (drop j ω).length ≤ cs.length (cs.wordProd (take j ω)) + cs.length (cs.wordProd (drop j ω))
⊢ cs.IsReduced (take j ω) ∧ cs.IsReduced (drop j ω)
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✝ * of ((equivPair i✝) w✝).head *
      (have __src := (equivPair i✝) w✝;
          { head := m✝ * ((equivPair i✝) w✝).head, tail := __src.tail, fstIdx_ne := ⋯ }).tail.prod =
    of m✝ * w✝.prod

Tactic:
mul_assoc,

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✝ *
      (of ((equivPair i✝) w✝).head *
        (have __src := (equivPair i✝) w✝;
            { head := m✝ * ((equivPair i✝) w✝).head, tail := __src.tail, fstIdx_ne := ⋯ }).tail.prod) =
    of m✝ * w✝.prod
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
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
⊢ cs.wordProd ω = cs.wordProd ω * t * t'

Tactic:
mul_assoc,

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
⊢ cs.wordProd ω = cs.wordProd ω * (t * t')
Module: Mathlib.GroupTheory.DoubleCoset

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

Tactic:
mul_assoc,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a h : G
hh : h ∈ ↑H
k : G
hk : k ∈ ↑K
hb : h * a * k ∈ doubleCoset a ↑H ↑K
⊢ ↑H * ({h} * {a} * {k} * ↑K) = ↑H * {a} * ↑K
Module: Mathlib.GroupTheory.DoubleCoset

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

Tactic:
mul_assoc,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a h : G
hh : h ∈ ↑H
k : G
hk : k ∈ ↑K
hb : h * a * k ∈ doubleCoset a ↑H ↑K
⊢ ↑H * ({h} * {a} * ({k} * ↑K)) = ↑H * {a} * ↑K
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ b = y⁻¹ * l * a * (r * r'⁻¹)

Tactic:
mul_assoc,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ b = y⁻¹ * l * (a * (r * r'⁻¹))
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ b = y⁻¹ * l * (a * (r * r'⁻¹))

Tactic:
mul_assoc,

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ b = y⁻¹ * (l * (a * (r * r'⁻¹)))
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
R S T : H.LeftTransversal
inst✝ : H.FiniteIndex
q : G ⧸ H
x✝ : q ∈ univ
⊢ (↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q) * ((↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q)) =
    (↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q)

Tactic:
mul_assoc,

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
R S T : H.LeftTransversal
inst✝ : H.FiniteIndex
q : G ⧸ H
x✝ : q ∈ univ
⊢ (↑(⋯.leftQuotientEquiv q))⁻¹ *
      (↑(⋯.leftQuotientEquiv q) * ((↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q))) =
    (↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
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 : n ≤ -1 := by
        apply Int.le_of_lt_add_one
        simpa using hgt
      calc
        a i ^ n • X' j ⊆ a i ^ n • (X i)ᶜ :=
          smul_set_mono ((hXdisj hij.symm).union_left (hXYdisj i j).symm).subset_compl_right
        _ ⊆ Y i := by
          clear hnne0 hgt
          induction n, h1n using Int.leInductionDown with
          | base => rw [zpow_neg, zpow_one]; exact hY i
          | pred n hle hi =>
            calc
              a i ^ (n - 1) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ := by rw [zpow_sub, zpow_one]
              _ = a i ^ n • (a i)⁻¹ • (X i)ᶜ := mul_smul _ _ _
              _ ⊆ a i ^ n • Y i := smul_set_mono <| hY i
              _ ⊆ a i ^ n • (X i)ᶜ := smul_set_mono (hXYdisj i i).symm.subset_compl_right
              _ ⊆ Y i := hi
        _ ⊆ X' i := Set.subset_union_right

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 (↑(f (r * s⁻¹)) * s)) = r

Tactic:
← Subtype.coe_mk r hr,

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 := 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 (↑(f (↑⟨r, hr⟩ * s⁻¹)) * s)) = ↑⟨r, hr⟩
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 := ⋯
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

Tactic:
mul_assoc,

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 := 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 (r * s⁻¹)) * (s * (↑⟨r, hr⟩)⁻¹) ∈ ↑H
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
⊢ ϕ
      (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, ⋯⟩

Tactic:
refine congrArg ϕ (Subtype.coe_injective ?_)

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
⊢ (fun a ↦ ↑a)
      (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 =
    (fun a ↦ ↑a) ⟨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
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : (⇑φ)^[2] = _root_.id
g : G
⊢ φ g = g⁻¹

Tactic:
have key : g * φ g = 1 := by simpa [List.range_succ] using hφ.prod_pow_eq_one h2 g

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
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : (⇑φ)^[2] = _root_.id
g : G
key : g * φ g = 1
⊢ φ g = g⁻¹
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
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
this : Fintype G
h : ¬Odd (Nat.card G)
⊢ False

Tactic:
rw [Nat.not_odd_iff_even, even_iff_two_dvd, Nat.card_eq_fintype_card] at 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
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
this : Fintype G
h : 2 ∣ Fintype.card G
⊢ False
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: case refine_1
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced (L₂ ++ (replicate n L₂).flatten)

Tactic:
← flatten_cons,

Goal state after:
case refine_1
α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
h' : (replicate (n + 1) L₂).flatten ≠ []
⊢ IsReduced (L₂ :: replicate n L₂).flatten
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x y : G
hx : x * y⁻¹ * x⁻¹ * y⁻¹⁻¹ ∈ N
⊢ x⁻¹ * y * x⁻¹⁻¹ * y⁻¹ ∈ N

Tactic:
mul_assoc,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x y : G
hx : x * y⁻¹ * (x⁻¹ * y⁻¹⁻¹) ∈ N
⊢ x⁻¹ * y * (x⁻¹⁻¹ * y⁻¹) ∈ N
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
this :
  ∀ {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)},
    reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)
⊢ reduce
      (conjugator L ++ (reduceCyclically L ++ (replicate (n + 1) (reduceCyclically L)).flatten) ++
        invRev (conjugator L)) =
    conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
← flatten_cons,

Goal state after:
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
ih :
  reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
this :
  ∀ {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)},
    reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)
⊢ reduce
      (conjugator L ++ (reduceCyclically L :: replicate (n + 1) (reduceCyclically L)).flatten ++
        invRev (conjugator L)) =
    conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
y : G
⊢ x * y * x⁻¹ * y⁻¹ ∈ (upperCentralSeriesAux G n).fst

Tactic:
mul_assoc,

Goal state after:
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
y : G
⊢ x * y * (x⁻¹ * y⁻¹) ∈ (upperCentralSeriesAux G n).fst
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
y : G
⊢ x * y * (x⁻¹ * y⁻¹) ∈ (upperCentralSeriesAux G n).fst

Tactic:
mul_assoc,

Goal state after:
G : Type u_1
inst✝ : Group G
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
y : G
⊢ x * (y * (x⁻¹ * y⁻¹)) ∈ (upperCentralSeriesAux G n).fst