mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
⊢ mlieBracketWithin I V₁ W₁ t =ᶠ[𝓝[s] x] mlieBracketWithin I V W t

Tactic:
by
  filter_upwards [hV, hW, eventually_eventually_nhdsWithin.2 hV,
    eventually_eventually_nhdsWithin.2 hW] with y hVy hWy hVy' hWy'
  apply Filter.EventuallyEq.mlieBracketWithin_vectorField_eq
  · apply nhdsWithin_mono _ ht
    exact hVy'
  · exact hVy
  · apply nhdsWithin_mono _ ht
    exact hWy'
  · exact hWy

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x✝¹ : EuclideanHalfSpace n
xval : EuclideanSpace ℝ (Fin n)
xprop : 0 ≤ xval.ofLp 0
x✝ : ⟨xval, xprop⟩ ∈ univ
⊢ ⟨toLp 2 (update (↑⟨xval, xprop⟩).ofLp 0 (max ((↑⟨xval, xprop⟩).ofLp 0) 0)), ⋯⟩ = ⟨xval, xprop⟩

Tactic:
rw [Subtype.mk_eq_mk, ← WithLp.equiv_symm_apply, Equiv.symm_apply_eq, update_eq_iff]

Goal state after:
n : ℕ
inst✝ : NeZero n
x✝¹ : EuclideanHalfSpace n
xval : EuclideanSpace ℝ (Fin n)
xprop : 0 ≤ xval.ofLp 0
x✝ : ⟨xval, xprop⟩ ∈ univ
⊢ max ((↑⟨xval, xprop⟩).ofLp 0) 0 = (WithLp.equiv 2 ((i : Fin n) → (fun x ↦ ℝ) i)) xval 0 ∧
    ∀ (x : Fin n), x ≠ 0 → (↑⟨xval, xprop⟩).ofLp x = (WithLp.equiv 2 ((i : Fin n) → (fun x ↦ ℝ) i)) xval x
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ frontier (range ↑(𝓡∂ n)) = {y | 0 = y.ofLp 0}

Tactic:
calc frontier (range (𝓡∂ n))
    _ = frontier ({ y | 0 ≤ y 0 }) := by
      congr!
      apply range_euclideanHalfSpace
    _ = { y | 0 = y 0 } := frontier_halfSpace 2 _ _

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: case neg
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
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : ¬MDiffAt f w
⊢ (mfderiv[Icc x y] (f ∘ projIcc x y ⋯) ↑w) 1 = (mfderiv% f w) 1

Tactic:
rw [mfderiv_zero_of_not_mdifferentiableAt hw, mfderivWithin_zero_of_not_mdifferentiableWithinAt]

Goal state after:
case neg
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
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : ¬MDiffAt f w
⊢ 0 1 = 0 1

case neg
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
x y : ℝ
h : Fact (x < y)
f : ↑(Icc x y) → M
w : ↑(Icc x y)
hw : ¬MDiffAt f w
⊢ ¬MDiffAt[Icc x y] (f ∘ projIcc x y ⋯) ↑w
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

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✝ : (x : M) → ENorm (TangentSpace I x)
a b c : ℝ
γ : ℝ → M
h : a ≤ b
h' : b ≤ c
this : Icc a c = Icc a b ∪ Ioc b c
⊢ Disjoint (Icc a b) (Ioc b c)

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✝ : (x : M) → ENorm (TangentSpace I x)
a b c : ℝ
γ : ℝ → M
h : a ≤ b
h' : b ≤ c
this : Icc a c = Icc a b ∪ Ioc b c
⊢ (∫⁻ (a : ℝ) in Icc a b, ‖(mfderiv% γ a) 1‖ₑ) + ∫⁻ (a : ℝ) in Ioc b c, ‖(mfderiv% γ a) 1‖ₑ =
    pathELength I γ a b + pathELength I γ b c

Tactic:
· exact disjoint_iff_forall_ne.mpr (fun a ha b hb ↦ (ha.2.trans_lt hb.1).ne)

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
inst✝ : (x : M) → ENorm (TangentSpace I x)
a b c : ℝ
γ : ℝ → M
h : a ≤ b
h' : b ≤ c
this : Icc a c = Icc a b ∪ Ioc b c
⊢ (∫⁻ (a : ℝ) in Icc a b, ‖(mfderiv% γ a) 1‖ₑ) + ∫⁻ (a : ℝ) in Ioc b c, ‖(mfderiv% γ a) 1‖ₑ =
    pathELength I γ a b + pathELength I γ b c
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
x : M
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C
r : ℝ
r_pos : r > 0
hr :
  ball (↑(extChartAt I x) x) r ∩ range ↑I ⊆
    (extChartAt I x).target ∩ {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
A : ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I) ∈ 𝓝 x
y : M
hy : y ∈ ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I)
h'y : y ∈ (chartAt H x).source
η : ℝ →ᴬ[ℝ] E := ContinuousAffineMap.lineMap (↑(extChartAt I x) x) (↑(extChartAt I x) y)
γ : ℝ → M := ↑(extChartAt I x).symm ∘ ⇑η
hη :
  Icc 0 1 ⊆ ⇑η ⁻¹' (extChartAt I x).target ∧ Icc 0 1 ⊆ ⇑η ⁻¹' {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
η_smooth : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 (⇑η) (Icc 0 1)
⊢ riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)

