mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
n : ℕ
inst✝¹ : NeZero n
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i : Fin (n + 1)
⊢ (Finset.affineCombination ℝ Finset.univ s.points) (s.touchpointWeights {i} i) ∈ (s.face ⋯).interior

Tactic:
s.affineCombination_mem_interior_face_iff_pos _ (s.sum_touchpointWeights _ _)

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
n : ℕ
inst✝¹ : NeZero n
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i : Fin (n + 1)
⊢ (∀ i_1 ∈ {i}ᶜ, 0 < s.touchpointWeights {i} i i_1) ∧ ∀ i_1 ∉ {i}ᶜ, s.touchpointWeights {i} i i_1 = 0
Module: Mathlib.Geometry.Euclidean.Congruence

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
h : ¬Collinear ℝ {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist c' a'
h' : ¬Collinear ℝ {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
⊢ ¬Collinear ℝ {b, c, a}

Tactic:
rwa [Set.insert_comm, Set.pair_comm] at h

Goal state after:
Module: Mathlib.Geometry.Euclidean.NinePointCircle

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ n = m

Tactic:
simpa using Fin.equiv_iff_eq.mp ⟨e⟩

Goal state after:
Module: Mathlib.Geometry.Euclidean.NinePointCircle

Goal state before:
pp: case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : ↑(n - 1) = ↑n - 1
⊢ ⅟2 •
      ((↑n)⁻¹ • (s.centroid -ᵥ s.circumcenter) +
        (s.centroid -ᵥ s.circumcenter + (↑(n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter))) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)

Tactic:
← add_assoc

Goal state after:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : ↑(n - 1) = ↑n - 1
⊢ ⅟2 •
      ((↑n)⁻¹ • (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) +
        (↑(n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (vectorSpan ℝ (Set.range s.points))ᗮ
hu : ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x ↦ s.points i₁ -ᵥ x) '' s.points '' (Set.univ \ {i₁})
hv : p -ᵥ s.mongePoint ∈ vectorSpan ℝ (Set.range s.points)
⊢ p -ᵥ s.mongePoint = 0

Tactic:
exact Submodule.disjoint_def.1 (vectorSpan ℝ (Set.range s.points)).orthogonal_disjoint _ hv hi

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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
n : WithTop ℕ∞
inst✝ : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : e ∈ atlas H M
he' : e' ∈ atlas H M
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : ↑(e.extend I) x ∈ interior (e.extend I).target
⊢ ↑(e'.extend I) x ∈ interior (e'.extend I).target

Tactic:
by
  /- Since transition maps are diffeomorphisms, it suffices to show that if `e'` were to send `x`
  to the boundary of `range I`, the differential of the transition map `φ` from `e` to `e'` at `x`
  could not be surjective. -/
  let φ := I.extendCoordChange e e'
  have hφ : ContDiffOn 𝕜 n φ φ.source := contDiffOn_extendCoordChange
    (IsManifold.subset_maximalAtlas he) (IsManifold.subset_maximalAtlas he')
  suffices h : Function.Surjective (fderivWithin 𝕜 φ φ.source (e.extend I x)) →
      e'.extend I x ∈ interior (range I) by
    refine e'.mem_interior_extend_target (by simp [hex']) <| h ?_
    exact (isInvertible_fderivWithin_extendCoordChange hn (IsManifold.subset_maximalAtlas he)
      (IsManifold.subset_maximalAtlas he') <| by simp [hex, hex']).surjective
  intro hφx'
  /- Reduce the situation to the real case, then apply
  `DifferentiableAt.mem_interior_convex_of_surjective_fderiv`. -/
  wlog _ : IsRCLikeNormedField 𝕜
  · simp [I.range_eq_univ_of_not_isRCLikeNormedField ‹_›]
  let _ := IsRCLikeNormedField.rclike 𝕜
  let _ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
  have hφx : φ.source ∈ 𝓝 (e.extend I x) := by
    simp_rw [φ, extendCoordChange, PartialEquiv.trans_source, PartialEquiv.symm_source,
      Filter.inter_mem_iff, mem_interior_iff_mem_nhds.1 hx, true_and, e'.extend_source]
    exact e.extend_preimage_mem_nhds hex <| e'.open_source.mem_nhds hex'
  rw [← ContinuousLinearMap.coe_restrictScalars' (R := ℝ),
    (hφ.differentiableOn hn _ (by simp [φ, hex, hex'])).restrictScalars_fderivWithin (𝕜 := ℝ)
      (uniqueDiffWithinAt_of_mem_nhds hφx), fderivWithin_of_mem_nhds <| hφx] at hφx'
  rw [show e'.extend I x = φ (e.extend I x) by simp [φ, hex]]
  replace hφ := ((hφ.restrict_scalars ℝ).differentiableOn hn).differentiableAt hφx
  exact hφ.mem_interior_convex_of_surjective_fderiv hφx I.convex_range I.isClosed_range
    I.nonempty_interior (φ.mapsTo.mono_right <| by simp [φ, inter_assoc]) hφx'

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : IsManifold I 1 M
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)
x₀ x : N
hx : f x ∈ (chartAt H (f x₀)).source
hy : g x ∈ (chartAt H' (g x₀)).source
⊢ inTangentCoordinates I I' f g ϕ x₀ x =
    mfderiv% ↑(extChartAt I' (g x₀)) (g x) ∘SL
      ϕ x ∘SL mfderiv[range ↑I] ↑(extChartAt I (f x₀)).symm (↑(extChartAt I (f x₀)) (f x))

Tactic:
inTangentCoordinates_eq _ _ _ hx hy,

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
inst✝⁶ : IsManifold I 1 M
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)
x₀ x : N
hx : f x ∈ (chartAt H (f x₀)).source
hy : g x ∈ (chartAt H' (g x₀)).source
⊢ (tangentBundleCore I' M').coordChange (achart H' (g x)) (achart H' (g x₀)) (g x) ∘SL
      ϕ x ∘SL (tangentBundleCore I M).coordChange (achart H (f x₀)) (achart H (f x)) (f x) =
    mfderiv% ↑(extChartAt I' (g x₀)) (g x) ∘SL
      ϕ x ∘SL mfderiv[range ↑I] ↑(extChartAt I (f x₀)).symm (↑(extChartAt I (f x₀)) (f x))
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
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3
fg : G → TangentBundle I G := fun g ↦ ⟨g, 0⟩
sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
fv : G → TangentBundle I G := fun x ↦ ⟨1, v⟩
sfv : ContMDiff I I.tangent (minSmoothness 𝕜 2) fv
F₁ : G → TangentBundle I G × TangentBundle I G := fun g ↦ (fg g, fv g)
S₁ : ContMDiff I (I.tangent.prod I.tangent) (minSmoothness 𝕜 2) F₁
⊢ ContMDiff I I.tangent (minSmoothness 𝕜 2) fun g ↦ ⟨g, mulInvariantVectorField v g⟩

Tactic:
let F₂ : (TangentBundle I G × TangentBundle I G) → TangentBundle (I.prod I) (G × G) :=
    (equivTangentBundleProd I G I G).symm

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
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3
fg : G → TangentBundle I G := fun g ↦ ⟨g, 0⟩
sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
fv : G → TangentBundle I G := fun x ↦ ⟨1, v⟩
sfv : ContMDiff I I.tangent (minSmoothness 𝕜 2) fv
F₁ : G → TangentBundle I G × TangentBundle I G := fun g ↦ (fg g, fv g)
S₁ : ContMDiff I (I.tangent.prod I.tangent) (minSmoothness 𝕜 2) F₁
F₂ : TangentBundle I G × TangentBundle I G → TangentBundle (I.prod I) (G × G) := ⇑(equivTangentBundleProd I G I G).symm
⊢ ContMDiff I I.tangent (minSmoothness 𝕜 2) fun g ↦ ⟨g, mulInvariantVectorField v g⟩
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
⊢ IsOpen {z | (↑z).ofLp 0 < y - x}

Tactic:
by
    have : IsOpen { z : ℝ | z < y - x } := isOpen_Iio
    have : IsOpen { z : EuclideanSpace ℝ (Fin 1) | z 0 < y - x } :=
      this.preimage (@PiLp.continuous_apply 2 (Fin 1) (fun _ ↦ ℝ) _ 0)
    exact this.preimage continuous_subtype_val

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

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
⊢ ↑((IccRightChart x y).extend (𝓡∂ 1)) ⊤ = 0

Tactic:
norm_num [IccRightChart, modelWithCornersEuclideanHalfSpace_zero]
  congr

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

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
⊢ ↑((chartAt (EuclideanHalfSpace 1) ⊤).extend (𝓡∂ 1)) ⊤ ∈ frontier (range ↑(𝓡∂ 1))

Tactic:
Icc_chartedSpaceChartAt_of_top_le (by simp)

Goal state after:
x y : ℝ
hxy : Fact (x < y)
⊢ ↑((IccRightChart x y).extend (𝓡∂ 1)) ⊤ ∈ frontier (range ↑(𝓡∂ 1))
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : x < ↑p ∧ ↑p < y
⊢ (𝓡∂ 1).IsInteriorPoint p

Tactic:
rw [ModelWithCorners.IsInteriorPoint, extChartAt, Icc_chartedSpaceChartAt_of_le_top hp.2,
    interior_range_modelWithCornersEuclideanHalfSpace]

Goal state after:
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : x < ↑p ∧ ↑p < y
⊢ ↑((IccLeftChart x y).extend (𝓡∂ 1)) p ∈ {y | 0 < y.ofLp 0}
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)ᗮ
h₁ : (ℝ ∙ v)ᗮ.orthogonalProjectionOnto v = 0
⊢ (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • ⟪v, ↑w⟫ + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • ⟪v, v⟫))) • (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • ⟪v, ↑w⟫ + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • ⟪v, v⟫))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto v =
    w

Tactic:
have h₂ : ⟪v, w⟫ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
w : ↥(ℝ ∙ v)ᗮ
h₁ : (ℝ ∙ v)ᗮ.orthogonalProjectionOnto v = 0
h₂ : ⟪v, ↑w⟫ = 0
⊢ (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • ⟪v, ↑w⟫ + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • ⟪v, v⟫))) • (‖↑w‖ ^ 2 + 4)⁻¹ • 4 • w +
      (2 / (1 - ((‖↑w‖ ^ 2 + 4)⁻¹ • 4 • ⟪v, ↑w⟫ + (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • ⟪v, v⟫))) •
        (‖↑w‖ ^ 2 + 4)⁻¹ • (‖↑w‖ ^ 2 - 4) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto v =
    w
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
⊢ ⇑(equivTangentBundleProd I M I' M') = fun p ↦
    (tangentMap (I.prod I') I Prod.fst p, tangentMap (I.prod I') I' Prod.snd p)

Tactic:
by
  simp only [tangentMap_prodFst, tangentMap_prodSnd]; rfl

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
⊢ ContMDiffAt (I.tangent.prod I'.tangent) (I.prod I').tangent n ⇑(equivTangentBundleProd I M I' M').symm (a, b)

Tactic:
contMDiffAt_totalSpace

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
⊢ ContMDiffAt (I.tangent.prod I'.tangent) (I.prod I') n (fun x ↦ ((equivTangentBundleProd I M I' M').symm x).proj)
      (a, b) ∧
    ContMDiffAt (I.tangent.prod I'.tangent) 𝓘(𝕜, E × E') n
      (fun x ↦
        (↑(trivializationAt (E × E') (TangentSpace (I.prod I')) ((equivTangentBundleProd I M I' M').symm (a, b)).proj)
            ((equivTangentBundleProd I M I' M').symm x)).2)
      (a, b)
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
⊢ ∀ (x y : M), riemannianEDist I y x ≤ riemannianEDist I x y

Tactic:
intro x y

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✝ x y : M
⊢ riemannianEDist I y x ≤ riemannianEDist I x y
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: case ha
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 z : M
r : ℝ≥0∞
hr : riemannianEDist I x y + riemannianEDist I y z < r
u : ℝ≥0∞
hu : u > riemannianEDist I x y
v : ℝ≥0∞
hv : v > riemannianEDist I y z
huv : u + v < r
γ₁ : ℝ → M
hγ₁0 : γ₁ 0 = x
hγ₁1 : γ₁ 1 = y
hγ₁_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₁
hγ₁ : pathELength I γ₁ 0 1 < u
hγ₁_const : γ₁ =ᶠ[𝓝 1] fun x ↦ y
γ₂ : ℝ → M
hγ₂1 : γ₂ 1 = y
hγ₂2 : γ₂ 2 = z
hγ₂_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₂
hγ₂ : pathELength I γ₂ 1 2 < v
hγ₂_const : γ₂ =ᶠ[𝓝 1] fun x ↦ y
γ : ℝ → M := ⋯
⊢ γ 0 = x

Tactic:
simp [γ, hγ₁0]

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 z : M
r : ℝ≥0∞
hr : riemannianEDist I x y + riemannianEDist I y z < r
u : ℝ≥0∞
hu : u > riemannianEDist I x y
v : ℝ≥0∞
hv : v > riemannianEDist I y z
huv : u + v < r
γ₁ : ℝ → M
hγ₁0 : γ₁ 0 = x
hγ₁1 : γ₁ 1 = y
hγ₁_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₁
hγ₁ : pathELength I γ₁ 0 1 < u
hγ₁_const : γ₁ =ᶠ[𝓝 1] fun x ↦ y
γ₂ : ℝ → M
hγ₂1 : γ₂ 1 = y
hγ₂2 : γ₂ 2 = z
hγ₂_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₂
hγ₂ : pathELength I γ₂ 1 2 < v
hγ₂_const : γ₂ =ᶠ[𝓝 1] fun x ↦ y
γ : ℝ → M := (Iic 1).piecewise γ₁ γ₂
this : riemannianEDist I x z ≤ pathELength I γ 0 2
⊢ pathELength I γ 1 2 = pathELength I γ₂ 1 2

Tactic:
apply pathELength_congr_Ioo

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 z : M
r : ℝ≥0∞
hr : riemannianEDist I x y + riemannianEDist I y z < r
u : ℝ≥0∞
hu : u > riemannianEDist I x y
v : ℝ≥0∞
hv : v > riemannianEDist I y z
huv : u + v < r
γ₁ : ℝ → M
hγ₁0 : γ₁ 0 = x
hγ₁1 : γ₁ 1 = y
hγ₁_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₁
hγ₁ : pathELength I γ₁ 0 1 < u
hγ₁_const : γ₁ =ᶠ[𝓝 1] fun x ↦ y
γ₂ : ℝ → M
hγ₂1 : γ₂ 1 = y
hγ₂2 : γ₂ 2 = z
hγ₂_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ₂
hγ₂ : pathELength I γ₂ 1 2 < v
hγ₂_const : γ₂ =ᶠ[𝓝 1] fun x ↦ y
γ : ℝ → M := ⋯
this : riemannianEDist I x z ≤ pathELength I γ 0 2
⊢ EqOn γ γ₂ (Ioo 1 2)
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
F' : Type u_6
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✝⁷ : 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
e : F ≃L[𝕜] F'
⊢ IsSubmersionAtOfComplement F' I J n f x

Tactic:
refine ⟨h.domChart, h.codChart, h.mem_domChart_source, h.mem_codChart_source,
    h.domChart_mem_maximalAtlas, h.codChart_mem_maximalAtlas, h.source_subset_preimage_source, ?_⟩
  use h.equiv.trans ((ContinuousLinearEquiv.refl 𝕜 E'').prodCongr e)
  apply Set.EqOn.trans h.writtenInCharts
  intro x hx
  simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
F : Type u_5
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
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
s : (x : M) → V x
hxe : x ∈ e.baseSet
i : ι
⊢ (localFrameCoeff I e b i x) (s x) = (b.repr (↑e ((fun x ↦ ⟨x, s x⟩) x)).2) i

Tactic:
simp [e.localFrameCoeff_apply_of_mem_baseSet b hxe, basisAt]

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

Goal state before:

Tactic:
‖γ' t₁ - γ' 0‖ₑ
    _ ≤ ∫⁻ t' in Icc 0 t₁, ‖derivWithin γ' (Icc 0 t₁) t'‖ₑ := by
      apply enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc _ ht₁0
      rwa [← contMDiffOn_iff_contDiffOn]
    _ = ∫⁻ t' in Icc 0 t₁, ‖mfderiv[Icc 0 t₁] γ' t' 1‖ₑ := by
      simp_rw [← fderivWithin_derivWithin, mfderivWithin_eq_fderivWithin]
      rfl
    _ ≤ ∫⁻ t' in Icc 0 t₁, C * ‖mfderiv[Icc 0 t₁] γ t' 1‖ₑ := by
      apply setLIntegral_mono' measurableSet_Icc (fun t' ht' ↦ ?_)
      have : mfderiv[Icc 0 t₁] γ' t' =
          (mfderiv% (extChartAt I x) (γ t')) ∘L (mfderiv[Icc 0 t₁] γ t') := by
        apply mfderiv_comp_mfderivWithin
        · refine mdifferentiableAt_extChartAt (uc' ?_)
          apply t₁_mem ht'
        · exact (γ_smooth.mdifferentiable one_ne_zero).mdifferentiableOn _ ht'
        · rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
          exact uniqueDiffOn_Icc h't' _ ht'
      have : mfderiv[Icc 0 t₁] γ' t' 1 =
          (mfderiv% (extChartAt I x) (γ t')) (mfderiv[Icc 0 t₁] γ t' 1) :=
        congr($this 1)
      rw [this]
      apply (ContinuousLinearMap.le_opENorm _ _).trans
      gcongr
      refine (hu ?_).le
      apply t₁_mem ht'
    _ = C * pathELength I γ 0 t₁ := by
      rw [lintegral_const_mul' _ _ ENNReal.coe_ne_top,
          pathELength_eq_lintegral_mfderivWithin_Icc]
    _ ≤ C * pathELength I γ 0 1 := by
      gcongr
    _ < C * (r / C) := by
      gcongr
      · exact ENNReal.coe_ne_top
      · exact hγ.trans_eq (ENNReal.coe_div C_pos.ne')
    _ = r := (ENNReal.eq_div_iff (by simpa using C_pos.ne') ENNReal.coe_ne_top).mp rfl

Goal state after: