mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
⊢ Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) ≤ Real.cos (angle x z)

Tactic:
← inner_eq_cos_angle_of_norm_eq_one hx hz,

Goal state after:
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x y + angle y z ≤ π
H1 :
  ⟪x, z⟫ =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
⊢ Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) ≤ ⟪x, z⟫
Module: Mathlib.Geometry.Euclidean.Simplex

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
t : Triangle ℝ P
x✝ :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
⊢ Simplex.AcuteAngled t

Tactic:
have h102 := angle_comm (t.points 2) _ _ ▸ h201

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
x✝ :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
⊢ Simplex.AcuteAngled t
Module: Mathlib.Geometry.Euclidean.MongePoint

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 : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
⊢ -(∑ i,
            ∑ i₂_1,
              (if i = i₁ ∨ i = i₂ then (↑(n + 1))⁻¹ else 0) *
                  (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
                (dist (s.points i) (s.pointsWithCircumcenter i₂_1) *
                  dist (s.points i) (s.pointsWithCircumcenter i₂_1)) +
          ∑ i₂_1,
            -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
              (dist s.circumcenter (s.pointsWithCircumcenter i₂_1) *
                dist s.circumcenter (s.pointsWithCircumcenter i₂_1))) /
      2 =
    0

Tactic:
(Tactic.tacticLet__
 "let"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId `fs)
   []
   [(Term.typeSpec
     ":"
     (Term.app
      `Finset
      [(Term.paren
        (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
        (Term.app
         `Fin
         [(Term.paren (Term.hygienicLParen "(" (hygieneInfo `[anonymous])) («term_+_» `n "+" (num "3")) ")")])
        ")")]))]
   ":="
   (choice
    («term{_}» "{" [`i₁ "," `i₂] "}")
    (Term.structInst
     "{"
     []
     (Term.structInstFields
      [(Term.structInstField (Term.structInstLVal `i₁ []) [])
       ","
       (Term.structInstField (Term.structInstLVal `i₂ []) [])])
     (Term.optEllipsis [])
     []
     "}")))))

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 : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
⊢ -(∑ i,
            ∑ i₂_1,
              (if i = i₁ ∨ i = i₂ then (↑(n + 1))⁻¹ else 0) *
                  (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
                (dist (s.points i) (s.pointsWithCircumcenter i₂_1) *
                  dist (s.points i) (s.pointsWithCircumcenter i₂_1)) +
          ∑ i₂_1,
            -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
              (dist s.circumcenter (s.pointsWithCircumcenter i₂_1) *
                dist s.circumcenter (s.pointsWithCircumcenter i₂_1))) /
      2 =
    0
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₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ ∀ x ∈ univ,
    x ∉ fs →
      ∑ i₂_1,
          (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
              (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
            (dist (s.points x) (s.pointsWithCircumcenter i₂_1) * dist (s.points x) (s.pointsWithCircumcenter i₂_1)) =
        0

Tactic:
intro i _ hi
    simp [hfs i hi]

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

Goal state before:
pp: case e'_3.e'_5
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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ s.points = (s.points ∘ ⇑e.symm) ∘ ⇑e.toEmbedding

pp: case e'_3.e'_6
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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ centroidWeights ℝ {e.symm i₁, e.symm i₂}ᶜ = centroidWeights ℝ {i₁, i₂}ᶜ ∘ ⇑e.toEmbedding

Tactic:
· simp [Function.comp_assoc]

Goal state after:
case e'_3.e'_6
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)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ centroidWeights ℝ {e.symm i₁, e.symm i₂}ᶜ = centroidWeights ℝ {i₁, i₂}ᶜ ∘ ⇑e.toEmbedding
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : ⟪v, p -ᵥ s.center⟫ = 0
⊢ 0 • v +ᵥ p = p

Tactic:
zero_smul,

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : ⟪v, p -ᵥ s.center⟫ = 0
⊢ 0 +ᵥ p = p
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

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
s : Sphere P
p : P
v : V
r : ℝ
hr : r ≠ 0
⊢ (-2 * (r * ⟪v, p -ᵥ s.center⟫) / (r * (r * ⟪v, v⟫)) * r) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p

Tactic:
div_mul_eq_div_div

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
r : ℝ
hr : r ≠ 0
⊢ (-2 * (r * ⟪v, p -ᵥ s.center⟫) / r / r / ⟪v, v⟫ * r) • v +ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
Module: Mathlib.Geometry.Group.Growth.QuotientInter

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x ↦ x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
⊢ #(image (⇑(QuotientGroup.mk' H)) (A ^ m)) * #({x ∈ A ^ n | x ∈ H}) ≤ #(A ^ (m + n))

Tactic:
set π := QuotientGroup.mk' H
  let φ := invFunOn π (A ^ m)
  have hφ : Set.InjOn φ (π '' (A ^ m)) := invFunOn_injOn_image ..
  have hφA {a} (ha : a ∈ π '' (A ^ m)) : φ a ∈ A ^ m := by
    have := invFunOn_mem (by simpa using ha)
    norm_cast at this
    simpa using this
  have hπφ {a} (ha : a ∈ π '' (A ^ m)) : π (φ a) = a := invFunOn_eq (by simpa using ha)
  calc
    #((A ^ m).image π) * #{x ∈ A ^ n | x ∈ H}
    _ = #(((A ^ m).image π).image φ) * #{x ∈ A ^ n | x ∈ H} := by
      rw [Finset.card_image_of_injOn (f := φ) (mod_cast hφ)]
    _ ≤ #(((A ^ m).image π).image φ * {x ∈ A ^ n | x ∈ H}) := by
      rw [Finset.card_mul_iff.2]
      simp only [Set.InjOn, coe_image, coe_pow, coe_filter, Set.mem_prod, Set.mem_image,
        exists_exists_and_eq_and, Set.mem_ofPred_eq, and_imp, forall_exists_index, Prod.forall,
        Prod.mk.injEq]
      rintro _ a₁ b₁ hb₁ rfl - ha₁ _ a₂ b₂ hb₂ rfl - ha₂ hab
      have hπa₁ : π a₁ = 1 := (QuotientGroup.eq_one_iff _).2 ha₁
      have hπa₂ : π a₂ = 1 := (QuotientGroup.eq_one_iff _).2 ha₂
      have hπb : π b₁ = π b₂ := by
        simpa [hπφ, Set.mem_image_of_mem π, hb₁, hb₂, hπa₁, hπa₂] using congr(π $hab)
      simp_all
    _ ≤ #(A ^ (m + n)) := by
      gcongr
      simp only [mul_subset_iff, mem_image, exists_exists_and_eq_and, Finset.mem_filter, and_imp,
        forall_exists_index, forall_apply_eq_imp_iff₂, pow_add]
      rintro a ha b hb -
      exact mul_mem_mul (hφA <| Set.mem_image_of_mem _ <| mod_cast ha) hb

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
x : M
hf : IsLocalDiffeomorphAt I J n f x
x' : M
hx' : x' ∈ hf.localInverse.target
⊢ ↑hf.localInverse.toPartialEquiv (f x') = x'

Tactic:
by
  rw [hf.choose_spec.2 (hf.choose.symm_target ▸ hx')]
  exact hf.choose.left_inv hx'

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
hn : n ≠ 0
⊢ IsOpen[inst✝²] (ModelWithCorners.interior M)

Tactic:
refine isOpen_iff_forall_mem_open.2 fun x hx ↦ ⟨_, ?_, isOpen_extChartAt_preimage (I := I) x
    isOpen_interior, mem_chart_source H x, isInteriorPoint_iff.1 hx⟩

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
n : WithTop ℕ∞
inst✝ : IsManifold I n M
hn : n ≠ 0
x : M
hx : x ∈ ModelWithCorners.interior M
⊢ (chartAt H x).source ∩ ↑(extChartAt I x) ⁻¹' interior (extChartAt I x).target ⊆ ModelWithCorners.interior M
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
t t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
hs : Set.range t.points = Set.range t₀.points
⊢ s = insert t.orthocenter (Set.range t.points)

Tactic:
· rw [hs]
    convert! ht₀s using 2
    exact Triangle.orthocenter_eq_of_range_eq hs

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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
⊢ (ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N)ᶜ =
    (ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ

Tactic:
rw [compl_prod_eq_union]

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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsBoundaryPoint x
⊢ I.IsBoundaryPoint (Sum.inl x)

Tactic:
rw [I.isBoundaryPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inl]

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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
hx : I.IsBoundaryPoint x
⊢ ↑(((chartAt H x).lift_openEmbedding ⋯).extend I) (Sum.inl x) ∈ frontier (range ↑I)
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
A : x + z.ofLp 0 ≤ y
⊢ (toLp 2 fun x_1 ↦ ↑⟨min ((↑⟨z, hz⟩).ofLp 0 + x) y, ⋯⟩ - x).ofLp i = z.ofLp i

Tactic:
rw [Subsingleton.elim i 0]

Goal state after:
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
A : x + z.ofLp 0 ≤ y
⊢ (toLp 2 fun x_1 ↦ ↑⟨min ((↑⟨z, hz⟩).ofLp 0 + x) y, ⋯⟩ - x).ofLp 0 = z.ofLp 0
Module: Mathlib.Geometry.Manifold.Instances.Real

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

Tactic:
by
    rintro ⟨z, hz⟩ h'z
    simp only [mem_ofPred_eq, mem_Icc] at hz h'z
    simp only [Fin.isValue, sub_eq_add_neg, neg_add_rev, neg_neg,
      add_neg_cancel_comm_assoc, hz, sup_of_le_left]

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

Goal state before:
pp: x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
A : x ≤ y - z.ofLp 0
⊢ (toLp 2 fun x_1 ↦ y - ↑⟨max (y - (↑⟨z, hz⟩).ofLp 0) x, ⋯⟩).ofLp i = z.ofLp i

Tactic:
rw [Subsingleton.elim i 0]

Goal state after:
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : EuclideanSpace ℝ (Fin 1)
hz : 0 ≤ z.ofLp 0
h'z : z.ofLp 0 < y - x
i : Fin 1
A : x ≤ y - z.ofLp 0
⊢ (toLp 2 fun x_1 ↦ y - ↑⟨max (y - (↑⟨z, hz⟩).ofLp 0) x, ⋯⟩).ofLp 0 = z.ofLp 0
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: 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)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : z.ofLp 0 + x < y
hz₂ : 0 < z.ofLp 0
i : Fin 1
⊢ ((↑(𝓡∂ 1) ∘ ↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) ∘ ↑(𝓡∂ 1).symm) (↑(𝓡∂ 1) ⟨z, hz₀⟩)).ofLp i =
    ((have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
          this)
          (↑(𝓡∂ 1) ⟨z, hz₀⟩)).ofLp
      i

Tactic:
rw [Subsingleton.elim i 0]

Goal state after:
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)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : z.ofLp 0 + x < y
hz₂ : 0 < z.ofLp 0
i : Fin 1
⊢ ((↑(𝓡∂ 1) ∘ ↑((IccLeftChart x y).symm ≫ₕ IccRightChart x y) ∘ ↑(𝓡∂ 1).symm) (↑(𝓡∂ 1) ⟨z, hz₀⟩)).ofLp 0 =
    ((have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
          this)
          (↑(𝓡∂ 1) ⟨z, hz₀⟩)).ofLp
      0
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: 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)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : x < y - z.ofLp 0
hz₂ : y - z.ofLp 0 < y ∧ x < y
i : Fin 1
⊢ ((↑(𝓡∂ 1) ∘ ↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) ∘ ↑(𝓡∂ 1).symm) (↑(𝓡∂ 1) ⟨z, hz₀⟩)).ofLp i =
    ((have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
          this)
          (↑(𝓡∂ 1) ⟨z, hz₀⟩)).ofLp
      i

Tactic:
rw [Subsingleton.elim i 0]

Goal state after:
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)
z : EuclideanSpace ℝ (Fin 1)
hz₀ : 0 ≤ z.ofLp 0
hz₁ : x < y - z.ofLp 0
hz₂ : y - z.ofLp 0 < y ∧ x < y
i : Fin 1
⊢ ((↑(𝓡∂ 1) ∘ ↑((IccRightChart x y).symm ≫ₕ IccLeftChart x y) ∘ ↑(𝓡∂ 1).symm) (↑(𝓡∂ 1) ⟨z, hz₀⟩)).ofLp 0 =
    ((have this := fun z ↦ toLp 2 fun i ↦ -z.ofLp i + (y - x);
          this)
          (↑(𝓡∂ 1) ⟨z, hz₀⟩)).ofLp
      0
Module: Mathlib.Geometry.Manifold.IntegralCurve.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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
⊢ IsMIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)

Tactic:
by
  rw [isMIntegralCurveAt_iff]
  constructor
  · intro ⟨s, hs, h⟩
    rw [Metric.mem_nhds_iff] at hs
    obtain ⟨ε, hε, hε'⟩ := hs
    refine ⟨ε, hε, fun t ht ↦ (h t (hε' ht)).mono hε'⟩
  · intro ⟨ε, hε, h⟩
    exact ⟨Metric.ball t₀ ε, Metric.ball_mem_nhds _ hε, h⟩

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

Goal state before:
pp: case hxs
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[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ UniqueMDiffAt[Icc a b] t

Tactic:
· rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
      exact uniqueDiffOn_Icc h _ ht

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

Goal state before:
pp: case hxs
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 : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ UniqueMDiffAt[Icc a b] t

Tactic:
· rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
      exact uniqueDiffOn_Icc h _ ht

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

Goal state before:
pp: EB : Type u_1
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace ℝ EB
HB : Type u_2
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
B : Type u_3
inst✝¹³ : TopologicalSpace B
inst✝¹² : ChartedSpace HB B
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
E : B → Type u_5
inst✝⁹ : TopologicalSpace (TotalSpace F E)
inst✝⁸ : (x : B) → NormedAddCommGroup (E x)
inst✝⁷ : (x : B) → InnerProductSpace ℝ (E x)
inst✝⁶ : FiberBundle F E
inst✝⁵ : VectorBundle ℝ F E
EM : Type u_6
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace ℝ EM
HM : Type u_7
inst✝² : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB 1 F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : (MDiffAt[s] fun m ↦ ⟨b m, v m⟩) x
hw : (MDiffAt[s] fun m ↦ ⟨b m, w m⟩) x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_smooth : ContMDiff IB (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) 1 fun b ↦ ⟨b, g b⟩
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
hb : MDiffAt[s] b x
⊢ (MDiffAt[s] fun m ↦ ((g (b m)) (v m)) (w m)) x

Tactic:
have : MDifferentiableWithinAt IM (IB.prod 𝓘(ℝ))
      (fun m ↦ TotalSpace.mk' ℝ (E := Bundle.Trivial B ℝ) (b m) (g (b m) (v m) (w m))) s x := by
    apply MDifferentiableWithinAt.clm_bundle_apply₂ (F₁ := F) (F₂ := F)
    · exact MDifferentiableAt.comp_mdifferentiableWithinAt x
        (g_smooth.mdifferentiableAt one_ne_zero) hb
    · exact hv
    · exact hw

Goal state after:
EB : Type u_1
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace ℝ EB
HB : Type u_2
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
B : Type u_3
inst✝¹³ : TopologicalSpace B
inst✝¹² : ChartedSpace HB B
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
E : B → Type u_5
inst✝⁹ : TopologicalSpace (TotalSpace F E)
inst✝⁸ : (x : B) → NormedAddCommGroup (E x)
inst✝⁷ : (x : B) → InnerProductSpace ℝ (E x)
inst✝⁶ : FiberBundle F E
inst✝⁵ : VectorBundle ℝ F E
EM : Type u_6
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace ℝ EM
HM : Type u_7
inst✝² : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB 1 F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : (MDiffAt[s] fun m ↦ ⟨b m, v m⟩) x
hw : (MDiffAt[s] fun m ↦ ⟨b m, w m⟩) x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_smooth : ContMDiff IB (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) 1 fun b ↦ ⟨b, g b⟩
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
hb : MDiffAt[s] b x
this : (MDiffAt[s] fun m ↦ ⟨b m, ((g (b m)) (v m)) (w m)⟩) x
⊢ (MDiffAt[s] fun m ↦ ((g (b m)) (v m)) (w m)) x