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

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
H' : Type u_5
inst✝⁷ : TopologicalSpace H'
E' : Type u_6
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
n : ℕ∞ω
t : Set M'
inst✝² : IsManifold I 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderiv[s] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : 2 ≤ n
hV : MDiffAt[t] (T% V) (f x₀)
⊢ (MDiffAt[s ∩ f ⁻¹' t] fun x ↦ ⟨x, mpullbackWithin I I' f V s x⟩) x₀

Tactic:
exact hV.mpullbackWithin_vectorField_inter hf hf' hx₀ hs hmn

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
x : M
V W : (x : M) → TangentSpace I x
c : 𝕜
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDiffAt (T% V) x
⊢ mlieBracket I (c • V) W x = c • mlieBracket I V W x

Tactic:
simp only [← mlieBracketWithin_univ] at hV ⊢

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
x : M
V W : (x : M) → TangentSpace I x
c : 𝕜
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDiffAt (T% V) x
⊢ mlieBracketWithin I (c • V) W univ x = c • mlieBracketWithin I V W univ x
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↑(sphere 0 1)
h : w ∈ {⟨v, ?m.125⟩}ᶜ
⊢ ↑w ∈ {x | ((innerSL ℝ) v) x ≠ 1}

Tactic:
by
      dsimp
      exact
        h ∘ Subtype.ext ∘ Eq.symm ∘ (inner_eq_one_iff_of_norm_eq_one hv (by simp)).mp

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

Goal state before:
pp: 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)
this : ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0) = ⇑((ℝ ∙ ↑(-v))ᗮ.subtypeL ∘SL ↑↑U.symm)
⊢ Injective ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0)

Tactic:
refine Eq.subst this.symm ?_

Goal state after:
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)
this : ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0) = ⇑((ℝ ∙ ↑(-v))ᗮ.subtypeL ∘SL ↑↑U.symm)
⊢ Injective ⇑((ℝ ∙ ↑(-v))ᗮ.subtypeL ∘SL ↑↑U.symm)
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 : F
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ IsVonNBounded ℝ (Metric.ball 0 1)

Tactic:
exact NormedSpace.isVonNBounded_ball ℝ F 1

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 : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x)),
    ‖mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y)‖ < C
this✝ : 𝓝 x = 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))
this : ContinuousAt (↑(extChartAt I x).symm) (↑(extChartAt I x) x)
⊢ ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ < C

Tactic:
filter_upwards [nhdsWithin_le_nhds (this.preimage_mem_nhds hC),
    extChartAt_target_mem_nhdsWithin x] with y hy h'y

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
x : M
C : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x)),
    ‖mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y)‖ < C
this✝ : 𝓝 x = 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))
this : ContinuousAt (↑(extChartAt I x).symm) (↑(extChartAt I x) x)
y : E
hy : y ∈ ↑(extChartAt I x).symm ⁻¹' {x_1 | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x_1)‖ < C}
h'y : y ∈ (extChartAt I x).target
⊢ ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ < C
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∞
hc : 0 < c
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
this : ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C) ∈ 𝓝 x
y : M
hy : y ∈ ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C)
h'y : riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
⊢ riemannianEDist I x y < c

Tactic:
apply h'y.trans_lt

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
x : M
c : ℝ≥0∞
hc : 0 < c
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
this : ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C) ∈ 𝓝 x
y : M
hy : y ∈ ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C)
h'y : riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
⊢ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) < c
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
t t' : (x : M) → V x
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : FiniteDimensional 𝕜 F
hs : IsLocalFrameOn I F n s u
hx : x ∈ u
this : Fintype ι := hs.fintypeOfFiniteDimensional hx
⊢ t x = t' x ↔ ∀ (i : ι), (hs.coeff i x) (t x) = (hs.coeff i x) (t' x)

Tactic:
exact ⟨fun h i ↦ hs.coeff_congr h i, fun h ↦ hs.eq_of_coeff_eq hx h⟩

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

Goal state before:
pp: case pos
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
⊢ e (x * y) = e x * e y

Tactic:
simp [hxy, mul_self, ← pow_two (e y), h ▸ Monoid.pow_exponent_eq_one (e y), he]

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

Goal state before:
pp: case zero
⊢ Nat.card (DihedralGroup 0) = 2 * 0

pp: case succ
n✝ : ℕ
⊢ Nat.card (DihedralGroup (n✝ + 1)) = 2 * (n✝ + 1)

Tactic:
· rw [Nat.card_eq_zero_of_infinite]

Goal state after:
case succ
n✝ : ℕ
⊢ Nat.card (DihedralGroup (n✝ + 1)) = 2 * (n✝ + 1)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
h1 : n ≠ 1
h2 : Odd n
⊢ reciprocalFactors n = n % 4 * n :: reciprocalFactors (n / 4 + 1)

Tactic:
by
  have h0 : n ≠ 0 := by
    rintro rfl
    norm_num [← Nat.not_even_iff_odd] at h2
  rw [reciprocalFactors, dif_neg h0, dif_neg h1, if_neg (Nat.not_even_iff_odd.2 h2)]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : 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).range ≤ s

Tactic:
rintro _ ⟨x, rfl⟩
  induction x using CoprodI.induction_on with
  | one => exact s.one_mem
  | of i x =>
    simp only [lift_of]
    exact h i (Set.mem_range_self x)
  | mul x y hx hy =>
    simp only [map_mul]
    exact s.mul_mem hx hy

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 i' : B
m : ℕ
hm : m ≤ M.M i i' * 2
⊢ (if Even ↑m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (↑m / ↑2) =
    (if Even ↑(M.M i i' * 2 - m) then 1 else cs.simple i) * (cs.simple i' * cs.simple i) ^ (↑(M.M i i' * 2 - m) / ↑2)

Tactic:
Int.ofNat_sub hm

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hm : m ≤ M.M i i' * 2
⊢ (if Even ↑m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (↑m / ↑2) =
    (if Even (↑(M.M i i' * 2) - ↑m) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i' * 2) - ↑m) / ↑2)
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
lt : j < ω.length
⊢ cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) *
      ((cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)

pp: case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
le : ω.length ≤ j
⊢ cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) *
      ((cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)

Tactic:
· simp only [getElem?_eq_getElem lt, wordProd_append, mul_assoc]
    simp

Goal state after:
case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
le : ω.length ≤ j
⊢ cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) *
      ((cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
lt : j < ω.length
⊢ cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)

pp: case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
le : ω.length ≤ j
⊢ cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)

Tactic:
· simp only [getElem?_eq_getElem lt, wordProd_append, mul_assoc]
    simp

Goal state after:
case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
le : ω.length ≤ j
⊢ cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case left
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.rightInvSeq ω
⊢ cs.IsReflection t

pp: case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.rightInvSeq ω
⊢ cs.length (cs.wordProd ω * t) < cs.length (cs.wordProd ω)

Tactic:
· exact cs.isReflection_of_mem_rightInvSeq ω ht

Goal state after:
case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.rightInvSeq ω
⊢ cs.length (cs.wordProd ω * t) < cs.length (cs.wordProd ω)
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
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
⊢ False

Tactic:
set! t' := (ris (ω.eraseIdx j)).getD (j' - 1) 1 with h₂

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
⊢ False
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⇑(setoid ↑H ↑⊥) = ⇑(QuotientGroup.rightRel H)

Tactic:
ext a b
  rw [rel_iff, QuotientGroup.rightRel_apply]
  constructor
  · rintro ⟨b, hb, a, rfl : a = 1, rfl⟩
    rwa [mul_one, mul_inv_cancel_right]
  · rintro (h : b * a⁻¹ ∈ H)
    exact ⟨b * a⁻¹, h, 1, rfl, by rw [mul_one, inv_mul_cancel_right]⟩

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case neg
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
k : ι
hcard : 3 ≤ #(H k)
hh : i = k
hl : ¬j = k
⊢ (lift f) w.prod ≠ 1

Tactic:
subst hh
      change j ≠ i at hl
      exact lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w hcard hl.symm

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
⊢ Function.Injective (⇑(lift fun i ↦ FreeGroup.lift fun x ↦ a i) ∘ ⇑freeGroupEquivCoprodI.toMonoidHom)

Tactic:
refine Function.Injective.comp ?_ (MulEquiv.injective freeGroupEquivCoprodI)

Goal state after:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
⊢ Function.Injective ⇑(lift fun i ↦ FreeGroup.lift fun x ↦ a i)
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: 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) ⋯

Tactic:
aux_archimedeanClassMk_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 : (archimedeanClassOrderHom M) (ArchimedeanClass.mk num✝¹) ≤ (archimedeanClassOrderHom M) (ArchimedeanClass.mk num✝)
⊢ (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: case h₁.mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s : ℕ+
⊢ ArchimedeanClass.mk (mk m 1) = ArchimedeanClass.mk (mk m s)

Tactic:
aux_archimedeanClassMk_mk

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
⊢ Function.Bijective fun g ↦ { toFun := fun φ ↦ φ g, map_one' := ⋯, map_mul' := ⋯ }

Tactic:
refine (Nat.bijective_iff_injective_and_card _).mpr ⟨fun _ _ h ↦ ?_, ?_⟩
      · rwa [mk.injEq, OneHom.mk.injEq, funext_iff, forall_apply_eq_apply_iff] at h
      · rw [card_monoidHom_of_hasEnoughRootsOfUnity, card_monoidHom_of_hasEnoughRootsOfUnity]

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hH : ¬H.index = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
f : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)) → ↥(zpowers g) :=
  fun q ↦ ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x ↦ g • x) q.out
hf : ∀ (q : Quotient (orbitRel (↥(zpowers g)) (G ⧸ H))), f q ∈ H.subgroupOf (zpowers g)
key : ∏ c, f c ∈ H.subgroupOf (zpowers g)
⊢ g ^ H.index ∈ H

Tactic:
simpa only [f, Finset.prod_pow_eq_pow_sum, index_eq_sum_minimalPeriod H g] using! key

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
f : G →* H
hf : Function.Surjective ⇑f
S : Set G
hSfinite : S.Finite
hSclosure : normalClosure S = N
⊢ normalClosure (⇑f '' S) = map f N

Tactic:
rw [← hSclosure, Subgroup.map_normalClosure _ _ hf]

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ : List (α × Bool)
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
hc : conjugator x.toWord = conjugator y.toWord
n : ℕ
hn : n + 1 ≠ 0
heq : g x (n + 1) = g y (n + 1)
heq₂ : g x (2 * (n + 1)) = g y (2 * (n + 1))
leq : f x (n + 1) = f y (n + 1)
leq₂ : f x (2 * (n + 1)) = f y (2 * (n + 1))
heq' :
  (replicate (n + 1) (reduceCyclically x.toWord)).flatten ++ invRev (conjugator x.toWord) =
    (replicate (n + 1) (reduceCyclically y.toWord)).flatten ++ invRev (conjugator y.toWord)
⊢ x = y

Tactic:
have hm : reduceCyclically x.toWord = reduceCyclically y.toWord := by
      simp only [replicate_succ, flatten_cons, append_assoc] at heq'
      exact (List.append_inj heq' <| mul_left_cancel₀ hn <| by grind).1

Goal state after:
α : Type u
L L₁ L₂ L₃ : List (α × Bool)
x y : FreeGroup α
f : FreeGroup α → ℕ → ℕ :=
  fun a n ↦ (conjugator a.toWord).length + (n * (reduceCyclically a.toWord).length + (conjugator a.toWord).length)
g : FreeGroup α → ℕ → List (α × Bool) :=
  fun a k ↦ conjugator a.toWord ++ ((replicate k (reduceCyclically a.toWord)).flatten ++ invRev (conjugator a.toWord))
hc : conjugator x.toWord = conjugator y.toWord
n : ℕ
hn : n + 1 ≠ 0
heq : g x (n + 1) = g y (n + 1)
heq₂ : g x (2 * (n + 1)) = g y (2 * (n + 1))
leq : f x (n + 1) = f y (n + 1)
leq₂ : f x (2 * (n + 1)) = f y (2 * (n + 1))
heq' :
  (replicate (n + 1) (reduceCyclically x.toWord)).flatten ++ invRev (conjugator x.toWord) =
    (replicate (n + 1) (reduceCyclically y.toWord)).flatten ++ invRev (conjugator y.toWord)
hm : reduceCyclically x.toWord = reduceCyclically y.toWord
⊢ x = y
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
a b : ℕ
ab : a < b
hn : upperCentralSeries G a = upperCentralSeries G b
hG : ¬Group.IsNilpotent G
⊢ nilpotencyClass G ≤ a

Tactic:
rw [nilpotencyClass_of_not_nilpotent hG]
    apply Nat.zero_le

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : IsNilpotent G
⊢ ∀ (H : Subgroup G), normalizer ↑H = H → H = ⊤

Tactic:
apply @nilpotent_center_quotient_ind _ G _ _

Goal state after:
case hbase
G : Type u_1
inst✝ : Group G
h : IsNilpotent G
⊢ ∀ (G : Type u_1) [inst : Group G] [Subsingleton G] (H : Subgroup G), normalizer ↑H = H → H = ⊤

case hstep
G : Type u_1
inst✝ : Group G
h : IsNilpotent G
⊢ ∀ (G : Type u_1) [inst : Group G] [IsNilpotent G],
    (∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤) → ∀ (H : Subgroup G), normalizer ↑H = H → H = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
G : Type u_1
inst✝¹ : Finite G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [Finite β], Nat.card β < Nat.card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
⊢ 1 < Nat.card ↥(center G)

Tactic:
exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)

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
ι : Sort u_3
B : ι → Set X
hB : ∀ (i : ι), IsBlock G (B i)
⊢ IsBlock G (⋂ i, B i)

Tactic:
simp only [isBlock_iff_smul_eq_smul_of_nonempty, smul_set_iInter] at hB ⊢
  rintro g₁ g₂ ⟨a, ha₁, ha₂⟩
  simp_rw [fun i ↦ hB i ⟨a, iInter_subset _ i ha₁, iInter_subset _ i ha₂⟩]

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

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B✝ : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
hBB' : ⟨stabilizer G B, ⋯⟩ ≤ ⟨stabilizer G B', ⋯⟩
k : G
hb : k • a ∈ B
⊢ k ∈ stabilizer G B'

Tactic:
exact hBB' (hB.smul_eq_of_mem ha hb)

Goal state after: