mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
e✝ : α ≃ β
inst✝³ : TopologicalSpace β
inst✝² : AddCommMonoid β
inst✝¹ : Semiring R
inst✝ : Module R β
e : α ≃ β
this✝¹ : TopologicalSpace α := e.topologicalSpace
this✝ : AddCommMonoid α := e.addCommMonoid
this : Module R α := Equiv.module R e
⊢ Continuous (linearEquiv R e).invFun

Tactic:
simp +instances only [Equiv.topologicalSpace, toFun_as_coe, ← coinduced_symm]

Goal state after:
R : Type u_1
α : Type u_2
β : Type u_3
e✝ : α ≃ β
inst✝³ : TopologicalSpace β
inst✝² : AddCommMonoid β
inst✝¹ : Semiring R
inst✝ : Module R β
e : α ≃ β
this✝¹ : TopologicalSpace α := e.topologicalSpace
this✝ : AddCommMonoid α := e.addCommMonoid
this : Module R α := Equiv.module R e
⊢ Continuous (linearEquiv R e).invFun
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : ⟨z, hz⟩ ∈ {z | (↑z).ofLp 0 < y - x}
⊢ ⟨toLp 2 fun x_1 ↦ ↑⟨min ((↑⟨z, hz⟩).ofLp 0 + x) y, ⋯⟩ - x, ⋯⟩ = ⟨z, hz⟩

Tactic:
Subtype.mk_eq_mk

Goal state after:
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : ⟨z, hz⟩ ∈ {z | (↑z).ofLp 0 < y - x}
⊢ (toLp 2 fun x_1 ↦ ↑⟨min ((↑⟨z, hz⟩).ofLp 0 + x) y, ⋯⟩ - x) = z
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : ⟨z, hz⟩ ∈ {z | (↑z).ofLp 0 < y - x}
⊢ ⟨toLp 2 fun x_1 ↦ y - ↑⟨max (y - (↑⟨z, hz⟩).ofLp 0) x, ⋯⟩, ⋯⟩ = ⟨z, hz⟩

Tactic:
Subtype.mk_eq_mk

Goal state after:
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : ⟨z, hz⟩ ∈ {z | (↑z).ofLp 0 < y - x}
⊢ (toLp 2 fun x_1 ↦ y - ↑⟨max (y - (↑⟨z, hz⟩).ofLp 0) x, ⋯⟩) = z
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
inst✝¹⁰ : NormedAddCommGroup E'''
inst✝⁹ : NormedSpace 𝕜 E'''
H : Type u_7
inst✝⁸ : TopologicalSpace H
G : Type u_9
inst✝⁷ : TopologicalSpace G
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f : M → N
φ : N → N'
hφ : IsImmersionAt J J' n φ (f x)
⊢ ContMDiffAt I J n f x ↔ ContinuousAt f x ∧ ContMDiffAt I J' n (φ ∘ f) x

Tactic:
by
  rw [← ContMDiffAt.iff_comp_isImmersionAtOfComplement hφ.isImmersionAtOfComplement_complement]

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

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
inst✝¹ : T2Space M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
⊢ IsMIntegralCurve (fun t ↦ γ (|t| + 1) t) v

Tactic:
by
  intro t
  have ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1) := by
    rw [mem_Ioo, ← abs_lt]
    exact lt_add_one _
  apply HasMFDerivAt.congr_of_eventuallyEq (f := γ (|t| + 1))
  · exact hγ (|t| + 1) (by positivity) _ ht |>.hasMFDerivAt (Ioo_mem_nhds ht.1 ht.2)
  · rw [Filter.eventuallyEq_iff_exists_mem]
    refine ⟨Ioo (-(|t| + 1)) (|t| + 1), ?_,
      eqOn_abs_add_one_of_isMIntegralCurveOn_Ioo hv γ hγx hγ⟩
    have : |t| < |t| + 1 := lt_add_of_pos_right |t| zero_lt_one
    rw [abs_lt] at this
    exact Ioo_mem_nhds this.1 this.2

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

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✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
⊢ riemannianEDist I x y ≤ pathELength I γ a b

Tactic:
let η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
  have hη : CMDiff[Icc 0 1] 1 (γ ∘ η) := by
    apply hγ.comp
    · rw [contMDiffOn_iff_contDiffOn]
      exact η.contDiff.contDiffOn
    · rw [← image_subset_iff, ContinuousAffineMap.coe_lineMap_eq, ← segment_eq_image_lineMap]
      simp [hab]
  let f : unitInterval → M := fun t ↦ (γ ∘ η) t
  have hf : CMDiff 1 f := by
    rw [← contMDiffOn_comp_projIcc_iff]
    apply hη.congr (fun t ht ↦ ?_)
    simp only [Function.comp_apply, f, projIcc_of_mem, ht]
  let g : Path x y := by
    refine ⟨⟨f, hf.continuous⟩, ?_, ?_⟩ <;>
    simp [f, η, ContinuousAffineMap.coe_lineMap_eq, ha, hb]
  have A : riemannianEDist I x y ≤ ∫⁻ x, ‖mfderiv% g x 1‖ₑ := by
    rw [riemannianEDist]; exact biInf_le _ hf
  apply A.trans_eq
  rw [lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc]
  have E : pathELength I (g ∘ projIcc 0 1 zero_le_one) 0 1 = pathELength I (γ ∘ η) 0 1 := by
    apply pathELength_congr (fun t ht ↦ ?_)
    simp only [Function.comp_apply, ht, projIcc_of_mem]
    rfl
  rw [E, pathELength_comp_of_monotoneOn zero_le_one _ η.differentiableOn]
  · simp [η, ContinuousAffineMap.coe_lineMap_eq]
  · simpa [η, ContinuousAffineMap.coe_lineMap_eq] using hγ.mdifferentiableOn one_ne_zero
  · apply (AffineMap.lineMap_mono hab).monotoneOn

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

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C
r : ℝ
r_pos : r > 0
hr :
  ball (↑(extChartAt I x) x) r ∩ range ↑I ⊆
    (extChartAt I x).target ∩ {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
A : ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I) ∈ 𝓝 x
y : M
hy : y ∈ ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I)
h'y : y ∈ (chartAt H x).source
η : ℝ →ᴬ[ℝ] E := ContinuousAffineMap.lineMap (↑(extChartAt I x) x) (↑(extChartAt I x) y)
γ : ℝ → M := ↑(extChartAt I x).symm ∘ ⇑η
hη :
  Icc 0 1 ⊆ ⇑η ⁻¹' (extChartAt I x).target ∧ Icc 0 1 ⊆ ⇑η ⁻¹' {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
⊢ ContDiff ℝ 1 ⇑η

Tactic:
exact ContinuousAffineMap.contDiff _

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : CompleteSpace E
n : ℕ∞ω
inst✝ : IsManifold I (n + 1) M
m : ℕ∞ω
U V : (x : M) → TangentSpace I x
s : Set M
x : M
hU : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, V x⟩) s x
hs : UniqueMDiff[s]
hx : x ∈ s
hmn : minSmoothness 𝕜 (m + 1) ≤ n
min2 : minSmoothness 𝕜 2 ≤ n + 1
m' : ℕ∞ω
hm' : m' ≤ m
h'm' : m' ≠ ∞
⊢ ContMDiffWithinAt I I.tangent m' (fun x₀ ↦ ⟨x₀, mlieBracketWithin I U V s x₀⟩) s x

Tactic:
have hn : 1 ≤ m' + 1 := le_add_self

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : CompleteSpace E
n : ℕ∞ω
inst✝ : IsManifold I (n + 1) M
m : ℕ∞ω
U V : (x : M) → TangentSpace I x
s : Set M
x : M
hU : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, V x⟩) s x
hs : UniqueMDiff[s]
hx : x ∈ s
hmn : minSmoothness 𝕜 (m + 1) ≤ n
min2 : minSmoothness 𝕜 2 ≤ n + 1
m' : ℕ∞ω
hm' : m' ≤ m
h'm' : m' ≠ ∞
hn : 1 ≤ m' + 1
⊢ ContMDiffWithinAt I I.tangent m' (fun x₀ ↦ ⟨x₀, mlieBracketWithin I U V s x₀⟩) s x
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: case e'_22
𝕜 : Type u
inst✝¹⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
EN : Type u_3
inst✝⁹ : NormedAddCommGroup EN
inst✝⁸ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝⁷ : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace HN N
EP : Type u_5
inst✝⁴ : NormedAddCommGroup EP
inst✝³ : NormedSpace 𝕜 EP
HP : Type u_6
inst✝² : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace HP P
U : Opens M
V : Opens ↑↑(ChartedSpace.locallyRingedSpace IM ↥U).toPresheafedSpace
x✝ :
  ↑(((TopCat.Presheaf.pushforward CommRingCat
              (LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.base).obj
          (ChartedSpace.locallyRingedSpace IM ↥U).presheaf).obj
      (Opposite.op (⋯.functor.obj V)))
g :
  (x :
      ↥(Opposite.unop
          ((Opens.map
                  (LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.base).op.obj
            (Opposite.op (⋯.functor.obj V))))) →
    (fun x ↦ 𝕜) ↑x
hg : (StructureGroupoid.LocalInvariantProp.localPredicate (↥U) 𝕜 ⋯).pred g
a : TopCat.of ↥U ⟶ TopCat.of M := TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ }
ha : IsOpenEmbedding ⇑(TopCat.Hom.hom a)
V' : Opens ↥U := (Opens.map a).obj (⋯.functor.obj V)
b : ↥V' ≃ₜ ↥(⋯.functor.obj V) := ⋯.homeomorphOfSubsetRange ⋯
x : ↥(Opposite.unop (Opposite.op (⋯.functor.obj V)))
⊢ (Subtype.val ∘ Subtype.val ∘ ⇑b.symm) x = ↑x

Tactic:
exact congr($(b.apply_symm_apply x).1)

Goal state after:
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t₁ t₂ : Triangle R P
h : (fun t ↦ { vertices := t.points }) t₁ = (fun t ↦ { vertices := t.points }) t₂
⊢ ∀ (i : Fin (2 + 1)), t₁.points i = t₂.points i

Tactic:
apply_fun Polygon.vertices at h

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t₁ t₂ : Triangle R P
h : ((fun t ↦ { vertices := t.points }) t₁).vertices = ((fun t ↦ { vertices := t.points }) t₂).vertices
⊢ ∀ (i : Fin (2 + 1)), t₁.points i = t₂.points i
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Fintype (ConjClasses G)
inst✝¹ : Fintype G
inst✝ : (x : ConjClasses G) → Fintype ↑x.carrier
⊢ ∑ x, x.carrier.toFinset.card = Fintype.card G

Tactic:
suffices (Σ x : ConjClasses G, x.carrier) ≃ G by simpa using! (Fintype.card_congr this)

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype (ConjClasses G)
inst✝¹ : Fintype G
inst✝ : (x : ConjClasses G) → Fintype ↑x.carrier
⊢ (x : ConjClasses G) × ↑x.carrier ≃ G
Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G✝ : Type u_3
H✝ : Type u_4
inst✝³ : Group G✝
inst✝² : Group H✝
G : Type u
inst✝¹ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), (lift f) (of a) = f a
H : Type u
inst✝ : Group H
f : G →* H
⊢ ∀ (a : X), lift.symm f a = f (of a)

Tactic:
a

Goal state after:
ι : Type u_1
ι' : Type u_2
G✝ : Type u_3
H✝ : Type u_4
inst✝³ : Group G✝
inst✝² : Group H✝
G : Type u
inst✝¹ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), (lift f) (of a) = f a
H : Type u
inst✝ : Group H
f : G →* H
a : X
⊢ lift.symm f a = f (of a)
Module: Mathlib.GroupTheory.Coxeter.Basic

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

Tactic:
PresentedGroup.toGroup.of,

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
f : { f // M.IsLiftable f }
⊢ (fun ι ↦ ⟨⇑ι ∘ cs.simple, ⋯⟩) ((fun f ↦ (Units.coeHom G).comp (cs.groupLift ⋯)) f) = f

Tactic:
by
    ext i
    simp only [MonoidHom.comp_apply, comp_apply, groupLift, simple]
    rw [← MonoidHom.toFun_eq_coe, toMonoidHom_apply_symm_apply, PresentedGroup.toGroup.of,
      OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, Units.coeHom_apply, restrictUnit]

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

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

Tactic:
PresentedGroup.toGroup.of,

Goal state after:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
ι : W →* G
i : B
⊢ (Units.coeHom G) (restrictUnit ⋯ i) = ι (cs.mulEquiv.symm (PresentedGroup.of i))
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
ι : W →* G
i : B
⊢ (Units.coeHom G) { val := (⇑ι ∘ cs.simple) i, inv := (⇑ι ∘ cs.simple) i, val_inv := ⋯, inv_val := ⋯ } =
    ι (cs.mulEquiv.symm (PresentedGroup.of i))

Tactic:
Units.coeHom_apply

Goal state after:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
ι : W →* G
i : B
⊢ ↑{ val := (⇑ι ∘ cs.simple) i, inv := (⇑ι ∘ cs.simple) i, val_inv := ⋯, inv_val := ⋯ } =
    ι (cs.mulEquiv.symm (PresentedGroup.of i))
Module: Mathlib.GroupTheory.Coxeter.Length

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

Tactic:
← Nat.add_one_le_iff

Goal state after:
case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : cs.length (w * cs.simple i) + 1 ≤ cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
Module: Mathlib.GroupTheory.Coxeter.Length

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

Tactic:
← Nat.add_one_le_iff

Goal state after:
case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : cs.length w + 1 ≤ cs.length (w * cs.simple i)
⊢ cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : doubleCoset a ↑H ↑K = doubleCoset b ↑H ↑K
⊢ mk H K a = mk H K b

Tactic:
rw [eq]
  exact mem_doubleCoset.mp (h.symm ▸ mem_doubleCoset_self H K b)

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y) → ∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H

Tactic:
rintro ⟨x, hx, y, hy, hxy⟩
    refine ⟨⟨y, hy⟩, ?_⟩
    simp only [hxy, ← mul_assoc, hx, mul_inv_cancel_right]

Goal state after:
Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Type u_2
N : Type u_3
inst✝¹ : Group H
inst✝ : Group N
f : G →* H
K : FiniteIndexNormalSubgroup H
⊢ (Subgroup.comap f K.toSubgroup).FiniteIndex

Tactic:
let g : G →* (H ⧸ K.toSubgroup) := (QuotientGroup.mk' K.toSubgroup).comp f

Goal state after:
G : Type u_1
inst✝² : Group G
H : Type u_2
N : Type u_3
inst✝¹ : Group H
inst✝ : Group N
f : G →* H
K : FiniteIndexNormalSubgroup H
g : G →* H ⧸ K.toSubgroup := (QuotientGroup.mk' K.toSubgroup).comp f
⊢ (Subgroup.comap f K.toSubgroup).FiniteIndex
Module: Mathlib.GroupTheory.Schreier

Goal state before:

Tactic:
Group.rank H ≤ #T := Group.rank_le hT
    _ ≤ H.index * #S := hT₀
    _ = H.index * Group.rank G := congr_arg (H.index * ·) hS₀

Goal state after:
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : IsFinitelyPresented G
inst✝ : IsFinitelyPresented H
w✝ : ℕ
sG : Set (FreeGroup (Fin w✝))
left✝ : Finite ↑sG
φG : G ≃* PresentedGroup sG
⊢ IsFinitelyPresented (Monoid.Coprod G H)

Tactic:
obtain ⟨_, sH, ⟨_ : Finite sH, ⟨φH⟩⟩⟩ := exists_mulEquiv_presentedGroup (G := H)

Goal state after:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : IsFinitelyPresented G
inst✝ : IsFinitelyPresented H
w✝¹ : ℕ
sG : Set (FreeGroup (Fin w✝¹))
left✝¹ : Finite ↑sG
φG : G ≃* PresentedGroup sG
w✝ : ℕ
sH : Set (FreeGroup (Fin w✝))
left✝ : Finite ↑sH
φH : H ≃* PresentedGroup sH
⊢ IsFinitelyPresented (Monoid.Coprod G H)
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
w : α × Bool
g : FreeGroup α
hC✝ : 0 < g.toWord.length
h : g.toWord[0].1 = w.1 → g.toWord[0].2 = w.2
hC : True
⊢ (List.rec [w] (fun head tail tail_ih ↦ if w.1 = head.1 ∧ w.2 = !head.2 then tail else w :: head :: tail)
        g.toWord)[0]? =
    some w

Tactic:
show g.toWord = g.toWord.head (by grind) :: g.toWord.tail by grind

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
w : α × Bool
g : FreeGroup α
hC✝ : 0 < g.toWord.length
h : g.toWord[0].1 = w.1 → g.toWord[0].2 = w.2
hC : True
⊢ (List.rec [w] (fun head tail tail_ih ↦ if w.1 = head.1 ∧ w.2 = !head.2 then tail else w :: head :: tail)
        (g.toWord.head ⋯ :: g.toWord.tail))[0]? =
    some w
Module: Mathlib.GroupTheory.FreeGroup.Orbit

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l : List (α × Bool) := g.toWord
hl : l = g.toWord
⊢ mk g.toWord ∈ startsWith w

Tactic:
simp [g.mk_toWord, hg]

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

Goal state before:
pp: case refine_2
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'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
⊢ E x = (Functor.mapEnd (root' T) F') x

Tactic:
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

Goal state after:
case refine_2
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'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
⊢ (functorOfMonoidHom T E).map x = F'.map x
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case inr
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
⊢ IsTrivialBlock B

Tactic:
· obtain ⟨g, hg⟩ := exists_smul_eq G b a
        rw [← IsTrivialBlock.smul_iff g]
        exact H ⟨b, hb, hg⟩ (hB.translate g)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ Nat.card α
⊢ Nontrivial ↥(alternatingGroup α)

Tactic:
have : Nontrivial α := by
    rw [← Fintype.one_lt_card_iff_nontrivial, ← Nat.card_eq_fintype_card]
    refine lt_of_lt_of_le (by decide) h3

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ Nat.card α
this : Nontrivial α
⊢ Nontrivial ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ Nat.card α
this : Nontrivial α
⊢ 2 * 1 < 2 * Nat.card ↥(alternatingGroup α)

Tactic:
rw [two_mul_nat_card_alternatingGroup, Nat.card_perm, ← Nat.succ_le_iff]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ Nat.card α
this : Nontrivial α
⊢ (2 * 1).succ ≤ (Nat.card α).factorial
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case mp
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a✝ : IsMultiplyPretransitive G α 2
⊢ ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d

Tactic:
a

Goal state after:
case mp
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a✝ : IsMultiplyPretransitive G α 2
a : α
⊢ ∀ {b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d