mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝ : IsManifold I 2 M
f : M → 𝕜
hf : MDiffAt[s] f x
⊢ let V' := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I);
  let W' := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I);
  mpullback I 𝓘(𝕜, E) (↑(extChartAt I x))
      (fun x₀ ↦
        (fderivWithin 𝕜 (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) x₀) (V' x₀) • W' x₀)
      x =
    (mfderiv[s] f x) (V x) • W x

Tactic:
simp only [mpullback, mfderivWithin, hf, map_smul, ← mfderiv_extChart_inverse_comp_aux x W,
    mpullbackWithin]
  congr 2
  rw [extChartAt_to_inv]
  exact mfderivWithin_extChartAt_symm_inverse_apply (v := V x)

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W V₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hV₁ : MDiffAt[s] (T% V₁) x
hs : UniqueMDiffAt[s] x
⊢ (mfderiv% ↑(extChartAt I x) x).inverse
      (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (V + V₁) (range ↑I))
        (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x)) =
    (mfderiv% ↑(extChartAt I x) x).inverse
      (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
          (↑(extChartAt I x) x) +
        lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V₁ (range ↑I))
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
          (↑(extChartAt I x) x))

Tactic:
mpullbackWithin_add,

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W V₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDiffAt[s] (T% V) x
hV₁ : MDiffAt[s] (T% V₁) x
hs : UniqueMDiffAt[s] x
⊢ (mfderiv% ↑(extChartAt I x) x).inverse
      (lieBracketWithin 𝕜
        (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) +
          mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V₁ (range ↑I))
        (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (↑(extChartAt I x) x)) =
    (mfderiv% ↑(extChartAt I x) x).inverse
      (lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
          (↑(extChartAt I x) x) +
        lieBracketWithin 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V₁ (range ↑I))
          (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
          (↑(extChartAt I x) x))
Module: Mathlib.Topology.Algebra.Module.TransferInstance

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : Group β
inst✝² : IsTopologicalGroup β
inst✝¹ : TopologicalSpace α
inst✝ : Group α
e : α ≃ₜ* β
f : β × β → β := fun q ↦ q.1 * q.2
this : Continuous fun p ↦ e.symm (f (e p.1, e p.2))
⊢ Continuous fun p ↦ p.1 * p.2

Tactic:
exact this.congr <| fun p ↦ by simp [f]

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

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
⊢ ∀ ⦃x_1 : EuclideanHalfSpace 1⦄,
    x_1 ∈ {z | (↑z).ofLp 0 < y - x} → ⟨toLp 2 fun x_2 ↦ ↑⟨min ((↑x_1).ofLp 0 + x) y, ⋯⟩ - x, ⋯⟩ = x_1

Tactic:
by
    rintro ⟨z, hz⟩ h'z
    rw [Subtype.mk_eq_mk]
    ext i
    dsimp at hz h'z
    have A : x + z 0 ≤ y := by linarith
    rw [Subsingleton.elim i 0]
    simp only [Fin.isValue, add_comm, A, inf_of_le_left, add_sub_cancel_left]

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

Goal state before:
pp: x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
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✝
x y : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
e e' : OpenPartialHomeomorph (↑(Icc x y)) (EuclideanHalfSpace 1)
he : e ∈ ChartedSpace.atlas
he' : e' ∈ ChartedSpace.atlas
⊢ ContDiffOn ℝ n (↑(𝓡∂ 1) ∘ ↑(e.symm ≫ₕ e') ∘ ↑(𝓡∂ 1).symm) (↑(𝓡∂ 1).symm ⁻¹' (e.symm ≫ₕ e').source ∩ range ↑(𝓡∂ 1))

Tactic:
rcases he with (rfl | rfl) <;> rcases he' with (rfl | rfl)

Goal state after:
case inl.inl
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
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✝
x y : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
⊢ ContDiffOn ℝ n (↑(𝓡∂ 1) ∘ ↑((IccLeftChart x y).symm ≫ₕ IccLeftChart x y) ∘ ↑(𝓡∂ 1).symm)
    (↑(𝓡∂ 1).symm ⁻¹' ((IccLeftChart x y).symm ≫ₕ IccLeftChart x y).source ∩ range ↑(𝓡∂ 1))

case inl.inr
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
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✝
x y : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
⊢ ContDiffOn ℝ n (↑(𝓡∂ 1) ∘ ↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) ∘ ↑(𝓡∂ 1).symm)
    (↑(𝓡∂ 1).symm ⁻¹' ((IccLeftChart x y).symm ≫ₕ IccRightChart x y).source ∩ range ↑(𝓡∂ 1))

case inr.inl
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
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✝
x y : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
⊢ ContDiffOn ℝ n (↑(𝓡∂ 1) ∘ ↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) ∘ ↑(𝓡∂ 1).symm)
    (↑(𝓡∂ 1).symm ⁻¹' ((IccRightChart x y).symm ≫ₕ IccLeftChart x y).source ∩ range ↑(𝓡∂ 1))

case inr.inr
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
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✝
x y : ℝ
inst✝ : Fact (x < y)
n : ℕ∞ω
M :
  ContDiff ℝ n
    (have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
    this)
⊢ ContDiffOn ℝ n (↑(𝓡∂ 1) ∘ ↑((IccRightChart x y).symm ≫ₕ IccRightChart x y) ∘ ↑(𝓡∂ 1).symm)
    (↑(𝓡∂ 1).symm ⁻¹' ((IccRightChart x y).symm ≫ₕ IccRightChart x y).source ∩ range ↑(𝓡∂ 1))
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
inst✝¹² : NormedAddCommGroup E'''
inst✝¹¹ : NormedSpace 𝕜 E'''
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁸ : TopologicalSpace H
G : Type u_9
inst✝⁷ : TopologicalSpace G
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f : M → N
φ : N → N'
hφ : IsImmersionAtOfComplement F J J' n φ (f x)
⊢ ContMDiffAt I J n f x ↔ ContinuousAt f x ∧ ContMDiffAt I J' n (φ ∘ f) x

Tactic:
refine ⟨fun hf ↦ ⟨hf.continuousAt, hφ.contMDiffAt.comp x hf⟩, fun ⟨hf, h'⟩ ↦ ?_⟩
  -- Since `f` is continuous at `x`, some neighbourhood `t` of `x` is mapped
  -- into `hφ.domChart.source` under `f`. By restriction, we may assume `t` is open,
  -- so it suffices to test smoothness on `t`.
  have : hφ.domChart.source ∈ 𝓝 (f x) := hφ.domChart.open_source.mem_nhds hφ.mem_domChart_source
  obtain ⟨t, ht, htopen, hxt⟩ := mem_nhds_iff.mp (hf this)
  suffices CMDiffAt[t] n f x from this.contMDiffAt <| htopen.mem_nhds hxt
  -- We test smoothness of `f` on `t` in the preferred chart at `x` and `hφ.codChart`.
  rw [contMDiffWithinAt_iff_of_mem_maximalAtlas'
    hφ.domChart_mem_maximalAtlas hφ.mem_domChart_source]
  refine ⟨hf.continuousWithinAt, ?_⟩
  exact aux hφ h' ht hxt

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

Goal state before:
pp: case e'_11
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v v' : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑v)ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
U' : ↥(ℝ ∙ ↑v')ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
H₁ : ContDiffOn ℝ ω (⇑U' ∘ stereoToFun ↑v') {x | ((innerSL ℝ) ↑v') x ≠ 1}
H₂ : ContDiff ℝ ω ((stereoInvFunAux ↑v ∘ ⇑(ℝ ∙ ↑v)ᗮ.subtypeL) ∘ ⇑U.symm)
⊢ ↑(𝓡 n).symm ⁻¹' ((stereographic' n v).symm ≫ₕ stereographic' n v').source ∩ Set.range ↑(𝓡 n) =
    Set.univ ∩ (stereoInvFunAux ↑v ∘ ⇑(ℝ ∙ ↑v)ᗮ.subtypeL) ∘ ⇑U.symm ⁻¹' {x | ((innerSL ℝ) ↑v') x ≠ 1}

Tactic:
simp only [OpenPartialHomeomorph.trans_toPartialEquiv,
        OpenPartialHomeomorph.symm_toPartialEquiv, PartialEquiv.trans_source,
        PartialEquiv.symm_source, stereographic'_target, stereographic'_source]

Goal state after:
case e'_11
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v v' : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑v)ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
U' : ↥(ℝ ∙ ↑v')ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
H₁ : ContDiffOn ℝ ω (⇑U' ∘ stereoToFun ↑v') {x | ((innerSL ℝ) ↑v') x ≠ 1}
H₂ : ContDiff ℝ ω ((stereoInvFunAux ↑v ∘ ⇑(ℝ ∙ ↑v)ᗮ.subtypeL) ∘ ⇑U.symm)
⊢ ↑(𝓡 n).symm ⁻¹' (Set.univ ∩ ↑(stereographic' n v).symm ⁻¹' {v'}ᶜ) ∩ Set.range ↑(𝓡 n) =
    Set.univ ∩ (stereoInvFunAux ↑v ∘ ⇑(ℝ ∙ ↑v)ᗮ.subtypeL) ∘ ⇑U.symm ⁻¹' {x | ((innerSL ℝ) ↑v') x ≠ 1}
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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a' b'
H : EqOn γ γ' (Ioo (max a a') (min b b'))
⊢ (Ioo a b).piecewise γ γ' t = γ' t

Tactic:
by_cases hmem : t ∈ Ioo a b
    · rw [piecewise, if_pos hmem]
      apply H
      simp [ht.1, ht.2, hmem.1, hmem.2]
    · rw [piecewise, if_neg hmem]

Goal state after:
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₀ : ℝ
inst✝ : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
⊢ EqOn γ γ' (Ioo a b)

Tactic:
by
  set s := {t | γ t = γ' t} ∩ Ioo a b with hs
  -- since `Ioo a b` is connected, we get `s = Ioo a b` by showing that `s` is clopen in `Ioo a b`
  -- in the subtype topology (`s` is also non-empty by assumption)
  -- here we use a slightly weaker alternative theorem
  suffices hsub : Ioo a b ⊆ s from fun t ht ↦ mem_ofPred.mp ((subset_def ▸ hsub) t ht).1
  apply isPreconnected_Ioo.subset_of_closure_inter_subset (s := Ioo a b) (u := s) _
    ⟨t₀, ⟨ht₀, ⟨h, ht₀⟩⟩⟩
  · -- is this really the most convenient way to pass to subtype topology?
    -- TODO: shorten this when better API around subtype topology exists
    rw [hs, inter_comm, ← Subtype.image_preimage_val, inter_comm, ← Subtype.image_preimage_val,
      image_subset_image_iff Subtype.val_injective, preimage_ofPred_eq]
    intro t ht
    rw [mem_preimage, ← closure_subtype] at ht
    revert ht t
    apply IsClosed.closure_subset (isClosed_eq _ _)
    · rw [continuous_iff_continuousAt]
      rintro ⟨_, ht⟩
      apply ContinuousAt.comp _ continuousAt_subtype_val
      rw [Subtype.coe_mk]
      exact hγ.continuousWithinAt ht |>.continuousAt (Ioo_mem_nhds ht.1 ht.2)
    · rw [continuous_iff_continuousAt]
      rintro ⟨_, ht⟩
      apply ContinuousAt.comp _ continuousAt_subtype_val
      rw [Subtype.coe_mk]
      exact hγ'.continuousWithinAt ht |>.continuousAt (Ioo_mem_nhds ht.1 ht.2)
  · rw [isOpen_iff_mem_nhds]
    intro t₁ ht₁
    have hmem := Ioo_mem_nhds ht₁.2.1 ht₁.2.2
    have heq : γ =ᶠ[𝓝 t₁] γ' := isMIntegralCurveAt_eventuallyEq_of_contMDiffAt
      (hγt _ ht₁.2) hv.contMDiffAt (hγ.isMIntegralCurveAt hmem) (hγ'.isMIntegralCurveAt hmem) ht₁.1
    apply (heq.and hmem).mono
    exact fun _ ht ↦ ht

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ≥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 ∧ Icc 0 1 ⊆ ⇑η ⁻¹' {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
η_smooth : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 (⇑η) (Icc 0 1)
this : riemannianEDist I x y ≤ pathELength I γ 0 1
⊢ pathELength I γ 0 1 ≤
    ↑C *
      ∫⁻ (t : ℝ) in Icc 0 1,
        ‖(fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap (↑(extChartAt I x) x) (↑(extChartAt I x) y))) (Icc 0 1) t) 1‖ₑ

Tactic:
pathELength_eq_lintegral_mfderivWithin_Icc,

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 ∧ Icc 0 1 ⊆ ⇑η ⁻¹' {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
η_smooth : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 (⇑η) (Icc 0 1)
this : riemannianEDist I x y ≤ pathELength I γ 0 1
⊢ ∫⁻ (t : ℝ) in Icc 0 1, ‖(mfderiv[Icc 0 1] γ t) 1‖ₑ ≤
    ↑C *
      ∫⁻ (t : ℝ) in Icc 0 1,
        ‖(fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap (↑(extChartAt I x) x) (↑(extChartAt I x) y))) (Icc 0 1) t) 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
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)
⊢ ∀ᶠ (y : M) in 𝓝 x, riemannianEDist I x y < c

