mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
hγ : IsMIntegralCurve γ v
dt : ℝ
⊢ IsMIntegralCurve (γ ∘ fun x ↦ x + dt) v

Tactic:
rw [isMIntegralCurve_iff_isMIntegralCurveOn] at *

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
hγ : IsMIntegralCurveOn γ v univ
dt : ℝ
⊢ IsMIntegralCurveOn (γ ∘ fun x ↦ x + dt) v univ
Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
hγ : IsMIntegralCurve γ v
a : ℝ
⊢ IsMIntegralCurve (γ ∘ fun x ↦ x * a) (a • v)

Tactic:
rw [isMIntegralCurve_iff_isMIntegralCurveOn] at *

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
hγ : IsMIntegralCurveOn γ v univ
a : ℝ
⊢ IsMIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v) univ
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

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✝² : IsManifold I 1 M
inst✝¹ : T2Space M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
x : M
⊢ (∃ γ, γ 0 = x ∧ IsMIntegralCurve γ v) ↔ ∀ (a : ℝ), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)

Tactic:
refine ⟨fun ⟨γ, h1, h2⟩ _ ↦ ⟨γ, h1, h2.isMIntegralCurveOn _⟩, fun h ↦ ?_⟩
  choose γ hγx hγ using h
  exact ⟨fun t ↦ γ (|t| + 1) t, hγx (|0| + 1),
    isMIntegralCurve_abs_add_one_of_isMIntegralCurveOn_Ioo hv γ hγx (fun a _ ↦  hγ a)⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: case refine_3
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
⊢ ContMDiffAt (I.tangent.prod I'.tangent) 𝓘(𝕜, E') n
    (Prod.snd ∘ fun x ↦
      (fderivWithin 𝕜
          (((fun p ↦ (↑I p.1, ↑I' p.2)) ∘ fun p ↦ (↑(chartAt H a.proj) p.1, ↑(chartAt H' b.proj) p.2)) ∘
            ↑((chartAt H x.1.proj).prod (chartAt H' x.2.proj).toPartialEquiv).symm ∘ ↑(I.prod I'.toPartialEquiv).symm)
          (range (Prod.map ↑I ↑I')) (↑I (↑(chartAt H x.1.proj) x.1.proj), ↑I' (↑(chartAt H' x.2.proj) x.2.proj)))
        (x.1.snd, x.2.snd))
    (a, b)

Tactic:
apply (contMDiffAt_totalSpace.1 smooth_pM').2.congr_of_eventuallyEq

Goal state after:
case refine_3
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
⊢ (Prod.snd ∘ fun x ↦
      (fderivWithin 𝕜
          (((fun p ↦ (↑I p.1, ↑I' p.2)) ∘ fun p ↦ (↑(chartAt H a.proj) p.1, ↑(chartAt H' b.proj) p.2)) ∘
            ↑((chartAt H x.1.proj).prod (chartAt H' x.2.proj).toPartialEquiv).symm ∘ ↑(I.prod I'.toPartialEquiv).symm)
          (range (Prod.map ↑I ↑I')) (↑I (↑(chartAt H x.1.proj) x.1.proj), ↑I' (↑(chartAt H' x.2.proj) x.2.proj)))
        (x.1.snd, x.2.snd)) =ᶠ[𝓝 (a, b)]
    fun x ↦ (↑(trivializationAt E' (TangentSpace I') (a, b).2.proj) x.2).2
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 : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f b) (f a)] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ ‖(mfderiv[Icc a b] (γ ∘ f) t) 1‖ₑ = ENNReal.ofReal (-derivWithin f (Icc a b) t) * ‖(mfderiv[f '' Icc a b] γ (f t)) 1‖ₑ

Tactic:
have : (mfderiv[Icc a b] (γ ∘ f) t)
      = (mfderiv[Icc (f b) (f a)] γ (f t)) ∘L mfderiv[Icc a b] f t := by
    rw [← f_im] at hγ ⊢
    apply mfderivWithin_comp
    · apply hγ _ (mem_image_of_mem _ ht)
    · rw [mdifferentiableWithinAt_iff_differentiableWithinAt]
      exact h'f _ ht
    · exact subset_preimage_image _ _
    · rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
      exact uniqueDiffOn_Icc h _ ht

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 : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f b) (f a)] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
this : mfderiv[Icc a b] (γ ∘ f) t = mfderiv[Icc (f b) (f a)] γ (f t) ∘SL mfderiv[Icc a b] f t
⊢ ‖(mfderiv[Icc a b] (γ ∘ f) t) 1‖ₑ = ENNReal.ofReal (-derivWithin f (Icc a b) t) * ‖(mfderiv[f '' Icc a b] γ (f t)) 1‖ₑ
Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian

Goal state before:
pp: EB : Type u_1
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace ℝ EB
HB : Type u_2
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
B : Type u_3
inst✝¹³ : TopologicalSpace B
inst✝¹² : ChartedSpace HB B
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
E : B → Type u_5
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
EM : Type u_6
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace ℝ EM
HM : Type u_7
inst✝² : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB 1 F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : (MDiffAt[s] fun m ↦ ⟨b m, v m⟩) x
hw : (MDiffAt[s] fun m ↦ ⟨b m, w m⟩) x
⊢ (MDiffAt[s] fun m ↦ ⟪v m, w m⟫) x

Tactic:
rcases h.exists_contMDiff with ⟨g, g_smooth, hg⟩
  have hb : MDiffAt[s] b x := by
    simp only [mdifferentiableWithinAt_totalSpace] at hv
    exact hv.1
  simp only [hg]
  have : MDifferentiableWithinAt IM (IB.prod 𝓘(ℝ))
      (fun m ↦ TotalSpace.mk' ℝ (E := Bundle.Trivial B ℝ) (b m) (g (b m) (v m) (w m))) s x := by
    apply MDifferentiableWithinAt.clm_bundle_apply₂ (F₁ := F) (F₂ := F)
    · exact MDifferentiableAt.comp_mdifferentiableWithinAt x
        (g_smooth.mdifferentiableAt one_ne_zero) hb
    · exact hv
    · exact hw
  simp only [mdifferentiableWithinAt_totalSpace] at this
  exact this.2

Goal state after:
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 := ⋯
γ : ℝ → M := ⋯
⊢ segment ℝ (↑(extChartAt I x) x) (↑(extChartAt I x) y) ⊆ ball (↑(extChartAt I x) x) r ∩ range ↑I

Tactic:
exact ((convex_ball _ _).inter I.convex_range).segment_subset (by simp [r_pos]) hy

Goal state after:
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 𝕜 2) M
inst✝¹ : CompleteSpace E
m n : ℕ∞
inst✝ : IsManifold I (↑n + 1) M
U V : (x : M) → TangentSpace I x
x : M
hU : ContMDiffAt I I.tangent (↑n) (fun x ↦ ⟨x, U x⟩) x
hV : ContMDiffAt I I.tangent (↑n) (fun x ↦ ⟨x, V x⟩) x
hmn : minSmoothness 𝕜 (↑m + 1) ≤ ↑n
⊢ ContMDiffAt I I.tangent (↑m) (fun x₀ ↦ ⟨x₀, mlieBracket I U V x₀⟩) x

Tactic:
simp only [← contMDiffWithinAt_univ, ← mlieBracketWithin_univ] at hU hV ⊢
  exact hU.mlieBracketWithin_vectorField hV uniqueMDiffOn_univ (mem_univ _) hmn

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
h2 : Even n
h1 : n ≠ 1
⊢ reciprocalFactors n = 3 :: reciprocalFactors (n / 2)

Tactic:
reciprocalFactors,

Goal state after:
n : ℕ
h0 : n ≠ 0
h2 : Even n
h1 : n ≠ 1
⊢ (if x : n = 0 then [0]
    else
      if x : n = 1 then []
      else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    3 :: reciprocalFactors (n / 2)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
h1 : n ≠ 1
h2 : Odd n
h0 : n ≠ 0
⊢ reciprocalFactors n = n % 4 * n :: reciprocalFactors (n / 4 + 1)

Tactic:
reciprocalFactors,

Goal state after:
n : ℕ
h1 : n ≠ 1
h2 : Odd n
h0 : n ≠ 0
⊢ (if x : n = 0 then [0]
    else
      if x : n = 1 then []
      else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    n % 4 * n :: reciprocalFactors (n / 4 + 1)
Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G✝ : Type u_3
H✝ : Type u_4
inst✝³ : Group G✝
inst✝² : Group H✝
G : Type u
inst✝¹ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), (lift f) (of a) = f a
H : Type u
inst✝ : Group H
f : G →* H
a : X
⊢ lift.symm f a = f (of a)

Tactic:
simp [← lift_of (lift.symm f)]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ Submonoid.closure (Set.range ⇑inl ∪ Set.range ⇑inr) = ⊤

Tactic:
rw [← mrange_mk, MonoidHom.mrange_eq_map, ← closure_range_of, MonoidHom.map_mclosure,
    ← range_comp, Sum.range_eq]; rfl

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
⊢ inl.range ⊔ inr.range = ⊤

Tactic:
by
  rw [← closure_range_inl_union_inr, Subgroup.closure_union, ← MonoidHom.coe_range,
    ← MonoidHom.coe_range, Subgroup.closure_eq, Subgroup.closure_eq]

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

Goal state before:
pp: B : Type u_1
M : CoxeterMatrix B
G : Type u_5
inst✝ : Group G
f : B → G
hf : M.IsLiftable f
i i' : B
⊢ (f (i, i').1 * (FreeGroup.lift f) (FreeGroup.of (i, i').2)) ^ M.M (i, i').1 (i, i').2 = 1

Tactic:
FreeGroup.lift_apply_of

Goal state after:
B : Type u_1
M : CoxeterMatrix B
G : Type u_5
inst✝ : Group G
f : B → G
hf : M.IsLiftable f
i i' : B
⊢ (f (i, i').1 * f (i, i').2) ^ M.M (i, i').1 (i, i').2 = 1
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 j : ι
m : M i
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx ≠ some k
h2 : g ≠ 1
ih :
  ⟨i, m⟩ ∈
      (↑(consRecOn tail ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x ↦
              if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
              else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ tail.toList.tail ∨ ¬i = j ∧ ∃ (h : ¬tail.toList = []), tail.toList.head h = ⟨i, m⟩
h : ¬j = k
⊢ ⟨i, m⟩ ∈ (↑⟨{ head := 1, tail := cons g tail h1 h2, fstIdx_ne := ⋯ }, ⋯⟩).tail.toList ↔
    ⟨i, m⟩ ∈ (cons g tail h1 h2).toList.tail ∨
      ¬i = j ∧ ∃ (h : ¬(cons g tail h1 h2).toList = []), (cons g tail h1 h2).toList.head h = ⟨i, m⟩

Tactic:
· by_cases hik : i = k
      · subst i; simp_all [@eq_comm _ m g, @eq_comm _ k j, or_comm]
      · simp [hik, Ne.symm hik]

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
t : W
ht : cs.IsReflection t
w : W
⊢ cs.length (w * t) ≠ cs.length w

Tactic:
suffices cs.lengthParity (w * t) ≠ cs.lengthParity w by
    contrapose this
    simp only [lengthParity_eq_ofAdd_length, this]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.lengthParity (w * t) ≠ cs.lengthParity w
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
j : ℕ
h : j < ω.length
⊢ (cs.rightInvSeq ω)[j] =
    (cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)

Tactic:
← List.getD_eq_getElem (ris ω) 1,

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
h : j < ω.length
⊢ (cs.rightInvSeq ω).getD j 1 =
    (cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons.head
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω ∈ cs.rightInvSeq ω →
    cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)
⊢ cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)

Tactic:
use (π ω)⁻¹, i
      group

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
w✝ : Word M
h✝ : w✝ ≠ empty
i j : ι
w : NeWord M i j
h : w.toWord.toList = w✝.toList
i✝ : ℕ
a✝ : (i : ι) × M i
⊢ w.toWord.toList[i✝]? = some a✝ ↔ w✝.toList[i✝]? = some a✝

Tactic:
rw [h]

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
h : 0 ≤ a
x : DivisibleHull M
this : 0 = a ∨ 0 < a
⊢ a • x =
    (have this := ⟨a, h⟩;
      this) •
      x

Tactic:
aesop (add simp [qsmul_def, abs_of_pos])

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doubleCoset a ↑H ↑K) (doubleCoset b ↑H ↑K)
⊢ b ∈ doubleCoset a ↑H ↑K

Tactic:
rw [Set.not_disjoint_iff] at h
  simp only [mem_doubleCoset] at *
  obtain ⟨x, ⟨l, hl, r, hr, hrx⟩, y, hy, ⟨r', hr', rfl⟩⟩ := h
  refine ⟨y⁻¹ * l, H.mul_mem (H.inv_mem hy) hl, r * r'⁻¹, K.mul_mem hr (K.inv_mem hr'), ?_⟩
  rwa [mul_assoc, mul_assoc, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc, eq_mul_inv_iff_mul_eq]

Goal state after:
Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : FiniteIndexNormalSubgroup G
h : A.toSubgroup = B.toSubgroup
x✝ : G
⊢ x✝ ∈ A.carrier ↔ x✝ ∈ B.carrier

Tactic:
rw [h]

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: 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)
⊢ ↑(closure U) * R = ⊤

Tactic:
refine top_le_iff.mp fun g _ => ?_

Goal state after:
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 ∈ ⊤
⊢ g ∈ ↑(closure U) * R
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : ↥H →* A
inst✝¹ : H.FiniteIndex
g : G
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
⊢ ∏ x,
      ϕ
        ⟨(g ^ x.cast * Quotient.out (Quotient.out q))⁻¹ *
            if x = 0 then g ^ Function.minimalPeriod (fun x ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
            else g ^ x.cast * Quotient.out (Quotient.out q),
          ⋯⟩ =
    ϕ
      ⟨(Quotient.out (Quotient.out q))⁻¹ * g ^ Function.minimalPeriod (fun x ↦ g • x) (Quotient.out q) *
          Quotient.out (Quotient.out q),
        ⋯⟩

Tactic:
Fintype.prod_eq_single (0 : ZMod (Function.minimalPeriod (g • ·) q.out)) _

Goal state after:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : ↥H →* A
inst✝¹ : H.FiniteIndex
g : G
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
⊢ ϕ
      ⟨(g ^ ZMod.cast 0 * Quotient.out (Quotient.out q))⁻¹ *
          if 0 = 0 then g ^ Function.minimalPeriod (fun x ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
          else g ^ ZMod.cast 0 * Quotient.out (Quotient.out q),
        ⋯⟩ =
    ϕ
      ⟨(Quotient.out (Quotient.out q))⁻¹ * g ^ Function.minimalPeriod (fun x ↦ g • x) (Quotient.out q) *
          Quotient.out (Quotient.out q),
        ⋯⟩

G : Type u_1
inst✝³ : Group G
H : Subgroup G
A : Type u_2
inst✝² : CommGroup A
ϕ : ↥H →* A
inst✝¹ : H.FiniteIndex
g : G
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
⊢ ∀ (x : ZMod (Function.minimalPeriod (fun x ↦ g • x) (Quotient.out q))),
    x ≠ 0 →
      ϕ
          ⟨(g ^ x.cast * Quotient.out (Quotient.out q))⁻¹ *
              if x = 0 then g ^ Function.minimalPeriod (fun x ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
              else g ^ x.cast * Quotient.out (Quotient.out q),
            ⋯⟩ =
        1
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ (List.map
        (fun q ↦ ϕ ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x ↦ g • x) q.out * Quotient.out q.out, ⋯⟩)
        Finset.univ.toList).prod =
    ϕ ⟨g ^ H.index, ⋯⟩

Tactic:
← Function.comp_def ϕ,

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ (List.map
        (⇑ϕ ∘ fun q ↦
          ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x ↦ g • x) q.out * Quotient.out q.out, ⋯⟩)
        Finset.univ.toList).prod =
    ϕ ⟨g ^ H.index, ⋯⟩
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h2 :
  0 ∣
    (center ↥(closureCommutatorRepresentatives G)).index ^
      ((center ↥(closureCommutatorRepresentatives G)).index *
          Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) +
        1)
h : Nat.card ↥(_root_.commutator G) = 0
⊢ False

Tactic:
zero_dvd_iff

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h2 :
  (center ↥(closureCommutatorRepresentatives G)).index ^
      ((center ↥(closureCommutatorRepresentatives G)).index *
          Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) +
        1) =
    0
h : Nat.card ↥(_root_.commutator G) = 0
⊢ False
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
hφ : FixedPointFree ⇑φ
x y : G
h : commutatorMap (⇑φ) x = commutatorMap (⇑φ) y
⊢ φ x⁻¹ * φ y = x⁻¹ * y

Tactic:
map_inv,

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
hφ : FixedPointFree ⇑φ
x y : G
h : commutatorMap (⇑φ) x = commutatorMap (⇑φ) y
⊢ (φ x)⁻¹ * φ y = x⁻¹ * y
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg.inr.refine_1
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ (↑P).index.Coprime (Nat.card G).minFac

Tactic:
Nat.coprime_comm,

Goal state after:
case neg.inr.refine_1
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ (Nat.card G).minFac.Coprime (↑P).index
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
← mul_assoc y x⁻¹ y⁻¹

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
h : S.lowerCentralSeries n ≤ center G
⊢ ∀ y ∈ {g | ∃ g₁ ∈ S.lowerCentralSeries n, ∃ g₂ ∈ S, ⁅g₁, g₂⁆ = g}, y = 1

Tactic:
rintro x ⟨y, hy1, z, _, rfl⟩

Goal state after:
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
h : S.lowerCentralSeries n ≤ center G
y : G
hy1 : y ∈ S.lowerCentralSeries n
z : G
left✝ : z ∈ S
⊢ ⁅y, z⁆ = 1