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

Goal state before:
pp: case pos
𝕜 : 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
H' : Type u_5
inst✝⁷ : TopologicalSpace H'
E' : Type u_6
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H' M'
inst✝² : IsManifold I 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
hfi : (mfderiv[s] f x₀).IsInvertible
this : CompleteSpace E'
u : Set M
u_open : IsOpen[inst✝⁹] u
x₀u : x₀ ∈ u
u_mem : u ∈ 𝓝 x₀
s' : Set M := s ∩ u
ut : s' ⊆ f ⁻¹' t
maps_u : s' ⊆ f ⁻¹' (extChartAt I' (f x₀)).source
u_smooth : ContMDiffOn I I' 2 f s'
hs' : s' = s ∩ u
⊢ mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ =
    mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀

Tactic:
have s'_eq : s' =ᶠ[𝓝 x₀] s := by
    filter_upwards [u_mem] with y hy
    change (y ∈ s ∩ u) = (y ∈ s)
    simp [hy]

Goal state after:
case pos
𝕜 : 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
H' : Type u_5
inst✝⁷ : TopologicalSpace H'
E' : Type u_6
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H' M'
inst✝² : IsManifold I 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
hfi : (mfderiv[s] f x₀).IsInvertible
this : CompleteSpace E'
u : Set M
u_open : IsOpen[inst✝⁹] u
x₀u : x₀ ∈ u
u_mem : u ∈ 𝓝 x₀
s' : Set M := s ∩ u
ut : s' ⊆ f ⁻¹' t
maps_u : s' ⊆ f ⁻¹' (extChartAt I' (f x₀)).source
u_smooth : ContMDiffOn I I' 2 f s'
hs' : s' = s ∩ u
s'_eq : s' =ᶠ[𝓝 x₀] s
⊢ mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ =
    mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀
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, ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C

Tactic:
by
  rcases eventually_norm_mfderiv_extChartAt_lt I x with ⟨C, C_pos, hC⟩
  lift C to ℝ≥0 using C_pos.le
  simp only [gt_iff_lt, NNReal.coe_pos] at C_pos
  refine ⟨C, C_pos, ?_⟩
  filter_upwards [hC] with y hy
  simp only [enorm, nnnorm]
  exact_mod_cast hy

Goal state after:
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
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
V : Opens M
hUV : V ≤ U
hV₀f : ∀ y ∈ Set.range (Set.inclusion hUV), f y ≠ 0
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion hUV))
x₀ : ↑↑V
hxx₀ : Set.inclusion hUV x₀ = ⟨x, hxU⟩
⊢ x = ↑x₀

Tactic:
exact congr_arg Subtype.val hxx₀.symm

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
hmn : minSmoothness 𝕜 (↑m + 1) ≤ ↑n
hU : ContMDiffOn I I.tangent (↑n) (fun x ↦ ⟨x, U x⟩) univ
hV : ContMDiffOn I I.tangent (↑n) (fun x ↦ ⟨x, V x⟩) univ
⊢ ContMDiffOn I I.tangent (↑m) (fun x₀ ↦ ⟨x₀, mlieBracket I U V x₀⟩) univ

Tactic:
exact hU.mlieBracketWithin_vectorField hV uniqueMDiffOn_univ hmn

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B) → AddCommMonoid (E x)
inst✝¹⁷ : (x : B) → Module 𝕜 (E x)
inst✝¹⁶ : NormedAddCommGroup F
inst✝¹⁵ : NormedSpace 𝕜 F
inst✝¹⁴ : TopologicalSpace (TotalSpace F E)
inst✝¹³ : (x : B) → TopologicalSpace (E x)
EB : Type u_6
inst✝¹² : NormedAddCommGroup EB
inst✝¹¹ : NormedSpace 𝕜 EB
HB : Type u_7
inst✝¹⁰ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁹ : TopologicalSpace B
inst✝⁸ : ChartedSpace HB B
EB' : Type u_8
inst✝⁷ : NormedAddCommGroup EB'
inst✝⁶ : NormedSpace 𝕜 EB'
HB' : Type u_9
inst✝⁵ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁴ : TopologicalSpace B'
inst✝³ : ChartedSpace HB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
⊢ ∀ (e e' : Trivialization F TotalSpace.proj) [inst : MemTrivializationAtlas e] [inst_1 : MemTrivializationAtlas e'],
    ContMDiffOn IB' 𝓘(𝕜, F →L[𝕜] F) n (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)

Tactic:
rintro _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩

Goal state after:
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B) → AddCommMonoid (E x)
inst✝¹⁷ : (x : B) → Module 𝕜 (E x)
inst✝¹⁶ : NormedAddCommGroup F
inst✝¹⁵ : NormedSpace 𝕜 F
inst✝¹⁴ : TopologicalSpace (TotalSpace F E)
inst✝¹³ : (x : B) → TopologicalSpace (E x)
EB : Type u_6
inst✝¹² : NormedAddCommGroup EB
inst✝¹¹ : NormedSpace 𝕜 EB
HB : Type u_7
inst✝¹⁰ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁹ : TopologicalSpace B
inst✝⁸ : ChartedSpace HB B
EB' : Type u_8
inst✝⁷ : NormedAddCommGroup EB'
inst✝⁶ : NormedSpace 𝕜 EB'
HB' : Type u_9
inst✝⁵ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁴ : TopologicalSpace B'
inst✝³ : ChartedSpace HB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
⊢ ContMDiffOn IB' 𝓘(𝕜, F →L[𝕜] F) n (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 (e.pullback f) (e'.pullback f) b))
    ((e.pullback f).baseSet ∩ (e'.pullback f).baseSet)
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
x : M
hU : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U x⟩) univ x
hV : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, V x⟩) univ x
hW : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, W x⟩) univ x
⊢ mlieBracketWithin I U (mlieBracketWithin I V W univ) univ x =
    mlieBracketWithin I (mlieBracketWithin I U V univ) W univ x +
      mlieBracketWithin I V (mlieBracketWithin I U W univ) univ x

Tactic:
exact leibniz_identity_mlieBracketWithin_apply uniqueMDiffOn_univ (by simp) (mem_univ _) hU hV hW

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
⊢ Nat.card (Additive G) = 4

Tactic:
← IsKleinFour.card_four (G := G)

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
⊢ Nat.card (Additive G) = Nat.card G
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case sr
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * sr i = sr i * g
heq : i - 1 = i + 1
⊢ sr i = 1

Tactic:
have : Fact (1 < n) := ⟨by grind⟩

Goal state after:
case sr
n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * sr i = sr i * g
heq : i - 1 = i + 1
this : Fact (1 < n)
⊢ sr i = 1
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
this : Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹
⊢ ⊤.toSubmonoid = ⊤

Tactic:
Subgroup.top_toSubmonoid

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
this : Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹
⊢ ⊤ = ⊤
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
⊢ ∃ δ, 0 < δ ∧ 1 + δ * C < r' ^ 2

Tactic:
have A : ∀ᶠ δ in 𝓝[>] (0 : ℝ), 0 < δ := self_mem_nhdsWithin
    have B : Tendsto (fun δ ↦ 1 + δ * C) (𝓝[>] 0) (𝓝 (1 + 0 * C)) := by
      apply tendsto_inf_left
      exact tendsto_const_nhds.add (tendsto_id.mul tendsto_const_nhds)
    have B' : ∀ᶠ δ in 𝓝[>] 0, 1 + δ * C < r' ^ 2 := by
      apply (tendsto_order.1 B).2
      simpa using hr'.trans_le (le_abs_self _)
    exact (A.and B').exists

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
i : B
⊢ cs.IsReflection (cs.simple i)

Tactic:
by use 1, i; simp

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
i : B
⊢ ¬cs.IsRightDescent 1 i

Tactic:
simp [IsRightDescent]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case of
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i✝ : ι
m✝ : M i✝
w✝ : Word M
⊢ (of m✝ • w✝).prod = of m✝ * w✝.prod

Tactic:
rw [of_smul_def, prod_rcons, of.map_mul, mul_assoc, ← prod_rcons, ← equivPair_symm,
      Equiv.symm_apply_apply]

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
i j : ι
w : NeWord M i j
⊢ ∀ l ∈ w.toList, l.snd ≠ 1

Tactic:
by
    induction w
    · simpa only [toList, List.mem_singleton, ne_eq, forall_eq]
    · intro l h
      simp only [toList, List.mem_append] at h
      cases h <;> aesop

Goal state after:
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⁻¹
hnot1 : h * w.head ≠ 1
w' : NeWord H i i := (w.mulHead h hnot1).append ⋯ (NeWord.singleton h⁻¹ ⋯)
hw' : (lift f) w'.prod ≠ 1
heq1 : (lift f) w.prod = 1
⊢ False

Tactic:
apply hw'

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⁻¹
hnot1 : h * w.head ≠ 1
w' : NeWord H i i := ⋯
hw' : (lift f) w'.prod ≠ 1
heq1 : (lift f) w.prod = 1
⊢ (lift f) w'.prod = 1
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
t : Finset (Quotient ↑H ↑K)
ht : Set.univ ⊆ ⋃ i ∈ t, Quot.mk ⇑(rightRel H) '' doubleCoset (out i) ↑H ↑K
⊢ ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K = Set.univ

Tactic:
contrapose ht
  simp only [Set.univ_subset_iff, ← ne_eq] at ⊢ ht
  obtain ⟨x, hx⟩ := (Set.ne_univ_iff_exists_notMem _).mp ht
  refine (Set.ne_univ_iff_exists_notMem _).mpr ⟨Quot.mk (rightRel H) x, ?_⟩
  simp only [Set.mem_iUnion, Set.mem_image, exists_prop, not_exists, not_and]
  intro y hy q hq
  contrapose hx
  simp only [Set.mem_iUnion, exists_prop]
  refine ⟨y, hy, ?_⟩
  rw [← doubleCoset_eq_of_mem hq, mem_doubleCoset]
  obtain ⟨a, ha⟩ : ∃ a : H, x = a * q := by
    obtain ⟨a, ha⟩ : ∃ a : H, a * x = q := Quotient.eq.mp hx
    exact ⟨⟨a⁻¹, by simp⟩, eq_inv_mul_of_mul_eq ha⟩
  exact ⟨a.1, a.2, ⟨1, Subgroup.one_mem K, by simpa using ha⟩⟩

Goal state after:
Module: Mathlib.GroupTheory.Transfer

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

Tactic:
← zpow_one_add,

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

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

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

Tactic:
· rw [if_pos hk, if_pos hk, zpow_natCast]

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

Goal state before:
pp: case refine_2
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'
a : A
b : (actionAsFunctor G A).obj PUnit.unit
e : IsFreeGroup.Generators G
h : IsFreeGroup.of e • a = b
⊢ (F' (IsFreeGroup.of ↑⟨e, h⟩)).left (ActionCategory.back ⟨PUnit.unit, b⟩) = f ⟨e, h⟩

Tactic:
rw [hF']

Goal state after:
case refine_2
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'
a : A
b : (actionAsFunctor G A).obj PUnit.unit
e : IsFreeGroup.Generators G
h : IsFreeGroup.of e • a = b
⊢ (f' ↑⟨e, h⟩).left (ActionCategory.back ⟨PUnit.unit, b⟩) = f ⟨e, h⟩
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
by
  refine antitone_nat_of_succ_le fun n => ?_
  rw [lowerCentralSeries_succ, ← le_normalizer_iff_commutator_le_left]
  exact S.self_le_normalizer_lowerCentralSeries n

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 : α × Bool
hl : [a] = g.toWord
⊢ (mk [w])⁻¹ • ⟨mk [w], ⋯⟩ • x ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x}

Tactic:
startsWith.smul_def,

Goal state after:
α : 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 : α × Bool
hl : [a] = g.toWord
⊢ (mk [w])⁻¹ • mk [w] • x ∈ (⋃ v ∈ {z | z ≠ (w.1, !w.2)}, MulAction.orbit (↑(startsWith v)) x) ∪ {x}
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)
⊢ (mk [w])⁻¹ • ⟨mk [w] * mk (b :: l), ⋯⟩ • x ∈ MulAction.orbit (↑(startsWith b)) x

Tactic:
startsWith.smul_def,

Goal state after:
α : 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)
⊢ (mk [w])⁻¹ • (mk [w] * mk (b :: l)) • x ∈ MulAction.orbit (↑(startsWith b)) x
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
⊢ map (MonoidHom.snd ↥G' ↥H') (P.prod Q).range = ⊤

Tactic:
simp only [← MonoidHom.range_comp, MonoidHom.range_eq_top]

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
⊢ Surjective ⇑((MonoidHom.snd ↥G' ↥H').comp (P.prod Q))
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_1.cons.inl
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : b✝ ⟶ c✝
eT : Sum.inl e ∈ T b✝ c✝
⊢ F'.map (Sum.recOn (↑⟨Sum.inl e, eT⟩) (fun e ↦ of e) fun e ↦ inv (of e)) = 1

Tactic:
rw [hF']

Goal state after:
case refine_1.cons.inl
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a b✝ c✝ : WideSubquiver.toType (Symmetrify (Generators G)) T
p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) b✝
ih : F'.map (homOfPath T p) = 1
e : b✝ ⟶ c✝
eT : Sum.inl e ∈ T b✝ c✝
⊢ f' e = 1