Tactic:
have : riemannianEDist I x y ≤ pathELength I γ 0 1 := by
    apply riemannianEDist_le_pathELength _ _ _ zero_le_one
    · exact (contMDiffOn_extChartAt_symm x).comp η_smooth hη.1
    · simp [γ, η, ContinuousAffineMap.coe_lineMap_eq]
    · simp [γ, η, ContinuousAffineMap.coe_lineMap_eq, h'y]

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
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C
r : ℝ
r_pos : r > 0
hr :
  ball (↑(extChartAt I x) x) r ∩ range ↑I ⊆
    (extChartAt I x).target ∩ {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
A : ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I) ∈ 𝓝 x
y : M
hy : y ∈ ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I)
h'y : y ∈ (chartAt H x).source
η : ℝ →ᴬ[ℝ] E := ContinuousAffineMap.lineMap (↑(extChartAt I x) x) (↑(extChartAt I x) y)
γ : ℝ → M := ↑(extChartAt I x).symm ∘ ⇑η
hη :
  Icc 0 1 ⊆ ⇑η ⁻¹' (extChartAt I x).target ∧ Icc 0 1 ⊆ ⇑η ⁻¹' {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
η_smooth : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 (⇑η) (Icc 0 1)
this : riemannianEDist I x y ≤ pathELength I γ 0 1
⊢ riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: 𝕜 : Type u
inst✝¹⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
EN : Type u_3
inst✝⁹ : NormedAddCommGroup EN
inst✝⁸ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝⁷ : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace HN N
EP : Type u_5
inst✝⁴ : NormedAddCommGroup EP
inst✝³ : NormedSpace 𝕜 EP
HP : Type u_6
inst✝² : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace HP P
x : M
⊢ IsLocalRing ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)

Tactic:
by
  apply IsLocalRing.of_nonunits_add
  rw [smoothSheafCommRing.nonunits_stalk]
  intro f g
  exact Ideal.add_mem _

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δ : (r' ^ 2)⁻¹ < 1 - δ * C
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' x - g' y‖ ≤ δ
v : E y
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y) v
hgy : ((g y) v) v = ((g' y) w) w
hgx : ((g x) ((trivializationAt F E x).symm x w)) ((trivializationAt F E x).symm x w) = ((g' x) w) w
⊢ ((g' x) w) w ≤ r' ^ 2 * ((g y) v) v

Tactic:
hgy

Goal state after:
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δ : (r' ^ 2)⁻¹ < 1 - δ * C
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' x - g' y‖ ≤ δ
v : E y
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y) v
hgy : ((g y) v) v = ((g' y) w) w
hgx : ((g x) ((trivializationAt F E x).symm x w)) ((trivializationAt F E x).symm x w) = ((g' x) w) w
⊢ ((g' x) w) w ≤ r' ^ 2 * ((g' y) w) w
Module: Mathlib.Geometry.Manifold.WhitneyEmbedding

Goal state before:
pp: ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (x_1 : ι),
    (↑(f.toFun x_1) x • ↑(extChartAt I (f.c x_1)) x, ↑(f.toFun x_1) x) =
      (↑(f.toFun x_1) y • ↑(extChartAt I (f.c x_1)) y, ↑(f.toFun x_1) y)
h₁ :
  ↑(f.toFun (f.ind x hx)) x • ↑(extChartAt I (f.c (f.ind x hx))) x =
    ↑(f.toFun (f.ind x hx)) y • ↑(extChartAt I (f.c (f.ind x hx))) y
h₂ : 1 = ↑(f.toFun (f.ind x hx)) y
⊢ x = y

Tactic:
rw [← h₂, f.apply_ind x hx, one_smul, one_smul] at h₁

Goal state after:
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (x_1 : ι),
    (↑(f.toFun x_1) x • ↑(extChartAt I (f.c x_1)) x, ↑(f.toFun x_1) x) =
      (↑(f.toFun x_1) y • ↑(extChartAt I (f.c x_1)) y, ↑(f.toFun x_1) y)
h₁ : ↑(extChartAt I (f.c (f.ind x hx))) x = ↑(extChartAt I (f.c (f.ind x hx))) y
h₂ : 1 = ↑(f.toFun (f.ind x hx)) y
⊢ x = y
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I (minSmoothness 𝕜 3) M
inst✝ : CompleteSpace E
U V W : (x : M) → TangentSpace I x
hU : ContMDiff I I.tangent (minSmoothness 𝕜 2) fun x ↦ ⟨x, U x⟩
hV : ContMDiff I I.tangent (minSmoothness 𝕜 2) fun x ↦ ⟨x, V x⟩
hW : ContMDiff I I.tangent (minSmoothness 𝕜 2) fun x ↦ ⟨x, W x⟩
⊢ mlieBracket I U (mlieBracket I V W) = mlieBracket I (mlieBracket I U V) W + mlieBracket I V (mlieBracket I U W)

Tactic:
ext x
  exact leibniz_identity_mlieBracket_apply (hU x) (hV x) (hW x)

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx ≠ some i
he : rcons { head := m, tail := w, fstIdx_ne := h } = rcons { head := m', tail := w', fstIdx_ne := h' }
hm : ¬m = 1
hm' : ¬m' = 1
⊢ m = m' ∧ w.toList = w'.toList

Tactic:
simpa [cons, rcons, dif_neg hm, dif_neg hm', eq_self_iff_true, Subtype.mk_eq_mk,
        heq_iff_eq, ← Subtype.ext_iff] using he

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case inl
ι : 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, m⟩ ∈ w.toList.tail
⊢ ⟨i, m⟩ ∈ w.toList

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:
· exact List.mem_of_mem_tail h

Goal state after:
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
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
w : W
i : B
this : cs.length (w⁻¹ * cs.simple i) = cs.length w⁻¹ + 1 ∨ cs.length (w⁻¹ * cs.simple i) + 1 = cs.length w⁻¹
⊢ cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w

Tactic:
rwa [(by simp : w⁻¹ * (s i) = ((s i) * w)⁻¹), length_inv, length_inv] at this

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
w : W
i : B
⊢ cs.IsLeftDescent w i ↔ cs.length (cs.simple i * w) + 1 = cs.length w

Tactic:
by
  unfold IsLeftDescent
  constructor
  · intro _
    exact (cs.length_simple_mul w i).resolve_left (by lia)
  · lia

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
ω : List B
⊢ (cs.rightInvSeq ω).prod = (cs.wordProd ω)⁻¹

Tactic:
induction ω with
  | nil => simp
  | cons i ω ih => simp [rightInvSeq, ih, wordProd_cons]

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
ω : List B
⊢ (cs.leftInvSeq ω).prod = (cs.wordProd ω)⁻¹

Tactic:
simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse, prod_reverse_noncomm, inv_inj]

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

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
x : M i
hne_one : x ≠ 1
⊢ (singleton x hne_one).prod = of x

Tactic:
simp [toWord, prod, Word.prod]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j k l : ι
w₁ : NeWord M i j
hne : j ≠ k
w₂ : NeWord M k l
⊢ (w₁.append hne w₂).prod = w₁.prod * w₂.prod

Tactic:
simp [toWord, prod, Word.prod]

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 := ⋯
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:
rw [mul_assoc, ← inv_inv s, ← mul_inv_rev, inv_inv]

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⁻¹)) * (↑⟨r, hr⟩ * s⁻¹)⁻¹ ∈ ↑H
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) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) ≤ r' ^ 2 * ((g' x) w) w

Tactic:
hgy

Goal state after:
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 ≤ r' ^ 2 * ((g' x) w) w
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x✝¹ : α × Bool
ha : (replicate (n + 1) (head :: tail)).flatten.getLast? = some x✝¹
x✝ : α × Bool
hb : x✝ ∈ (replicate (n + 1) (head :: tail)).flatten.head?
⊢ n + 1 ≠ 0

Tactic:
simp +arith

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
head : α × Bool
tail : List (α × Bool)
h : IsCyclicallyReduced (head :: tail)
x✝¹ : α × Bool
ha : (head :: tail).getLast? = some x✝¹
x✝ : α × Bool
hb : (replicate (n + 1) (head :: tail)).flatten.head? = some x✝
⊢ n + 1 ≠ 0

Tactic:
simp +arith

Goal state after:
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 + 1) L₂).flatten)

Tactic:
replicate_succ,

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₁ ++ (L₂ :: replicate n L₂).flatten)
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)
⊢ reduce (replicate (n + 1 + 1) L).flatten =
    conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
replicate_succ,

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)
⊢ reduce (L :: replicate (n + 1) L).flatten =
    conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)
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:
simp [h1, startsWith, FreeGroup.toWord_one] at h

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
· intro h
    rw [eq_top_iff, ← upperCentralSeries_nilpotencyClass]
    exact upperCentralSeries_mono _ h

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ
⊢ Monotone fun S ↦ S.lowerCentralSeries n

Tactic:
induction n with
  | zero => intro S T h; simpa
  | succ d hd => intro S T h; simp only [lowerCentralSeries_succ]; exact commutator_mono (hd h) h

Goal state after: