mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
v' : E → E :=
  fun x ↦
    (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x))
      (v (↑(extChartAt I (γ t₀)).symm x))
hv' :
  v' = fun x ↦
    (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x))
      (v (↑(extChartAt I (γ t₀)).symm x))
left✝ : ContinuousAt (fun x ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨γ t₀, v (γ t₀)⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I (γ t₀)).symm)
    (range ↑I) (↑(extChartAt I (γ t₀)) (γ t₀))
⊢ γ =ᶠ[𝓝 t₀] γ'

Tactic:
obtain ⟨K, s, hs, hlip⟩ : ∃ K, ∃ s ∈ 𝓝 _, LipschitzOnWith K v' s :=
    (hv.contDiffAt (range_mem_nhds_isInteriorPoint hγt₀)).snd.exists_lipschitzOnWith

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
v' : E → E :=
  fun x ↦
    (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x))
      (v (↑(extChartAt I (γ t₀)).symm x))
hv' :
  v' = fun x ↦
    (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x))
      (v (↑(extChartAt I (γ t₀)).symm x))
left✝ : ContinuousAt (fun x ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨γ t₀, v (γ t₀)⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I (γ t₀)).symm)
    (range ↑I) (↑(extChartAt I (γ t₀)) (γ t₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 (↑(extChartAt I (γ t₀)) (γ t₀))
hlip : LipschitzOnWith K v' s
⊢ γ =ᶠ[𝓝 t₀] γ'
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
M : Type u_4
inst✝ : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContinuousWithinAt (fun m ↦ { proj := b m, snd := v m }) s x
hw : ContinuousWithinAt (fun m ↦ { proj := b m, snd := w m }) s x
⊢ ContinuousWithinAt (fun m ↦ ⟪v m, w m⟫) s x

Tactic:
rcases h.exists_continuous with ⟨g, g_cont, hg⟩

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
M : Type u_4
inst✝ : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContinuousWithinAt (fun m ↦ { proj := b m, snd := v m }) s x
hw : ContinuousWithinAt (fun m ↦ { proj := b m, snd := w m }) s x
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
⊢ ContinuousWithinAt (fun m ↦ ⟪v m, w m⟫) s x
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 ∘ ⇑η
⊢ riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)

Tactic:
have hη : Icc 0 1 ⊆ ⇑η ⁻¹' ((extChartAt I x).target ∩
        {y | ‖mfderiv[range I] (extChartAt I x).symm y‖ₑ < C}) := by
    simp only [← image_subset_iff, ContinuousAffineMap.coe_lineMap_eq,
     ← segment_eq_image_lineMap, η]
    apply Subset.trans _ hr
    exact ((convex_ball _ _).inter I.convex_range).segment_subset (by simp [r_pos]) hy

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
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 ∩ {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C})
⊢ riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
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
⊢ ∀ᶠ (y : B) in 𝓝 x,
    ‖Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
          Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
      r

