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
inst✝ : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC✝ : ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst✝⁵] u
us : u ⊆ s
hu : u ⊆ {y | ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (chartAt H x).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst✝⁵] v
r : ℝ≥0
hr : ball (↑(extChartAt I x) x) ↑r ⊆ ↑(extChartAt I x).symm ⁻¹' v
r_pos : 0 < r
y : M
hy : y ∈ {y | riemannianEDist I x y < ↑(r / C)}
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < ↑(r / C)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := ↑(extChartAt I x) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
⊢ ∫⁻ (t' : ℝ) in Icc 0 t₁, ‖(fderivWithin ℝ γ' (Icc 0 t₁) t') 1‖ₑ =
    ∫⁻ (t' : ℝ) in Icc 0 t₁, ‖(mfderiv[Icc 0 t₁] γ' t') 1‖ₑ

Tactic:
mfderivWithin_eq_fderivWithin

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
inst✝ : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC✝ : ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst✝⁵] u
us : u ⊆ s
hu : u ⊆ {y | ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (chartAt H x).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst✝⁵] v
r : ℝ≥0
hr : ball (↑(extChartAt I x) x) ↑r ⊆ ↑(extChartAt I x).symm ⁻¹' v
r_pos : 0 < r
y : M
hy : y ∈ {y | riemannianEDist I x y < ↑(r / C)}
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < ↑(r / C)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := ↑(extChartAt I x) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
⊢ ∫⁻ (t' : ℝ) in Icc 0 t₁, ‖(fderivWithin ℝ γ' (Icc 0 t₁) t') 1‖ₑ =
    ∫⁻ (t' : ℝ) in Icc 0 t₁, ‖(fderivWithin ℝ γ' (Icc 0 t₁) t') 1‖ₑ
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
n : ℕ∞ω
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
inst✝² : VectorBundle 𝕜 F V
inst✝¹ : ContMDiffVectorBundle n F V I
ι : Type u_7
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
b : Basis ι 𝕜 F
i : ι
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, e.localFrame b i x⟩) e.baseSet

Tactic:
rw [e.contMDiffOn_section_baseSet_iff]
  apply (contMDiffOn_const (c := b i)).congr
  intro y hy
  simp [hy, basisAt]

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
inst✝⁵ : VectorBundle 𝕜 F V
inst✝⁴ : ContMDiffVectorBundle 1 F V I
e : Trivialization F TotalSpace.proj
inst✝³ : MemTrivializationAtlas e
ι : Type u_7
b : Basis ι 𝕜 F
s : (x : M) → V x
k : ℕ∞ω
x : M
inst✝² : FiniteDimensional 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : ContMDiffVectorBundle k F V I
hxe : x ∈ e.baseSet
hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) k (fun x ↦ ⟨x, s x⟩) x
i : ι
aux : M → 𝕜 := fun x ↦ (b.repr (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) i
h₁ : ContMDiffAt I 𝓘(𝕜, F) k (fun x ↦ (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) x
breprl : F →ₗ[𝕜] 𝕜 := { toFun := fun v ↦ (b.repr v) i, map_add' := ⋯, map_smul' := ⋯ }
⊢ ContDiffAt 𝕜 k (⇑(LinearMap.toContinuousLinearMap breprl)) (↑e ((fun x ↦ ⟨x, s x⟩) x)).2

Tactic:
by fun_prop

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
inst✝⁴ : VectorBundle 𝕜 F V
inst✝³ : ContMDiffVectorBundle 1 F V I
e : Trivialization F TotalSpace.proj
inst✝² : MemTrivializationAtlas e
ι : Type u_7
b : Basis ι 𝕜 F
s : (x : M) → V x
x : M
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : CompleteSpace 𝕜
hxe : x ∈ e.baseSet
hs : MDiffAt (T% s) x
i : ι
aux : M → 𝕜 := fun x ↦ (b.repr (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) i
h₁ : (MDiffAt fun x ↦ (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) x
breprl : F →ₗ[𝕜] 𝕜 := { toFun := fun v ↦ (b.repr v) i, map_add' := ⋯, map_smul' := ⋯ }
⊢ DifferentiableAt 𝕜 (⇑(LinearMap.toContinuousLinearMap breprl)) (↑e ((fun x ↦ ⟨x, s x⟩) x)).2

Tactic:
by fun_prop

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:
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.GroupTheory.ClassEquation

Goal state before:
pp: case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑x.carrier =
    ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier +
      ∑ x ∈ (noncenter G).toFinset, Fintype.card ↑x.carrier

Tactic:
congr 1

Goal state after:
case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card ↥(Subgroup.center G) = ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier

case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑x.carrier =
    ∑ x ∈ (noncenter G).toFinset, Fintype.card ↑x.carrier
Module: Mathlib.GroupTheory.GroupAction.CardCommute

Goal state before:
pp: G : Type u_3
inst✝ : Group G
val✝ : Fintype G
⊢ card (Quotient (MulAction.orbitRel (ConjAct G) G)) * card (ConjAct G) = card (ConjClasses G) * card G

Tactic:
congr 1

Goal state after:
case e_a
G : Type u_3
inst✝ : Group G
val✝ : Fintype G
⊢ card (Quotient (MulAction.orbitRel (ConjAct G) G)) = card (ConjClasses G)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ commProb (DihedralGroup (n % 4 * n)) * (1 / ↑(n / 4 + 1)) = 1 / ↑n

Tactic:
commProb_odd (hn.mul h2),

Goal state after:
case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ (↑(n % 4 * n) + 3) / (4 * ↑(n % 4 * n)) * (1 / ↑(n / 4 + 1)) = 1 / ↑n
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: case one
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
motive : M ∗ N → Prop
one : motive 1
inl_mul : ∀ (m : M) (x : M ∗ N), motive x → motive (inl m * x)
inr_mul : ∀ (n : N) (x : M ∗ N), motive x → motive (inr n * x)
⊢ motive (mk 1)

Tactic:
| one =>

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

Goal state before:
pp: case one
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
⊢ mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList 1)).reverse) * mk 1 = 1

Tactic:
| one =>

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

Goal state before:
pp: case one
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x ↦ p w
⊢ p 1

Tactic:
| one =>

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

Goal state before:
pp: case one
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x ↦ p w
⊢ p 1

Tactic:
| one =>

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case one
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
one : motive 1
mul : ∀ {i : ι} (m : M i) (x : CoprodI M), motive x → motive (of m * x)
⊢ motive 1

Tactic:
| one =>

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case one
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
N : Type u_3
inst✝¹ : Monoid N
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
⊢ MulOpposite.unop ((lift fun i ↦ (MonoidHom.op of).comp (MulEquiv.inv' (G i)).toMonoidHom) 1) * 1 = 1

Tactic:
| one =>

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case one
ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
s : Subgroup N
h : ∀ (i : ι), (f i).range ≤ s
⊢ (lift f) 1 ∈ s

Tactic:
| one =>

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
⊢ cs.wordProd [] = 1

Tactic:
by simp [wordProd]

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
ω : List B
⊢ cs.wordProd (i :: ω) = cs.simple i * cs.wordProd ω

Tactic:
by simp [wordProd]

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
⊢ cs.wordProd [i] = cs.simple i

Tactic:
by simp [wordProd]

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
ω : List B
⊢ cs.wordProd (ω.concat i) = cs.wordProd ω * cs.simple i

Tactic:
by simp [wordProd]

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
ω ω' : List B
⊢ cs.wordProd (ω ++ ω') = cs.wordProd ω * cs.wordProd ω'

Tactic:
by simp [wordProd]

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

Goal state before:
pp: case neg
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : ¬Even (p + k)
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i

Tactic:
rw [if_neg h_even, ← add_assoc]

Goal state after:
case neg
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : ¬Even (p + k)
⊢ (if Even (p + k + 1) then i else j) = i
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ ¬cs.length (w * cs.simple i) < cs.length w → cs.length (w * cs.simple i) = cs.length w + 1

pp: case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) = cs.length w + 1 → ¬cs.length (w * cs.simple i) < cs.length w

Tactic:
· intro _
    exact (cs.length_mul_simple w i).resolve_right (by lia)

Goal state after:
case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) = cs.length w + 1 → ¬cs.length (w * cs.simple i) < cs.length w
Module: Mathlib.GroupTheory.CoprodI

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

Tactic:
| one =>

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
w_ih_w₂ : ∀ (x : M k✝) (hnotone : x * _w₂✝.head ≠ 1), (replaceHead (x * _w₂✝.head) hnotone _w₂✝).prod = of x * _w₂✝.prod
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
w_ih_w₁ : (replaceHead (x * _w₁✝.head) hnotone _w₁✝).prod = of x * _w₁✝.prod
⊢ (replaceHead (x * (_w₁✝.append _hne✝ _w₂✝).head) hnotone _w₁✝).prod * _w₂✝.prod = of x * _w₁✝.prod * _w₂✝.prod

Tactic:
congr 1

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ x ∈ ⋃ k, op (a * ↑k) • ↑H ↔ x ∈ doubleCoset a ↑H ↑K

Tactic:
simp only [mem_rightCoset_iff, mul_inv_rev, Set.mem_iUnion, mem_doubleCoset,
    SetLike.mem_coe]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H) ↔ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.refine_2
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : 0 < mk m s
⊢ 0 < m

Tactic:
← mk_zero 1,

Goal state after:
case mk.refine_2
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : mk 0 1 < mk m s
⊢ 0 < m
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := hR.toRightFun
U : Set G := (fun g ↦ g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
⊢ ∀ x ∈ closure S, ∀ y ∈ S, x ∈ ↑(closure U) * R → x * y ∈ ↑(closure U) * R

Tactic:
rintro - - s hs ⟨u, hu, r, hr, rfl⟩
    rw [show u * r * s = u * (r * s * (f (r * s) : G)⁻¹) * f (r * s) by group]
    refine Set.mul_mem_mul ((closure U).mul_mem hu ?_) (f (r * s)).coe_prop
    exact subset_closure ⟨r * s, Set.mul_mem_mul hr hs, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
N : Subgroup G
hN : N.IsFinitelyNormallyGenerated
f : G →* H
hf : Function.Surjective ⇑f
⊢ (map f N).IsFinitelyNormallyGenerated

Tactic:
by
  obtain ⟨S, hSfinite, hSclosure⟩ := hN
  refine ⟨f '' S, hSfinite.image _, ?_⟩
  rw [← hSclosure, Subgroup.map_normalClosure _ _ hf]

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
T : H.LeftTransversal
inst✝ : (center G).FiniteIndex
a b : G
⊢ ⟨(a * b) ^ (center G).index, ⋯⟩ = ⟨a ^ (center G).index, ⋯⟩ * ⟨b ^ (center G).index, ⋯⟩

Tactic:
← show ∀ _, (_ : center G) = _ from transfer_center_eq_pow,

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
T : H.LeftTransversal
inst✝ : (center G).FiniteIndex
a b : G
⊢ (id ↥(center G)).transfer (a * b) = (id ↥(center G)).transfer a * (id ↥(center G)).transfer b
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: case one
G : Type u_1
inst✝ : Group G
H : Subgroup G
n g : G
hg : g ∈ H
⊢ g * 1 * g⁻¹ ∈ H.focalSubgroup

Tactic:
| one =>

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ map H.subtype H.focalSubgroupOf = map H.subtype (closure {g | ∃ x ∈ H, ∃ u, ↑g = ⁅x, u⁆})

Tactic:
map_focalSubgroupOf,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.focalSubgroup = map H.subtype (closure {g | ∃ x ∈ H, ∃ u, ↑g = ⁅x, u⁆})
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
inst✝ : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
ih : IsReduced l → IsCyclicallyReduced (reduceCyclically l)
h : IsReduced (a :: (l ++ [b]))
h' : ¬(b.1 = a.1 ∧ (!b.2) = a.2)
⊢ b.1 = a.1 → b.2 = a.2

Tactic:
by simpa using h'

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ
⊢ {g | ∃ g₁ ∈ upperCentralSeries G (n + 1), ∃ g₂ ∈ ⊤, ⁅g₁, g₂⁆ = g} ⊆ ↑(upperCentralSeries G n)

Tactic:
rintro _ ⟨h, hh, g, _, rfl⟩

Goal state after:
G : Type u_1
inst✝ : Group G
n : ℕ
h : G
hh : h ∈ upperCentralSeries G (n + 1)
g : G
left✝ : g ∈ ⊤
⊢ ⁅h, g⁆ ∈ ↑(upperCentralSeries G n)
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)
this :
  ∀ {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)},
    reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)
⊢ reduce (conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)) =
    conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L)

Tactic:
← isReduced_iff_reduce_eq

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)
this :
  ∀ {L₁ L₂ L₃ L₄ L₅ : List (α × Bool)},
    reduce (L₁ ++ L₂ ++ invRev L₃ ++ (L₃ ++ L₄ ++ L₅)) = reduce (L₁ ++ (L₂ ++ L₄) ++ L₅)
⊢ IsReduced (conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L))
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)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
x y : G × H
hx : x ∈ I
hy : y ∈ I
⊢ ↑x.1 = ↑y.1 ↔ ↑x.2 = ↑y.2

Tactic:
have := normal_goursatFst hI₁

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
x y : G × H
hx : x ∈ I
hy : y ∈ I
this : I.goursatFst.Normal
⊢ ↑x.1 = ↑y.1 ↔ ↑x.2 = ↑y.2
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)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
⊢ have this := ⋯;
  have this_1 := ⋯;
  ∃ e,
    (((QuotientGroup.mk' I.goursatFst).prodMap (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).range =
      e.toMonoidHom.graph

Tactic:
have := normal_goursatFst hI₁

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
this : I.goursatFst.Normal
⊢ have this := ⋯;
  have this_1 := ⋯;
  ∃ e,
    (((QuotientGroup.mk' I.goursatFst).prodMap (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).range =
      e.toMonoidHom.graph
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G n.succ
Hn : Subgroup (G ⧸ center G) := upperCentralSeries (G ⧸ center G) n
⊢ comap (mk' (center G)) Hn.upperCentralSeriesStep =
    comap (mk' (center G)) (comap (mk' Hn) (center ((G ⧸ center G) ⧸ Hn)))

Tactic:
upperCentralSeriesStep_eq_comap_center

Goal state after:
G : Type u_1
inst✝ : Group G
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G n.succ
Hn : Subgroup (G ⧸ center G) := upperCentralSeries (G ⧸ center G) n
⊢ comap (mk' (center G)) (comap (mk' Hn) (center ((G ⧸ center G) ⧸ Hn))) =
    comap (mk' (center G)) (comap (mk' Hn) (center ((G ⧸ center G) ⧸ Hn)))
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : ℕ
ab : a < b
hn : upperCentralSeries G a = upperCentralSeries G b
⊢ nilpotencyClass G ≤ a

Tactic:
by_cases hG : IsNilpotent G
  · grind only [IsNilpotent.nilpotent', IsNilpotent.nilpotent, upperCentralSeries.eq_top,
      upperCentralSeries_eq_top_iff_nilpotencyClass_le]
  · rw [nilpotencyClass_of_not_nilpotent hG]
    apply Nat.zero_le

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
Ss : (i : η) → Subgroup (Gs i)
n : ℕ
⊢ (pi Set.univ Ss).lowerCentralSeries n ≤ pi Set.univ fun i ↦ (Ss i).lowerCentralSeries n

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    simp_rw [lowerCentralSeries_succ]
    grw [commutator_mono ih le_rfl, commutator_pi_pi_le]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
n : ℕ
⊢ (pi Set.univ fun i ↦ ⊤).lowerCentralSeries n ≤ pi Set.univ fun i ↦ ⊤.lowerCentralSeries n

Tactic:
exact lowerCentralSeries_pi_le _ _

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Embedding

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : ↑s.ncard + ↑n ≤ ENat.card α
hα : Finite α
x✝ : Fintype α := Fintype.ofFinite α
⊢ s.ncard + n ≤ s.ncard + sᶜ.ncard

Tactic:
ncard_add_ncard_compl,

Goal state after:
case inl
α : Type u_1
n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : ↑s.ncard + ↑n ≤ ENat.card α
hα : Finite α
x✝ : Fintype α := Fintype.ofFinite α
⊢ s.ncard + n ≤ Nat.card α