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

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
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✝⁵ : 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 g : M → N
x : M
hf : IsSubmersionAt I J n f x
hfg : f =ᶠ[𝓝 x] g
⊢ IsSubmersionAt I J n g x

Tactic:
use hf.complement, by infer_instance, by infer_instance
  exact hf.isSubmersionAtOfComplement_complement.congr_of_eventuallyEq hfg

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

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✝² : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
t : (x : M) → V x
inst✝¹ : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F 1 s u
inst✝ : FiniteDimensional 𝕜 F
h : ∀ (i : ι), MDiff[u] ((LinearMap.piApply (hs.coeff i)) t)
⊢ MDiff[u] (T% t)

Tactic:
by
  rcases u.eq_empty_or_nonempty with rfl | ⟨x, hx⟩; · simp
  have := fintypeOfFiniteDimensional hs hx
  have this (i) : MDiff[u] (T% ((LinearMap.piApply (hs.coeff i)) t • s i)) :=
    (h i).smul_section ((hs.contMDiffOn i).mdifferentiableOn one_ne_zero)
  have almost : MDiff[u] (T% (fun x ↦ ∑ i, hs.coeff i x (t x) • s i x)) :=
    .sum_section (fun i _ _ hx ↦ this i _ hx)
  apply almost.congr
  intro y hy
  simpa using congrArg (TotalSpace.mk' F y) (hs.coeff_sum_eq t hy)

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
inst✝² : ContMDiffVectorBundle 1 F V I
inst✝¹ : IsManifold I 1 M
inst✝ : FiniteDimensional ℝ F
⊢ cov.IsMetricCompatible ↔
    ∀ {x : M} {X : (x : M) → TangentSpace I x} {σ τ : (x : M) → V x},
      MDiffAt (T% X) x →
        MDiffAt (T% σ) x →
          MDiffAt (T% τ) x →
            ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) =
              (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x +
                (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x

Tactic:
by
  refine ⟨fun hcov x X σ τ hX ↦ hcov.mvfderiv_inner_eq X, fun h ↦ ?_⟩
  ext1 x
  apply VectorBundle.injective_eval_mdifferentiableAt_sec I F; ext1 σ; ext1 hσ
  apply VectorBundle.injective_eval_mdifferentiableAt_sec I F; ext1 τ; ext1 hτ
  apply VectorBundle.injective_eval_mdifferentiableAt_sec I E (TangentSpace I); ext X hX
  simp (disch := assumption) [derivMetricTensor_apply]
  linear_combination h hX hσ hτ

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

Goal state before:
pp: case a
𝕜 : 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
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
i : ι
hi : i ∈ s
⊢ f i x • cov i (g • σ) x = g x • f i x • cov i σ x + f i x • (d% g x).smulRight (σ x)

Tactic:
rw [(h i).leibniz hσ hg]

Goal state after:
case a
𝕜 : 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
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
i : ι
hi : i ∈ s
⊢ f i x • (g x • cov i σ x + (d% g x).smulRight (σ x)) = g x • f i x • cov i σ x + f i x • (d% g x).smulRight (σ x)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inl
⊢ orderOf (r 1) = 0

Tactic:
rw [orderOf_eq_zero_iff']
    intro n hn
    rw [r_one_pow, one_def]
    apply mt r.inj
    simpa using hn.ne'

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

Goal state before:
pp: x✝¹ : 0 ≠ 1
x✝ : 0 ≠ 2
h' : IsMulCommutative (DihedralGroup 0)
⊢ False

Tactic:
by simpa using h'.is_comm.comm (r 1) (sr 0)

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : IsFreeGroup G
H : Type u_2
inst✝ : Group H
f : Generators G → H
⊢ ∃! F, ∀ (a : Generators G), F (of a) = f a

Tactic:
by
  simpa only [funext_iff] using! lift.symm.bijective.existsUnique f

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 : B
this : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
⊢ cs.simple i * cs.simple i = 1

Tactic:
have : (PresentedGroup.mk _ (FreeGroup.of i * FreeGroup.of i) : M.Group) = 1 :=
    (QuotientGroup.eq_one_iff _).mpr (Subgroup.subset_normalClosure this)

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
this✝ : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) (FreeGroup.of i * FreeGroup.of i) = 1
⊢ cs.simple i * cs.simple i = 1
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
⊢ (fun f ↦ (Units.coeHom G).comp (cs.groupLift ⋯)) ((fun ι ↦ ⟨⇑ι ∘ cs.simple, ⋯⟩) ι) = ι

Tactic:
by
    apply cs.ext_simple
    intro i
    dsimp only
    rw [groupLift, simple, MonoidHom.comp_apply, MonoidHom.comp_apply, toMonoidHom_apply_symm_apply,
      PresentedGroup.toGroup.of, CoxeterSystem.restrictUnit, Units.coeHom_apply]
    simp only [comp_apply, simple]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

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

Tactic:
exfalso
    simp only [rcons, dif_pos hm, dif_neg hm'] at he
    rw [he] at h
    exact h rfl

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

Goal state before:
pp: case pos
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ (take k (alternatingWord i j (2 * p))).concat (alternatingWord i j (2 * p))[k] = (alternatingWord i j k).concat i

Tactic:
← hk

Goal state after:
case pos
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ (take k (alternatingWord i j (2 * p))).concat (alternatingWord i j (2 * p))[k] =
    (take k (alternatingWord i j (2 * p))).concat i
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
⊢ ⟨i, m⟩ ∈ ((equivPair j) w).tail.toList → ⟨i, m⟩ ∈ w.toList

Tactic:
rw [mem_equivPair_tail_iff]

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
w : Word M
m : M i
⊢ (⟨i, m⟩ ∈ w.toList.tail ∨ i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m⟩) → ⟨i, m⟩ ∈ w.toList
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD (j' + 1) 1 =
    cs.wordProd (take (j' + 1) (i :: ω)) * (Option.map cs.simple (i :: ω)[j' + 1]?).getD 1 *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹

Tactic:
rw [getD_cons_succ]

Goal state after:
case cons.succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.leftInvSeq ω).getD j 1 =
      cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹
j' : ℕ
⊢ (List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω)).getD j' 1 =
    cs.wordProd (take (j' + 1) (i :: ω)) * (Option.map cs.simple (i :: ω)[j' + 1]?).getD 1 *
      (cs.wordProd (take (j' + 1) (i :: ω)))⁻¹
Module: Mathlib.GroupTheory.DivisibleHull

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

Tactic:
have := h.eq_or_lt
  aesop (add simp [qsmul_def, abs_of_pos])

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case inr
ι : 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 : ∃ i, 3 ≤ #(H i)
⊢ (lift f) w.prod ≠ 1

Tactic:
obtain ⟨k, hcard⟩ := hcard

Goal state after:
case inr
ι : 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
k : ι
hcard : 3 ≤ #(H k)
⊢ (lift f) w.prod ≠ 1
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
ma : M
sa : ℕ+
mb : M
sb : ℕ+
h : ↑sb • ma ≤ ↑sa • mb
h' : ↑sa • mb ≤ ↑sb • ma
⊢ mk ma sa = mk mb sb

Tactic:
rw [mk_eq_mk_iff_smul_eq_smul]

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
ma : M
sa : ℕ+
mb : M
sb : ℕ+
h : ↑sb • ma ≤ ↑sa • mb
h' : ↑sa • mb ≤ ↑sb • ma
⊢ ↑sb • ma = ↑sa • mb
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 : ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K ≠ Set.univ
⊢ ⋃ i ∈ t, Quot.mk ⇑(leftRel K) '' doubleCoset (out i) ↑H ↑K ≠ Set.univ

Tactic:
obtain ⟨x, hx⟩ := (Set.ne_univ_iff_exists_notMem _).mp ht

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
t : Finset (Quotient ↑H ↑K)
ht : ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K ≠ Set.univ
x : G
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K
⊢ ⋃ i ∈ t, Quot.mk ⇑(leftRel K) '' doubleCoset (out i) ↑H ↑K ≠ Set.univ
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 : ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K ≠ Set.univ
⊢ ⋃ i ∈ t, Quot.mk ⇑(rightRel H) '' doubleCoset (out i) ↑H ↑K ≠ Set.univ

Tactic:
obtain ⟨x, hx⟩ := (Set.ne_univ_iff_exists_notMem _).mp ht

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
t : Finset (Quotient ↑H ↑K)
ht : ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K ≠ Set.univ
x : G
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K
⊢ ⋃ i ∈ t, Quot.mk ⇑(rightRel H) '' doubleCoset (out i) ↑H ↑K ≠ Set.univ
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pred
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n✝ n : ℤ
hle : n ≤ -1
hi : a i ^ n • (X i)ᶜ ⊆ Y i
⊢ a i ^ (n - 1) • (X i)ᶜ ⊆ Y i

Tactic:
calc
              a i ^ (n - 1) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ := by rw [zpow_sub, zpow_one]
              _ = a i ^ n • (a i)⁻¹ • (X i)ᶜ := mul_smul _ _ _
              _ ⊆ a i ^ n • Y i := smul_set_mono <| hY i
              _ ⊆ a i ^ n • (X i)ᶜ := smul_set_mono (hXYdisj i i).symm.subset_compl_right
              _ ⊆ Y i := hi

Goal state after:
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:
rw [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.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
h : Group.FG ↥N
⊢ N.IsFinitelyNormallyGenerated

Tactic:
obtain ⟨S, rfl, hS⟩ := N.fg_iff.mp ((Group.fg_iff_subgroup_fg N).mp h)
  exact ⟨S, hS, le_antisymm (normalClosure_le_normal subset_closure) closure_le_normalClosure⟩

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case pos
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
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P

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
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P

Tactic:
· have := (Nat.card_eq_one_iff_unique.mp hn).1
    rw [Subsingleton.elim (MonoidHom.transferSylow P (hP.normalizer_le_centralizer rfl)).ker ⊥,
      Subsingleton.elim P.1 ⊤]
    exact isComplement'_bot_top

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
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case neg
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
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : m < n
⊢ ⁅x, g⁆ ∈ (fun m ↦ H (n - m)) (m + 1)

Tactic:
apply hH

Goal state after:
case neg
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
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : m < n
⊢ x ∈ H (n - (m + 1) + 1)
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)
⊢ Surjective ⇑((MonoidHom.snd ↥G' ↥H').comp (P.prod Q))

Tactic:
exact (MonoidHom.snd ..).subgroupMap_surjective I

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)
⊢ ∀ {H : Type u} [inst : Group H] (f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → H),
    ∃! F, ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), F (loopOfHom T (of (↑a).hom)) = f a

Tactic:
intro X _ f
      let f' : Labelling (Generators G) X := fun a b e =>
        if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨⟨a, b, e⟩, h⟩
      rcases unique_lift f' with ⟨F', hF', uF'⟩
      refine ⟨F'.mapEnd _, ?_, ?_⟩
      · suffices ∀ {x y} (q : x ⟶ y), F'.map (loopOfHom T q) = (F'.map q : X) by
          rintro ⟨⟨a, b, e⟩, h⟩
          simp only [Functor.mapEnd, DFunLike.coe, this, hF']
          exact dif_neg h
        intro x y q
        suffices ∀ {a} (p : Path (root T) a), F'.map (homOfPath T p) = 1 by
          simp only [this, treeHom, comp_as_mul, inv_as_inv, loopOfHom, inv_one, mul_one,
            one_mul, Functor.map_inv, Functor.map_comp]
        intro a p
        induction p with
        | nil => rw [homOfPath, F'.map_id, id_as_one]
        | cons p e ih =>
          rw [homOfPath, F'.map_comp, comp_as_mul, ih, mul_one]
          rcases e with ⟨e | e, eT⟩
          · rw [hF']
            exact dif_pos (Or.inl eT)
          · rw [F'.map_inv, inv_as_inv, inv_eq_one, hF']
            exact dif_pos (Or.inr eT)
      · intro E hE
        ext x
        suffices (functorOfMonoidHom T E).map x = F'.map x by
          simpa only [loopOfHom, functorOfMonoidHom, IsIso.inv_id, treeHom_root,
            Category.id_comp, Category.comp_id] using! this
        congr
        apply uF'
        intro a b e
        change E (loopOfHom T _) = dite _ _ _
        split_ifs with h
        · rw [loopOfHom_eq_id T e h, ← End.one_def, E.map_one]
        · exact hE ⟨⟨a, b, e⟩, h⟩

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos.a
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
a b : ℕ
ab : a < b
ha : a ≤ nilpotencyClass G
hb : b ≤ nilpotencyClass G
⊢ upperCentralSeries G a ≤ upperCentralSeries G b

Tactic:
exact upperCentralSeries_mono _ ab.le

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

Goal state before:
pp: G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (symgen b)) * (FreeGroup.of (WeaklyConnectedComponent.mk (symgen a)))⁻¹ = 1

Tactic:
let f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)

Goal state after:
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))
f : G → X := fun g ↦ FreeGroup.of (WeaklyConnectedComponent.mk g)
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (symgen b)) * (FreeGroup.of (WeaklyConnectedComponent.mk (symgen a)))⁻¹ = 1
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ IsBlock G univ

Tactic:
· exact .univ

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
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
⊢ ∀ ⦃g : G⦄, (g • orbit (↥H) a ∩ orbit (↥H) a).Nonempty → g • orbit (↥H) a = orbit (↥H) a

Tactic:
rintro g ⟨-, ⟨-, ⟨h₁, rfl⟩, h⟩, h₂, rfl⟩

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x ↦ g • x) ((fun m ↦ m • a) h₁) = (fun m ↦ m • a) h₂
⊢ g • orbit (↥H) a = orbit (↥H) a
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x ↦ g • x) ((fun m ↦ m • a) h₁) = (fun m ↦ m • a) h₂
⊢ ↑h₂⁻¹ * g * ↑h₁ ∈ H

Tactic:
apply hH

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
g : G
h₁ h₂ : ↥H
h : (fun x ↦ g • x) ((fun m ↦ m • a) h₁) = (fun m ↦ m • a) h₂
⊢ ↑h₂⁻¹ * g * ↑h₁ ∈ stabilizer G a