Tactic:
rcases h.exists_continuous with ⟨g, g_cont, hg⟩

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
⊢ ∀ᶠ (y : B) in 𝓝 x,
    ‖Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
          Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
      r
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E' : Type u_2
E'' : Type u_3
E''' : Type u_4
F : Type u_5
F' : Type u_6
H : Type u_7
H' : Type u_8
G : Type u_9
G' : Type u_10
E : Type u
inst✝²⁸ : NontriviallyNormedField 𝕜
inst✝²⁷ : NormedAddCommGroup E
inst✝²⁶ : NormedSpace 𝕜 E
inst✝²⁵ : NormedAddCommGroup E'
inst✝²⁴ : NormedSpace 𝕜 E'
inst✝²³ : NormedAddCommGroup E''
inst✝²² : NormedSpace 𝕜 E''
inst✝²¹ : NormedAddCommGroup E'''
inst✝²⁰ : NormedSpace 𝕜 E'''
inst✝¹⁹ : NormedAddCommGroup F
inst✝¹⁸ : NormedSpace 𝕜 F
inst✝¹⁷ : NormedAddCommGroup F'
inst✝¹⁶ : NormedSpace 𝕜 F'
inst✝¹⁵ : TopologicalSpace H
inst✝¹⁴ : TopologicalSpace H'
inst✝¹³ : TopologicalSpace G
inst✝¹² : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
M' : Type u_12
N : Type u_13
N' : Type u_14
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
inst✝⁹ : TopologicalSpace M'
inst✝⁸ : ChartedSpace H' M'
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace G' N'
n : ℕ∞ω
x✝¹ : M
f✝ : M → N
g✝ : M' → N'
x' : M'
inst✝³ : IsManifold I n M
inst✝² : IsManifold I' n M'
inst✝¹ : IsManifold J n N
inst✝ : IsManifold J' n N'
hf : IsSubmersionAtOfComplement F I J n f✝ x✝¹
hg : IsSubmersionAtOfComplement F' I' J' n g✝ x'
f : M → N
φ₁ : OpenPartialHomeomorph M H
ψ₁ : OpenPartialHomeomorph N G
g : M' → N'
φ₂ : OpenPartialHomeomorph M' H'
ψ₂ : OpenPartialHomeomorph N' G'
equiv₁ : E ≃L[𝕜] E'' × F
hfprop : EqOn (↑(ψ₁.extend J) ∘ f ∘ ↑(φ₁.extend I).symm) (Prod.fst ∘ ⇑equiv₁) (φ₁.extend I).target
equiv₂ : E' ≃L[𝕜] E''' × F'
hgprop : EqOn (↑(ψ₂.extend J') ∘ g ∘ ↑(φ₂.extend I').symm) (Prod.fst ∘ ⇑equiv₂) (φ₂.extend I').target
x : E × E'
x✝ : x ∈ (φ₁.extend I).target ×ˢ (φ₂.extend I').target
hx : x.1 ∈ (φ₁.extend I).target
hx' : x.2 ∈ (φ₂.extend I').target
⊢ (Prod.fst ∘ ↑((ψ₁.extend J).prod (ψ₂.extend J')) ∘ Prod.map f g ∘ ↑((φ₁.extend I).prod (φ₂.extend I')).symm) x =
    (Prod.fst ∘ Prod.fst ∘ ⇑((equiv₁.prodCongr equiv₂).trans (ContinuousLinearEquiv.prodProdProdComm 𝕜 E'' F E''' F')))
      x

Tactic:
by simpa using hfprop hx

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

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✝² : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝¹ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝ : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
h : ∀ (i : ι), IsCovariantDerivativeOn F (cov i) u
f : ι → M → 𝕜
hf : ∑ i ∈ s, f i = 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
⊢ ∑ i ∈ s, (g x • f i x • cov i σ x + f i x • (d% g x).smulRight (σ x)) =
    g x • ∑ i ∈ s, f i x • cov i σ x + (∑ i ∈ s, f i) x • (d% g x).smulRight (σ x)

Tactic:
rw [Finset.sum_add_distrib, Finset.smul_sum, Finset.sum_apply, Finset.sum_smul]

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card M) ^ 2 ≠ 0

Tactic:
· exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr card_ne_zero)

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

Goal state before:
pp: M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : MulOneClass M'
inst✝¹ : MulOneClass N'
inst✝ : MulOneClass P
⊢ (mk.comp (FreeMonoid.map Sum.swap)) (of (Sum.inr 1)) = 1

Tactic:
simp only [MonoidHom.comp_apply, map_of, Sum.swap_inr, mk_of_inl, map_one]

Goal state after:
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: case mk.C1
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x : PresentedGroup rels
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) 1 ∈ H

pp: case mk.of
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x : PresentedGroup rels
x✝ : α
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) (FreeGroup.of x✝) ∈ H

pp: case mk.inv_of
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x : PresentedGroup rels
x✝ : α
a✝ : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) (FreeGroup.of x✝) ∈ H
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) (FreeGroup.of x✝)⁻¹ ∈ H

pp: case mk.mul
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x : PresentedGroup rels
x✝ y✝ : FreeGroup α
a✝¹ : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) x✝ ∈ H
a✝ : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) y✝ ∈ H
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) (x✝ * y✝) ∈ H

Tactic:
· exact one_mem H

Goal state after:
case mk.of
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x : PresentedGroup rels
x✝ : α
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) (FreeGroup.of x✝) ∈ H

case mk.inv_of
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x : PresentedGroup rels
x✝ : α
a✝ : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) (FreeGroup.of x✝) ∈ H
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) (FreeGroup.of x✝)⁻¹ ∈ H

case mk.mul
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x : PresentedGroup rels
x✝ y✝ : FreeGroup α
a✝¹ : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) x✝ ∈ H
a✝ : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) y✝ ∈ H
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) (x✝ * y✝) ∈ H
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 : B
this✝ : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) (FreeGroup.of i * FreeGroup.of i) = 1
⊢ cs.mulEquiv.symm (PresentedGroup.of i * PresentedGroup.of i) = 1

Tactic:
PresentedGroup.of,

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
this✝ : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
this : (PresentedGroup.mk M.relationsSet) (FreeGroup.of i * FreeGroup.of i) = 1
⊢ cs.mulEquiv.symm
      ((PresentedGroup.mk M.relationsSet) (FreeGroup.of i) * (PresentedGroup.mk M.relationsSet) (FreeGroup.of i)) =
    1
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
fi : (i : ι) → M i →* N
x✝¹ x✝ : FreeMonoid ((i : ι) × M i)
⊢ Rel M x✝¹ x✝ ≤ ((FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) x✝¹ = (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) x✝)

Tactic:
rintro (i | ⟨x, y⟩) <;> simp

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ Submonoid.closure (range fun p ↦ (f p.fst) p.snd) = ⨆ i, MonoidHom.mrange (f i)

Tactic:
range_sigma_eq_iUnion_range,

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ Submonoid.closure (⋃ a, range fun b ↦ (f ⟨a, b⟩.fst) ⟨a, b⟩.snd) = ⨆ i, MonoidHom.mrange (f i)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : p.head = 1
⊢ (rcons p).prod = of p.head * p.tail.prod

Tactic:
rw [rcons, dif_pos hm, hm, map_one, one_mul]

Goal state after:
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'δ : 1 + δ * C < r' ^ 2
⊢ ∀ᶠ (y : B) in 𝓝 x,
    ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
          Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ <
      r

Tactic:
rcases h.exists_continuous with ⟨g, g_cont, hg⟩

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'δ : 1 + δ * C < r' ^ 2
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
⊢ ∀ᶠ (y : B) in 𝓝 x,
    ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
          Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ <
      r
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
i : B
⊢ cs.IsReflection (cs.simple i)

Tactic:
use 1, i; simp

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

Goal state before:
pp: case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
ω : List B
ih : cs.rightInvSeq (ω.concat i) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)
⊢ (cs.wordProd (ω.concat i))⁻¹ * cs.simple j * cs.wordProd (ω.concat i) :: cs.rightInvSeq (ω.concat i) =
    (List.map (⇑(MulAut.conj (cs.simple i)))
          ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω :: cs.rightInvSeq ω)).concat
      (cs.simple i)

Tactic:
rw [ih]

Goal state after:
case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
ω : List B
ih : cs.rightInvSeq (ω.concat i) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)
⊢ (cs.wordProd (ω.concat i))⁻¹ * cs.simple j * cs.wordProd (ω.concat i) ::
      (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i) =
    (List.map (⇑(MulAut.conj (cs.simple i)))
          ((cs.wordProd ω)⁻¹ * cs.simple j * cs.wordProd ω :: cs.rightInvSeq ω)).concat
      (cs.simple i)
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 : ι
hij : i ≠ j
m₁ : M i
m₂ : M j
w : Word M
⊢ ⟨i, m₁⟩ ∈ (of m₂ • w).toList ↔ ⟨i, m₁⟩ ∈ w.toList

Tactic:
simp [mem_smul_iff, *]

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 : ι
w : Word M
⊢ of ((equivPair i) w).head • ((equivPair i) w).tail = w

Tactic:
by
  rw [← rcons_eq_smul, ← equivPair_symm, Equiv.symm_apply_apply]

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
ω : List B
j : ℕ
h : j < ω.length
⊢ (cs.leftInvSeq ω)[j] = cs.wordProd (take j ω) * cs.simple ω[j] * (cs.wordProd (take j ω))⁻¹

Tactic:
rw [← List.getD_eq_getElem (lis ω) 1, getD_leftInvSeq]
  simp [h]

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]
    simp [← mul_assoc]

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 (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]
    simp [← mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: case refine_1
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
H₁' : s * ↑f.range = Set.univ
c' : ℝ := max c₀ (c g)
H₃' : ∀ (x : G), b * h x - c' ≤ h (f x)
U : Subgroup G
u : G
hu : u ∈ Subgroup.map f U
⊢ u ∈ U

Tactic:
obtain ⟨u', hu₁, rfl⟩ := mem_map.mp hu

Goal state after:
case refine_1
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
H₁' : s * ↑f.range = Set.univ
c' : ℝ := max c₀ (c g)
H₃' : ∀ (x : G), b * h x - c' ≤ h (f x)
U : Subgroup G
u' : G
hu₁ : u' ∈ U
hu : f u' ∈ Subgroup.map f U
⊢ f u' ∈ U
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
h : G → ℝ
C : ℝ
H₁ : (powMonoidHom 2).range.FiniteIndex
H₂ : ∀ (x : G), 0 ≤ h x
H₃ : ∀ (x y : G), |h (x * y) + h (x / y) - 2 * (h x + h y)| ≤ C
inst✝ : Northcott h
⊢ Group.FG G

Tactic:
have H₃' x : 4 * h x - (h 1 + C) ≤ h (x ^ 2) := by grind [pow_two, div_self']

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
h : G → ℝ
C : ℝ
H₁ : (powMonoidHom 2).range.FiniteIndex
H₂ : ∀ (x : G), 0 ≤ h x
H₃ : ∀ (x y : G), |h (x * y) + h (x / y) - 2 * (h x + h y)| ≤ C
inst✝ : Northcott h
H₃' : ∀ (x : G), 4 * h x - (h 1 + C) ≤ h (x ^ 2)
⊢ Group.FG G