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

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
hz : z ≠ 0
⊢ angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
hz : z = 0
⊢ angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)

Tactic:
· simpa [hkx, hkz, NNReal.smul_def] using
        angle_eq_angle_add_add_angle_add (kx • x) (smul_ne_zero hkz.ne' hz)

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
hz : z = 0
⊢ angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)
Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane

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
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R ⁻¹' sphere y (dist y c) = insert c ↑(perpBisector c (inversion c R y))

Tactic:
ext x
  rcases eq_or_ne x c with rfl | hx; · simp [dist_comm]
  rw [mem_preimage, mem_sphere, ← inversion_mem_perpBisector_inversion_iff hR] <;> simp [*]

Goal state after:
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
⊢ s.secondInter p 0 = p

Tactic:
simp [Sphere.secondInter]

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

Goal state before:
pp: case e_a.e_direction
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)
x✝ : V
⊢ x✝ ∈ ℝ ∙ (s.points i₁ -ᵥ s.points i₂) ↔ x✝ ∈ ℝ ∙ (s.points i₂ -ᵥ s.points i₁)

Tactic:
Submodule.mem_span_singleton

Goal state after:
case e_a.e_direction
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)
x✝ : V
⊢ (∃ a, a • (s.points i₁ -ᵥ s.points i₂) = x✝) ↔ ∃ a, a • (s.points i₂ -ᵥ s.points i₁) = x✝
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

Goal state before:
pp: case refine_1.inr
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
hp : p ∈ s
v : V
p' : P
hp' : p' ∈ AffineSubspace.mk' p (ℝ ∙ v)
h : p' = s.secondInter p v
⊢ p' ∈ s

Tactic:
· rwa [h, Sphere.secondInter_mem]

Goal state after:
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
hp : p ∈ s
v : V
p' : P
hp' : p' -ᵥ p ∈ ℝ ∙ v
h : p' ∈ s
⊢ p' = p ∨ p' = s.secondInter p v

Tactic:
Submodule.mem_span_singleton

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
hp : p ∈ s
v : V
p' : P
hp' : ∃ a, a • v = p' -ᵥ p
h : p' ∈ s
⊢ p' = p ∨ p' = s.secondInter p v
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
n : ℕ
inst✝ : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Ioo 0 1
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P := (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points) w)) r
hp' : p' -ᵥ sx.points i = r • ((Finset.affineCombination ℝ Finset.univ sx.points) w -ᵥ sx.points i)
⊢ r •
        ((Finset.affineCombination ℝ Finset.univ sx.points) w -ᵥ
          (Finset.affineCombination ℝ Finset.univ sx.points) (Pi.single i 1)) +ᵥ
      (Finset.affineCombination ℝ Finset.univ sx.points) (Pi.single i 1) ∈
    (sx.faceOpposite i).interior

Tactic:
Finset.affineCombination_vsub,

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
n : ℕ
inst✝ : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Ioo 0 1
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P := (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points) w)) r
hp' : p' -ᵥ sx.points i = r • ((Finset.affineCombination ℝ Finset.univ sx.points) w -ᵥ sx.points i)
⊢ r • (Finset.univ.weightedVSub sx.points) (w - Pi.single i 1) +ᵥ
      (Finset.affineCombination ℝ Finset.univ sx.points) (Pi.single i 1) ∈
    (sx.faceOpposite i).interior
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case right.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ i₂ i₃ j₂ j₃ : Fin 3
left✝² : i₁ ≠ i₂
left✝¹ : i₁ ≠ i₃
left✝ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : p i₁ = t.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t.points j₂ = p i₂
h₃ : t.points j₃ = p i₃
⊢ dist (p i₃) ((reflection (affineSpan ℝ (t.points '' {j₂, j₃}))) (Simplex.circumcenter t)) = Simplex.circumradius t

Tactic:
rw [← h₃,
        dist_reflection_eq_of_mem _
          (mem_affineSpan ℝ
            (Set.mem_image_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))))]
      exact t.dist_circumcenter_eq_circumradius _

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
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
y : M
hyl : y ∈ Φ.toOpenPartialHomeomorph.symm.target
hyr : y ∈ ↑Φ.toOpenPartialHomeomorph.symm.symm ⁻¹' Ψ.toOpenPartialHomeomorph.source
hfy : f y ∈ Ψ.source
⊢ (g ∘ f) y = ↑(Φ.trans Ψ).toPartialEquiv y

Tactic:
simp [← heq.eq_of_mem hyl, ← heq'.eq_of_mem hfy]

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
x : M
h : I.IsInteriorPoint x
⊢ ∃ t ⊆ range ↑I, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ ↑(extChartAt I x) x ∈ t

Tactic:
exact ⟨interior (range I), interior_subset, isOpen_interior, h⟩

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
x : M
h : I.IsInteriorPoint x
⊢ range ↑I ∈ 𝓝 (↑(extChartAt I x) x)

Tactic:
rw [mem_nhds_iff]
  exact ⟨interior (range I), interior_subset, isOpen_interior, h⟩

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
hf : IsLocalDiffeomorphOn I J n f univ
⊢ IsLocalHomeomorphOn f univ

Tactic:
exact hf.isLocalHomeomorphOn

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 : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : e ∈ atlas H M
hx : x ∈ e.source
⊢ I.IsBoundaryPoint x ↔ ↑(e.extend I) x ∈ frontier (e.extend I).target

Tactic:
rw [← not_iff_not, ← I.isInteriorPoint_iff_not_isBoundaryPoint,
    I.isInteriorPoint_iff_of_mem_atlas hn he hx, mem_interior_iff_notMem_frontier]

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
e : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : e ∈ atlas H M
hx : x ∈ e.source
⊢ ↑(e.extend I) x ∈ (e.extend I).target
Module: Mathlib.Topology.VectorBundle.Hom

Goal state before:
pp: 𝕜₁ : Type u_1
inst✝²⁰ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝¹⁹ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝¹⁸ : NormedAddCommGroup F₁
inst✝¹⁷ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁶ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁵ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹³ : NormedAddCommGroup F₂
inst✝¹² : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝¹¹ : (x : B) → AddCommGroup (E₂ x)
inst✝¹⁰ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝⁹ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁸ : TopologicalSpace B
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁷ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁶ : FiberBundle F₁ E₁
inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
inst✝³ : Trivialization.IsLinear 𝕜₁ e₁
inst✝² : Trivialization.IsLinear 𝕜₁ e₁'
inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂
inst✝ : Trivialization.IsLinear 𝕜₂ e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
L : F₁ →SL[σ] F₂
v : F₁
⊢ (((Trivialization.coordChangeL 𝕜₁ e₁' e₁ b).symm.arrowCongrSL (Trivialization.coordChangeL 𝕜₂ e₂ e₂' b)) L) v =
    (↑(continuousLinearMap σ e₁' e₂') { proj := b, snd := (continuousLinearMap σ e₁ e₂).symm b L }).2 v

Tactic:
ContinuousLinearEquiv.arrowCongrSL_apply,

Goal state after:
𝕜₁ : Type u_1
inst✝²⁰ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝¹⁹ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝¹⁸ : NormedAddCommGroup F₁
inst✝¹⁷ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁶ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁵ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹³ : NormedAddCommGroup F₂
inst✝¹² : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝¹¹ : (x : B) → AddCommGroup (E₂ x)
inst✝¹⁰ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝⁹ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁸ : TopologicalSpace B
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁷ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁶ : FiberBundle F₁ E₁
inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
inst✝³ : Trivialization.IsLinear 𝕜₁ e₁
inst✝² : Trivialization.IsLinear 𝕜₁ e₁'
inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂
inst✝ : Trivialization.IsLinear 𝕜₂ e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
L : F₁ →SL[σ] F₂
v : F₁
⊢ (↑(Trivialization.coordChangeL 𝕜₂ e₂ e₂' b) ∘SL L ∘SL ↑(Trivialization.coordChangeL 𝕜₁ e₁' e₁ b).symm.symm) v =
    (↑(continuousLinearMap σ e₁' e₂') { proj := b, snd := (continuousLinearMap σ e₁ e₂).symm b L }).2 v
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'
V : (x : M') → TangentSpace I' x
c : 𝕜
⊢ mpullback I I' f (c • V) = c • mpullback I I' f V

Tactic:
ext x
  simp [mpullback_apply]

Goal state after:
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'
V : (x : M') → TangentSpace I' x
g : M' → 𝕜
⊢ mpullback I I' f (g • V) = g ∘ f • mpullback I I' f V

Tactic:
ext x
  simp [mpullback_apply]

Goal state after:
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'
V V₁ : (x : M') → TangentSpace I' x
⊢ mpullback I I' f (V + V₁) = mpullback I I' f V + mpullback I I' f V₁

Tactic:
ext x
  simp [mpullback_apply]

Goal state after:
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'
V : (x : M') → TangentSpace I' x
⊢ mpullback I I' f (-V) = -mpullback I I' f V

Tactic:
ext x
  simp [mpullback_apply]

Goal state after:
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✝
inst✝⁴ : CompleteSpace E
G : Type u_5
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : AddGroup G
inst✝ : LieAddGroup I (minSmoothness 𝕜 3) G
c : 𝕜
v w : AddGroupLieAlgebra I G
⊢ ⁅v, c • w⁆ = c • ⁅v, w⁆

Tactic:
simp only [AddGroupLieAlgebra.bracket_def, addInvariantVectorField_smul]

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✝
inst✝⁴ : CompleteSpace E
G : Type u_5
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : AddGroup G
inst✝ : LieAddGroup I (minSmoothness 𝕜 3) G
c : 𝕜
v w : AddGroupLieAlgebra I G
⊢ mlieBracket I (addInvariantVectorField v) (c • addInvariantVectorField w) 0 =
    c • mlieBracket I (addInvariantVectorField v) (addInvariantVectorField w) 0
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

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

Tactic:
set s' := (extChartAt I x).symm ⁻¹' s ∩ range I

Goal state after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
f : M → 𝕜
hf : MDiffAt[s] f x
hW : (MDiffAt[s] fun x ↦ ⟨x, W x⟩) x
hs : UniqueMDiffAt[s] x
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)
W' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) W (range ↑I)
f' : E → 𝕜 := f ∘ ↑(extChartAt I x).symm
s' : Set E := ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I
⊢ mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (lieBracketWithin 𝕜 V' (f' • W') s') x =
    (d[s] f x) (V x) • W x + f x • mpullback I 𝓘(𝕜, E) (↑(extChartAt I x)) (lieBracketWithin 𝕜 V' W' s') 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'
y₀ : M'
inst✝² : CompleteSpace E
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
hV : ContMDiffWithinAt I' I'.tangent m (fun x ↦ ⟨x, V x⟩) t y₀
hf : ContMDiffWithinAt I I' n f s x₀
hf' : (mfderiv[s] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : m + 1 ≤ n
hst : MapsTo f s t
h : f x₀ = y₀
⊢ ContMDiffWithinAt I I.tangent m (fun x ↦ ⟨x, mpullbackWithin I I' f V s x⟩) s x₀

Tactic:
by
  subst h
  exact ContMDiffWithinAt.mpullbackWithin_vectorField hV hf hf' hx₀ hs hmn hst

Goal state after:
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'
u : Set M
hV : ContMDiffWithinAt I' I'.tangent m (fun x ↦ ⟨x, V x⟩) t (f x₀)
hf : ContMDiffWithinAt I I' n f u x₀
hf' : (mfderiv[u] f x₀).IsInvertible
hx₀ : x₀ ∈ s
hs : UniqueMDiff[s]
hmn : m + 1 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hu : s ⊆ u
hn : 1 ≤ n
⊢ mfderiv[s] f x₀ = mfderiv[u] f x₀

Tactic:
exact (hf.mdifferentiableWithinAt <| by positivity).mfderivWithin_mono (hs _ hx₀) hu

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:
by
  norm_num [IccRightChart, modelWithCornersEuclideanHalfSpace_zero]
  congr

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

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

Tactic:
· simp only [h', if_false]
      apply lt_of_lt_of_le h.out
      simpa only [not_lt] using h'

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

Goal state before:
pp: case hφ
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) := ⋯
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := ⋯
hz : ↑z < y
⊢ ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) n (↑(Homeomorph.addLeft (-x)).toOpenPartialHomeomorph)
    (Homeomorph.addLeft (-x)).toOpenPartialHomeomorph.source

pp: case hφ'
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) := ⋯
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := ⋯
hz : ↑z < y
⊢ ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) n (↑(Homeomorph.addLeft (-x)).toOpenPartialHomeomorph.symm)
    (Homeomorph.addLeft (-x)).toOpenPartialHomeomorph.target

Tactic:
· have : ContDiff ℝ n (fun y ↦ -x + y) := by fun_prop
        simpa [contMDiffOn_iff_contDiffOn, contDiffOn_univ]

Goal state after:
case hφ'
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) := ⋯
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := ⋯
hz : ↑z < y
⊢ ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) n (↑(Homeomorph.addLeft (-x)).toOpenPartialHomeomorph.symm)
    (Homeomorph.addLeft (-x)).toOpenPartialHomeomorph.target
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
n : ℕ∞ω
⊢ ∀ x ∈ {x | ((innerSL ℝ) v) x ≠ 1}, 1 - ((innerSL ℝ) v) x ≠ 0

Tactic:
intro x h h'
    exact h (sub_eq_zero.mp h').symm

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : ↑(sphere 0 1)
⊢ ↑(stereographic ⋯) v = 0

Tactic:
by
  convert! stereographic_apply_neg (-v)
  ext1
  simp

Goal state after: