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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
n : ℕ∞ω
⊢ ∀ x ∈ {x | ((innerSL ℝ) v) x ≠ 1}, 1 - ((innerSL ℝ) v) x ≠ 0

Tactic:
intro x h h'

Goal state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
n : ℕ∞ω
x : E
h : x ∈ {x | ((innerSL ℝ) v) x ≠ 1}
h' : 1 - ((innerSL ℝ) v) x = 0
⊢ False
Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
a : ℝ
ha : a ≠ 0
⊢ IsMIntegralCurveOn (γ ∘ fun x ↦ x * a) (a • v) {t | t * a ∈ s} ↔ IsMIntegralCurveOn γ v s

Tactic:
by
  refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul a⟩
  convert! hγ.comp_mul a⁻¹
  · ext t
    simp only [Function.comp_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one]
  · simp only [smul_smul, inv_mul_eq_div, div_self ha, one_smul]
  · simp only [mem_ofPred_eq, mul_assoc, inv_mul_eq_div, div_self ha, mul_one, ofPred_mem_eq]

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: case e'_3.hs
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (ℝ ∙ ↑(-v))ᗮ.subtypeL (U.symm 0)
⊢ ↑v ∈ ℝ ∙ -↑v

Tactic:
← Submodule.neg_mem_iff

Goal state after:
case e'_3.hs
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (ℝ ∙ ↑(-v))ᗮ.subtypeL (U.symm 0)
⊢ -↑v ∈ ℝ ∙ -↑v
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

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✝¹ : IsManifold I 1 M
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst✝ : CompleteSpace E
hx : I.IsInteriorPoint x₀
left✝ : ContinuousAt (fun x ↦ ⟨x, v x⟩) x₀
hv :
  ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (range ↑I)
    (↑(extChartAt I x₀) x₀)
f : ℝ → E
hf1 : f t₀ = ↑(extChartAt I x₀) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y
hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀
hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'
s : Set ℝ
hs : s ∈ 𝓝 t₀
haux :
  ∀ y ∈ s,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y ∧
      f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y
t : ℝ
ht : t ∈ s
xₜ : M := ↑(extChartAt I x₀).symm (f t)
h :
  HasDerivAt f
    ((fderivWithin ℝ (↑(extChartAt I x₀) ∘ ↑(extChartAt I xₜ).symm) (range ↑I) (↑(extChartAt I xₜ) xₜ)) (v xₜ)) t
⊢ HasMFDerivAt[s] (↑(extChartAt I x₀).symm ∘ f) t
    (ContinuousLinearMap.smulRight 1 (v ((↑(extChartAt I x₀).symm ∘ f) t)))

Tactic:
rw [← tangentCoordChange_def] at h

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✝¹ : IsManifold I 1 M
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst✝ : CompleteSpace E
hx : I.IsInteriorPoint x₀
left✝ : ContinuousAt (fun x ↦ ⟨x, v x⟩) x₀
hv :
  ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (range ↑I)
    (↑(extChartAt I x₀) x₀)
f : ℝ → E
hf1 : f t₀ = ↑(extChartAt I x₀) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y
hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀
hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'
s : Set ℝ
hs : s ∈ 𝓝 t₀
haux :
  ∀ y ∈ s,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y ∧
      f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y
t : ℝ
ht : t ∈ s
xₜ : M := ↑(extChartAt I x₀).symm (f t)
h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ)) t
⊢ HasMFDerivAt[s] (↑(extChartAt I x₀).symm ∘ f) t
    (ContinuousLinearMap.smulRight 1 (v ((↑(extChartAt I x₀).symm ∘ f) t)))
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

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✝ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hv : ContMDiffAt I I.tangent 1 (fun x ↦ ⟨x, v x⟩) (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
⊢ γ =ᶠ[𝓝 t₀] γ'

Tactic:
by
  -- first define `v'` as the vector field expressed in the local chart around `γ t₀`
  -- this is basically what the function looks like when `hv` is unfolded
  set v' : E → E := fun x ↦
    tangentCoordChange I ((extChartAt I (γ t₀)).symm x) (γ t₀) ((extChartAt I (γ t₀)).symm x)
      (v ((extChartAt I (γ t₀)).symm x)) with hv'
  -- extract a set `s` on which `v'` is Lipschitz
  rw [contMDiffAt_iff] at hv
  obtain ⟨_, hv⟩ := hv
  obtain ⟨K, s, hs, hlip⟩ : ∃ K, ∃ s ∈ 𝓝 _, LipschitzOnWith K v' s :=
    (hv.contDiffAt (range_mem_nhds_isInteriorPoint hγt₀)).snd.exists_lipschitzOnWith
  have hlip (t : ℝ) : LipschitzOnWith K ((fun _ ↦ v') t) ((fun _ ↦ s) t) := hlip
  -- internal lemmas to reduce code duplication
  have hsrc {g} (hg : IsMIntegralCurveAt g v t₀) :
    ∀ᶠ t in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t := eventually_mem_nhds_iff.mpr <|
      continuousAt_def.mp hg.continuousAt _ <| extChartAt_source_mem_nhds (g t₀)
  have hmem {g : ℝ → M} {t} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t) :
    g t ∈ (extChartAt I (g t₀)).source := mem_preimage.mp <| mem_of_mem_nhds ht
  have hdrv {g} (hg : IsMIntegralCurveAt g v t₀) (h' : γ t₀ = g t₀) : ∀ᶠ t in 𝓝 t₀,
      HasDerivAt ((extChartAt I (g t₀)) ∘ g) ((fun _ ↦ v') t (((extChartAt I (g t₀)) ∘ g) t)) t ∧
      ((extChartAt I (g t₀)) ∘ g) t ∈ (fun _ ↦ s) t := by
    apply Filter.Eventually.and
    · apply (hsrc hg |>.and hg.eventually_hasDerivAt).mono
      rintro t ⟨ht1, ht2⟩
      rw [hv', h']
      apply ht2.congr_deriv
      congr <;>
      rw [Function.comp_apply, PartialEquiv.left_inv _ (hmem ht1)]
    · apply ((continuousAt_extChartAt (g t₀)).comp hg.continuousAt).preimage_mem_nhds
      rw [Function.comp_apply, ← h']
      exact hs
  have heq {g} (hg : IsMIntegralCurveAt g v t₀) :
    g =ᶠ[𝓝 t₀] (extChartAt I (g t₀)).symm ∘ ↑(extChartAt I (g t₀)) ∘ g := by
    apply (hsrc hg).mono
    intro t ht
    rw [Function.comp_apply, Function.comp_apply, PartialEquiv.left_inv _ (hmem ht)]
  -- main proof
  suffices (extChartAt I (γ t₀)) ∘ γ =ᶠ[𝓝 t₀] (extChartAt I (γ' t₀)) ∘ γ' from
    (heq hγ).trans <| (this.fun_comp (extChartAt I (γ t₀)).symm).trans (h ▸ (heq hγ').symm)
  exact ODE_solution_unique_of_eventually (.of_forall hlip)
    (hdrv hγ rfl) (hdrv hγ' h) (by rw [Function.comp_apply, Function.comp_apply, h])

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

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✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t | γ t = γ' t} ∩ Ioo a b
hs : s = {t | γ t = γ' t} ∩ Ioo a b
t₁ : ℝ
ht₁ : t₁ ∈ s
hmem : Ioo a b ∈ 𝓝 t₁
⊢ s ∈ 𝓝 t₁

Tactic:
have heq : γ =ᶠ[𝓝 t₁] γ' := isMIntegralCurveAt_eventuallyEq_of_contMDiffAt
      (hγt _ ht₁.2) hv.contMDiffAt (hγ.isMIntegralCurveAt hmem) (hγ'.isMIntegralCurveAt hmem) ht₁.1

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✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t | γ t = γ' t} ∩ Ioo a b
hs : s = {t | γ t = γ' t} ∩ Ioo a b
t₁ : ℝ
ht₁ : t₁ ∈ s
hmem : Ioo a b ∈ 𝓝 t₁
heq : γ =ᶠ[𝓝 t₁] γ'
⊢ s ∈ 𝓝 t₁
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₁
⊢ ↑C ≠ 0

Tactic:
simpa using C_pos.ne'

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

Goal state before:
pp: ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ (ContinuousLinearMap.fst ℝ E ℝ ∘SL ContinuousLinearMap.proj (f.ind x hx)) ∘SL mfderiv% ⇑f.embeddingPiTangent x =
    mfderiv% ↑(chartAt H (f.c (f.ind x hx))) x

Tactic:
set L :=
    (ContinuousLinearMap.fst ℝ E ℝ).comp
      (@ContinuousLinearMap.proj ℝ _ ι (fun _ => E × ℝ) _ _ (fun _ => inferInstance) (f.ind x hx))
  have := L.hasMFDerivAt.comp x
    (f.embeddingPiTangent.contMDiff.mdifferentiableAt (by simp)).hasMFDerivAt
  convert! hasMFDerivAt_unique this _
  refine (hasMFDerivAt_extChartAt (f.mem_chartAt_ind_source x hx)).congr_of_eventuallyEq ?_
  refine (f.eventuallyEq_one x hx).mono fun y hy => ?_
  simp only [L, embeddingPiTangent_coe, ContinuousLinearMap.coe_comp, (· ∘ ·),
    ContinuousLinearMap.coe_fst', ContinuousLinearMap.proj_apply]
  rw [hy, Pi.one_apply, one_smul]

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case neg
G : Type u_2
inst✝ : Group G
h : ¬↑(Nat.card G) = 0
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)

Tactic:
exact mul_div_mul_right _ _ h

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

Goal state before:
pp: case h
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
ω : List B
⊢ cs.wordProd (i :: ω) = cs.simple i * cs.wordProd ω

Tactic:
wordProd_cons

Goal state after:
case h
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
ω : List B
⊢ cs.simple i * cs.wordProd ω = cs.simple i * cs.wordProd ω
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
ω : List B
hω : cs.IsReduced ω
⊢ (List.map (⇑cs.lengthParity) (List.map cs.simple ω)).prod = Multiplicative.ofAdd ↑ω.length

Tactic:
List.map_map,

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
⊢ (List.map (⇑cs.lengthParity ∘ cs.simple) ω).prod = Multiplicative.ofAdd ↑ω.length
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsRightInversion (w * t) t ↔ ¬cs.IsRightInversion w t

Tactic:
unfold IsRightInversion

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsReflection t ∧ cs.length (w * t * t) < cs.length (w * t) ↔ ¬(cs.IsReflection t ∧ cs.length (w * t) < cs.length w)
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)
m : CoprodI M
⊢ ∀ (w : Word M), (m • w).prod = m * w.prod

Tactic:
by
  induction m using CoprodI.induction_on with
  | one =>
    intro
    rw [one_smul, one_mul]
  | of _ =>
    intros
    rw [of_smul_def, prod_rcons, of.map_mul, mul_assoc, ← prod_rcons, ← equivPair_symm,
      Equiv.symm_apply_apply]
  | mul x y hx hy =>
    intro w
    rw [mul_smul, hx, hy, mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x y : (i : ι) × M i
l : List ((i : ι) × M i)
hnot1✝ : ∀ l_1 ∈ x :: y :: l, l_1.snd ≠ 1
hnot1 : x.snd ≠ 1 ∧ ∀ x ∈ y :: l, x.snd ≠ 1
hchain✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (x :: y :: l)
hchain : x.fst ≠ y.fst ∧ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (y :: l)
h : { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain✝ } ≠ empty
i j : ι
w' : NeWord M i j
hw' : w'.toList = y :: l
⊢ y = ⟨i, w'.head⟩

Tactic:
simpa [hw'] using w'.toList_head?

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case inr
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
this : a.num.natAbs • m = -a.num • m
⊢ -((have this := ⟨-a, ⋯⟩;
        this) •
        mk m s) =
    mk (a.num • m) (⟨a.den, ⋯⟩ * s)

Tactic:
simp [nnqsmul_mk, this, ← neg_mk]

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
a b : ℚ
m : M
s : ℕ+
⊢ (a + b) • mk m s = a • mk m s + b • mk m s

Tactic:
simp_rw [qsmul_mk, mk_add_mk, mk_eq_mk]

Goal state after:
case mk
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ ∃ u,
    ↑u • ↑(⟨a.den, ⋯⟩ * s * (⟨b.den, ⋯⟩ * s)) • (a + b).num • m =
      ↑u • ↑(⟨(a + b).den, ⋯⟩ * s) • (↑(⟨b.den, ⋯⟩ * s) • a.num • m + ↑(⟨a.den, ⋯⟩ * s) • b.num • m)
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a b c : DivisibleHull M
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c

Tactic:
induction a with | mk ma sa
    induction b with | mk mb sb
    induction c with | mk mc sc
    rw [mk_le_mk] at ⊢ hab hbc
    rw [← nsmul_le_nsmul_iff_right (show sb.val ≠ 0 by simp), smul_comm _ _ ma, smul_comm _ _ mc]
    rw [← nsmul_le_nsmul_iff_right (show sc.val ≠ 0 by simp), smul_comm _ _ mb] at hab
    rw [← nsmul_le_nsmul_iff_right (show sa.val ≠ 0 by simp)] at hbc
    exact hab.trans hbc

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a b : DivisibleHull M
h : a ≤ b
h' : b ≤ a
⊢ a = b

Tactic:
induction a with | mk ma sa
    induction b with | mk mb sb
    rw [mk_le_mk] at h h'
    rw [mk_eq_mk_iff_smul_eq_smul]
    exact le_antisymm h h'

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a b : DivisibleHull M
⊢ a ≤ b ∨ b ≤ a

Tactic:
induction a with | mk ma sa
    induction b with | mk mb sb
    simp_rw [mk_le_mk]
    exact le_total _ _

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

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

Tactic:
rw [ArchimedeanClass.mk_smul _ (by simp)] at this

Goal state after:
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s s' : ℕ+
this : ArchimedeanClass.mk (mk m s) = ArchimedeanClass.mk (↑↑s' • mk m s')
⊢ ArchimedeanClass.mk (mk m s) = ArchimedeanClass.mk (mk m s')
Module: Mathlib.GroupTheory.DivisibleHull

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

Tactic:
rw [ArchimedeanClass.mk_smul _ (by simp)] at this

Goal state after:
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s s' : ℕ+
this : ArchimedeanClass.mk (mk m s) = ArchimedeanClass.mk (mk m s')
⊢ ArchimedeanClass.mk (mk m s) = ArchimedeanClass.mk (mk m s')
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
T : Set G
hT_fin : T.Finite
hT : normalClosure T = f.ker
S : Set G
hS_fin : S.Finite
hS : normalClosure (⇑f '' S) = N
⊢ normalClosure (S ∪ T) = comap f N

Tactic:
← hS,

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
T : Set G
hT_fin : T.Finite
hT : normalClosure T = f.ker
S : Set G
hS_fin : S.Finite
hS : normalClosure (⇑f '' S) = N
⊢ normalClosure (S ∪ T) = comap f (normalClosure (⇑f '' S))
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
g : ↥P
hQ : IsPGroup p (↥↑P ⧸ (↑P).focalSubgroupOf)
⊢ g ∈ ((↑P).transferFocal.domRestrict P).ker ↔ g ∈ (↑P).focalSubgroupOf

Tactic:
MonoidHom.mem_ker,

Goal state after:
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
g : ↥P
hQ : IsPGroup p (↥↑P ⧸ (↑P).focalSubgroupOf)
⊢ ((↑P).transferFocal.domRestrict P) g = 1 ↔ g ∈ (↑P).focalSubgroupOf
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₅)
⊢ IsReduced (conjugator L ++ (replicate (n + 1 + 1) (reduceCyclically L)).flatten ++ invRev (conjugator L))

Tactic:
apply IsReduced.append_flatten_replicate_append (hn := by simp)

Goal state after:
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₅)
⊢ IsCyclicallyReduced (reduceCyclically L)

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))
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_2
inst✝ : CommGroup G
⊢ nilpotencyClass G ≤ 1

Tactic:
by
  rw [← upperCentralSeries_eq_top_iff_nilpotencyClass_le, upperCentralSeries_one]
  apply CommGroup.center_eq_top

Goal state after:
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)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : ↥(map (MonoidHom.fst G H) I)
h : ↥(map (MonoidHom.snd G H) I)
⊢ (g, h) ∈
      ((QuotientGroup.mk' (P.prod Q).range.goursatFst).prodMap (QuotientGroup.mk' (P.prod Q).range.goursatSnd)).ker ↔
    (g, h) ∈ (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd

Tactic:
MonoidHom.mem_ker,

Goal state after:
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)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : ↥(map (MonoidHom.fst G H) I)
h : ↥(map (MonoidHom.snd G H) I)
⊢ ((QuotientGroup.mk' (P.prod Q).range.goursatFst).prodMap (QuotientGroup.mk' (P.prod Q).range.goursatSnd)) (g, h) = 1 ↔
    (g, h) ∈ (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd