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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ dist (s.excenter signs) (s.touchpoint signs i) = s.exradius signs

Tactic:
h.dist_excenter

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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ s.exradius signs = s.exradius signs
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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
this : s.excenter signs -ᵥ s.touchpoint signs i ∈ (vectorSpan ℝ (Set.range s.points))ᗮ
h' : s.excenter signs -ᵥ s.touchpoint signs i ∈ vectorSpan ℝ (Set.range s.points)
h0 : dist (s.excenter signs) (s.touchpoint signs i) = 0
⊢ False

Tactic:
h.dist_excenter

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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
this : s.excenter signs -ᵥ s.touchpoint signs i ∈ (vectorSpan ℝ (Set.range s.points))ᗮ
h' : s.excenter signs -ᵥ s.touchpoint signs i ∈ vectorSpan ℝ (Set.range s.points)
h0 : s.exradius signs = 0
⊢ False
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case neg.refine_1
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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
⊢ s.excenter signs -ᵥ s.touchpoint signs i ∈ ↑(affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ

Tactic:
← range_faceOpposite_points

Goal state after:
case neg.refine_1
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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
⊢ s.excenter signs -ᵥ s.touchpoint signs i ∈ ↑(affineSpan ℝ (Set.range (s.faceOpposite i).points)).directionᗮ
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case neg.refine_2
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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
⊢ s.excenter signs -ᵥ s.touchpoint signs j ∈ ↑(affineSpan ℝ (s.points '' {j}ᶜ)).directionᗮ

Tactic:
← range_faceOpposite_points

Goal state after:
case neg.refine_2
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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
⊢ s.excenter signs -ᵥ s.touchpoint signs j ∈ ↑(affineSpan ℝ (Set.range (s.faceOpposite j).points)).directionᗮ
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case neg
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 z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
by_cases H4 : angle x y = π

Goal state after:
case pos
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 z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : angle x y = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

case neg
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 z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂
h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂
hne : ∠ p₂ p₂ p₃ ≠ ∠ p₂ p₃ p₂ ∨ ∠ p₂ p₂ p₃ ≠ ∠ p₃ p₂ p₂ ∨ ∠ p₂ p₃ p₂ ≠ ∠ p₃ p₂ p₂
h₂₃ : p₂ = p₃
⊢ ∠ p₂ p₂ p₃ < π / 3

Tactic:
subst h₂₃
      simp at hne

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

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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).AcuteAngled
i₁ i₂ i₃ : Fin (m + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) < π / 2

Tactic:
convert! h (i₁ := e i₁) (i₂ := e i₂) (i₃ := e i₃) ?_ ?_ ?_ using 1

Goal state after:
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 m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).AcuteAngled
i₁ i₂ i₃ : Fin (m + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) =
    ∠ ((s.reindex e).points (e i₁)) ((s.reindex e).points (e i₂)) ((s.reindex e).points (e i₃))

case refine_1.convert_1
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 m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).AcuteAngled
i₁ i₂ i₃ : Fin (m + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ e i₁ ≠ e i₂

case refine_1.convert_2
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 m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).AcuteAngled
i₁ i₂ i₃ : Fin (m + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ e i₁ ≠ e i₃

case refine_1.convert_3
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 m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).AcuteAngled
i₁ i₂ i₃ : Fin (m + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ e i₂ ≠ e i₃
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
i : Fin 3
⊢ dist (t.points i) (Simplex.faceOppositeCentroid t i) =
    3 * dist (Simplex.centroid t) (Simplex.faceOppositeCentroid t i)

Tactic:
rw [Affine.Simplex.dist_point_faceOppositeCentroid]
  norm_cast

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 : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v = 0
hv : ¬v = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0

Tactic:
smul_eq_zero,

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
s : Sphere P
p : P
v : V
hp : -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = 0 ∨ v = 0
hv : ¬v = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : {i₂, i₃}ᶜ = {i₁}
he : {i₁}ᶜ = {i₂, i₃}
⊢ mk' (t.points i₁) (vectorSpan ℝ (t.points '' {i₂, i₃}))ᗮ ⊓ affineSpan ℝ (Set.range t.points) =
    mk' (Finset.centroid ℝ {i₁} t.points) (ℝ ∙ (t.points i₂ -ᵥ t.points i₃))ᗮ ⊓ affineSpan ℝ (Set.range t.points)

Tactic:
centroid_singleton,

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
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hs : {i₂, i₃}ᶜ = {i₁}
he : {i₁}ᶜ = {i₂, i₃}
⊢ mk' (t.points i₁) (vectorSpan ℝ (t.points '' {i₂, i₃}))ᗮ ⊓ affineSpan ℝ (Set.range t.points) =
    mk' (t.points i₁) (ℝ ∙ (t.points i₂ -ᵥ t.points i₃))ᗮ ⊓ affineSpan ℝ (Set.range t.points)
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
t : Triangle ℝ P
i₁ : Fin 3
⊢ ∃ i₂ i₃, i₁ ≠ i₂ ∧ i₂ ≠ i₃ ∧ i₁ ≠ i₃

Tactic:
by
    decide +revert

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

Goal state before:
pp: P : Type u_2
inst✝ : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
⊢ s.radius ^ 2 < dist p s.center ^ 2 ↔ s.radius < dist p s.center

Tactic:
pow_lt_pow_iff_left₀ hr dist_nonneg two_ne_zero

Goal state after:
P : Type u_2
inst✝ : MetricSpace P
s : Sphere P
p : P
hr : 0 ≤ s.radius
⊢ s.radius < dist p s.center ↔ s.radius < dist p s.center
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
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
hu : {i₁, i₂} ⊆ univ
⊢ ∃ i₃, univ \ {i₁, i₂} = {i₃} ∧ i₃ ≠ i₁ ∧ i₃ ≠ i₂

Tactic:
by
    decide +revert

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_5
n : WithTop ℕ∞
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝³⁰ : NontriviallyNormedField 𝕜
inst✝²⁹ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁸ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁷ : NormedAddCommGroup F₁
inst✝²⁶ : NormedSpace 𝕜 F₁
inst✝²⁵ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²⁴ : (x : B) → TopologicalSpace (E₁ x)
inst✝²³ : (x : B) → AddCommGroup (E₂ x)
inst✝²² : (x : B) → Module 𝕜 (E₂ x)
inst✝²¹ : NormedAddCommGroup F₂
inst✝²⁰ : NormedSpace 𝕜 F₂
inst✝¹⁹ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁸ : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_8
inst✝¹⁷ : NormedAddCommGroup EB
inst✝¹⁶ : NormedSpace 𝕜 EB
HB : Type u_9
inst✝¹⁵ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹⁴ : TopologicalSpace B
inst✝¹³ : ChartedSpace HB B
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✝⁷ : FiberBundle F₁ E₁
inst✝⁶ : VectorBundle 𝕜 F₁ E₁
inst✝⁵ : FiberBundle F₂ E₂
inst✝⁴ : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝² : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
inst✝¹ : ContMDiffVectorBundle n F₁ E₁ IB
inst✝ : ContMDiffVectorBundle n F₂ E₂ IB
⊢ ∀ e ∈ (vectorPrebundle (RingHom.id 𝕜) F₁ E₁ F₂ E₂).pretrivializationAtlas,
    ∀ e' ∈ (vectorPrebundle (RingHom.id 𝕜) F₁ E₁ F₂ E₂).pretrivializationAtlas,
      ∃ f,
        ContMDiffOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) n f (e.baseSet ∩ e'.baseSet) ∧
          ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F₁ →L[𝕜] F₂), (f b) v = (↑e' ⟨b, e.symm b v⟩).2

Tactic:
rintro _ ⟨e₁, e₂, he₁, he₂, rfl⟩ _ ⟨e₁', e₂', he₁', he₂', rfl⟩
    exact ⟨continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂',
      contMDiffOn_continuousLinearMapCoordChange,
      continuousLinearMapCoordChange_apply (RingHom.id 𝕜) e₁ e₁' e₂ e₂'⟩

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

Goal state before:
pp: 𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B₁) → AddCommGroup (E₁ x)
inst✝¹⁷ : (x : B₁) → Module 𝕜 (E₁ x)
inst✝¹⁶ : NormedAddCommGroup F₁
inst✝¹⁵ : NormedSpace 𝕜 F₁
inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹³ : (x : B₁) → TopologicalSpace (E₁ x)
inst✝¹² : (x : B₂) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B₂) → Module 𝕜 (E₂ x)
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B₂) → TopologicalSpace (E₂ x)
inst✝⁶ : TopologicalSpace B₁
inst✝⁵ : TopologicalSpace B₂
inst✝⁴ : TopologicalSpace M
inst✝³ : FiberBundle F₁ E₁
inst✝² : VectorBundle 𝕜 F₁ E₁
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ : ContinuousWithinAt (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) (insert m₀ s) m₀
hv : ContinuousWithinAt (fun m ↦ { proj := b₁ m, snd := v m }) (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
⊢ ContinuousWithinAt (fun m ↦ { proj := b₂ m, snd := (ϕ m) (v m) }) (insert m₀ s) m₀

Tactic:
FiberBundle.continuousWithinAt_totalSpace

Goal state after:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B₁) → AddCommGroup (E₁ x)
inst✝¹⁷ : (x : B₁) → Module 𝕜 (E₁ x)
inst✝¹⁶ : NormedAddCommGroup F₁
inst✝¹⁵ : NormedSpace 𝕜 F₁
inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹³ : (x : B₁) → TopologicalSpace (E₁ x)
inst✝¹² : (x : B₂) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B₂) → Module 𝕜 (E₂ x)
inst✝¹⁰ : NormedAddCommGroup F₂
inst✝⁹ : NormedSpace 𝕜 F₂
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B₂) → TopologicalSpace (E₂ x)
inst✝⁶ : TopologicalSpace B₁
inst✝⁵ : TopologicalSpace B₂
inst✝⁴ : TopologicalSpace M
inst✝³ : FiberBundle F₁ E₁
inst✝² : VectorBundle 𝕜 F₁ E₁
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ : ContinuousWithinAt (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) (insert m₀ s) m₀
hv :
  ContinuousWithinAt (fun x ↦ { proj := b₁ x, snd := v x }.proj) (insert m₀ s) m₀ ∧
    ContinuousWithinAt
      (fun x ↦ (↑(trivializationAt F₁ E₁ { proj := b₁ m₀, snd := v m₀ }.proj) { proj := b₁ x, snd := v x }).2)
      (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
⊢ ContinuousWithinAt (fun x ↦ { proj := b₂ x, snd := (ϕ x) (v x) }.proj) (insert m₀ s) m₀ ∧
    ContinuousWithinAt
      (fun x ↦
        (↑(trivializationAt F₂ E₂ { proj := b₂ m₀, snd := (ϕ m₀) (v m₀) }.proj) { proj := b₂ x, snd := (ϕ x) (v x) }).2)
      (insert m₀ s) m₀
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
this :
  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₀
⊢ 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:
apply ContMDiffWithinAt.mono_of_mem_nhdsWithin this

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 := ⋯
ht't : t' ⊆ t
this :
  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₀
⊢ t' ∈ 𝓝[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
s : Set M
x : M
V W : (x : M) → TangentSpace I x
hV : V x = 0
hW : W x = 0
⊢ mlieBracketWithin I V W s x = 0

Tactic:
by
  simp only [mlieBracketWithin, mpullback_apply]
  rw [lieBracketWithin_eq_zero_of_eq_zero]
  · simp
  · simp only [mpullbackWithin_apply]
    have : (extChartAt I x).symm ((extChartAt I x) x) = x := by simp
    rw [this, hV]
    simp +instances
  · simp only [mpullbackWithin_apply]
    have : (extChartAt I x).symm ((extChartAt I x) x) = x := by simp
    rw [this, hW]
    simp +instances

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
W : (x : M) → TangentSpace I x
⊢ mlieBracketWithin I W 0 s = 0

Tactic:
mlieBracketWithin_swap

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
W : (x : M) → TangentSpace I x
⊢ -mlieBracketWithin I 0 W s = 0
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₁
F₂ : TangentBundle I G × TangentBundle I G → TangentBundle (I.prod I) (G × G) := ⇑(equivTangentBundleProd I G I G).symm
S₂ : ContMDiff (I.tangent.prod I.tangent) (I.prod I).tangent (minSmoothness 𝕜 2) F₂
F₃ : TangentBundle (I.prod I) (G × G) → TangentBundle I G := tangentMap (I.prod I) I fun p ↦ p.1 * p.2
⊢ ContMDiff (I.prod I) I (minSmoothness 𝕜 3) fun p ↦ p.1 * p.2

Tactic:
exact contMDiff_mul I (minSmoothness 𝕜 3)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : (MDiffAt[s] fun x ↦ ⟨x, V x⟩) x
⊢ DifferentiableWithinAt 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
    (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
apply MDifferentiableWithinAt.differentiableWithinAt

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 : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : (MDiffAt[s] fun x ↦ ⟨x, V x⟩) x
⊢ MDiffAt[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] (mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I))
    (↑(extChartAt I x) x)
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'
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderiv[s] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : m + 1 ≤ n
hV : ContMDiffWithinAt I' I'.tangent m (fun x ↦ ⟨x, V x⟩) t (f x₀)
⊢ ContMDiffWithinAt I I.tangent m (fun x ↦ ⟨x, mpullbackWithin I I' f V s x⟩) (s ∩ f ⁻¹' t) x₀

Tactic:
exact ContMDiffWithinAt.mpullbackWithin_vectorField_inter hV hf hf' hx₀ hs hmn

Goal state after: