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

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type u_2
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : RiemannianBundle fun x ↦ TangentSpace I x
inst✝² : IsManifold I 1 M
inst✝¹ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
inst✝ : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC✝ : ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst✝⁵] u
us : u ⊆ s
hu : u ⊆ {y | ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (chartAt H x).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst✝⁵] v
r : ℝ≥0
hr : ball (↑(extChartAt I x) x) ↑r ⊆ ↑(extChartAt I x).symm ⁻¹' v
r_pos : 0 < r
y : M
hy : y ∈ {y | riemannianEDist I x y < ↑(r / C)}
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < ↑(r / C)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := ↑(extChartAt I x) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
this✝ : ‖γ' t₁ - γ' 0‖ₑ < ↑r
this : γ' t₁ ∈ ↑(extChartAt I x).symm ⁻¹' v
⊢ γ t₁ = ↑(extChartAt I x).symm (γ' t₁)

Tactic:
simp only [Function.comp_apply, γ', (extChartAt I x).left_inv <| uc <| t₁_mem
    (right_mem_Icc.mpr ht₁0)]

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

Goal state before:
pp: case hττ'
𝕜 : 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
F' : Type u_7
inst✝¹⁸ : NormedAddCommGroup F'
inst✝¹⁷ : NormedSpace 𝕜 F'
V' : M → Type u_8
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
inst✝⁹ : VectorBundle 𝕜 F V
inst✝⁸ : VectorBundle 𝕜 F' V'
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : FiniteDimensional 𝕜 F
inst✝⁵ : FiniteDimensional 𝕜 F'
inst✝⁴ : ContMDiffVectorBundle 1 F V I
inst✝³ : ContMDiffVectorBundle 1 F' V' I
inst✝² : TopologicalSpace A
inst✝¹ : IsTopologicalAddGroup A
inst✝ : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → ((x : M) → V' x) → A
x : M
hΦ₁ : ∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun x ↦ Φ x τ) x
hΦ₂ : ∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (Φ σ) x
this✝⁶ : T2Space (V x)
this✝⁵ : FiniteDimensional 𝕜 (V x)
this✝⁴ : T2Space (V' x)
this✝³ : FiniteDimensional 𝕜 (V' x)
this✝² : IsTopologicalAddGroup (V x)
this✝¹ : IsTopologicalAddGroup (V' x)
this✝ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
this : ∀ (x : M), ContinuousSMul 𝕜 (V' x)
c : 𝕜
v : V x
w : V' x
⊢ extend F' w x = extend F' w x

Tactic:
· rfl

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
ι : 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✝
i : ι
hxsi : x✝ ∈ (fun i ↦ s i) i
⊢ cov (g✝ • σ✝) x✝ = g✝ x✝ • cov σ✝ x✝ + (d% g✝ x✝).smulRight (σ✝ x✝)

Tactic:
exact (hcov i).leibniz hσ hf'

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

Goal state before:
pp: E : Type u_1
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
H : Type u_2
inst✝¹² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → NormedAddCommGroup (V x)
inst✝⁵ : (x : M) → InnerProductSpace ℝ (V x)
inst✝⁴ : FiberBundle F V
σ τ : (x : M) → V x
cov : CovariantDerivative I F V
inst✝³ : VectorBundle ℝ F V
inst✝² : IsContMDiffRiemannianBundle I 1 F V
X : (x : M) → TangentSpace I x
inst✝¹ : ContMDiffVectorBundle 1 F V I
inst✝ : FiniteDimensional ℝ F
x : M
hσ : MDiffAt (T% σ) x
hτ : MDiffAt (T% τ) x
⊢ (((cov.derivMetricTensor x) (σ x)) (τ x)) (X x) =
    ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) - (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x -
      (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x

Tactic:
unfold derivMetricTensor

Goal state after:
E : Type u_1
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
H : Type u_2
inst✝¹² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
F : Type u_4
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → NormedAddCommGroup (V x)
inst✝⁵ : (x : M) → InnerProductSpace ℝ (V x)
inst✝⁴ : FiberBundle F V
σ τ : (x : M) → V x
cov : CovariantDerivative I F V
inst✝³ : VectorBundle ℝ F V
inst✝² : IsContMDiffRiemannianBundle I 1 F V
X : (x : M) → TangentSpace I x
inst✝¹ : ContMDiffVectorBundle 1 F V I
inst✝ : FiniteDimensional ℝ F
x : M
hσ : MDiffAt (T% σ) x
hτ : MDiffAt (T% τ) x
⊢ (((TensorialAt.mkHom₂ (fun x1 x2 ↦ derivMetricTensorAux I cov x1 x2 x) x ⋯ ⋯) (σ x)) (τ x)) (X x) =
    ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) - (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x -
      (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

Goal state before:
pp: case mp
𝕜 : 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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
h : cov.torsion = 0
X : (x : M) → TangentSpace I x
⊢ ∀ {Y : (x : M) → TangentSpace I x} {x : M},
    MDiffAt (T% X) x → MDiffAt (T% Y) x → (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y x

Tactic:
Y

Goal state after:
case mp
𝕜 : 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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
h : cov.torsion = 0
X Y : (x : M) → TangentSpace I x
⊢ ∀ {x : M}, MDiffAt (T% X) x → MDiffAt (T% Y) x → (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y 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✝ : VectorBundle 𝕜 F V
cov : CovariantDerivative I F V
⊢ ↑cov 0 = 0

Tactic:
by
  ext1 x
  simp [cov.isCovariantDerivativeOnUniv.zero]

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

Goal state before:
pp: case pos
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(H i)
h : j = i
⊢ (MonoidHom.mulSingle Gs i) x ∈ comap (Pi.evalMonoidHom Gs j) (H j)

Tactic:
subst h

Goal state after:
case pos
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs j
hx : x ∈ ↑(H j)
⊢ (MonoidHom.mulSingle Gs j) x ∈ comap (Pi.evalMonoidHom Gs j) (H j)
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: case pos
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(K i)
h : j = i
⊢ (MonoidHom.mulSingle Gs i) x ∈ comap (Pi.evalMonoidHom Gs j) (K j)

Tactic:
subst h

Goal state after:
case pos
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs j
hx : x ∈ ↑(K j)
⊢ (MonoidHom.mulSingle Gs j) x ∈ comap (Pi.evalMonoidHom Gs j) (K j)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inl
⊢ IsMulCommutative (DihedralGroup 1)

Tactic:
exact ⟨⟨by decide⟩⟩

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

Goal state before:
pp: case inr
⊢ IsMulCommutative (DihedralGroup 2)

Tactic:
exact ⟨⟨by decide⟩⟩

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

Goal state before:
pp: M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : MulOneClass M'
inst✝¹ : MulOneClass N'
inst✝ : MulOneClass P
f : M →* M'
g : N →* N'
⊢ (mk.comp (FreeMonoid.map (Sum.map ⇑f ⇑g))) (of (Sum.inr 1)) = 1

Tactic:
simp only [MonoidHom.comp_apply, map_of, Sum.map_inr, map_one, mk_of_inr]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : Monoid P
P' : Type u_4
inst✝ : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
⊢ (f.comp (lift g₁ g₂)).comp inr = (lift (f.comp g₁) (f.comp g₂)).comp inr

Tactic:
rw [MonoidHom.comp_assoc, lift_comp_inr, lift_comp_inr]

Goal state after:
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) * y = 1

Tactic:
ihy

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
⊢ 1 = 1
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case neg
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : ¬Even (p + k)
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i

Tactic:
· 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.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
motive : Word M → Sort u_4
w : Word M
empty : motive Word.empty
cons :
  (i : ι) → (m : M i) → (w : Word M) → (h1 : w.fstIdx ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Word.cons m w h1 h2)
⊢ motive w

Tactic:
rcases w with ⟨w, h1, h2⟩

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

Goal state before:
pp: case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i head : ι
m✝ : M head
w✝ : Word M
h1✝ : w✝.fstIdx ≠ some head
h2✝ : m✝ ≠ 1
a✝ :
  ({
          toFun := fun w ↦
            ↑(consRecOn w ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j m w h1 h2 x ↦
                if ij : i = j then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
                else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩),
          invFun := rcons, left_inv := ⋯, right_inv := ⋯ }
        w✝).head =
    if h : ∃ (h : w✝.toList ≠ []), (w✝.toList.head h).fst = i then ⋯ ▸ (w✝.toList.head ⋯).snd else 1
hi : ¬i = head
⊢ ({
          toFun := fun w ↦
            ↑(consRecOn w ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j m w h1 h2 x ↦
                if ij : i = j then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
                else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩),
          invFun := rcons, left_inv := ⋯, right_inv := ⋯ }
        (cons m✝ w✝ h1✝ h2✝)).head =
    if h : ∃ (h : (cons m✝ w✝ h1✝ h2✝).toList ≠ []), ((cons m✝ w✝ h1✝ h2✝).toList.head h).fst = i then
      ⋯ ▸ ((cons m✝ w✝ h1✝ h2✝).toList.head ⋯).snd
    else 1

Tactic:
simp [hi, Ne.symm hi]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos.mpr.inl
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList = []
m₂ w✝ : M (w.toList.head hnil).fst
hw : ⟨(w.toList.head hnil).fst, m₂ * w✝⟩ ∉ w.toList.tail
hm1 : ¬m₂ * w✝ = 1
h : (w.toList.head hnil).snd = w✝
⊢ m₂ * w✝ = m₂ * (w.toList.head ⋯).snd

Tactic:
subst h

Goal state after:
case pos.mpr.inl
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList = []
m₂ : M (w.toList.head hnil).fst
hw : ⟨(w.toList.head hnil).fst, m₂ * (w.toList.head hnil).snd⟩ ∉ w.toList.tail
hm1 : ¬m₂ * (w.toList.head hnil).snd = 1
⊢ m₂ * (w.toList.head hnil).snd = m₂ * (w.toList.head ⋯).snd
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 ω.reverse.reverse

Tactic:
wordProd_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)⁻¹
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
x : M i✝
hnotone : x ≠ 1
⊢ (replaceHead x hnotone (singleton x✝ a✝)).head = x

pp: case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ∀ (x : M i✝) (hnotone : x ≠ 1), (replaceHead x hnotone _w₁✝).head = x
_w₂_ih✝ : ∀ (x : M k✝) (hnotone : x ≠ 1), (replaceHead x hnotone _w₂✝).head = x
x : M i✝
hnotone : x ≠ 1
⊢ (replaceHead x hnotone (_w₁✝.append _hne✝ _w₂✝)).head = x

Tactic:
· rfl

Goal state after:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ∀ (x : M i✝) (hnotone : x ≠ 1), (replaceHead x hnotone _w₁✝).head = x
_w₂_ih✝ : ∀ (x : M k✝) (hnotone : x ≠ 1), (replaceHead x hnotone _w₂✝).head = x
x : M i✝
hnotone : x ≠ 1
⊢ (replaceHead x hnotone (_w₁✝.append _hne✝ _w₂✝)).head = x
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
x : M i✝
hnotone : x * (singleton x✝ a✝).head ≠ 1
⊢ ((singleton x✝ a✝).mulHead x hnotone).head = x * (singleton x✝ a✝).head

pp: case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ∀ (x : M i✝) (hnotone : x * _w₁✝.head ≠ 1), (_w₁✝.mulHead x hnotone).head = x * _w₁✝.head
_w₂_ih✝ : ∀ (x : M k✝) (hnotone : x * _w₂✝.head ≠ 1), (_w₂✝.mulHead x hnotone).head = x * _w₂✝.head
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
⊢ ((_w₁✝.append _hne✝ _w₂✝).mulHead x hnotone).head = x * (_w₁✝.append _hne✝ _w₂✝).head

Tactic:
· rfl

Goal state after:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ∀ (x : M i✝) (hnotone : x * _w₁✝.head ≠ 1), (_w₁✝.mulHead x hnotone).head = x * _w₁✝.head
_w₂_ih✝ : ∀ (x : M k✝) (hnotone : x * _w₂✝.head ≠ 1), (_w₂✝.mulHead x hnotone).head = x * _w₂✝.head
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
⊢ ((_w₁✝.append _hne✝ _w₂✝).mulHead x hnotone).head = x * (_w₁✝.append _hne✝ _w₂✝).head
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
α : 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 ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ w.head⁻¹
⊢ h * w.head ≠ 1

Tactic:
← div_inv_eq_mul

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
α : 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 ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ w.head⁻¹
⊢ h / w.head⁻¹ ≠ 1
Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Type u_2
N : Type u_3
inst✝¹ : Group H
inst✝ : Group N
f : G →* H
K : FiniteIndexNormalSubgroup H
g : G →* H ⧸ K.toSubgroup := (QuotientGroup.mk' K.toSubgroup).comp f
⊢ (Subgroup.comap f K.toSubgroup).FiniteIndex

Tactic:
have hker : K.toSubgroup.comap f = g.ker := by
      simpa using MonoidHom.comap_ker (g := QuotientGroup.mk' K.toSubgroup) (f := f)

Goal state after:
G : Type u_1
inst✝² : Group G
H : Type u_2
N : Type u_3
inst✝¹ : Group H
inst✝ : Group N
f : G →* H
K : FiniteIndexNormalSubgroup H
g : G →* H ⧸ K.toSubgroup := (QuotientGroup.mk' K.toSubgroup).comp f
hker : Subgroup.comap f K.toSubgroup = g.ker
⊢ (Subgroup.comap f K.toSubgroup).FiniteIndex
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 := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
inhabited_h : Inhabited ι
⊢ 3 ≤ #(H default)

Tactic:
simp only [H]

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 ≤ #(FreeGroup Unit)
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
mem_comap,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x✝ : G
⊢ x✝ ∈ N.upperCentralSeriesStep ↔ (mk' N) x✝ ∈ center (G ⧸ N)
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case right
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 := ⋯
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
e : IsFreeGroup.Generators G
⊢ ((curry E) (IsFreeGroup.of e)).right = (f' e).right

Tactic:
· rfl

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case left
G : Type u_1
inst✝ : Group G
⊢ ⊤.lowerCentralSeries 0 = ⊤

pp: case right
G : Type u_1
inst✝ : Group G
⊢ ∀ (x : G) (n : ℕ), x ∈ ⊤.lowerCentralSeries n → ∀ (g : G), ⁅x, g⁆ ∈ ⊤.lowerCentralSeries (n + 1)

Tactic:
· rfl

Goal state after:
case right
G : Type u_1
inst✝ : Group G
⊢ ∀ (x : G) (n : ℕ), x ∈ ⊤.lowerCentralSeries n → ∀ (g : G), ⁅x, g⁆ ∈ ⊤.lowerCentralSeries (n + 1)