mathlib-initiative/mathlib-tactics huggingface dataset:
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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
this : Nonempty ↥S
⊢ ↑(s.restrict S hS).mongePoint = s.mongePoint

Tactic:
mongePoint

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 : ℕ
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
this : Nonempty ↥S
⊢ ↑((↑(n + 1) / ↑(n - 1)) • (Finset.centroid ℝ univ (s.restrict S hS).points -ᵥ (s.restrict S hS).circumcenter) +ᵥ
        (s.restrict S hS).circumcenter) =
    (↑(n + 1) / ↑(n - 1)) • (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) +ᵥ s.circumcenter
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
s : Triangle ℝ P
i : Fin 3
⊢ Simplex.altitudeFoot s i ∈ Simplex.ninePointCircle s

Tactic:
by
  convert! s.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle i
  rw [Simplex.altitudeFoot]
  unfold Simplex.orthogonalProjectionSpan
  congr 1
  rw [orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem,
    Simplex.points_vsub_eulerPoint, Submodule.smul_mem_iff _ (by norm_num),
    ← orthocenter_eq_mongePoint, direction_affineSpan, Simplex.range_faceOpposite_points]
  refine Set.mem_of_mem_of_subset ?_ (s.vectorSpan_isOrtho_altitude_direction i).ge
  exact vsub_mem_direction (s.mem_altitude i) (s.orthocenter_mem_altitude)

Goal state after:
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
n : ℕ
s : Simplex ℝ P n
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
⊢ Real.arccos
      ((‖s.points i₁ -ᵥ s.points i₂‖ * ‖s.points i₁ -ᵥ s.points i₂‖ +
              ‖s.points i₃ -ᵥ s.points i₂‖ * ‖s.points i₃ -ᵥ s.points i₂‖ -
            ‖s.points i₁ -ᵥ s.points i₂ - (s.points i₃ -ᵥ s.points i₂)‖ *
              ‖s.points i₁ -ᵥ s.points i₂ - (s.points i₃ -ᵥ s.points i₂)‖) /
          2 /
        (‖s.points i₁ -ᵥ s.points i₂‖ * ‖s.points i₃ -ᵥ s.points i₂‖)) =
    π / 3

Tactic:
refine Real.arccos_eq_of_eq_cos (by linarith [Real.pi_nonneg]) (by linarith [Real.pi_nonneg]) ?_

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 : ℕ
s : Simplex ℝ P n
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
⊢ (‖s.points i₁ -ᵥ s.points i₂‖ * ‖s.points i₁ -ᵥ s.points i₂‖ +
            ‖s.points i₃ -ᵥ s.points i₂‖ * ‖s.points i₃ -ᵥ s.points i₂‖ -
          ‖s.points i₁ -ᵥ s.points i₂ - (s.points i₃ -ᵥ s.points i₂)‖ *
            ‖s.points i₁ -ᵥ s.points i₂ - (s.points i₃ -ᵥ s.points i₂)‖) /
        2 /
      (‖s.points i₁ -ᵥ s.points i₂‖ * ‖s.points i₃ -ᵥ s.points i₂‖) =
    Real.cos (π / 3)
Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy

Goal state before:
pp: case hab
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
⊢ dist c p = dist c p / dist b p * dist b p

pp: case hcb
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
⊢ dist d p = dist c p / dist b p * dist a p

Tactic:
all_goals simp [field, mul_comm, hmul]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy

Goal state before:
pp: case hab
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
⊢ dist d p = dist a p / dist b p * dist c p

pp: case hcb
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
⊢ dist a p = dist a p / dist b p * dist b p

Tactic:
all_goals simp [field, mul_comm, hmul]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

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
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
hv : ¬v = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0

Tactic:
rwa [Sphere.secondInter, eq_comm, eq_vadd_iff_vsub_eq, vsub_self, eq_comm, smul_eq_zero,
      or_iff_left hv, div_eq_zero_iff, inner_self_eq_zero, or_iff_left hv, mul_eq_zero,
      or_iff_right (by simp : (-2 : ℝ) ≠ 0)] at hp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p a b : P
hp : p ∈ line[ℝ, a, b]
ha : a ∈ s
hb : b ∈ s
hp_on : p ∈ s
hq : dist a s.center = dist b s.center
⊢ dist p a * dist p b = 0

Tactic:
rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq,
      mem_sphere.mp hb, mem_sphere.mp hp_on, sub_self, abs_zero]

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

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ t₁.points i₁ ∈ altitude t₂ j₂

Tactic:
rw [altitude_replace_orthocenter_eq_affineSpan hi₁₂ hi₁₃ hi₂₃ hj₁₂ hj₁₃ hj₂₃ h₁ h₂ h₃]

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ t₁.points i₁ ∈ line[ℝ, t₁.points i₁, t₁.points i₂]
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:
hf.choose_spec.2 (hf.choose.symm_target ▸ hx')

Goal state after:
𝕜 : 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 (↑(Exists.choose hf).toPartialEquiv x') = x'
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
F' : Type u_4
inst✝¹⁰ : NormedAddCommGroup F'
inst✝⁹ : NormedSpace 𝕜 F'
H₁ : Type u_5
inst✝⁸ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁷ : TopologicalSpace H₂
H₃ : Type u_7
inst✝⁶ : TopologicalSpace H₃
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
K : 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
P : Type u_10
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace H₃ P
n : WithTop ℕ∞
f : M → N
x : M
g : N → P
Φ : PartialDiffeomorph I J M N n
hx : x ∈ Φ.source
heq : EqOn f (↑Φ.toPartialEquiv) Φ.source
Ψ : PartialDiffeomorph J K N P n
hy : f x ∈ Ψ.source
heq' : EqOn g (↑Ψ.toPartialEquiv) Ψ.source
⊢ x ∈ (Φ.trans Ψ).source

Tactic:
simp [hx, ← heq.eq_of_mem hx, hy]

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
u : Opens M
x✝ : ↥u
⊢ x✝ ∈ ModelWithCorners.interior ↥u ↔ x✝ ∈ Subtype.val ⁻¹' ModelWithCorners.interior M

Tactic:
exact I.isInteriorPoint_iff_isInteriorPoint_val

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

Goal state before:
pp: case refine_1.h
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
f : B → 𝕜
s : (x : B) → E x
u : Set B
x₀ : B
hf : MDiffAt[u] f x₀
e : Trivialization F TotalSpace.proj := ⋯
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
⊢ ∀ x ∈ e.baseSet, (fun b ↦ (↑e ⟨b, (f • s) b⟩).2) x = (fun p ↦ f p • (↑e ⟨p, s p⟩).2) x

Tactic:
· exact fun x hx ↦ (e.linear 𝕜 hx).2 ..

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m 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'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiff[u]
t' : Set N := t ∩ g ⁻¹' (extChartAt I (g x₀)).source
ht't : t' ⊆ t
⊢ ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv[u] (f x) (g x)) x₀) t x₀

Tactic:
suffices CMDiffAt[t'] m (inTangentCoordinates I I' g (fun x ↦ f x (g x))
      (fun x ↦ mfderiv[u] (f x) (g x)) x₀) x₀ by
    apply ContMDiffWithinAt.mono_of_mem_nhdsWithin this
    apply inter_mem self_mem_nhdsWithin
    exact hg.continuousWithinAt.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds (g x₀))

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m 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'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiff[u]
t' : Set N := t ∩ g ⁻¹' (extChartAt I (g x₀)).source
ht't : t' ⊆ t
⊢ ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv[u] (f x) (g x)) x₀) t' x₀
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m 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'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiff[u]
t' : Set N := t ∩ g ⁻¹' (extChartAt I (g x₀)).source
ht't : t' ⊆ t
hx₀gx₀ : (x₀, g x₀) ∈ t ×ˢ u
⊢ ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv[u] (f x) (g x)) x₀) t' x₀

Tactic:
have h4f : ContinuousWithinAt (fun x ↦ f x (g x)) t x₀ := by
    change ContinuousWithinAt ((Function.uncurry f) ∘ (fun x ↦ (x, g x))) t x₀
    refine ContinuousWithinAt.comp hf.continuousWithinAt ?_ (fun y hy ↦ by simp [hy, hu hy])
    exact (continuousWithinAt_id.prodMk hg.continuousWithinAt)

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m 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'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiff[u]
t' : Set N := t ∩ g ⁻¹' (extChartAt I (g x₀)).source
ht't : t' ⊆ t
hx₀gx₀ : (x₀, g x₀) ∈ t ×ˢ u
h4f : ContinuousWithinAt (fun x ↦ f x (g x)) t x₀
⊢ ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv[u] (f x) (g x)) x₀) t' 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
x : M
V W W₁ : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hW : MDiffAt (T% W) x
hW₁ : MDiffAt (T% W₁) x
⊢ mlieBracket I V (W + W₁) x = mlieBracket I V W x + mlieBracket I V W₁ x

Tactic:
simp only [← mlieBracketWithin_univ] at hW hW₁ ⊢

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

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
⊢ (𝓡∂ 1).IsBoundaryPoint ⊤

Tactic:
rw [ModelWithCorners.isBoundaryPoint_iff, extChartAt,
    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.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)
h' : ContMDiffAt I J' n (φ ∘ f) x
t : Set M
ht : t ⊆ f ⁻¹' h.domChart.source
hxt : x ∈ t
f' : E → E'' := ↑(h.domChart.extend J) ∘ f ∘ ↑(extChartAt I x).symm
φ' : E'' → E''' := ↑(h.codChart.extend J') ∘ φ ∘ ↑(h.domChart.extend J).symm
x' : E := ↑(extChartAt I x) x
s : Set E := ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I
hx' : ↑(extChartAt I x) x ∈ s
h'loc :
  ContDiffWithinAt 𝕜 n (↑(h.codChart.extend J') ∘ (φ ∘ f) ∘ ↑(extChartAt I x).symm)
    (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I) (↑(extChartAt I x) x)
h'' : ContDiffWithinAt 𝕜 n (φ' ∘ f') s x'
f'' : E → E''' := (⇑h.equiv ∘ fun x ↦ (x, 0)) ∘ f'
h''' : ContDiffWithinAt 𝕜 n f'' s x'
h'''' : ContDiffWithinAt 𝕜 n ((Prod.fst ∘ ⇑h.equiv.symm) ∘ f'') s x'
y : E
hy : y ∈ s
⊢ f' y = ((Prod.fst ∘ ⇑h.equiv.symm) ∘ f'') y

Tactic:
by simp [f'']

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
w : ↥(ℝ ∙ v)ᗮ
⊢ stereoInvFun hv w ≠ ⟨v, ⋯⟩

Tactic:
refine Subtype.coe_ne_coe.1 ?_
  rw [← inner_lt_one_iff_real_of_norm_eq_one _ hv]
  · have hw : ⟪v, w⟫_ℝ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2
    have hw' : (‖(w : E)‖ ^ 2 + 4)⁻¹ * (‖(w : E)‖ ^ 2 - 4) < 1 := by
      rw [inv_mul_lt_iff₀']
      · linarith
      positivity
    simpa [real_inner_comm, inner_add_right, inner_smul_right, real_inner_self_eq_norm_mul_norm, hw,
      hv] using hw'
  · simpa using stereoInvFunAux_mem hv w.2

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₀
s : Set ℝ := {t | γ t = γ' t} ∩ Ioo a b
hs : s = {t | γ t = γ' t} ∩ Ioo a b
t : { x // x ∈ Ioo a b }
ht : t ∈ closure {a_1 | γ ↑a_1 = γ' ↑a_1}
⊢ t ∈ {a_1 | γ ↑a_1 = γ' ↑a_1}

Tactic:
revert ht t

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I 1 M
γ γ' : ℝ → 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₀
s : Set ℝ := {t | γ t = γ' t} ∩ Ioo a b
hs : s = {t | γ t = γ' t} ∩ Ioo a b
⊢ ∀ ⦃t : { x // x ∈ Ioo a b }⦄, t ∈ closure {a_1 | γ ↑a_1 = γ' ↑a_1} → t ∈ {a_1 | γ ↑a_1 = γ' ↑a_1}
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y 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
⊢ riemannianEDist I x z < r

Tactic:
rcases exists_lt_locally_constant_of_riemannianEDist_lt hu zero_lt_one with
    ⟨γ₁, hγ₁0, hγ₁1, hγ₁_smooth, hγ₁, -, hγ₁_const⟩

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
⊢ riemannianEDist I x z < r
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 : ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ < ↑C
C_pos : 0 < C
y : M
hy : ‖mfderiv% ↑(extChartAt I x) y‖ < ↑C
⊢ ↑(NNReal.mk ‖mfderiv% ↑(extChartAt I x) y‖ ⋯) < ↑C

Tactic:
exact_mod_cast hy

Goal state after: