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

Goal state before:
pp: 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✝ : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
hs : IsLocalFrameOn I F n s u
hs' : IsLocalFrameOn I F n s' u
hss' : ∀ (i : ι), s i x = s' i x
t : (x : M) → V x
i : ι
hxe : x ∈ u
⊢ (hs.coeff i x) (t x) = (hs'.coeff i x) (t x)

pp: 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✝ : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
hs : IsLocalFrameOn I F n s u
hs' : IsLocalFrameOn I F n s' u
hss' : ∀ (i : ι), s i x = s' i x
t : (x : M) → V x
i : ι
hxe : x ∉ u
⊢ (hs.coeff i x) (t x) = (hs'.coeff i x) (t x)

Tactic:
· simp [coeff, hxe]
    simp_all only [toBasisAt]

Goal state after:
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✝ : FiberBundle F V
ι : Type u_7
s s' : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
hs : IsLocalFrameOn I F n s u
hs' : IsLocalFrameOn I F n s' u
hss' : ∀ (i : ι), s i x = s' i x
t : (x : M) → V x
i : ι
hxe : x ∉ u
⊢ (hs.coeff i x) (t x) = (hs'.coeff i x) (t x)
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

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

Tactic:
simpa using congrArg (TotalSpace.mk' F y) (hs.coeff_sum_eq t hy)

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

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

Tactic:
simpa using congrArg (TotalSpace.mk' F y) (hs.coeff_sum_eq t hy)

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

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
A : Type u_9
inst✝¹ : AddCommGroup A
inst✝ : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : M → 𝕜 := fun x' ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
x' : M
⊢ (if σ x' = σ' x' then 1 else 0) • σ x' = (if σ x' = σ' x' then 1 else 0) • σ' x'

Tactic:
split_ifs with hx'

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✝² : FiberBundle F V
A : Type u_9
inst✝¹ : AddCommGroup A
inst✝ : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : M → 𝕜 := fun x' ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
x' : M
hx' : σ x' = σ' x'
⊢ 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✝² : FiberBundle F V
A : Type u_9
inst✝¹ : AddCommGroup A
inst✝ : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : M → 𝕜 := fun x' ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
x' : M
hx' : ¬σ x' = σ' x'
⊢ 0 • σ x' = 0 • σ' 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
ι : Type u_7
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : ι → Set M
hcov : ∀ (i : ι), IsCovariantDerivativeOn F cov (s i)
σ✝ : (x : M) → V x
g✝ : M → 𝕜
x✝ : M
hσ : MDiffAt (T% σ✝) x✝
hf' : MDiffAt g✝ x✝
hx : x✝ ∈ ⋃ i, s i
⊢ cov (g✝ • σ✝) x✝ = g✝ x✝ • cov σ✝ x✝ + (d% g✝ x✝).smulRight (σ✝ x✝)

Tactic:
by
    obtain ⟨si, ⟨i, rfl⟩, hxsi⟩ := hx
    exact (hcov i).leibniz hσ hf'

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

Goal state before:
pp: n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h✝ : Commute (sr i, sr j).1 (sr i, sr j).2
h : i = j
⊢ ↑u⁻¹ * (2 * j) = j

Tactic:
exact u.inv_mul_cancel_left j

Goal state after:
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 (mk (of _)),

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
G : Type u_3
inst✝ : Group G
rels : Set (FreeGroup α)
φ ψ : PresentedGroup rels →* G
hx : ∀ (x : α), φ (of x) = ψ (of x)
⊢ φ = ψ

Tactic:
unfold PresentedGroup

Goal state after:
α : Type u_1
G : Type u_3
inst✝ : Group G
rels : Set (FreeGroup α)
φ ψ : PresentedGroup rels →* G
hx : ∀ (x : α), φ (of x) = ψ (of x)
⊢ φ = ψ
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := ⋯
⊢ uncurry M'.relation ∘ Prod.map ⇑e ⇑e = ⇑(FreeGroup.freeGroupCongr e) ∘ uncurry M.relation

Tactic:
ext ⟨i, i'⟩

Goal state after:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
i i' : B
⊢ (uncurry M'.relation ∘ Prod.map ⇑e ⇑e) (i, i') = (⇑(FreeGroup.freeGroupCongr e) ∘ uncurry M.relation) (i, 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
⊢ Submonoid.closure (Set.range cs.simple) = ⊤

Tactic:
have : range cs.simple = range cs.simple ∪ (range cs.simple)⁻¹ := by
    simp_rw [inv_range, inv_simple, union_self]
  rw [this, ← Subgroup.closure_toSubmonoid, subgroup_closure_range_simple, Subgroup.top_toSubmonoid]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
⊢ (lift f).range ≤ s

Tactic:
rintro _ ⟨x, rfl⟩

Goal state after:
ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
x : CoprodI G
⊢ (lift f) x ∈ s
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
⊢ (alternatingWord i j p)[k + 1] = (alternatingWord j i p)[k]

Tactic:
rw [getElem_alternatingWord i j p (k + 1) (by lia),
    getElem_alternatingWord j i p k (by lia)]
  by_cases h_even : Even (p + k)
  · rw [if_pos h_even, ← add_assoc]
    simp only [ite_eq_right_iff, isEmpty_Prop, Nat.not_even_iff_odd, Even.add_one h_even,
      IsEmpty.forall_iff]
  · rw [if_neg h_even, ← add_assoc]
    simp [Odd.add_one (Nat.not_even_iff_odd.mp h_even)]

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
ω₁ : List B
hω₁ : cs.IsReduced ω₁
ω₂ : List B
hω₂ : cs.IsReduced ω₂
⊢ cs.length (cs.wordProd ω₁ * cs.wordProd ω₂) ≤ cs.length (cs.wordProd ω₁) + cs.length (cs.wordProd ω₂)

Tactic:
have := cs.length_wordProd_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 ω₁
ω₂ : List B
hω₂ : cs.IsReduced ω₂
this : cs.length (cs.wordProd (ω₁ ++ ω₂)) ≤ (ω₁ ++ ω₂).length
⊢ cs.length (cs.wordProd ω₁ * cs.wordProd ω₂) ≤ cs.length (cs.wordProd ω₁) + cs.length (cs.wordProd ω₂)
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
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < r' ^ 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ∀ ε > 0, ∀ᶠ (x_1 : B) in 𝓝 x, dist (g' x_1) (g' x) < ε
⊢ ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ

Tactic:
apply hg' _ δpos

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

Goal state before:
pp: case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (MulAut.conj (cs.simple i)) ((cs.leftInvSeq ω).getD j' 1) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (i :: ω)[j' + 1]?).getD ((MulAut.conj (cs.simple i)) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹

Tactic:
ih j'

Goal state after:
case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (MulAut.conj (cs.simple i))
      (cs.wordProd (take j' ω) * (Option.map cs.simple ω[j']?).getD 1 * (cs.wordProd (take j' ω))⁻¹) =
    cs.wordProd (take (j' + 1) (i :: ω)) *
        (Option.map cs.simple (i :: ω)[j' + 1]?).getD ((MulAut.conj (cs.simple i)) 1) *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : (powMonoidHom n).range.FiniteIndex
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
f : G →* G := powMonoidHom n
q : G → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
x : G
| ∃ y ∈ ↑f.range, qi (q x) * y = x

Tactic:
enter [1, y]; rw [eq_comm, ← div_eq_iff_eq_mul', SetLike.mem_coe]

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : (powMonoidHom n).range.FiniteIndex
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
f : G →* G := powMonoidHom n
q : G → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
x y : G
| y ∈ f.range ∧ x / qi (q x) = y
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
this : List.map (fun x ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω

Tactic:
nth_rw 2 [← reverse_reverse ω]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
this : List.map (fun x ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω.reverse.reverse
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
α : Type u_2
x : DivisibleHull M
f : M → ℕ+ → α
h : ∀ (m m' : M) (s s' : ℕ+), mk m s = mk m' s' → f m s = f m' s'
p p' : M × ↥(nonZeroDivisors ℕ)
u : ↥(nonZeroDivisors ℕ)
hu : u • p'.2 • p.1 = u • p.2 • p'.1
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact mk_eq_mk.mpr ⟨↑ⁿ.symm u, hu⟩

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
α : Type u_2
x y : DivisibleHull M
f : M → ℕ+ → M → ℕ+ → α
h : ∀ (m n m' n' : M) (s t s' t' : ℕ+), mk m s = mk m' s' → mk n t = mk n' t' → f m s n t = f m' s' n' t'
p q p' q' : M × ↥(nonZeroDivisors ℕ)
heq' : q ≈ q'
u : ↥(nonZeroDivisors ℕ)
hu : u • p'.2 • p.1 = u • p.2 • p'.1
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact mk_eq_mk.mpr ⟨↑ⁿ.symm u, hu⟩

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
α : Type u_2
x y : DivisibleHull M
f : M → ℕ+ → M → ℕ+ → α
h : ∀ (m n m' n' : M) (s t s' t' : ℕ+), mk m s = mk m' s' → mk n t = mk n' t' → f m s n t = f m' s' n' t'
p q p' q' : M × ↥(nonZeroDivisors ℕ)
heq : p ≈ p'
u : ↥(nonZeroDivisors ℕ)
hu : u • q'.2 • q.1 = u • q.2 • q'.1
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact mk_eq_mk.mpr ⟨↑ⁿ.symm u, hu⟩

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
x : G
⊢ ∃ i, ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out i * y

Tactic:
use mk H K x

Goal state after:
case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
x : G
⊢ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out (mk H K x) * y
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 := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
hne1 : FreeGroup.freeGroupUnitEquivInt.symm 0 ≠ 1
⊢ FreeGroup.freeGroupUnitEquivInt.symm 0 = 1

Tactic:
simp [H, FreeGroup.freeGroupUnitEquivInt]

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)
φ : G →* Mˣ
η : (G →* Mˣ) →* Mˣ
⊢ φ ((monoidHomMonoidHomEquiv G M) η) = η φ

Tactic:
← monoidHomMonoidHomEquiv_symm_apply_apply G M (monoidHomMonoidHomEquiv G M η) φ,

Goal state after:
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
φ : G →* Mˣ
η : (G →* Mˣ) →* Mˣ
⊢ ((monoidHomMonoidHomEquiv G M).symm ((monoidHomMonoidHomEquiv G M) η)) φ = η φ
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ g ^ (1 + ((if k = 0 then ↑(minimalPeriod (fun x ↦ g • x) (Quotient.out ⟨q, k - 1⟩.fst)) else k.cast) - 1)) *
      Quotient.out (Quotient.out ⟨q, k - 1⟩.fst) =
    if k = 0 then g ^ minimalPeriod (fun x ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else g ^ k.cast * Quotient.out (Quotient.out q)

Tactic:
add_sub_cancel

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ (g ^ if k = 0 then ↑(minimalPeriod (fun x ↦ g • x) (Quotient.out ⟨q, k - 1⟩.fst)) else k.cast) *
      Quotient.out (Quotient.out ⟨q, k - 1⟩.fst) =
    if k = 0 then g ^ minimalPeriod (fun x ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else g ^ k.cast * Quotient.out (Quotient.out q)
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
hG : IsFinitelyPresented G
f : G →* H
hf_surj : Function.Surjective ⇑f
hf_ker : f.ker.IsFinitelyNormallyGenerated
⊢ IsFinitelyPresented H

Tactic:
by
  obtain ⟨n, φ, hφ_surj, hφ_ker⟩ := hG.out
  refine ⟨n, f.comp φ, hf_surj.comp hφ_surj, ?_⟩
  rw [← MonoidHom.comap_ker]
  exact hf_ker.comap hφ_surj hφ_ker

Goal state after:
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 ⇑φ
g : G
hg : orderOf g = 2
⊢ g ^ orderOf g = 1

Tactic:
pow_orderOf_eq_one

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 ⇑φ
g : G
hg : orderOf g = 2
⊢ 1 = 1
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ map (↑P).subtype ((↑P).transferFocal.ker.subgroupOf ↑P) = (↑P).focalSubgroup

Tactic:
← MonoidHom.ker_domRestrict,

Goal state after:
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ map (↑P).subtype ((↑P).transferFocal.domRestrict ↑P).ker = (↑P).focalSubgroup
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤
H : Subgroup G
hH : normalizer ↑H = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
hH' : normalizer ↑H' = H'
⊢ H = ⊤

Tactic:
apply map_injective_of_ker_le (mk' (center G)) hkh le_top

Goal state after:
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤
H : Subgroup G
hH : normalizer ↑H = H
hch : center G ≤ H
hkh : (mk' (center G)).ker ≤ H
hsur : Function.Surjective ⇑(mk' (center G))
H' : Subgroup (G ⧸ center G) := ⋯
hH' : normalizer ↑H' = H'
⊢ Subgroup.map (mk' (center G)) H = Subgroup.map (mk' (center G)) ⊤
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = 1
hG0 : ¬Nat.card G = 0
hG1 : Nat.card G = 1
⊢ H.Normal

Tactic:
exact normal_of_index_eq_one hHp

Goal state after:
Module: Mathlib.GroupTheory.Perm.ConjAct

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ c ∈ (k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset

Tactic:
rw [← mem_cycleFactorsFinset_conj' k⁻¹ (k • g) c]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k⁻¹ • c ∈ (k⁻¹ • k • g).cycleFactorsFinset ↔ c ∈ k • g.cycleFactorsFinset