mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ ∀ (e e' : OpenPartialHomeomorph (↑(sphere 0 1)) (EuclideanSpace ℝ (Fin n))),
    e ∈ atlas (EuclideanSpace ℝ (Fin n)) ↑(sphere 0 1) →
      e' ∈ atlas (EuclideanSpace ℝ (Fin n)) ↑(sphere 0 1) →
        ContDiffOn ℝ ω (↑(𝓡 n) ∘ ↑(e.symm ≫ₕ e') ∘ ↑(𝓡 n).symm)
          (↑(𝓡 n).symm ⁻¹' (e.symm ≫ₕ e').source ∩ Set.range ↑(𝓡 n))

Tactic:
by
      rintro _ _ ⟨v, rfl⟩ ⟨v', rfl⟩
      let U :=
        (-- Removed type ascription, and this helped for some reason with timeout issues?
            OrthonormalBasis.fromOrthogonalSpanSingleton (𝕜 := ℝ)
            n (ne_zero_of_mem_unit_sphere v)).repr
      let U' :=
        (-- Removed type ascription, and this helped for some reason with timeout issues?
            OrthonormalBasis.fromOrthogonalSpanSingleton (𝕜 := ℝ)
            n (ne_zero_of_mem_unit_sphere v')).repr
      have H₁ := U'.contDiff.comp_contDiffOn (contDiffOn_stereoToFun (n := ω))
      -- Porting note: need to help with implicit variables again
      have H₂ := (contDiff_stereoInvFunAux (m := ω) (v := v.val) |>.comp
        (ℝ ∙ (v : E))ᗮ.subtypeL.contDiff).comp U.symm.contDiff
      convert! H₁.comp_inter (H₂.contDiffOn : ContDiffOn ℝ ω _ Set.univ) using 1
        -- -- squeezed from `ext, simp [sphere_ext_iff, stereographic'_symm_apply, real_inner_comm]`

      -- -- squeezed from `ext, simp [sphere_ext_iff, stereographic'_symm_apply, real_inner_comm]`
      simp only [OpenPartialHomeomorph.trans_toPartialEquiv,
        OpenPartialHomeomorph.symm_toPartialEquiv, PartialEquiv.trans_source,
        PartialEquiv.symm_source, stereographic'_target, stereographic'_source]
      simp only [modelWithCornersSelf_coe, modelWithCornersSelf_coe_symm,
        Set.range_id, Set.inter_univ, Set.univ_inter, Set.compl_singleton_eq,
        Set.preimage_ofPred_eq]
      simp only [id, comp_apply, OpenPartialHomeomorph.coe_toPartialEquiv_symm,
        innerSL_apply_apply, Ne, sphere_ext_iff, real_inner_comm (v' : E)]
      rfl

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

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : ∀ (x : ℝ), ∃ y ∈ s, x < y
⊢ ∀ (a : ℝ), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)

Tactic:
intro a

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
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : ∀ (x : ℝ), ∃ y ∈ s, x < y
a : ℝ
⊢ ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)
Module: Mathlib.MeasureTheory.Constructions.UnitInterval

Goal state before:
pp: ⊢ volume univ = 1

Tactic:
Measure.Subtype.volume_univ nullMeasurableSet_Icc,

Goal state after:
⊢ volume (Icc 0 1) = 1
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := fun t ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
⊢ ∃ γ,
    γ a = x ∧
      γ b = y ∧ ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun x_1 ↦ x) ∧ γ =ᶠ[𝓝 b] fun x ↦ y

Tactic:
have B (t) (ht : b' < t) : η t = 1 := by
    simp only [η, Real.smoothTransition.eq_one_iff_one_le, inv_mul_eq_div]
    rw [one_le_div₀] <;> linarith

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✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := fun t ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
B : ∀ (t : ℝ), b' < t → η t = 1
⊢ ∃ γ,
    γ a = x ∧
      γ b = y ∧ ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun x_1 ↦ x) ∧ γ =ᶠ[𝓝 b] fun x ↦ y
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
pp: case refine_1
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
γ : Path x y
⊢ ContMDiff (𝓡∂ 1) 𝓘(ℝ, F) 1 ⇑γ → edist x y ≤ ∫⁻ (x_1 : ↑unitInterval), ‖(mfderiv% ⇑γ x_1) 1‖ₑ

Tactic:
hγ

Goal state after:
case refine_1
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
γ : Path x y
hγ : ContMDiff (𝓡∂ 1) 𝓘(ℝ, F) 1 ⇑γ
⊢ edist x y ≤ ∫⁻ (x_1 : ↑unitInterval), ‖(mfderiv% ⇑γ x_1) 1‖ₑ
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 y : F
γ : Path x y
hγ : ContMDiff (𝓡∂ 1) 𝓘(ℝ, F) 1 ⇑γ
e : ℝ → F := ⇑γ ∘ projIcc 0 1 ⋯
D : ContDiffOn ℝ 1 e (Icc 0 1)
| ‖y - e 0‖ₑ

Tactic:
show y = e 1 by simp [e]

Goal state after:
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
γ : Path x y
hγ : ContMDiff (𝓡∂ 1) 𝓘(ℝ, F) 1 ⇑γ
e : ℝ → F := ⇑γ ∘ projIcc 0 1 ⋯
D : ContDiffOn ℝ 1 e (Icc 0 1)
| ‖e 1 - e 0‖ₑ
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace N
f g : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hfg : EqOn f g φ.source
⊢ SubmersionAtProp F I J M N f φ ψ → SubmersionAtProp F I J M N g φ ψ

Tactic:
intro ⟨equiv, hf⟩

Goal state after:
𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace N
f g : M → N
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
hfg : EqOn f g φ.source
equiv : E ≃L[𝕜] E'' × F
hf : EqOn (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (Prod.fst ∘ ⇑equiv) (φ.extend I).target
⊢ SubmersionAtProp F I J M N g φ ψ
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)
this : edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) < c / ↑C
⊢ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) < c

Tactic:
rwa [ENNReal.lt_div_iff_mul_lt, mul_comm] at this

Goal state after:
case hb0
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)
this : edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) < c / ↑C
⊢ ↑C ≠ 0 ∨ edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) ≠ ∞

case hbt
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)
this : edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) < c / ↑C
⊢ ↑C ≠ ∞ ∨ edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) ≠ 0
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
h : IsSubmersionAtOfComplement F I J n f x
⊢ ContMDiffOn I J n f h.domChart.source

Tactic:
rw [← contMDiffOn_writtenInExtend_iff h.domChart_mem_maximalAtlas
    h.codChart_mem_maximalAtlas le_rfl h.mapsto_domChart_source_codChart_source,
    ← h.domChart.extend_target_eq_image_source]

Goal state after:
𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
h : IsSubmersionAtOfComplement F I J n f x
⊢ ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E'') n (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm)
    (h.domChart.extend I).target
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
ι : Type u_7
e : Trivialization F TotalSpace.proj
inst✝¹ : MemTrivializationAtlas e
b : Basis ι 𝕜 F
inst✝ : ContMDiffVectorBundle 1 F V I
x : M
hx : x ∈ e.baseSet
s : (x : M) → V x
i : ι
⊢ (localFrameCoeff I e b i x) (s x) = ((e.basisAt b hx).repr (s x)) i

Tactic:
have he := e.isLocalFrameOn_localFrame_baseSet I 1 b
  have hbasis : e.basisAt b hx = he.toBasisAt hx := by
    ext j
    simp [IsLocalFrameOn.toBasisAt, localFrame, basisAt, hx]
  simp [localFrameCoeff, IsLocalFrameOn.coeff, hx, hbasis]

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
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
hσσ' : ∃ v ∈ 𝓝 x, ∀ y ∈ v, σ y = σ' y
⊢ cov σ x = cov σ' x

Tactic:
choose s' hs' b using hσσ'

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
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
cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
σ σ' : (x : M) → V x
x : M
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hxs : s ∈ 𝓝 x
s' : Set M
hs' : s' ∈ 𝓝 x
b : ∀ y ∈ s', σ y = σ' y
⊢ cov σ x = cov σ' x
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case zero
n : ℕ
i : ZMod n
⊢ r i ^ 0 = r (i * ↑0)

Tactic:
| zero =>

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (fst x, snd x) = toProd x

Tactic:
by
  rw [← fst_prod_snd, MonoidHom.prod_apply]

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

Goal state before:
pp: case zero
B : Type u_1
i i' : B
⊢ alternatingWord i i' (0 + 1) = (if Even 0 then i' else i) :: alternatingWord i i' 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
B : Type u_1
i i' : B
⊢ (alternatingWord i i' 0).length = 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
B : Type u_1
i j : B
⊢ ∀ (k : ℕ) (hk : k < 0), (alternatingWord i j 0)[k] = if Even (0 + k) then i else j

Tactic:
| zero =>

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

Goal state before:
pp: case zero
B : Type u_1
i j : B
p : ℕ
h : 0 < 2 * p
⊢ take 0 (alternatingWord i j (2 * p)) = if Even 0 then alternatingWord i j 0 else alternatingWord j i 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
⊢ cs.wordProd (alternatingWord i i' 0) = (if Even 0 then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (0 / 2)

Tactic:
| zero =>

Goal state after:
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
⊢ cs.IsRightDescent w i ↔ ¬cs.IsRightDescent (w * cs.simple i) i

Tactic:
isRightDescent_iff,

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
⊢ cs.length (w * cs.simple i) + 1 = cs.length w ↔ ¬cs.IsRightDescent (w * cs.simple i) i
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:
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.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j : ι
w : NeWord M i j
⊢ w.toList.head? = some ⟨i, w.head⟩

Tactic:
by
  fun_induction toList with grind [head]

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:
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.Coxeter.Inversion

Goal state before:
pp: case zero
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ cs.rightInvSeq (drop 0 ω) = drop 0 (cs.rightInvSeq ω)

Tactic:
| zero =>

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 : ℕ
⊢ (cs.rightInvSeq (take j ω).reverse).reverse = take j (cs.rightInvSeq ω.reverse).reverse

Tactic:
rw [List.take_reverse]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ (cs.rightInvSeq (take j ω).reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse
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 (take j ω.reverse.reverse).reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse

Tactic:
rw [List.take_reverse]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ (cs.rightInvSeq (drop (ω.reverse.length - j) ω.reverse).reverse.reverse).reverse =
    (drop ((cs.rightInvSeq ω.reverse).length - j) (cs.rightInvSeq ω.reverse)).reverse
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 ∧ x = qi (q x) * y

Tactic:
← div_eq_iff_eq_mul',

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.CoprodI

Goal state before:
pp: 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)
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)
hchain : x.fst ≠ y.fst ∧ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (y :: l)
hi : ∃ i j w', w'.toWord.toList = { toList := y :: l, ne_one := ⋯, chain_ne := ⋯ }.toList
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

Tactic:
obtain ⟨i, j, w', hw' : w'.toList = y::l⟩ := hi

Goal state after:
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)
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)
hchain : x.fst ≠ y.fst ∧ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (y :: l)
h : { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain✝ } ≠ empty
i j : ι
w' : NeWord M i j
hw' : w'.toList = y :: l
⊢ ∃ i j w', w'.toWord.toList = { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain✝ }.toList