Tactic:
have : (extChartAt I x) ⁻¹' (Metric.eball (extChartAt I x x) (c / C)) ∈ 𝓝 x := by
    apply (continuousAt_extChartAt x).preimage_mem_nhds
    exact Metric.eball_mem_nhds _ (ENNReal.div_pos hc.ne' (by simp))

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
c : ℝ≥0∞
hc : 0 < c
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
this : ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C) ∈ 𝓝 x
⊢ ∀ᶠ (y : M) in 𝓝 x, riemannianEDist I x y < c
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁵ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁴ : TopologicalSpace M
inst✝¹³ : ChartedSpace H M
F : Type u_5
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝¹⁰ : TopologicalSpace (TotalSpace F V)
inst✝⁹ : (x : M) → AddCommGroup (V x)
inst✝⁸ : (x : M) → Module 𝕜 (V x)
inst✝⁷ : (x : M) → TopologicalSpace (V x)
inst✝⁶ : FiberBundle F V
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
k : ℕ∞ω
x : M
inst✝² : FiniteDimensional 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : ContMDiffVectorBundle k F V I
hxe : x ∈ e.baseSet
hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) k (fun x ↦ ⟨x, s x⟩) x
i : ι
aux : M → 𝕜 := fun x ↦ (b.repr (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) i
this : ContMDiffAt I 𝓘(𝕜, 𝕜) k aux x
⊢ ContMDiffAt I 𝓘(𝕜, 𝕜) k ((LinearMap.piApply (Trivialization.localFrameCoeff I e b i)) s) x

Tactic:
apply this.congr_of_eventuallyEq ?_

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✝⁶ : 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
k : ℕ∞ω
x : M
inst✝² : FiniteDimensional 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : ContMDiffVectorBundle k F V I
hxe : x ∈ e.baseSet
hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) k (fun x ↦ ⟨x, s x⟩) x
i : ι
aux : M → 𝕜 := fun x ↦ (b.repr (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) i
this : ContMDiffAt I 𝓘(𝕜, 𝕜) k aux x
⊢ (LinearMap.piApply (Trivialization.localFrameCoeff I e b i)) s =ᶠ[𝓝 x] aux
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σσ' : ∀ x ∈ s, σ x = σ' x
⊢ cov σ x = cov σ' x

Tactic:
classical
  have hxs' : x ∈ s := mem_of_mem_nhds hxs
  let ψ (x' : M) : 𝕜 := if x' ∈ s then 1 else 0
  have hψx : ψ x = 1 := by simp [ψ, hxs']
  -- Observe that `ψ • σ = ψ • σ'` as dependent functions.
  have H (x' : M) : ((ψ : M → 𝕜) • σ) x' = ((ψ : M → 𝕜) • σ') x' := by
    dsimp [ψ]
    split_ifs with hx's
    · simpa using hσσ' _ hx's
    · simp
  have hψ' : HasMFDerivAt I 𝓘(𝕜) ψ x 0 := by
    have : HasMFDerivAt I 𝓘(𝕜, 𝕜) (fun (_x : M) ↦ (1 : 𝕜)) x 0 := hasMFDerivAt_const ..
    refine this.congr_of_eventuallyEq ?_
    apply Filter.eventuallyEq_of_mem hxs
    intro t ht
    simp [ψ, ht]
  have := hcov.leibniz hσ hψ'.mdifferentiableAt
  -- Then, it's a chain of (dependent) equalities.
  calc cov σ x
    _ = cov ((ψ : M → 𝕜) • σ) x := by
      simp [hcov.leibniz hσ hψ'.mdifferentiableAt, hψx, mvfderiv, hψ'.mfderiv]
    _ = cov ((ψ : M → 𝕜) • σ') x := by rw [funext H]
    _ = cov σ' x := by
      simp [hcov.leibniz hσ' hψ'.mdifferentiableAt, hψx, mvfderiv, hψ'.mfderiv]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ orderOf (r 1) / (orderOf (r 1)).gcd i.val = n / n.gcd i.val

Tactic:
orderOf_r_one

Goal state after:
n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ n / n.gcd i.val = n / n.gcd i.val
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inr.a.hab
n : ℕ
hn : NeZero n
⊢ n ∣ Monoid.exponent (DihedralGroup n)

pp: case hcb
n : ℕ
hn : NeZero n
⊢ 2 ∣ Monoid.exponent (DihedralGroup n)

Tactic:
· convert! Monoid.order_dvd_exponent (r (1 : ZMod n))
      exact orderOf_r_one.symm

Goal state after:
case hcb
n : ℕ
hn : NeZero n
⊢ 2 ∣ Monoid.exponent (DihedralGroup n)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
⊢ IsMulCommutative (DihedralGroup n) → n = 1 ∨ n = 2

Tactic:
contrapose!; rintro ⟨h1, h2⟩; exact not_commutative h1 h2

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

Goal state before:
pp: case of_mul.inl
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
motive : M ∗ N → Prop
one : motive 1
inl_mul : ∀ (m : M) (x : M ∗ N), motive x → motive (inl m * x)
inr_mul : ∀ (n : N) (x : M ∗ N), motive x → motive (inr n * x)
xs : FreeMonoid (M ⊕ N)
ih : motive (mk xs)
m : M
⊢ motive (mk (of (Sum.inl m) * xs))

Tactic:
simpa using inl_mul m _ ih

Goal state after: