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

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I m M
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), f x ∈ sphere 0 1
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
h : ContDiffOn ℝ ω (⇑U) Set.univ
⊢ ContMDiffOn I (𝓡 n) m (↑(extChartAt (𝓡 n) v) ∘ Set.codRestrict f (sphere 0 1) hf')
    (Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt (𝓡 n) v).source)

Tactic:
have H₁ := (h.comp_inter contDiffOn_stereoToFun).contMDiffOn

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I m M
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), f x ∈ sphere 0 1
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
h : ContDiffOn ℝ ω (⇑U) Set.univ
H₁ :
  ContMDiffOn 𝓘(ℝ, E) (𝓡 n) ω (⇑U ∘ stereoToFun ↑(-v))
    ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)
⊢ ContMDiffOn I (𝓡 n) m (↑(extChartAt (𝓡 n) v) ∘ Set.codRestrict f (sphere 0 1) hf')
    (Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt (𝓡 n) v).source)
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
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
γ : Path x y
hγ : ContMDiff (𝓡∂ 1) 𝓘(ℝ, F) 1 ⇑γ
e : ℝ → F := ⇑γ ∘ projIcc 0 1 ⋯
D : ContDiffOn ℝ 1 e (Icc 0 1)
| edist x y

Tactic:
edist_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
n : ℕ∞ω
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
γ : Path x y
hγ : ContMDiff (𝓡∂ 1) 𝓘(ℝ, F) 1 ⇑γ
e : ℝ → F := ⇑γ ∘ projIcc 0 1 ⋯
D : ContDiffOn ℝ 1 e (Icc 0 1)
| edist y x
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
H : Type u_7
E : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
x : M
y : E
hy : y ∈ ((chartAt H x).extend I).target
⊢ ↑I.symm y ∈ (chartAt H x).target

Tactic:
by simp_all

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

Goal state before:
pp: 𝕜 : Type u_1
H : Type u_7
E : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
x : M
y : E
hy : y ∈ ((chartAt H x).extend I).target
⊢ y ∈ range ↑I

Tactic:
by simp_all

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

Goal state before:
pp: case hxs
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 ℝ := ⋯
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 := ⋯
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
t' : ℝ
ht' : t' ∈ Icc 0 t₁
⊢ UniqueMDiffAt[Icc 0 t₁] t'

Tactic:
· rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
          exact uniqueDiffOn_Icc h't' _ ht'

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

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
F' : Type u_7
inst✝¹⁸ : NormedAddCommGroup F'
inst✝¹⁷ : NormedSpace 𝕜 F'
V' : M → Type u_8
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'
A : Type u_9
inst✝¹¹ : AddCommGroup A
inst✝¹⁰ : Module 𝕜 A
Φ✝ : ((x : M) → V x) → A
x✝ : M
inst✝⁹ : VectorBundle 𝕜 F V
inst✝⁸ : VectorBundle 𝕜 F' V'
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : FiniteDimensional 𝕜 F
inst✝⁵ : FiniteDimensional 𝕜 F'
inst✝⁴ : ContMDiffVectorBundle 1 F V I
inst✝³ : ContMDiffVectorBundle 1 F' V' I
inst✝² : TopologicalSpace A
inst✝¹ : IsTopologicalAddGroup A
inst✝ : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → ((x : M) → V' x) → A
x : M
hΦ₁ : ∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun x ↦ Φ x τ) x
hΦ₂ : ∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (Φ σ) x
this✝⁶ : T2Space (V x)
this✝⁵ : FiniteDimensional 𝕜 (V x)
this✝⁴ : T2Space (V' x)
this✝³ : FiniteDimensional 𝕜 (V' x)
this✝² : IsTopologicalAddGroup (V x)
this✝¹ : IsTopologicalAddGroup (V' x)
this✝ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
this : ∀ (x : M), ContinuousSMul 𝕜 (V' x)
v₁ v₂ : V x
w : V' x
⊢ Φ (extend F (v₁ + v₂)) (extend F' w) = Φ (extend F v₁) (extend F' w) + Φ (extend F v₂) (extend F' w)

Tactic:
by
      rw [← (hΦ₁ _ (mdifferentiableAt_extend ..)).add (mdifferentiableAt_extend ..)
        (mdifferentiableAt_extend ..)]
      apply TensorialAt.pointwise₂ hΦ₁ hΦ₂ (mdifferentiableAt_extend ..) _
        (mdifferentiableAt_extend ..) (mdifferentiableAt_extend ..) _ rfl
      · exact mdifferentiableAt_add_section (mdifferentiableAt_extend ..)
          (mdifferentiableAt_extend ..)
      · simp

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

Goal state before:
pp: case e_f
𝕜 : 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
x✝¹ : M
hσ : MDiffAt (T% σ✝) x✝¹
hσ' : MDiffAt (T% σ'✝) x✝¹
hx : x✝¹ ∈ u
i : ι
x✝ : TangentSpace I x✝¹
⊢ (f i x✝¹ • cov i (σ✝ + σ'✝) x✝¹) x✝ = (f i x✝¹ • (cov i σ✝ x✝¹ + cov i σ'✝ x✝¹)) x✝

Tactic:
(h i).add hσ hσ' hx

Goal state after:
case e_f
𝕜 : 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
x✝¹ : M
hσ : MDiffAt (T% σ✝) x✝¹
hσ' : MDiffAt (T% σ'✝) x✝¹
hx : x✝¹ ∈ u
i : ι
x✝ : TangentSpace I x✝¹
⊢ (f i x✝¹ • (cov i σ✝ x✝¹ + cov i σ'✝ x✝¹)) x✝ = (f i x✝¹ • (cov i σ✝ x✝¹ + cov i σ'✝ x✝¹)) x✝
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: case h₁
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ map (MonoidHom.mulSingle Gs i) (H i) ≤ pi Set.univ H

Tactic:
· rw [le_pi_iff]
        intro j _hj
        rintro _ ⟨x, hx, rfl⟩
        by_cases h : j = i
        · subst h
          simpa using hx
        · simp [h, one_mem]

Goal state after:
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: case h₂
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ map (MonoidHom.mulSingle Gs i) (K i) ≤ pi Set.univ K

Tactic:
· rw [le_pi_iff]
        intro j _hj
        rintro _ ⟨x, hx, rfl⟩
        by_cases h : j = i
        · subst h
          simpa using hx
        · simp [h, one_mem]

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

Goal state before:
pp: case neg
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
univ₂ : {e (x * y), e x, e y, 1} = univ
⊢ e (x * y) = e x * e y

Tactic:
← e.injective.ne_iff

Goal state after:
case neg
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 : e x ≠ e 1
hy : e y ≠ e 1
hxy : e x ≠ e y
univ₂ : {e (x * y), e x, e y, 1} = univ
⊢ e (x * y) = e x * e y
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:
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
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 (restrictUnit ⋯ i) = ↑f i

Tactic:
OneHom.toFun_eq_coe,

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) (restrictUnit ⋯ i) = ↑f i
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case case1
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ [⟨i✝, x✝⟩].head? = some ⟨i✝, (singleton x✝ a✝).head⟩

Tactic:
grind [head]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case case2
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j x✝¹ x✝ j✝ k✝ : ι
w₁✝ : NeWord M x✝¹ j✝
_hne✝ : j✝ ≠ k✝
w₂✝ : NeWord M k✝ x✝
ih2✝ : w₁✝.toList.head? = some ⟨x✝¹, w₁✝.head⟩
ih1✝ : w₂✝.toList.head? = some ⟨k✝, w₂✝.head⟩
⊢ (w₁✝.toList ++ w₂✝.toList).head? = some ⟨x✝¹, (w₁✝.append _hne✝ w₂✝).head⟩

Tactic:
grind [head]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
x : M i✝
hnotone : x * (singleton x✝ a✝).head ≠ 1
⊢ (replaceHead (x * (singleton x✝ a✝).head) hnotone (singleton x✝ a✝)).prod = of x * (singleton x✝ a✝).prod

Tactic:
simp [replaceHead]

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

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k + 1 < (cs.leftInvSeq (alternatingWord i j (2 * p))).length

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a b : M
h : a ≤ b
⊢ (↑(coeAddMonoidHom M)).toFun a ≤ (↑(coeAddMonoidHom M)).toFun b

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
b : DivisibleHull M
num✝ : M
den✝ : ℕ+
h : ArchimedeanClass.mk (mk num✝ den✝) ≤ ArchimedeanClass.mk b
⊢ (mk num✝ den✝).liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯ ≤ b.liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯

Tactic:
induction b with | mk _ _

Goal state after:
case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
num✝¹ : M
den✝¹ : ℕ+
num✝ : M
den✝ : ℕ+
h : ArchimedeanClass.mk (mk num✝¹ den✝¹) ≤ ArchimedeanClass.mk (mk num✝ den✝)
⊢ (mk num✝¹ den✝¹).liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯ ≤
    (mk num✝ den✝).liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s : ℕ+
this : ArchimedeanClass.mk (mk m 1) = ArchimedeanClass.mk (mk m s)
⊢ ((archimedeanClassOrderHom M).comp (archimedeanClassOrderHomInv M)) (ArchimedeanClass.mk (mk m s)) =
    OrderHom.id (ArchimedeanClass.mk (mk m s))

Tactic:
by
      simpa [archimedeanClassOrderHom, archimedeanClassOrderHomInv]

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: 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)
⊢ ↑(closure ((fun g ↦ g * (↑(hR.toRightFun g))⁻¹) '' (R * S))) * R = ⊤

Tactic:
change (closure U : Set G) * R = ⊤

Goal state after:
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)
⊢ ↑(closure U) * R = ⊤
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 : (⇑φ)^[2] = _root_.id
⊢ ⇑φ = fun x ↦ x⁻¹

Tactic:
by
  ext g
  have key : g * φ g = 1 := by simpa [List.range_succ] using hφ.prod_pow_eq_one h2 g
  rwa [← inv_eq_iff_mul_eq_one, eq_comm] at key

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ map H.subtype (_root_.commutator ↥H) ≤ H.focalSubgroup

Tactic:
H.commutator_le_focalSubgroupOf,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ map H.subtype H.focalSubgroupOf ≤ H.focalSubgroup
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅H, H⁆ ≤ H.focalSubgroup

Tactic:
grw [← map_subtype_commutator, H.commutator_le_focalSubgroupOf, map_focalSubgroupOf]

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
eq : 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:
reduceCyclically.cons_append,

Goal state after:
α : Type u
inst✝ : DecidableEq α
a : α × Bool
l : List (α × Bool)
b : α × Bool
eq : conjugator l ++ reduceCyclically l ++ invRev (conjugator l) = l
⊢ (conjugator (a :: (l ++ [b])) ++ if b.1 = a.1 ∧ (!b.2) = a.2 then reduceCyclically l else a :: l ++ [b]) ++
      invRev (conjugator (a :: (l ++ [b]))) =
    a :: (l ++ [b])
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
X✝ Y✝ Z✝ : G
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ f (loopOfHom T (f✝ ≫ g✝)) = f (loopOfHom T f✝) ≫ f (loopOfHom T g✝)

Tactic:
comp_as_mul,

Goal state after:
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
X✝ Y✝ Z✝ : G
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ f (loopOfHom T (f✝ ≫ g✝)) = f (loopOfHom T g✝) * f (loopOfHom T f✝)
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

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

Tactic:
comp_as_mul,

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

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

Tactic:
← pi_top (I := Set.univ),

Goal state after:
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
n : ℕ
⊢ (pi Set.univ fun i ↦ ⊤).lowerCentralSeries n = pi Set.univ fun i ↦ ⊤.lowerCentralSeries n
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
this : B.ncard < 2
⊢ B.Subsingleton

Tactic:
by simp_all

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
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

Tactic:
let B' := ⋂ (k : G) (_ : a ∈ k • B), k • B
  rcases Set.eq_empty_or_nonempty B with hfB_e | hfB_ne
  · simp [hfB_e]
  have hB'₀ : ∀ (k : G) (_ : a ∈ k • B), B' ≤ k • B := by
    intro k hk
    exact Set.biInter_subset_of_mem hk
  have hfB' : B'.Finite := by
    obtain ⟨b, hb : b ∈ B⟩ := hfB_ne
    obtain ⟨k, hk : k • b = a⟩ := exists_smul_eq G b a
    apply Set.Finite.subset (Set.Finite.map _ hfB) (hB'₀ k ⟨b, hb, hk⟩)
  have hag : ∀ g : G, a ∈ g • B' → B' ≤ g • B' := by
    intro g hg x hx
    -- a = g • b; b ∈ B'; a ∈ k • B → b ∈ k • B
    simp only [B', Set.mem_iInter, Set.mem_smul_set_iff_inv_smul_mem,
      smul_smul, ← mul_inv_rev] at hg hx ⊢
    exact fun _ ↦ hx _ ∘ hg _
  have hag' (g : G) (hg : a ∈ g • B') : B' = g • B' := by
    rw [eq_comm, ← mem_stabilizer_iff, mem_stabilizer_set_iff_subset_smul_set hfB']
    exact hag g hg
  rw [isBlock_iff_smul_eq_of_nonempty]
  rintro g ⟨b : X, hb' : b ∈ g • B', hb : b ∈ B'⟩
  obtain ⟨k : G, hk : k • a = b⟩ := exists_smul_eq G a b
  have hak : a ∈ k⁻¹ • B' := by
    refine ⟨b, hb, ?_⟩
    simp only [← hk, inv_smul_smul]
  have hagk : a ∈ (k⁻¹ * g) • B' := by
    rw [mul_smul, Set.mem_smul_set_iff_inv_smul_mem, inv_inv, hk]
    exact hb'
  have hkB' : B' = k⁻¹ • B' := hag' k⁻¹ hak
  have hgkB' : B' = (k⁻¹ * g) • B' := hag' (k⁻¹ * g) hagk
  rw [mul_smul] at hgkB'
  rw [← smul_eq_iff_eq_inv_smul] at hkB' hgkB'
  rw [← hgkB', hkB']

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
⊢ ∃ g y, g • x = ofStabilizer.snoc y

Tactic:
by
  obtain ⟨g, hgx⟩ := exists_smul_eq G (x (Fin.last n)) a
  have H : ∀ i, Fin.Embedding.init (g • x) i ∈ ofStabilizer G a := fun i ↦ by
    simp only [mem_ofStabilizer_iff,
      Nat.succ_eq_add_one, ← hgx, ← smul_apply, ne_eq]
    suffices Fin.Embedding.init (g • x) i = (g • x) i.castSucc by
      simp [this]
    simp [Fin.Embedding.init, Fin.init_def]
  use g, (Fin.Embedding.init (g • x)).codRestrict (ofStabilizer G a) H
  ext i
  rcases Fin.eq_castSucc_or_eq_last i with ⟨i, rfl⟩ | ⟨rfl⟩
  · simpa [ofStabilizer.snoc] using!
      Subtype.ext_iff.mp <| Function.Embedding.codRestrict_apply _ _ H i
  · simpa only [smul_apply, ofStabilizer.snoc, Fin.Embedding.snoc_last]

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
g : G
hg : a ∈ g • A
this : A = g⁻¹ • Set.univ
⊢ A = Set.univ

Tactic:
rw [this, Set.smul_set_univ]

Goal state after: