mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : NormedAddCommGroup F
inst✝¹⁸ : NormedSpace 𝕜 F
inst✝¹⁷ : TopologicalSpace (TotalSpace F E)
inst✝¹⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁵ : NormedAddCommGroup EB
inst✝¹⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst✝¹² : NormedAddCommGroup EM
inst✝¹¹ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝¹⁰ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace HM M
inst✝⁷ : TopologicalSpace B
inst✝⁶ : ChartedSpace HB B
inst✝⁵ : FiberBundle F E
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle 1 F E IB
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
f : M → TotalSpace F E
x₀ : M
he : f x₀ ∈ e.source
hf : (MDiffAt fun x ↦ (f x).proj) x₀
⊢ (MDiffAt fun x ↦ (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀ ↔ (MDiffAt fun x ↦ (↑e (f x)).2) x₀

Tactic:
rw [Trivialization.mdifferentiableAt_snd_comp_iff₂ IB
    (FiberBundle.mem_trivializationAt_proj_source) he hf]

Goal state after:
Module: Mathlib.Topology.VectorBundle.Hom

Goal state before:
pp: 𝕜₁ : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝²⁰ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝¹⁹ : NormedAddCommGroup F₁
inst✝¹⁸ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁷ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁶ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹⁵ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹⁴ : NormedAddCommGroup F₂
inst✝¹³ : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝¹² : (x : B) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : TopologicalSpace B
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁸ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁷ : FiberBundle F₁ E₁
inst✝⁶ : VectorBundle 𝕜₁ F₁ E₁
inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
inst✝³ : VectorBundle 𝕜₂ F₂ E₂
inst✝² : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝¹ : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)
inst✝ : RingHomIsometric σ
b : B
⊢ IsInducing (↑(continuousLinearMap σ (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) ∘ TotalSpace.mk b)

Tactic:
let L₁ : E₁ b ≃L[𝕜₁] F₁ :=
      (trivializationAt F₁ E₁ b).continuousLinearEquivAt 𝕜₁ b
        (mem_baseSet_trivializationAt _ _ _)

Goal state after:
𝕜₁ : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝²⁰ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝¹⁹ : NormedAddCommGroup F₁
inst✝¹⁸ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁷ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁶ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹⁵ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹⁴ : NormedAddCommGroup F₂
inst✝¹³ : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝¹² : (x : B) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : TopologicalSpace B
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁸ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁷ : FiberBundle F₁ E₁
inst✝⁶ : VectorBundle 𝕜₁ F₁ E₁
inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
inst✝³ : VectorBundle 𝕜₂ F₂ E₂
inst✝² : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝¹ : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)
inst✝ : RingHomIsometric σ
b : B
L₁ : E₁ b ≃L[𝕜₁] F₁ := Trivialization.continuousLinearEquivAt 𝕜₁ (trivializationAt F₁ E₁ b) b ⋯
⊢ IsInducing (↑(continuousLinearMap σ (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) ∘ TotalSpace.mk b)
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

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
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : LieGroup I (minSmoothness 𝕜 3) G
g h : G
M : minSmoothness 𝕜 3 ≠ 0
A : (mfderiv% fun x ↦ g⁻¹ * x) (g * h) ∘SL (mfderiv% fun x ↦ g * x) h = ContinuousLinearMap.id 𝕜 (TangentSpace I h)
A' :
  (mfderiv% fun x ↦ g * x) (g⁻¹ * (g * h)) ∘SL (mfderiv% fun x ↦ g⁻¹ * x) (g * h) =
    ContinuousLinearMap.id 𝕜 (TangentSpace I (g * h))
⊢ ((mfderiv% fun b ↦ g * b) h).inverse = (mfderiv% fun b ↦ g⁻¹ * b) (g * h)

Tactic:
inv_mul_cancel_left g h

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
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : LieGroup I (minSmoothness 𝕜 3) G
g h : G
M : minSmoothness 𝕜 3 ≠ 0
A : (mfderiv% fun x ↦ g⁻¹ * x) (g * h) ∘SL (mfderiv% fun x ↦ g * x) h = ContinuousLinearMap.id 𝕜 (TangentSpace I h)
A' :
  (mfderiv% fun x ↦ g * x) h ∘SL (mfderiv% fun x ↦ g⁻¹ * x) (g * h) = ContinuousLinearMap.id 𝕜 (TangentSpace I (g * h))
⊢ ((mfderiv% fun b ↦ g * b) h).inverse = (mfderiv% fun b ↦ g⁻¹ * b) (g * h)
Module: Mathlib.Geometry.Manifold.VectorField.Pullback

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
H' : Type u_5
inst✝⁷ : TopologicalSpace H'
E' : Type u_6
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H' M'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
hV : ContMDiffWithinAt I' I'.tangent m (fun x ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderiv[s] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := id
v : (x : M) → TangentSpace I' (f x) := V ∘ f
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := fun x ↦ (mfderiv[s] f x).inverse
⊢ ContMDiffWithinAt I I'.tangent m (fun x ↦ ⟨f x, v x⟩) (s ∩ f ⁻¹' t) x₀

Tactic:
apply hV.comp x₀ ((hf.of_le (le_trans (le_self_add) hmn)).mono inter_subset_left)

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
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'
f : M → M'
s : Set M
x₀ : M
V : (x : M') → TangentSpace I' x
m n : ℕ∞ω
t : Set M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
hV : ContMDiffWithinAt I' I'.tangent m (fun x ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderiv[s] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : m + 1 ≤ n
b₁ : M → M' := f
b₂ : M → M := ⋯
v : (x : M) → TangentSpace I' (f x) := ⋯
ϕ : (x : M) → TangentSpace I' (f x) →L[𝕜] TangentSpace I x := ⋯
⊢ MapsTo f (s ∩ f ⁻¹' t) t
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
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hV : (MDiffAt[s] fun x ↦ ⟨x, V x⟩) x
hs : UniqueMDiffAt[s] x
⊢ (-mlieBracketWithin I W (f • V) s) x = -(d[s] f x) (W x) • V x + f x • mlieBracketWithin I V W s x

Tactic:
Pi.neg_apply,

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 : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hV : (MDiffAt[s] fun x ↦ ⟨x, V x⟩) x
hs : UniqueMDiffAt[s] x
⊢ -mlieBracketWithin I W (f • V) s x = -(d[s] f x) (W x) • V x + f x • mlieBracketWithin I V W s x
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDiffAt[s] (T% W) x
hW₁ : MDiffAt[s] (T% W₁) x
hs : UniqueMDiffAt[s] x
⊢ (-mlieBracketWithin I (W + W₁) V s) x = mlieBracketWithin I V W s x + mlieBracketWithin I V W₁ s x

Tactic:
Pi.neg_apply,

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 W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDiffAt[s] (T% W) x
hW₁ : MDiffAt[s] (T% W₁) x
hs : UniqueMDiffAt[s] x
⊢ -mlieBracketWithin I (W + W₁) V s x = mlieBracketWithin I V W s x + mlieBracketWithin I V W₁ s x
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDiffAt[s] (T% W) x
hW₁ : MDiffAt[s] (T% W₁) x
hs : UniqueMDiffAt[s] x
⊢ -(mlieBracketWithin I W V s x + mlieBracketWithin I W₁ V s x) =
    (-mlieBracketWithin I W V s) x + (-mlieBracketWithin I W₁ V s) x

Tactic:
Pi.neg_apply,

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 W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDiffAt[s] (T% W) x
hW₁ : MDiffAt[s] (T% W₁) x
hs : UniqueMDiffAt[s] x
⊢ -(mlieBracketWithin I W V s x + mlieBracketWithin I W₁ V s x) =
    -mlieBracketWithin I W V s x + (-mlieBracketWithin I W₁ V s) x
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: n : ℕ
⊢ (interior {y | ∀ (i : Fin n), 0 ≤ y.ofLp i}).Nonempty

Tactic:
interior_euclideanQuadrant

Goal state after:
n : ℕ
⊢ {y | ∀ (i : Fin n), 0 < y.ofLp i}.Nonempty
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: case pos
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ↑z < y
⊢ z ∈ (if ↑z < y then IccLeftChart x y else IccRightChart x y).source

Tactic:
simp only [h', if_true]

Goal state after:
case pos
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ↑z < y
⊢ z ∈ (IccLeftChart x y).source
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
⊢ v ∈ sphere 0 1

Tactic:
by simp [hv]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
⊢ v ∈ sphere 0 1

Tactic:
by simp [hv]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
x : ↑(sphere 0 1)
hx : x ∈ {⟨v, ⋯⟩}ᶜ
h : ↑x = v
⊢ x ∈ {⟨v, ⋯⟩}

Tactic:
rw [← h] at hv
    apply Subtype.ext
    dsimp
    exact h

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 y : ℝ
hlt : a < y
γ : ℝ → M
hγ1 : γ 0 = x
hγ2 : IsMIntegralCurveOn γ v (Ioo (-y) y)
⊢ ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)

Tactic:
exact ⟨γ, hγ1, hγ2.mono <| Ioo_subset_Ioo (neg_le_neg hlt.le) hlt.le⟩

Goal state after:
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)
a b c : ℝ
γ : ℝ → M
h : a ≤ b
h' : b ≤ c
⊢ pathELength I γ a b + pathELength I γ b c = pathELength I γ a c

Tactic:
symm
  have : Icc a c = Icc a b ∪ Ioc b c := (Icc_union_Ioc_eq_Icc h h').symm
  rw [pathELength, this, lintegral_union measurableSet_Ioc]; swap
  · exact disjoint_iff_forall_ne.mpr (fun a ha b hb ↦ (ha.2.trans_lt hb.1).ne)
  simp [restrict_Ioc_eq_restrict_Icc, pathELength]

Goal state after:
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)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f a) (f b)

Tactic:
rcases h.eq_or_lt with rfl | h
  · simp
  have f_im : f '' (Icc a b) = Icc (f a) (f b) := h'f.continuousOn.image_Icc_of_monotoneOn h.le hf
  simp only [pathELength_eq_lintegral_mfderivWithin_Icc, ← f_im]
  have B (t) (ht : t ∈ Icc a b) : HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t :=
    (h'f t ht).hasDerivWithinAt
  rw [lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn measurableSet_Icc B hf]
  apply setLIntegral_congr_fun measurableSet_Icc (fun t ht ↦ ?_)
  have : (mfderiv[Icc a b] (γ ∘ f) t) =
      (mfderiv[Icc (f a) (f b)] γ (f t)) ∘L mfderiv[Icc a b] f t := by
    rw [← f_im] at hγ ⊢
    apply mfderivWithin_comp
    · apply hγ _ (mem_image_of_mem _ ht)
    · rw [mdifferentiableWithinAt_iff_differentiableWithinAt]
      exact h'f _ ht
    · exact subset_preimage_image _ _
    · rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
      exact uniqueDiffOn_Icc h _ ht
  rw [this]
  simp only [Function.comp_apply, ContinuousLinearMap.comp_apply]
  have : mfderiv[Icc a b] f t 1 = derivWithin f (Icc a b) t • (1 : TangentSpace% (f t)) := by
    simp only [mfderivWithin_eq_fderivWithin, ← fderivWithin_derivWithin, smul_eq_mul, mul_one]
    rfl
  rw [this]
  have : 0 ≤ derivWithin f (Icc a b) t := hf.derivWithin_nonneg
  simp only [map_smul, enorm_smul, ← Real.enorm_of_nonneg this, f_im]

Goal state after:
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
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
⊢ ContMDiff (𝓡∂ 1) I 1 f

Tactic:
← contMDiffOn_comp_projIcc_iff

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
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
⊢ ContMDiffOn 𝓘(ℝ, ℝ) I 1 (f ∘ projIcc 0 1 ⋯) (Icc 0 1)
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: case mpr.refine_2.refine_1
𝕜 : 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
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
V : Opens M
hUV : V ≤ U
hV₀f : ∀ y ∈ Set.range (Set.inclusion hUV), f y ≠ 0
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion hUV))
hxV₀ : ⟨x, hxU⟩ ∈ Set.range (Set.inclusion hUV)
hxV : x ∈ ↑V
hVf : ∀ (y : ↥V), f (Set.inclusion hUV y) ≠ 0
g : C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯ := ⟨(⇑f ∘ Set.inclusion hUV)⁻¹, ?mpr.refine_1⟩
⊢ (CategoryTheory.ConcreteCategory.hom (S.germ V x hxV)) ((ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV) f * g) = 1

Tactic:
convert! RingHom.map_one _

Goal state after:
case e'_2.e'_6
𝕜 : 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
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
V : Opens M
hUV : V ≤ U
hV₀f : ∀ y ∈ Set.range (Set.inclusion hUV), f y ≠ 0
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion hUV))
hxV₀ : ⟨x, hxU⟩ ∈ Set.range (Set.inclusion hUV)
hxV : x ∈ ↑V
hVf : ∀ (y : ↥V), f (Set.inclusion hUV y) ≠ 0
g : C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯ := ⟨(⇑f ∘ Set.inclusion hUV)⁻¹, ?mpr.refine_1⟩
⊢ (ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV) f * g = 1
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: case mpr.refine_2.refine_2
𝕜 : 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
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
V : Opens M
hUV : V ≤ U
hV₀f : ∀ y ∈ Set.range (Set.inclusion hUV), f y ≠ 0
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion hUV))
hxV₀ : ⟨x, hxU⟩ ∈ Set.range (Set.inclusion hUV)
hxV : x ∈ ↑V
hVf : ∀ (y : ↥V), f (Set.inclusion hUV y) ≠ 0
g : C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯ := ⟨(⇑f ∘ Set.inclusion hUV)⁻¹, ?mpr.refine_1⟩
⊢ (CategoryTheory.ConcreteCategory.hom (S.germ V x hxV)) (g * (ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV) f) = 1

Tactic:
convert! RingHom.map_one _

Goal state after:
case e'_2.e'_6
𝕜 : 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
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
V : Opens M
hUV : V ≤ U
hV₀f : ∀ y ∈ Set.range (Set.inclusion hUV), f y ≠ 0
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion hUV))
hxV₀ : ⟨x, hxU⟩ ∈ Set.range (Set.inclusion hUV)
hxV : x ∈ ↑V
hVf : ∀ (y : ↥V), f (Set.inclusion hUV y) ≠ 0
g : C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯ := ⟨(⇑f ∘ Set.inclusion hUV)⁻¹, ?mpr.refine_1⟩
⊢ g * (ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV) f = 1
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
⊢ ContMDiffAt I 𝓘(𝕜, 𝕜) k (fun x ↦ (b.repr (↑e ⟨x, s x⟩).2) i) x

Tactic:
have h₁ : CMDiffAt k (fun x ↦ (e ((T% s) x)).2) x := by
    simpa using (e.contMDiffAt_section_iff hxe).1 hs

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
h₁ : ContMDiffAt I 𝓘(𝕜, F) k (fun x ↦ (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) x
⊢ ContMDiffAt I 𝓘(𝕜, 𝕜) k (fun x ↦ (b.repr (↑e ⟨x, s x⟩).2) i) x
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case succ
n : ℕ
i : ZMod n
k : ℕ
IH : r i ^ k = r (i * ↑k)
⊢ r i ^ (k + 1) = r (i * ↑(k + 1))

Tactic:
rw [pow_add, pow_one, IH, r_mul_r, Nat.cast_add, Nat.cast_one, r.injEq, mul_add, mul_one]

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

Goal state before:
pp: n : ℕ
k : ℤ
⊢ r 1 ^ k = r ↑k

Tactic:
by
  simp only [r_zpow, one_mul]

Goal state after: