mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
pp: case refine_2
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
γ : ℝ →ᴬ[ℝ] F := ⋯
this : riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) (⇑γ) 0 1
⊢ pathELength 𝓘(ℝ, F) (⇑γ) 0 1 = edist x y

Tactic:
rw [pathELength_eq_lintegral_mfderivWithin_Icc]

Goal state after:
case refine_2
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
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
this : riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) (⇑γ) 0 1
⊢ ∫⁻ (t : ℝ) in Icc 0 1, ‖(mfderiv[Icc 0 1] ⇑γ t) 1‖ₑ = edist x y
Module: Mathlib.Geometry.Manifold.Sheaf.Smooth

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
U : (OpenNhds x)ᵒᵖ
⊢ colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U ≫
      (forgetStalk IM I M R x).inv ≫ ↾⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) =
    colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U ≫ smoothSheaf.evalHom IM I R x

Tactic:
smoothSheafCommRing.ι_forgetStalk_inv_assoc,

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
U : (OpenNhds x)ᵒᵖ
⊢ ↾⇑(CommRingCat.Hom.hom (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U)) ≫
      ↾⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) =
    colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U ≫ smoothSheaf.evalHom IM I R x
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
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'
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : IsManifold I' (minSmoothness 𝕜 2) M'
inst✝ : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
⊢ mpullback I I' f (mlieBracketWithin I' V W t) x₀ = mlieBracketWithin I (mpullback I I' f V) (mpullback I I' f W) s x₀

Tactic:
have : mpullback I I' f (mlieBracketWithin I' V W t) x₀ =
      mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ := by
    simp only [mpullback, mpullbackWithin]
    congr
    apply (mfderivWithin_eq_mfderiv (hu _ hx₀) _).symm
    exact hf.mdifferentiableAt (two_pos.trans_le (le_minSmoothness.trans hn)).ne'
  rw [this, mpullbackWithin_mlieBracketWithin' hV hW hu uniqueMDiffOn_univ hf.contMDiffWithinAt
    hx₀ hn hst (by simp) (subset_univ _)]
  apply Filter.EventuallyEq.mlieBracketWithin_vectorField_of_insert
  · rw [insert_eq_of_mem hx₀]
    filter_upwards [nhdsWithin_le_nhds ((contMDiffAt_iff_contMDiffAt_nhds (by simp)).1
      (hf.of_le (le_minSmoothness.trans hn))), self_mem_nhdsWithin] with y hy h'y
    simp only [mpullback, mpullbackWithin]
    congr
    apply mfderivWithin_eq_mfderiv (hu _ h'y)
    exact hy.mdifferentiableAt two_ne_zero
  · rw [insert_eq_of_mem hx₀]
    filter_upwards [nhdsWithin_le_nhds ((contMDiffAt_iff_contMDiffAt_nhds (by simp)).1
      (hf.of_le (le_minSmoothness.trans hn))), self_mem_nhdsWithin] with y hy h'y
    simp only [mpullback, mpullbackWithin]
    congr
    apply mfderivWithin_eq_mfderiv (hu _ h'y)
    exact hy.mdifferentiableAt two_ne_zero

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

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

Tactic:
by
  simp [coeff, hx]

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

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

Tactic:
by
  simp [coeff, hx]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹³ : TopologicalSpace M
inst✝¹² : ChartedSpace H M
F : Type u_5
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁹ : TopologicalSpace (TotalSpace F V)
inst✝⁸ : (x : M) → AddCommGroup (V x)
inst✝⁷ : (x : M) → Module 𝕜 (V x)
inst✝⁶ : (x : M) → TopologicalSpace (V x)
inst✝⁵ : FiberBundle F V
inst✝⁴ : VectorBundle 𝕜 F V
inst✝³ : ContMDiffVectorBundle 1 F V I
e : Trivialization F TotalSpace.proj
inst✝² : MemTrivializationAtlas e
ι : Type u_7
b : Basis ι 𝕜 F
s : (x : M) → V x
x : M
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : CompleteSpace 𝕜
hxe : x ∈ e.baseSet
hs : MDiffAt (T% s) x
i : ι
⊢ MDiffAt ((LinearMap.piApply (Trivialization.localFrameCoeff I e b i)) s) x

Tactic:
let aux := fun x ↦ b.repr (e ((T% s) x)).2 i
  -- Since `e.baseSet` is open, this is sufficient.
  suffices MDiffAt aux x by
    apply this.congr_of_eventuallyEq
    apply eventuallyEq_of_mem (s := e.baseSet) (by simp [e.open_baseSet.mem_nhds hxe])
    intro y hy
    simp [aux, e.localFrameCoeff_eq_coeff hy]
  simp only [aux]
  -- step 2: `s` read in trivialization `e` is differentiable
  have h₁ : MDiffAt (fun x ↦ (e ((T% s) x)).2) x := by
    simpa using (e.mdifferentiableAt_section_iff I s hxe).1 hs
  -- step 3: `b.repr` is a linear map, so the composition is smooth
  let breprl : F →ₗ[𝕜] 𝕜 :=
    { toFun v := b.repr v i
      map_add' m m' := by simp
      map_smul' m x := by simp }
  have : MDifferentiableAt 𝓘(𝕜, F) 𝓘(𝕜) breprl.toContinuousLinearMap (e ((T% s) x)).2 :=
    mdifferentiableAt_iff_differentiableAt.mpr <| by fun_prop
  exact this.comp x h₁

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

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
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E cov
x : M
X σ✝ σ'✝ : (x : M) → TangentSpace I x
hY : MDiffAt (T% σ✝) x
hY' : MDiffAt (T% σ'✝) x
⊢ torsionAux cov X (σ✝ + σ'✝) x = torsionAux cov X σ✝ x + torsionAux cov X σ'✝ x

Tactic:
simp [torsionAux, hcov.add hY hY', VectorField.mlieBracket_add_right hY hY']

Goal state after:
𝕜 : 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
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
hcov : IsCovariantDerivativeOn E cov
x : M
X σ✝ σ'✝ : (x : M) → TangentSpace I x
hY : MDiffAt (T% σ✝) x
hY' : MDiffAt (T% σ'✝) x
⊢ (cov σ✝ x) (X x) + (cov σ'✝ x) (X x) - ((cov X x) (σ✝ x) + (cov X x) (σ'✝ x)) -
      (VectorField.mlieBracket I X σ✝ x + VectorField.mlieBracket I X σ'✝ x) =
    (cov σ✝ x) (X x) - (cov X x) (σ✝ x) - VectorField.mlieBracket I X σ✝ x +
      ((cov σ'✝ x) (X x) - (cov X x) (σ'✝ x) - VectorField.mlieBracket I X σ'✝ x)
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
hδ : (r' ^ 2)⁻¹ < 1 - δ * C
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' x - g' y‖ ≤ δ
v : E y
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y) v
hgy : ((g y) v) v = ((g' y) w) w
hgx : ((g x) ((trivializationAt F E x).symm x w)) ((trivializationAt F E x).symm x w) = ((g' x) w) w
⊢ ‖g' x - g' y‖ * ‖w‖ * ‖w‖ + ((g' y) w) w ≤ δ * ‖w‖ ^ 2 + ((g' y) w) w

Tactic:
rw [pow_two, mul_assoc]

Goal state after:
B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
hδ : (r' ^ 2)⁻¹ < 1 - δ * C
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' x - g' y‖ ≤ δ
v : E y
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y) v
hgy : ((g y) v) v = ((g' y) w) w
hgx : ((g x) ((trivializationAt F E x).symm x w)) ((trivializationAt F E x).symm x w) = ((g' x) w) w
⊢ ‖g' x - g' y‖ * (‖w‖ * ‖w‖) + ((g' y) w) w ≤ δ * (‖w‖ * ‖w‖) + ((g' y) w) w
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

Goal state before:
pp: case mpr
𝕜 : 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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
h :
  ∀ {X Y : (x : M) → TangentSpace I x} {x : M},
    MDiffAt (T% X) x → MDiffAt (T% Y) x → (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y x
⊢ cov.torsion = 0

Tactic:
ext x u v

Goal state after:
case mpr
𝕜 : 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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
h :
  ∀ {X Y : (x : M) → TangentSpace I x} {x : M},
    MDiffAt (T% X) x → MDiffAt (T% Y) x → (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y x
x : M
u v : TangentSpace I x
⊢ ((cov.torsion x) u) v = ((0 x) u) v
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case intro.e_a.mk
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ 1 = Fintype.card ↑(carrier (Quot.mk (⇑(IsConj.setoid G)) g))

Tactic:
eq_comm,

Goal state after:
case intro.e_a.mk
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ Fintype.card ↑(carrier (Quot.mk (⇑(IsConj.setoid G)) g)) = 1
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case pos
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : n = 2
⊢ False

Tactic:
simpa [exponent, card, h2] using h.exponent_eq_card

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

Goal state before:
pp: case neg
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : ¬n = 2
⊢ False

Tactic:
exact not_commutative h1 h2 h.isMulCommutative

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) / (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2) =
    ↑(Nat.card { p // Commute p.1 p.2 } * Nat.card { p // Commute p.1 p.2 }) / (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2)

Tactic:
← Nat.card_prod,

Goal state after:
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) / (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2) =
    ↑(Nat.card ({ p // Commute p.1 p.2 } × { p // Commute p.1 p.2 })) / (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2)
Module: Mathlib.GroupTheory.CoprodI

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

Tactic:
exact mul m y ihy

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx ≠ some i
he : rcons { head := m, tail := w, fstIdx_ne := h } = rcons { head := m', tail := w', fstIdx_ne := h' }
hm : m = 1
hm' : m' = 1
⊢ { head := m, tail := w, fstIdx_ne := h } = { head := m', tail := w', fstIdx_ne := h' }

Tactic:
simp only [rcons, dif_pos hm, dif_pos hm'] at he
    simp_all

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case cons.refine_1
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
motive : Word M → Sort u_4
empty : motive Word.empty
cons :
  (i : ι) → (m : M i) → (w : Word M) → (h1 : w.fstIdx ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Word.cons m w h1 h2)
m : (i : ι) × M i
w : List ((i : ι) × M i)
ih :
  (h1 : ∀ l ∈ w, l.snd ≠ 1) →
    (h2 : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) w) → motive { toList := w, ne_one := h1, chain_ne := h2 }
h1 : ∀ l ∈ m :: w, l.snd ≠ 1
h2 : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (m :: w)
⊢ { toList := w, ne_one := ⋯, chain_ne := ⋯ }.fstIdx ≠ some m.fst

Tactic:
rw [List.isChain_cons] at h2
      simp only [fstIdx, ne_eq, Option.map_eq_some_iff,
        Sigma.exists, exists_and_right, exists_eq_right, not_exists]
      intro m' hm'
      exact h2.1 _ hm' rfl

Goal state after:
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)
i j : ι
m₁ : M i
m₂ : M j
w : Word M
⊢ ⟨i, m₁⟩ ∈ (of m₂ • w).toList ↔
    ¬i = j ∧ ⟨i, m₁⟩ ∈ w.toList ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          ⟨i, m₁⟩ ∈ w.toList.tail ∨
            (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = ⋯ ▸ (m₂ * m')) ∨ w.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂

Tactic:
rw [of_smul_def, mem_rcons_iff, mem_equivPair_tail_iff, equivPair_head, or_assoc]
  by_cases hij : i = j
  · subst i
    simp only [not_true, ne_eq, false_and, exists_prop, true_and, false_or]
    by_cases hw : ⟨j, m₁⟩ ∈ w.toList.tail
    · simp [hw, show m₁ ≠ 1 from w.ne_one _ (List.mem_of_mem_tail hw)]
    · simp only [hw, false_or, Option.mem_def, and_congr_right_iff]
      intro hm1
      split_ifs with h
      · rcases h with ⟨hnil, rfl⟩
        simp only [List.head?_eq_some_head hnil, Option.some.injEq]
        constructor
        · rintro rfl
          exact Or.inl ⟨_, rfl, rfl⟩
        · rintro (⟨_, h, rfl⟩ | hm')
          · simp only [Sigma.ext_iff, heq_eq_eq, true_and] at h
            subst h
            rfl
          · simp only [fstIdx, Option.map_eq_some_iff, Sigma.exists,
              exists_and_right, exists_eq_right, not_exists] at hm'
            exact (hm'.1 (w.toList.head hnil).2 (by rw [List.head?_eq_some_head])).elim
      · revert h
        rw [fstIdx]
        cases w.toList
        · simp
        · simp +contextual [Sigma.ext_iff]
  · rcases w with ⟨_ | _, _, _⟩ <;>
    simp [or_comm, hij, Ne.symm hij, eq_comm]

Goal state after:
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 : ℕ
hj : j < ω.length
⊢ (cs.wordProd (drop (j + 1) ω))⁻¹ *
      ((Option.map cs.simple ω[j]?).getD 1 *
        (cs.wordProd (drop (j + 1) ω) *
          ((cs.wordProd (drop (j + 1) ω))⁻¹ * ((Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω))))) =
    1

Tactic:
rw [getElem?_eq_getElem hj]

Goal state after:
case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
hj : j < ω.length
⊢ (cs.wordProd (drop (j + 1) ω))⁻¹ *
      ((Option.map cs.simple (some ω[j])).getD 1 *
        (cs.wordProd (drop (j + 1) ω) *
          ((cs.wordProd (drop (j + 1) ω))⁻¹ *
            ((Option.map cs.simple (some ω[j])).getD 1 * cs.wordProd (drop (j + 1) ω))))) =
    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 : ℕ
hj : j < ω.length
⊢ cs.wordProd (take j ω) *
      ((Option.map cs.simple ω[j]?).getD 1 *
        ((cs.wordProd (take j ω))⁻¹ *
          (cs.wordProd (take j ω) * ((Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹)))) =
    1

Tactic:
rw [getElem?_eq_getElem hj]

Goal state after:
case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
hj : j < ω.length
⊢ cs.wordProd (take j ω) *
      ((Option.map cs.simple (some ω[j])).getD 1 *
        ((cs.wordProd (take j ω))⁻¹ *
          (cs.wordProd (take j ω) * ((Option.map cs.simple (some ω[j])).getD 1 * (cs.wordProd (take j ω))⁻¹)))) =
    1
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * ↑f.range = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h (f x)
inst✝ : Northcott h
q : G → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U)ᶜ.Nonempty
g : G
hg : g ∈ s
y : G
hx₁ : g * f y ∈ (↑U)ᶜ
hx₂ : ∀ a' ∈ (↑U)ᶜ, h (g * f y) ≤ h a'
this : 2 * c / (b - a) < h (g * f y)
⊢ a * h (g * f y) + 2 * c < b * h (g * f y)

Tactic:
field_simp [sub_pos.mpr H₀] at this; grind

Goal state after:
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : (powMonoidHom n).range.FiniteIndex
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
f : G →* G := powMonoidHom n
q : G → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
x y : G
| y ∈ ↑f.range ∧ qi (q x) * y = x

Tactic:
eq_comm,

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : (powMonoidHom n).range.FiniteIndex
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
f : G →* G := powMonoidHom n
q : G → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
x y : G
| y ∈ ↑f.range ∧ x = qi (q x) * y
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
⊢ b = a * (a⁻¹ * b)

Tactic:
mul_inv_cancel_left

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
⊢ b = b
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
t : Finset (Quotient ↑H ↑K)
ht : ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K ≠ Set.univ
x : G
y : Quotient ↑H ↑K
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) ↑H ↑K
hx : Quot.mk (⇑(rightRel H)) q = Quot.mk (⇑(rightRel H)) x
a : ↥H
ha : x = ↑a * q
⊢ ∃ x_1 ∈ ↑H, ∃ y ∈ ↑K, x = x_1 * q * y

Tactic:
exact ⟨a.1, a.2, ⟨1, Subgroup.one_mem K, by simpa using ha⟩⟩

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
R S T : H.LeftTransversal
inst✝ : H.FiniteIndex
q : G ⧸ H
x✝ : q ∈ univ
⊢ (↑(⋯.leftQuotientEquiv q))⁻¹ *
      (↑(⋯.leftQuotientEquiv q) * ((↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q))) =
    (↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q)

Tactic:
mul_inv_cancel_left

Goal state after: