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

Goal state before:
pp: case neg.hV
𝕜 : 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 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
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 : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
hfi : ¬(mfderiv[s] f x₀).IsInvertible
⊢ (mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)).inverse ((mfderiv[s] f x₀).inverse (V (f x₀))) = 0

Tactic:
ContinuousLinearMap.inverse_of_not_isInvertible hfi

Goal state after:
case neg.hV
𝕜 : 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 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
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 : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
hfi : ¬(mfderiv[s] f x₀).IsInvertible
⊢ (mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)).inverse (0 (V (f x₀))) = 0
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case neg.hW
𝕜 : 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 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
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 : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
hfi : ¬(mfderiv[s] f x₀).IsInvertible
⊢ (mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)).inverse ((mfderiv[s] f x₀).inverse (W (f x₀))) = 0

Tactic:
ContinuousLinearMap.inverse_of_not_isInvertible hfi

Goal state after:
case neg.hW
𝕜 : 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 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
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 : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
hfi : ¬(mfderiv[s] f x₀).IsInvertible
⊢ (mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)).inverse (0 (W (f x₀))) = 0
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 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ < C
⊢ ∃ C > 0, ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C

Tactic:
lift C to ℝ≥0 using C_pos.le

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

Tactic:
lift C to ℝ≥0 using C_pos.le

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
C_pos : ↑C > 0
hC : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ < ↑C
⊢ ∃ C > 0, ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: 𝕜 : 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
x : M
f g : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)
⊢ f ∈ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)) →
    g ∈ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)) → f + g ∈ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x))

Tactic:
exact Ideal.add_mem _

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

Goal state before:
pp: case pos
𝕜 : 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
hs : IsLocalFrameOn I F n s u
htt' : t x = t' x
i : ι
hxe : x ∈ u
⊢ (hs.coeff i x) (t x) = (hs.coeff i x) (t' x)

Tactic:
simp [coeff, hxe, htt']

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

Goal state before:
pp: case neg
𝕜 : 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
hs : IsLocalFrameOn I F n s u
htt' : t x = t' x
i : ι
hxe : x ∉ u
⊢ (hs.coeff i x) (t x) = (hs.coeff i x) (t' x)

Tactic:
simp [coeff, hxe, htt']

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
n : ℕ∞ω
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 n F V I
ι : Type u_7
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
b : Basis ι 𝕜 F
i : ι
y : M
hy : y ∈ e.baseSet
⊢ (↑e ⟨y, e.localFrame b i y⟩).2 = b i

Tactic:
simp [hy, basisAt]

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
f✝ : M → 𝕜
σ✝ : (x : M) → TangentSpace I x
hf : MDiffAt f✝ x
hY : MDiffAt (T% σ✝) x
⊢ torsionAux cov X (f✝ • σ✝) x = f✝ x • torsionAux cov X σ✝ x

Tactic:
simp [torsionAux, hcov.leibniz hY hf, VectorField.mlieBracket_smul_right hf 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
f✝ : M → 𝕜
σ✝ : (x : M) → TangentSpace I x
hf : MDiffAt f✝ x
hY : MDiffAt (T% σ✝) x
⊢ f✝ x • (cov σ✝ x) (X x) + (d% f✝ x) (X x) • σ✝ x - f✝ x • (cov X x) (σ✝ x) -
      ((d% f✝ x) (X x) • σ✝ x + f✝ x • VectorField.mlieBracket I X σ✝ x) =
    f✝ 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
⊢ δ * C * ‖G.symm w‖ ^ 2 + ((g' y) w) w = δ * C * ((g x) (G.symm w)) (G.symm w) + ((g' y) w) w

Tactic:
simp [← hg]

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Mul β
⊢ commProb (α → β) = commProb β ^ card α

Tactic:
by
  rw [commProb_pi, Finset.prod_const, Finset.card_univ]

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

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsRightInversion w⁻¹ t ↔ cs.IsLeftInversion w t

Tactic:
apply and_congr_right

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
⊢ cs.IsReflection t → (cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w)
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
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : cs.length w % 2 = (cs.length w + cs.length (cs.simple i)) % 2
⊢ False

Tactic:
length_simple

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : cs.length w % 2 = (cs.length w + 1) % 2
⊢ False
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case neg
ι : 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
hij : ¬i = j
⊢ (⟨i, m₁⟩ ∈ w.toList.tail ∨
      (i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m₁⟩) ∨
        m₁ ≠ 1 ∧
          ∃ (h : j = i),
            m₁ =
              h ▸
                (have __src := (equivPair j) w;
                  {
                    head :=
                      m₂ *
                        if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = j then ⋯ ▸ (w.toList.head ⋯).snd else 1,
                    tail := __src.tail, fstIdx_ne := ⋯ }).head) ↔
    ¬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:
rcases w with ⟨_ | _, _, _⟩ <;>
    simp [or_comm, hij, Ne.symm hij, eq_comm]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case of
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i✝ : ι
m✝ : M i✝
w✝ : Word M
⊢ of m✝ *
      (of ((equivPair i✝) w✝).head *
        (have __src := (equivPair i✝) w✝;
            { head := m✝ * ((equivPair i✝) w✝).head, tail := __src.tail, fstIdx_ne := ⋯ }).tail.prod) =
    of m✝ * w✝.prod

Tactic:
← prod_rcons,

Goal state after:
case of
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i✝ : ι
m✝ : M i✝
w✝ : Word M
⊢ of m✝ * (rcons ((equivPair i✝) w✝)).prod = of m✝ * w✝.prod
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
j : ℕ
⊢ (cs.rightInvSeq ω).getD j 1 * (cs.rightInvSeq ω).getD j 1 = 1

Tactic:
by
  simp_rw [getD_rightInvSeq, mul_assoc]
  rcases em (j < ω.length) with hj | nhj
  · rw [getElem?_eq_getElem hj]
    simp [← mul_assoc]
  · rw [getElem?_eq_none_iff.mpr (by lia)]
    simp

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₁✝.toList
_w₂_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₂✝.toList
x : (i : ι) × M i
hx : x ∈ _w₁✝.toList.getLast?
y : (i : ι) × M i
hy : y ∈ _w₂✝.toList.head?
⊢ x.fst ≠ y.fst

Tactic:
toList_getLast?,

Goal state after:
case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₁✝.toList
_w₂_ih✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) _w₂✝.toList
x : (i : ι) × M i
hx : x ∈ some ⟨j✝, _w₁✝.last⟩
y : (i : ι) × M i
hy : y ∈ _w₂✝.toList.head?
⊢ x.fst ≠ y.fst
Module: Mathlib.GroupTheory.CoprodI

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

Tactic:
rcases l with - | ⟨y, l⟩

Goal state after:
case cons.nil
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) × M i
hi :
  ∀ (hnot1 : ∀ l ∈ [], l.snd ≠ 1) (hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) []),
    { toList := [], ne_one := hnot1, chain_ne := hchain } ≠ empty →
      ∃ i j w', w'.toWord.toList = { toList := [], ne_one := hnot1, chain_ne := hchain }.toList
hnot1✝ : ∀ l ∈ [x], l.snd ≠ 1
hnot1 : x.snd ≠ 1 ∧ ∀ x ∈ [], x.snd ≠ 1
hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) [x]
h : { toList := [x], ne_one := hnot1✝, chain_ne := hchain } ≠ empty
⊢ ∃ i j w', w'.toWord.toList = { toList := [x], ne_one := hnot1✝, chain_ne := hchain }.toList

case cons.cons
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x y : (i : ι) × M i
l : List ((i : ι) × M i)
hi :
  ∀ (hnot1 : ∀ l_1 ∈ y :: l, l_1.snd ≠ 1) (hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (y :: l)),
    { toList := y :: l, ne_one := hnot1, chain_ne := hchain } ≠ empty →
      ∃ i j w', w'.toWord.toList = { toList := y :: l, ne_one := hnot1, chain_ne := hchain }.toList
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)
h : { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain } ≠ empty
⊢ ∃ i j w', w'.toWord.toList = { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain }.toList
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
n : ℕ
h : M → ℝ
b c₀ : ℝ
hb : 1 < b
H : ∀ (x : M), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
t : M
ht : t ∈ {x | IsOfFinOrder x}
this : Finite ↥(Submonoid.powers t)
C : ℝ := ⨆ g, h ↑g
hC : ∀ g ∈ Submonoid.powers t, h g ≤ C
t₀ : ↥(Submonoid.powers t)
ht₀ : h ↑t₀ = C
⊢ (b - 1) * C ≤ c₀

Tactic:
grind [Submonoid.pow_mem]

Goal state after:
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 (⇑(leftRel K)) q = Quot.mk (⇑(leftRel K)) x
a' : ↥K.op
ha' : (fun m ↦ m • x) a' = q
⊢ x = 1 * q * unop (↑a')⁻¹

Tactic:
simpa
    using

Goal state after:
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 (⇑(leftRel K)) q = Quot.mk (⇑(leftRel K)) x
a' : ↥K.op
ha' : (fun m ↦ m • x) a' = q
⊢ x = q * (unop ↑a')⁻¹
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 : ↑↑s • mk m s = ↑↑s' • mk m s'
⊢ ArchimedeanClass.mk (mk m s) = ArchimedeanClass.mk (mk m s')

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

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case hXdisj
ι : 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
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
⊢ Pairwise (Disjoint on X')

Tactic:
show Pairwise (Disjoint on X')
    intro i j hij
    simp only [X']
    apply Disjoint.union_left <;> apply Disjoint.union_right
    · exact hXdisj hij
    · exact hXYdisj i j
    · exact (hXYdisj j i).symm
    · exact hYdisj hij

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : ↥S) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ ∏ a, Nat.card ↥(zpowers ↑a)
⊢ Nat.card G ∣ ∏ _x, Monoid.exponent G

Tactic:
refine hf.trans (Finset.prod_dvd_prod_of_dvd _ _ fun g _ => ?_)

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : ↥S) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ ∏ a, Nat.card ↥(zpowers ↑a)
g : ↥S
x✝ : g ∈ Finset.univ
⊢ Nat.card ↥(zpowers ↑g) ∣ Monoid.exponent G
Module: Mathlib.Order.Radical

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
⊢ a = ⊤

Tactic:
have q : a ⊔ radical α ≤ m := sup_le le (radical_le_coatom c)

Goal state after:
case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : a ⊔ radical α ≤ m
⊢ a = ⊤