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

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
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}
⊢ ball (↑(extChartAt I x) x) r ∩ range ↑I ∈ 𝓝[range ↑I] ↑(extChartAt I x) x

Tactic:
inter_comm

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}
⊢ range ↑I ∩ ball (↑(extChartAt I x) x) r ∈ 𝓝[range ↑I] ↑(extChartAt I x) x
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace N
f : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
s : Set M
hs : IsOpen[inst✝¹] s
x✝ : SubmersionAtProp F I J M N f φ ψ
equiv : E ≃L[𝕜] E'' × F
hf : EqOn (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (Prod.fst ∘ ⇑equiv) (φ.extend I).target
⊢ ((φ.restr s).extend I).target ⊆ (φ.extend I).target

Tactic:
by simp; grind

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

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
h : IsSubmersionAtOfComplement F I J n f x
⊢ ContMDiffOn I J n f h.domChart.source

Tactic:
by
  rw [← contMDiffOn_writtenInExtend_iff h.domChart_mem_maximalAtlas
    h.codChart_mem_maximalAtlas le_rfl h.mapsto_domChart_source_codChart_source,
    ← h.domChart.extend_target_eq_image_source]
  have : CMDiff n (Prod.fst ∘ h.equiv) := by rw [contMDiff_iff_contDiff]; fun_prop
  exact this.contMDiffOn.congr h.writtenInCharts

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
n : ℕ∞ω
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : RiemannianBundle fun x ↦ TangentSpace I x
inst✝² : IsManifold I 1 M
inst✝¹ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
inst✝ : RegularSpace M
⊢ IsRiemannianManifold I M

Tactic:
by
  let : PseudoEMetricSpace M := .ofRiemannianMetric I M
  exact ⟨fun x y ↦ rfl⟩

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

Goal state before:
pp: E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → NormedAddCommGroup (V x)
inst✝³ : (x : M) → InnerProductSpace ℝ (V x)
inst✝² : FiberBundle F V
cov : CovariantDerivative I F V
inst✝¹ : VectorBundle ℝ F V
inst✝ : IsContMDiffRiemannianBundle I 1 F V
x : M
τ : (x : M) → V x
hτ : MDiffAt (T% τ) x
f✝ : M → ℝ
σ✝ : (x : M) → V x
hf : MDiffAt f✝ x
hσ : MDiffAt (T% σ✝) x
X₀ : TangentSpace I x
⊢ (derivMetricTensorAux I cov (f✝ • σ✝) τ x) X₀ = (f✝ x • derivMetricTensorAux I cov σ✝ τ x) X₀

Tactic:
simp [mvfderiv_fun_mul hf (hσ.inner_bundle hτ),
      cov.isCovariantDerivativeOn.leibniz hσ hf, inner_add_left, inner_smul_left]

Goal state after:
E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
H : Type u_2
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
V : M → Type u_5
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → NormedAddCommGroup (V x)
inst✝³ : (x : M) → InnerProductSpace ℝ (V x)
inst✝² : FiberBundle F V
cov : CovariantDerivative I F V
inst✝¹ : VectorBundle ℝ F V
inst✝ : IsContMDiffRiemannianBundle I 1 F V
x : M
τ : (x : M) → V x
hτ : MDiffAt (T% τ) x
f✝ : M → ℝ
σ✝ : (x : M) → V x
hf : MDiffAt f✝ x
hσ : MDiffAt (T% σ✝) x
X₀ : TangentSpace I x
⊢ f✝ x * ((d% fun b ↦ inner ℝ (σ✝ b) (τ b)) x) X₀ + inner ℝ (σ✝ x) (τ x) * (d% f✝ x) X₀ -
        (f✝ x * inner ℝ ((↑cov σ✝ x) X₀) (τ x) + (d% f✝ x) X₀ * inner ℝ (σ✝ x) (τ x)) -
      f✝ x * inner ℝ (σ✝ x) ((↑cov τ x) X₀) =
    f✝ x * (((d% fun b ↦ inner ℝ (σ✝ b) (τ b)) x) X₀ - inner ℝ ((↑cov σ✝ x) X₀) (τ x) - inner ℝ (σ✝ x) ((↑cov τ x) X₀))
Module: Mathlib.GroupTheory.Commensurable

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : ConjAct G
⊢ (g • H).Commensurable H ↔ H.Commensurable (g⁻¹ • H)

Tactic:
rw [commensurable_conj, inv_smul_smul]

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
hy : ¬y = 1
hxy : ¬x = y
⊢ {e (x * y), e x, e y, 1} = univ

Tactic:
simpa [map_univ_equiv e, map_insert, he]
          using congr(Finset.map e.toEmbedding $(eq_finset_univ hx hy hxy))

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

Goal state before:
pp: n : ℕ
i : ZMod n
⊢ orderOf (sr i) = 2

Tactic:
by
  apply orderOf_eq_prime
  · rw [sq, sr_mul_self]
  · simp [← r_zero]

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

Goal state before:
pp: case inr.a.sr
n : ℕ
hn : NeZero n
m : ZMod n
⊢ orderOf (sr m) ∣ lcm n 2

Tactic:
orderOf_sr

Goal state after:
case inr.a.sr
n : ℕ
hn : NeZero n
m : ZMod n
⊢ 2 ∣ lcm n 2
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card M) ^ 2 = 1 ↔ IsMulCommutative M

Tactic:
← Set.coe_ofPred,

Goal state after:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(Nat.card ↑{x | Commute x.1 x.2}) / ↑(Nat.card M) ^ 2 = 1 ↔ IsMulCommutative M
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
⊢ (lift FreeGroup.of).comp (FreeGroup.lift of) = MonoidHom.id (FreeGroup X)

Tactic:
by
        apply FreeGroup.ext_hom; intro x
        simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.id_apply,
          FreeGroup.lift_apply_of, lift_of]

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
K : Type u_3
inst✝ : Group K
f : G →* K
g : H →* K
⊢ (lift f g).range = f.range ⊔ g.range

Tactic:
simp [range_eq]

Goal state after:
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
i i' : B
this✝ : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) ((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') = 1
⊢ cs.mulEquiv.symm (PresentedGroup.of i * PresentedGroup.of i') ^ M.M i i' = 1

Tactic:
← map_pow

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this✝ : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) ((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') = 1
⊢ cs.mulEquiv.symm ((PresentedGroup.of i * PresentedGroup.of i') ^ M.M i i') = 1
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ MonoidHom.mrange
      ({ toFun := fun fi ↦ (conGen (Rel M)).lift (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) ⋯,
          invFun := fun f x ↦ f.comp of, left_inv := ⋯, right_inv := ⋯ }
        f) =
    ⨆ i, MonoidHom.mrange (f i)

Tactic:
Equiv.coe_fn_mk,

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ MonoidHom.mrange ((conGen (Rel M)).lift (FreeMonoid.lift fun p ↦ (f p.fst) p.snd) ⋯) = ⨆ i, MonoidHom.mrange (f i)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ ⨆ i, MonoidHom.mrange of = ⊤

Tactic:
by
  simp [← mrange_eq_iSup]

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
f : { f // M.IsLiftable f }
i : B
⊢ (↑(Units.coeHom G)).toFun
      ((PresentedGroup.toGroup (@CoxeterSystem.relations_liftable B M Gˣ Units.instGroup (restrictUnit ⋯) ⋯))
        (cs.mulEquiv.toMonoidHom (cs.mulEquiv.symm (PresentedGroup.of i)))) =
    ↑f i

Tactic:
toMonoidHom_apply_symm_apply,

Goal state after:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
f : { f // M.IsLiftable f }
i : B
⊢ (↑(Units.coeHom G)).toFun
      ((PresentedGroup.toGroup (@CoxeterSystem.relations_liftable B M Gˣ Units.instGroup (restrictUnit ⋯) ⋯))
        (PresentedGroup.of i)) =
    ↑f i
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
f : { f // M.IsLiftable f }
i : B
⊢ (Units.coeHom G)
      ((PresentedGroup.toGroup (@CoxeterSystem.relations_liftable B M Gˣ Units.instGroup (restrictUnit ⋯) ⋯))
        (cs.mulEquiv.toMonoidHom (cs.mulEquiv.symm (PresentedGroup.of i)))) =
    ↑f i

Tactic:
rw [← MonoidHom.toFun_eq_coe, toMonoidHom_apply_symm_apply, PresentedGroup.toGroup.of,
      OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, Units.coeHom_apply, restrictUnit]

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
ι : W →* G
i : B
⊢ (Units.coeHom G)
      ((PresentedGroup.toGroup (@CoxeterSystem.relations_liftable B M Gˣ Units.instGroup (restrictUnit ⋯) ⋯))
        (cs.mulEquiv.toMonoidHom (cs.mulEquiv.symm (PresentedGroup.of i)))) =
    ι (cs.mulEquiv.symm (PresentedGroup.of i))

Tactic:
toMonoidHom_apply_symm_apply,

Goal state after:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
ι : W →* G
i : B
⊢ (Units.coeHom G)
      ((PresentedGroup.toGroup (@CoxeterSystem.relations_liftable B M Gˣ Units.instGroup (restrictUnit ⋯) ⋯))
        (PresentedGroup.of i)) =
    ι (cs.mulEquiv.symm (PresentedGroup.of i))
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
⊢ ∃ ω, cs.IsReduced ω ∧ w = cs.wordProd ω

Tactic:
obtain ⟨ω, hω, rfl⟩ := Nat.find_spec (cs.exists_word_with_prod w)

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : Nat.find ⋯ = ω.length
⊢ ∃ ω_1, cs.IsReduced ω_1 ∧ cs.wordProd ω = cs.wordProd ω_1
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case singleton
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (singleton x✝ a✝).toList

Tactic:
exact List.isChain_singleton _

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

Goal state before:
pp: case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.rightInvSeq ω).length
ht : (cs.rightInvSeq ω)[j] ∈ cs.rightInvSeq ω
⊢ cs.length (cs.wordProd ω * (cs.rightInvSeq ω)[j]) < cs.length (cs.wordProd ω)

Tactic:
rw [← List.getD_eq_getElem _ 1 hj, wordProd_mul_getD_rightInvSeq]

Goal state after:
case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
hj : j < (cs.rightInvSeq ω).length
ht : (cs.rightInvSeq ω)[j] ∈ cs.rightInvSeq ω
⊢ cs.length (cs.wordProd (ω.eraseIdx j)) < cs.length (cs.wordProd ω)
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : mk mb sb < mk mc sc
⊢ a • mk mb sb < a • mk mc sc

Tactic:
simp_rw [mk_lt_mk] at h

Goal state after:
case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
⊢ a • mk mb sb < a • mk mc sc
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s : ℕ+
⊢ ArchimedeanClass.mk (mk m s) = ArchimedeanClass.mk ↑m

Tactic:
apply archimedeanClassMk_mk_eq

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
H₁ H₂ : Subgroup G
⊢ { toFun := fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker,
          invFun := fun Φ ↦ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker,
          left_inv := ⋯, right_inv := ⋯ }
        H₁ ≤
      { toFun := fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker,
          invFun := fun Φ ↦ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker,
          left_inv := ⋯, right_inv := ⋯ }
        H₂ ↔
    H₁ ≤ H₂

Tactic:
Equiv.coe_fn_mk,

Goal state after:
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
H₁ H₂ : Subgroup G
⊢ OrderDual.toDual (domRestrictHom H₁ Mˣ).ker ≤ OrderDual.toDual (domRestrictHom H₂ Mˣ).ker ↔ H₁ ≤ H₂
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
⊢ ϕ.transfer g = ϕ ⟨g ^ H.index, ⋯⟩

Tactic:
transfer_eq_prod_quotient_orbitRel_zpowers_quot,

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
⊢ ∏ q, ϕ ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x ↦ g • x) q.out * Quotient.out q.out, ⋯⟩ =
    ϕ ⟨g ^ H.index, ⋯⟩
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
N : Subgroup H
f : G →* H
hf : Surjective ⇑f
hf' : f.ker.IsFinitelyNormallyGenerated
S : Set H
hS_fin : S.Finite
hS : normalClosure S = N
⊢ (comap f N).IsFinitelyNormallyGenerated

Tactic:
obtain ⟨T, hT_fin, hT⟩ := hf'

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
N : Subgroup H
f : G →* H
hf : Surjective ⇑f
S : Set H
hS_fin : S.Finite
hS : normalClosure S = N
T : Set G
hT_fin : T.Finite
hT : normalClosure T = f.ker
⊢ (comap f N).IsFinitelyNormallyGenerated
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg
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)
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime (Nat.card (MulAut ↥↑P))

Tactic:
obtain ⟨k, hk⟩ := P.2.exists_card_eq

Goal state after:
case neg
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
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime (Nat.card (MulAut ↥↑P))
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ {g | ∃ g₁ ∈ ⊤, ∃ g₂ ∈ ⊤, ⁅g₁, g₂⁆ = g} ⊆ {g | ∃ x ∈ H, ∃ u, ↑g = ⁅x, u⁆}

Tactic:
rintro - ⟨a, -, b, -, -, rfl⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : ↥H
⊢ ⁅a, b⁆ ∈ {g | ∃ x ∈ H, ∃ u, ↑g = ⁅x, u⁆}
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
a b : α × Bool
⊢ IsCyclicallyReduced (b :: L ++ [a]) ↔ IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)

Tactic:
rw [isCyclicallyReduced_iff, List.getLast?_concat]
  simp

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

Goal state before:
pp: case refine_2
α : 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 (replicate n L₂ ++ [L₂]).flatten

Tactic:
← replicate_succ'

Goal state after:
case refine_2
α : 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 (replicate (n + 1) 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)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)

Tactic:
apply reduce.sound

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)
L₁ L₂ L₃ L₄ L₅ : List (α × Bool)
⊢ mk (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = mk (L₁ ++ (L₂ ++ L₄) ++ L₅)
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: case h₂
α : 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)
this :
  ∀ {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)},
    reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)
⊢ IsReduced (conjugator L ++ reduceCyclically L ++ invRev (conjugator L))

Tactic:
rwa [conj_conjugator_reduceCyclically]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
m : ℕ
g : G
hm : n ≤ m
⊢ 1 ∈ (fun m ↦ H (n - m)) (m + 1)

Tactic:
exact Subgroup.one_mem _

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

Goal state before:
pp: 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.18
inst✝ : Monoid X
f : End (root' T) →* X
a : G
⊢ f (treeHom T a ≫ 𝟙 a ≫ inv (treeHom T a)) = 𝟙 ()

Tactic:
rw [Category.id_comp, IsIso.hom_inv_id, ← End.one_def, f.map_one, id_as_one]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
x y : X
h : ¬Function.onFun Disjoint id (orbit G x) (orbit G y)
⊢ orbit G x = orbit G y

Tactic:
exact (orbit.eq_or_disjoint x y).resolve_right h

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

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M X
B : Set X
s : Set M
hB : IsBlock M B
hs : ¬B ⊆ s • B
⊢ ¬1 • B ⊆ s • B

Tactic:
by simpa using hs

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
⊢ IsBlock G B ↔ ∀ ⦃g : G⦄, (g • B ∩ B).Nonempty → g • B = B

Tactic:
simp_rw [isBlock_iff_disjoint_smul_of_ne, ← not_disjoint_iff_nonempty_inter, not_imp_comm]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)

Tactic:
by
    simp only [this]
    apply (hB.smul_eq_or_disjoint ⟨h, hH⟩).imp
    · intro; congr
    · exact Set.disjoint_image_of_injective (MulAction.injective g)

Goal state after:
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
⊢ Nat.card ↥(toPermHom G (G ⧸ H)).range ∣ (Nat.card (G ⧸ H))!

Tactic:
← Nat.card_perm

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
⊢ Nat.card ↥(toPermHom G (G ⧸ H)).range ∣ Nat.card (Equiv.Perm (G ⧸ H))