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
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' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
hgx : ((g x) v) v = ((g' x) w) w
hgy : ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) = ((g' y) w) w
⊢ ((g' y) w) w = ((g' y - g' x) w) w + ((g' x) w) w

Tactic:
by

Goal state after:
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)
⊢ b.1 = a.1 → b.2 = a.2

Tactic:
by

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
⊢ IsCyclicallyReduced (reduceCyclically L)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
⊢ conjugator [] = []

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a : α × Bool
⊢ conjugator [a] = []

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a b : α × Bool
L : List (α × Bool)
⊢ conjugator (a :: (L ++ [b])) = if b.1 = a.1 ∧ (!b.2) = a.2 then a :: conjugator L else []

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
L : List (α × Bool)
⊢ conjugator L ++ reduceCyclically L ++ invRev (conjugator L) = L

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
a b : G
ha : a ∈ {x | ∀ (y : G), ⁅x, y⁆ ∈ N}
hb : b ∈ {x | ∀ (y : G), ⁅x, y⁆ ∈ N}
y : G
⊢ ⁅a * b, y⁆ ∈ N

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
y : G
⊢ ⁅1, y⁆ ∈ N

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x : G
hx : x ∈ {x | ∀ (y : G), ⁅x, y⁆ ∈ N}
y : G
⊢ ⁅x⁻¹, y⁆ ∈ N

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
⊢ N.upperCentralSeriesStep = comap (mk' N) (center (G ⧸ N))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x✝ y : G
⊢ ⁅x✝, y⁆ = 1 ↔ y * x✝ = x✝ * y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ upperCentralSeries G 1 = center G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
x✝ y : G
⊢ ⁅x✝, y⁆ = 0 ↔ y + x✝ = x✝ + y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
⊢ AddSubgroup.upperCentralSeries G 1 = AddSubgroup.center G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ
⊢ ⁅upperCentralSeries G (n + 1), ⊤⁆ ≤ upperCentralSeries G n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : H ≃* G
⊢ comap (↑e) (upperCentralSeries G 0) = upperCentralSeries H 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : H ≃* G
n : ℕ
⊢ comap (↑e) (upperCentralSeries G (n + 1)) = upperCentralSeries H (n + 1)

Tactic:
by

Goal state after:
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)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)

Tactic:
by

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

Goal state before:
pp: G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
this : SemidirectProduct.rightHom.comp F' = MonoidHom.id G
⊢ ∀ (g : G), (F' g).right = g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : G ≃* H
⊢ IsNilpotent G ↔ IsNilpotent H

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ IsNilpotent ↥⊤

Tactic:
by

Goal state after:
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₅)
h₁✝ : IsCyclicallyReduced (reduceCyclically L)
h₂✝ : IsReduced (conjugator L ++ reduceCyclically L ++ invRev (conjugator L))
⊢ n + 1 + 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
⊢ H (n + 1) ≤ upperCentralSeries G (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ Monotone (upperCentralSeries G)

Tactic:
by

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
⊢ reduce (replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
by

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
h : IsReduced L
n : ℕ
⊢ reduce (replicate 0 L).flatten =
    if 0 = 0 then [] else conjugator L ++ (replicate 0 (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ Group.IsNilpotent G ↔ ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
heq : (fun a ↦ a ^ n) x = (fun a ↦ a ^ n) y
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
⊢ x ^ (2 * n) = y ^ (2 * n)

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
heq : (fun a ↦ a ^ n) x = (fun a ↦ a ^ n) y
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
heq₂ : x ^ (2 * n) = y ^ (2 * n)
⊢ g x n = g y n

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
heq₂ : x ^ (2 * n) = y ^ (2 * n)
heq : g x n = g y n
⊢ g x (2 * n) = g y (2 * n)

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
heq : g x n = g y n
heq₂ : g x (2 * n) = g y (2 * n)
⊢ f x n = f y n

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
heq : g x n = g y n
heq₂ : g x (2 * n) = g y (2 * n)
leq : f x n = f y n
⊢ f x (2 * n) = f y (2 * n)

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
heq : g x n = g y n
heq₂ : g x (2 * n) = g y (2 * n)
leq : f x n = f y n
leq₂ : f x (2 * n) = f y (2 * n)
⊢ (conjugator x.toWord).length = (conjugator y.toWord).length

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
hc : conjugator x.toWord = conjugator y.toWord
n : ℕ
hn : n + 1 ≠ 0
heq : g x (n + 1) = g y (n + 1)
heq₂ : g x (2 * (n + 1)) = g y (2 * (n + 1))
leq : f x (n + 1) = f y (n + 1)
leq₂ : f x (2 * (n + 1)) = f y (2 * (n + 1))
heq' :
  reduceCyclically x.toWord ++ ((replicate n (reduceCyclically x.toWord)).flatten ++ invRev (conjugator x.toWord)) =
    reduceCyclically y.toWord ++ ((replicate n (reduceCyclically y.toWord)).flatten ++ invRev (conjugator y.toWord))
⊢ (n + 1) * (reduceCyclically x.toWord).length = (n + 1) * (reduceCyclically y.toWord).length

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
hc : conjugator x.toWord = conjugator y.toWord
n : ℕ
hn : n + 1 ≠ 0
heq : g x (n + 1) = g y (n + 1)
heq₂ : g x (2 * (n + 1)) = g y (2 * (n + 1))
leq : f x (n + 1) = f y (n + 1)
leq₂ : f x (2 * (n + 1)) = f y (2 * (n + 1))
heq' :
  (replicate (n + 1) (reduceCyclically x.toWord)).flatten ++ invRev (conjugator x.toWord) =
    (replicate (n + 1) (reduceCyclically y.toWord)).flatten ++ invRev (conjugator y.toWord)
⊢ reduceCyclically x.toWord = reduceCyclically y.toWord

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
hasc : IsAscendingCentralSeries H
⊢ IsDescendingCentralSeries fun m ↦ H (n - m)

Tactic:
by

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

Goal state before:
pp: G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE : ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), E.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g
⊢ curry E = F'

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
n : ℕ
hn : n ≠ 0
x y : FreeGroup α
heq : (fun a ↦ a ^ n) x = (fun a ↦ a ^ n) y
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
hdesc : IsDescendingCentralSeries H
⊢ IsAscendingCentralSeries fun m ↦ H (n - m)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
hdesc : IsDescendingCentralSeries H
⊢ IsAscendingCentralSeries fun m ↦ H (n - m)

Tactic:
by
  obtain ⟨h0, hH⟩ := hdesc
  refine ⟨hn, fun x m hx g => ?_⟩
  dsimp only at hx ⊢
  by_cases! hm : n ≤ m
  · have hnm : n - m = 0 := tsub_eq_zero_iff_le.mpr hm
    rw [hnm, h0]
    exact mem_top _
  · convert! hH x _ hx g using 1
    rw [tsub_add_eq_add_tsub (Nat.succ_le_of_lt hm), Nat.succ_eq_add_one, Nat.add_sub_add_right]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
w : α × Bool
g : FreeGroup α
h : g ∈ startsWith w
h1 : g = 1
⊢ False

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
w w' : α × Bool
h : ∀ (x : FreeGroup α), x.toWord[0]? = some w → ¬w = w'
⊢ (mk [w]).toWord[0]? = some w

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
w w' : α × Bool
⊢ ¬w = w' → ∀ (x : FreeGroup α), x.toWord[0]? = some w → ¬w = w'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
w w' : α × Bool
⊢ Disjoint (startsWith w) (startsWith w') ↔ w ≠ w'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α × Bool
h : startsWith a = startsWith b
⊢ a = b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
w : α × Bool
g : FreeGroup α
hC✝ : 0 < g.toWord.length
h : g.toWord[0].1 = w.1 → g.toWord[0].2 = w.2
hC : True
⊢ g.toWord ≠ []

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
w : α × Bool
g : FreeGroup α
h : g ∉ startsWith (w.1, !w.2)
⊢ mk [w] * g ∈ startsWith w

Tactic:
by

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

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
w : α × Bool
g : ↑(startsWith w)
x : X
⊢ g • x = ↑g • x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ Group.IsNilpotent G ↔ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Characteristic
n : ℕ
⊢ (S.lowerCentralSeries n).Characteristic

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
⊢ S ≤ normalizer ↑(S.lowerCentralSeries (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
⊢ Antitone S.lowerCentralSeries

Tactic:
by

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

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
hl : l = g.toWord
⊢ mk g.toWord ∈ startsWith w

Tactic:
by

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

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
hl : l = g.toWord
⊢ mk g.toWord ∈ startsWith w

Tactic:
by simp [g.mk_toWord, hg]

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

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
hl : l = g.toWord
⊢ ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ IsDescendingCentralSeries ⊤.lowerCentralSeries

Tactic:
by

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

Goal state before:
pp: G A : Type u
inst✝² : Group G
inst✝¹ : IsFreeGroup G
inst✝ : MulAction G A
⊢ ∀ {X : Type u} [inst : Group X] (f : Labelling (Generators (ActionCategory G A)) X),
    ∃! F, ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), F.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
S : Subgroup G
K : Type u_2
inst✝ : Group K
f : G →* K
n : ℕ
⊢ map f (S.lowerCentralSeries n) = (map f S).lowerCentralSeries n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
n : ℕ
⊢ map H.subtype (⊤.lowerCentralSeries n) = H.lowerCentralSeries n

Tactic:
by

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)
a : G
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a
⊢ treeHom T a = homOfPath T p

Tactic:
by

Goal state after:
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' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
hgx : ((g x) v) v = ((g' x) w) w
hgy : ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) = ((g' y) w) w
⊢ ((g' y - g' x) w) w + ((g' x) w) w ≤ ‖g' y - g' x‖ * ‖w‖ * ‖w‖ + ((g' x) w) w

Tactic:
by

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

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l✝ : List (α × Bool) := g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
⊢ a = w

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
⊢ Group.IsNilpotent ↥S ↔ ∃ n, S.lowerCentralSeries n = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ upperCentralSeries G (nilpotencyClass G) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
n : ℕ
⊢ upperCentralSeries G n = ⊤ ↔ nilpotencyClass G ≤ n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l✝ : List (α × Bool) := g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
ha : a = w
h1 : (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: l)
⊢ b ∈ {z | z ≠ (w.1, !w.2)}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
by

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)
a b : Generators G
e : a ⟶ b
H : e ∈ wideSubquiverSymmetrify T a b
⊢ loopOfHom T (of e) = 𝟙 (root' T)

Tactic:
by

Goal state after: