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
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 := ⋯
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
t' : Set M' := ⋯
ht' : t' = t ∩ (extChartAt I' (f x₀)).source
⊢ mpullbackWithin I I' f V s' =ᶠ[𝓝[s] x₀] mpullbackWithin I I' f V s

Tactic:
apply nhdsWithin_le_nhds
      filter_upwards [mfderivWithin_eventually_congr_set (I := I) (I' := I') (f := f) s'_eq]
        with y hy using by simp [mpullbackWithin, 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
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 := ⋯
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
t' : Set M' := ⋯
ht' : t' = t ∩ (extChartAt I' (f x₀)).source
⊢ mpullbackWithin I I' f W s' =ᶠ[𝓝[s] x₀] mpullbackWithin I I' f W s

Tactic:
apply nhdsWithin_le_nhds
      filter_upwards [mfderivWithin_eventually_congr_set (I := I) (I' := I') (f := f) s'_eq]
        with y hy using by simp [mpullbackWithin, hy]

Goal state after:
Module: Mathlib.Geometry.Manifold.Sheaf.Basic

Goal state before:
pp: H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
⊢ ∀ {U : Opens ↑(TopCat.of M)} (f : ↥U → M'),
    (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, ChartedSpace.LiftProp P fun x ↦ f (i x)) → ChartedSpace.LiftProp P f

Tactic:
by
    intro V f h x
    obtain ⟨U, hxU, i, hU : ChartedSpace.LiftProp P (f ∘ _)⟩ := h x
    let x' : U := ⟨x, hxU⟩
    have hUV : U ≤ V := CategoryTheory.leOfHom i
    have : ChartedSpace.LiftPropAt P f (Opens.inclusion hUV x') := by
      rw [hG.liftPropAt_iff_comp_inclusion hUV]
      exact hU x'
    convert! this

Goal state after:
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: case mpr
𝕜 : 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₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, f y ≠ 0
hV₀ : IsOpen[instTopologicalSpaceSubtype] V₀
hxV₀ : ⟨x, hxU⟩ ∈ V₀
V : Opens M := { carrier := Subtype.val '' V₀, is_open' := ⋯ }
⊢ IsUnit ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f)

Tactic:
have hUV : V ≤ U := Subtype.coe_image_subset (U : Set M) V₀

Goal state after:
case mpr
𝕜 : 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₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, f y ≠ 0
hV₀ : IsOpen[instTopologicalSpaceSubtype] V₀
hxV₀ : ⟨x, hxU⟩ ∈ V₀
V : Opens M := { carrier := Subtype.val '' V₀, is_open' := ⋯ }
hUV : V ≤ U
⊢ IsUnit ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f)
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
s : Set M
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
hcov : IsCovariantDerivativeOn F cov s
A : (x : M) → V x →L[𝕜] TangentSpace I x →L[𝕜] V x
σ✝ σ'✝ : (x : M) → V x
x✝ : M
hσ : MDiffAt (T% σ✝) x✝
hσ' : MDiffAt (T% σ'✝) x✝
hx : x✝ ∈ s
⊢ cov (σ✝ + σ'✝) x✝ + (A x✝) ((σ✝ + σ'✝) x✝) = cov σ✝ x✝ + (A x✝) (σ✝ x✝) + (cov σ'✝ x✝ + (A x✝) (σ'✝ x✝))

Tactic:
simp [hcov.add hσ hσ']
    abel

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

Goal state before:
pp: 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✝ : CompactSpace M
ι : Type uM
f : SmoothBumpCovering ι I M
this : Fintype ι
n : ℕ
e : M → EuclideanSpace ℝ (Fin n)
hsmooth : ContMDiff I (𝓡 n) ∞ e
hinj : Injective e
hinj_mfderiv : ∀ (x : M), Injective ⇑(mfderiv% e x)
⊢ ∃ n e, ContMDiff I (𝓡 n) ∞ e ∧ IsClosedEmbedding e ∧ ∀ (x : M), Injective ⇑(mfderiv% e x)

Tactic:
exact ⟨n, e, hsmooth, hsmooth.continuous.isClosedEmbedding hinj, hinj_mfderiv⟩

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

Goal state before:
pp: n : ℕ
⊢ Monoid.exponent (DihedralGroup n) = lcm n 2

Tactic:
rcases eq_zero_or_neZero n with (rfl | hn)
  · exact Monoid.exponent_eq_zero_of_order_zero orderOf_r_one
  apply Nat.dvd_antisymm
  · apply Monoid.exponent_dvd_of_forall_pow_eq_one
    rintro (m | m)
    · rw [← orderOf_dvd_iff_pow_eq_one, orderOf_r]
      refine Nat.dvd_trans ⟨gcd n m.val, ?_⟩ (dvd_lcm_left n 2)
      exact (Nat.div_mul_cancel (Nat.gcd_dvd_left n m.val)).symm
    · rw [← orderOf_dvd_iff_pow_eq_one, orderOf_sr]
      exact dvd_lcm_right n 2
  · apply lcm_dvd
    · convert! Monoid.order_dvd_exponent (r (1 : ZMod n))
      exact orderOf_r_one.symm
    · convert! Monoid.order_dvd_exponent (sr (0 : ZMod n))
      exact (orderOf_sr 0).symm

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

Goal state before:
pp: n : ℕ
⊢ n = 1 ∨ n = 2 → IsMulCommutative (DihedralGroup n)

Tactic:
rintro (rfl | rfl) <;> exact ⟨⟨by decide⟩⟩

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
⊢ commProb M = 1 ↔ IsMulCommutative M

Tactic:
have := Fintype.ofFinite M
  rw [commProb, ← Set.coe_ofPred, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
  rw [div_eq_one_iff_eq, ← Nat.cast_pow, Nat.cast_inj, sq, ← card_prod,
    set_fintype_card_eq_univ_iff, Set.eq_univ_iff_forall]
  · exact ⟨fun h ↦ ⟨⟨fun x y ↦ h (x, y)⟩⟩, fun h x ↦ mul_comm' ..⟩
  · exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr card_ne_zero)

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

Goal state before:
pp: n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h✝ : Commute (sr i, sr j).1 (sr i, sr j).2
h : i = j
⊢ (fun x ↦
        match x with
        | Sum.inl i => ⟨(sr i, r 0), ⋯⟩
        | Sum.inr (Sum.inl j) => ⟨(r 0, sr j), ⋯⟩
        | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)), ⋯⟩
        | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(r i, r j), ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨(sr i, r a), property⟩ => Sum.inl i
          | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j)
          | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j)))
          | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j))))
        ⟨(sr i, sr j), h✝⟩) =
    ⟨(sr i, sr j), h✝⟩

Tactic:
rw [Subtype.ext_iff, Prod.ext_iff, sr.injEq, sr.injEq, h, and_self, ← two_mul]

Goal state after:
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h✝ : Commute (sr i, sr j).1 (sr i, sr j).2
h : i = j
⊢ ↑u⁻¹ * (2 * j) = j
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ 0 < ↑(Nat.card (G ⧸ H))

Tactic:
· exact Nat.cast_pos.mpr Finite.card_pos

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (fst x, snd x) = toProd x

Tactic:
← fst_prod_snd,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (fst x, snd x) = (fst.prod snd) x
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (MonoidHom.fst M N).comp toProd = fst

Tactic:
← fst_prod_snd,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (MonoidHom.fst M N).comp (fst.prod snd) = fst
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (MonoidHom.snd M N).comp toProd = snd

Tactic:
← fst_prod_snd,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (MonoidHom.snd M N).comp (fst.prod snd) = snd
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
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
e : M ≃* N
e' : M' ≃* N'
⊢ (Coprod.map ↑e.symm ↑e'.symm).comp (Coprod.map ↑e ↑e') = MonoidHom.id (M ∗ M')

Tactic:
by ext <;> simp

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
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
e : M ≃* N
e' : M' ≃* N'
⊢ (Coprod.map ↑e ↑e').comp (Coprod.map ↑e.symm ↑e'.symm) = MonoidHom.id (N ∗ N')

Tactic:
by ext <;> simp

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

Goal state before:
pp: case cons
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
x : B
ω' : List B
ih : cs.wordProd ω'.reverse = (cs.wordProd ω')⁻¹
⊢ cs.wordProd (x :: ω').reverse = (cs.wordProd (x :: ω'))⁻¹

Tactic:
| cons x ω' ih =>

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

Tactic:
mul_inv_rev,

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
ht : cs.IsReflection t
⊢ cs.length (t⁻¹ * w⁻¹⁻¹) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length 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
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsRightInversion (t * w)⁻¹ t ↔ ¬cs.IsRightInversion w⁻¹ t

Tactic:
mul_inv_rev,

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.IsRightInversion (w⁻¹ * t⁻¹) t ↔ ¬cs.IsRightInversion w⁻¹ t
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 : ℕ
⊢ (cs.leftInvSeq ω).getD j 1 * (cs.leftInvSeq ω).getD j 1 = 1

Tactic:
by
  simp_rw [getD_leftInvSeq, mul_assoc]
  rcases em (j < ω.length) with hj | nhj
  · rw [getElem?_eq_getElem hj]
    simp [← mul_assoc]
  · rw [getElem?_eq_none_iff.mpr (by lia)]
    simp

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
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
⊢ False

Tactic:
have h₅ := calc
    π ω = π ω * t * t' := by rw [mul_assoc, h₄]; group
    _ = (π (ω.eraseIdx j)) * t' :=
        congrArg (· * t') (cs.wordProd_mul_getD_rightInvSeq _ _)
    _ = π ((ω.eraseIdx j).eraseIdx (j' - 1)) :=
        cs.wordProd_mul_getD_rightInvSeq _ _

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
h₅ : cs.wordProd ω = cs.wordProd ((ω.eraseIdx j).eraseIdx (j' - 1))
⊢ False
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case singleton
ι : 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 α
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
i j i✝ : ι
x : H i✝
hne_one : x ≠ 1
k : ι
hk : i✝ ≠ k
⊢ (lift f) (NeWord.singleton x hne_one).prod • X k ⊆ X i✝

Tactic:
| singleton x hne_one =>

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

Goal state before:
pp: case succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p k : ℕ
hk :
  ∀ (i j : B) (h : k < 2 * p),
    (cs.leftInvSeq (alternatingWord i j (2 * p)))[k] = cs.wordProd (alternatingWord j i (2 * k + 1))
i j : B
h : k + 1 < 2 * p
⊢ (cs.leftInvSeq (alternatingWord i j (2 * p)))[k + 1] = cs.wordProd (alternatingWord j i (2 * (k + 1) + 1))

Tactic:
simp only [getElem_succ_leftInvSeq_alternatingWord cs i j p k h, hk _ _ (by lia),
      MulAut.conj_apply, inv_simple, alternatingWord_succ' j i, even_two, Even.mul_right,
      ↓reduceIte, wordProd_cons]
    rw [(by ring : 2 * (k + 1) = 2 * k + 1 + 1), alternatingWord_succ j i, wordProd_concat]
    simp [mul_assoc]

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
i j k : ι
w : NeWord H i j
hhead : k ≠ i
hlast : k ≠ j
heq1 : (lift f) w.prod = 1
this : X k ⊆ X i
⊢ False

Tactic:
obtain ⟨x, hx⟩ := hXnonempty k

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
i j k : ι
w : NeWord H i j
hhead : k ≠ i
hlast : k ≠ j
heq1 : (lift f) w.prod = 1
this : X k ⊆ X i
x : α
hx : x ∈ X k
⊢ 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
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g h : G
key : g * h = ((fun x ↦ x⁻¹) g * (fun x ↦ x⁻¹) h)⁻¹
⊢ Commute g h

Tactic:
mul_inv_rev,

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
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
g h : G
key : g * h = ((fun x ↦ x⁻¹) h)⁻¹ * ((fun x ↦ x⁻¹) g)⁻¹
⊢ Commute g h
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

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

pp: case cons_append
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
a✝¹ : α × Bool
l✝ : List (α × Bool)
b✝ : α × Bool
a✝ : IsReduced l✝ → IsCyclicallyReduced (reduceCyclically l✝)
h : IsReduced (a✝¹ :: (l✝ ++ [b✝]))
⊢ IsCyclicallyReduced (reduceCyclically (a✝¹ :: (l✝ ++ [b✝])))

Tactic:
case singleton => simp

Goal state after:
case cons_append
α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
a✝¹ : α × Bool
l✝ : List (α × Bool)
b✝ : α × Bool
a✝ : IsReduced l✝ → IsCyclicallyReduced (reduceCyclically l✝)
h : IsReduced (a✝¹ :: (l✝ ++ [b✝]))
⊢ IsCyclicallyReduced (reduceCyclically (a✝¹ :: (l✝ ++ [b✝])))
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: case singleton
α : Type u
inst✝ : DecidableEq α
a✝ : α × Bool
⊢ conjugator [a✝] ++ reduceCyclically [a✝] ++ invRev (conjugator [a✝]) = [a✝]

pp: case cons_append
α : Type u
inst✝ : DecidableEq α
a✝¹ : α × Bool
l✝ : List (α × Bool)
b✝ : α × Bool
a✝ : conjugator l✝ ++ reduceCyclically l✝ ++ invRev (conjugator l✝) = l✝
⊢ conjugator (a✝¹ :: (l✝ ++ [b✝])) ++ reduceCyclically (a✝¹ :: (l✝ ++ [b✝])) ++
      invRev (conjugator (a✝¹ :: (l✝ ++ [b✝]))) =
    a✝¹ :: (l✝ ++ [b✝])

Tactic:
case singleton => simp

Goal state after:
case cons_append
α : Type u
inst✝ : DecidableEq α
a✝¹ : α × Bool
l✝ : List (α × Bool)
b✝ : α × Bool
a✝ : conjugator l✝ ++ reduceCyclically l✝ ++ invRev (conjugator l✝) = l✝
⊢ conjugator (a✝¹ :: (l✝ ++ [b✝])) ++ reduceCyclically (a✝¹ :: (l✝ ++ [b✝])) ++
      invRev (conjugator (a✝¹ :: (l✝ ++ [b✝]))) =
    a✝¹ :: (l✝ ++ [b✝])
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x✝ y : G
⊢ ⁅x✝, y⁆ ∈ N ↔ x✝ * y * (y * x✝)⁻¹ ∈ N

Tactic:
mul_inv_rev,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x✝ y : G
⊢ ⁅x✝, y⁆ ∈ N ↔ x✝ * y * (x✝⁻¹ * y⁻¹) ∈ N
Module: Mathlib.GroupTheory.Nilpotent

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

Tactic:
by simpa

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
this : nilpotencyClass (G ⧸ center G) = n
⊢ nilpotencyClass (G ⧸ center G) = n + 1 - 1

Tactic:
by simpa

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

Goal state before:
pp: case refine_2.e_5
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'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
a b : Generators G
e : a ⟶ b
⊢ (functorOfMonoidHom T E).map (of e) = f' e

Tactic:
change E (loopOfHom T _) = dite _ _ _

Goal state after:
case refine_2.e_5
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'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
a b : Generators G
e : a ⟶ b
⊢ E (loopOfHom T (of e)) =
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
s : Set G
g : G
hB : IsBlock G B
hgs : ¬g • B ⊆ s • B
⊢ Disjoint (g • B) (s • B)

Tactic:
rw [← iUnion_smul_set, disjoint_iUnion₂_right]
  exact fun b hb ↦ hB fun h ↦ hgs <| h.trans_subset <| smul_set_subset_smul hb

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Iwasawa

Goal state before:
pp: case inl
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : fixedPoints (↥N) α = Set.univ
n : M
hn : n ∈ N
x : α
⊢ n • x = x

Tactic:
exact Set.eq_univ_iff_forall.mp h x ⟨n, hn⟩

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

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
β : Type u_2
inst✝¹ : Fintype β
inst✝ : DecidableEq β
e : α ≃ β
⊢ map (↑e.permCongrHom) (alternatingGroup α) = alternatingGroup β

Tactic:
by simp [Subgroup.ext_iff, Subgroup.map_equiv_eq_comap_symm]

Goal state after: