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

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
fs : Finset (Fin (n + 1))
⊢ ∑ i ∈ fs, centroidWeights ℝ fs i • (s.points i -ᵥ Classical.choice ⋯) +ᵥ Classical.choice ⋯ =
    (∑ i, (if i ∈ fs then (↑(#fs))⁻¹ else 0) • (s.points i -ᵥ Classical.choice ⋯) + 0) +ᵥ Classical.choice ⋯

Tactic:
add_zero,

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
fs : Finset (Fin (n + 1))
⊢ ∑ i ∈ fs, centroidWeights ℝ fs i • (s.points i -ᵥ Classical.choice ⋯) +ᵥ Classical.choice ⋯ =
    ∑ i, (if i ∈ fs then (↑(#fs))⁻¹ else 0) • (s.points i -ᵥ Classical.choice ⋯) +ᵥ Classical.choice ⋯
Module: Mathlib.Geometry.Euclidean.Triangle

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
a b c : P
h : ¬Collinear ℝ {a, b, c}
⊢ ∠ a c b < ∠ a b c → dist a b < dist a c

Tactic:
have hsin := law_sin c b a

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
h : ¬Collinear ℝ {a, b, c}
hsin : Real.sin (∠ c b a) * dist b a = Real.sin (∠ a c b) * dist a c
⊢ ∠ a c b < ∠ a b c → dist a b < dist a c
Module: Mathlib.Geometry.Euclidean.Circumcenter

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₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ x,
        ((if x ∈ {i₁, i₂} then
            (↑(#{i₁, i₂}))⁻¹ • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) +
              (↑(#{i₁, i₂}))⁻¹ • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
          else 0 + 0) -
          if x = i₁ ∨ x = i₂ then 1 • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) else 0) +
      (0 - 1 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) + 0 -
        -1 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯)) =
    0

Tactic:
add_zero,

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₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ x,
        ((if x ∈ {i₁, i₂} then
            (↑(#{i₁, i₂}))⁻¹ • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) +
              (↑(#{i₁, i₂}))⁻¹ • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
          else 0) -
          if x = i₁ ∨ x = i₂ then 1 • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) else 0) +
      (0 - 1 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) -
        -1 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯)) =
    0
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
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
⊢ k ∈ {j}ᶜ

Tactic:
by simp [hkj]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case mp
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
⊢ angle x z = angle x y + angle y z → angle x z = π ∨ y ∈ Submodule.span ℝ≥0 {x, z}

Tactic:
rintro h

Goal state after:
case mp
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
⊢ angle x z = π ∨ y ∈ Submodule.span ℝ≥0 {x, z}
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case mpr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
⊢ angle x z = π ∨ y ∈ Submodule.span ℝ≥0 {x, z} → angle x z = angle x y + angle y z

Tactic:
rintro h

Goal state after:
case mpr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = π ∨ y ∈ Submodule.span ℝ≥0 {x, z}
⊢ angle x z = angle x y + angle y 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 '' ↑(perpBisector c y) = sphere (inversion c R y) (R ^ 2 / dist y c) \ {c}

Tactic:
rw [image_eq_preimage_of_inverse (inversion_involutive _ hR) (inversion_involutive _ hR),
    preimage_inversion_perpBisector hR hy]

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' : P
hp : p ∈ s
hp' : dist p' s.center < s.radius
⊢ p' ≠ s.secondInter p (p' -ᵥ p)

Tactic:
rintro h

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' : P
hp : p ∈ s
hp' : dist p' s.center < s.radius
h : p' = s.secondInter p (p' -ᵥ p)
⊢ False
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
a b c d p : P
h : Cospherical {a, b, c, d}
hab : a ≠ b
hcd : c ≠ d
hcpd : ∠ c p d = 0
hapb : Collinear ℝ {a, p, b}
⊢ dist a p * dist b p = dist c p * dist d p

Tactic:
apply collinear_of_angle_eq_zero at hcpd

Goal state after:
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}
hab : a ≠ b
hcd : c ≠ d
hapb : Collinear ℝ {a, p, b}
hcpd : Collinear ℝ {c, p, d}
⊢ dist a p * dist b p = dist c p * dist d p
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
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : dist p t ^ 2 = s.power p
h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
x : P
hx : x ∈ line[ℝ, p, t]
r : ℝ
hr : r • (p -ᵥ t) = x -ᵥ t
⊢ ⟪r • (p -ᵥ t), t -ᵥ s.center⟫ = 0

Tactic:
inner_smul_left,

Goal state after:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : dist p t ^ 2 = s.power p
h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
x : P
hx : x ∈ line[ℝ, p, t]
r : ℝ
hr : r • (p -ᵥ t) = x -ᵥ t
⊢ (starRingEnd ℝ) r * ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
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 ℕ∞
e✝ e'✝ : OpenPartialHomeomorph M✝ H✝
x✝¹ : M✝
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : e ∈ atlas H M
he' : e' ∈ atlas H M
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : ↑(e.extend I) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange e e'
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφx' : Surjective ⇑(fderivWithin 𝕜 (↑φ) φ.source (↑(e.extend I) x))
h✝ : IsRCLikeNormedField 𝕜
x✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ ↑(e'.extend I) x ∈ interior (range ↑I)

Tactic:
let _ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E

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 ℕ∞
e✝ e'✝ : OpenPartialHomeomorph M✝ H✝
x✝² : M✝
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
e e' : OpenPartialHomeomorph M H
x : M
hn : n ≠ 0
he : e ∈ atlas H M
he' : e' ∈ atlas H M
hex : x ∈ e.source
hex' : x ∈ e'.source
hx : ↑(e.extend I) x ∈ interior (e.extend I).target
φ : PartialEquiv E E := extendCoordChange e e'
hφ : ContDiffOn 𝕜 n (↑φ) φ.source
hφx' : Surjective ⇑(fderivWithin 𝕜 (↑φ) φ.source (↑(e.extend I) x))
h✝ : IsRCLikeNormedField 𝕜
x✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ ↑(e'.extend I) x ∈ interior (range ↑I)
Module: Mathlib.Geometry.Manifold.Complex

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝³ : I.Boundaryless
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range ↑I = univ
⊢ 𝓝[univ] ↑e c = 𝓝 (↑e c)

Tactic:
nhdsWithin_univ

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝³ : I.Boundaryless
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
f : M → F
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range ↑I = univ
⊢ 𝓝 (↑e c) = 𝓝 (↑e c)
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'✝
I'✝ : ModelWithCorners 𝕜✝ E'✝ H'✝
N✝ : Type u_7
inst✝¹² : TopologicalSpace N✝
inst✝¹¹ : ChartedSpace H'✝ N✝
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hf' : Surjective ⇑(mfderiv% f x)
hx : I.IsInteriorPoint x
h✝ : IsRCLikeNormedField 𝕜
x✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ I'.IsInteriorPoint (f x)

Tactic:
let _ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E

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✝
E'✝ : Type u_5
inst✝¹⁵ : NormedAddCommGroup E'✝
inst✝¹⁴ : NormedSpace 𝕜✝ E'✝
H'✝ : Type u_6
inst✝¹³ : TopologicalSpace H'✝
I'✝ : ModelWithCorners 𝕜✝ E'✝ H'✝
N✝ : Type u_7
inst✝¹² : TopologicalSpace N✝
inst✝¹¹ : ChartedSpace H'✝ N✝
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hf' : Surjective ⇑(mfderiv% f x)
hx : I.IsInteriorPoint x
h✝ : IsRCLikeNormedField 𝕜
x✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ I'.IsInteriorPoint (f x)
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
h : I'.IsInteriorPoint (f x)
⊢ Surjective ⇑(mfderiv% ↑hf.localInverse.toPartialEquiv (f x))

Tactic:
exact (hf.mfderivToContinuousLinearEquiv hn).symm.surjective

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
s t : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization F TotalSpace.proj := ⋯
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
ht : (MDiffAt[u] fun b ↦ (↑e ⟨b, t b⟩).2) x₀
⊢ ∀ x ∈ e.baseSet, (fun b ↦ (↑e ⟨b, (s + t) b⟩).2) x = ((fun b ↦ (↑e ⟨b, s b⟩).2) + fun b ↦ (↑e ⟨b, t b⟩).2) x

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

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

Goal state before:
pp: 𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
F₃ : Type u_12
M : Type u_13
inst✝²⁸ : NontriviallyNormedField 𝕜
E₁ : B → Type u_14
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)
E₂ : B → Type u_15
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)
E₃ : B → Type u_16
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 M
inst✝⁷ : FiberBundle F₁ E₁
inst✝⁶ : VectorBundle 𝕜 F₁ E₁
inst✝⁵ : FiberBundle F₂ E₂
inst✝⁴ : VectorBundle 𝕜 F₂ E₂
inst✝³ : FiberBundle F₃ E₃
inst✝² : VectorBundle 𝕜 F₃ E₃
b : M → B
v : (x : M) → E₁ (b x)
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₃ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₃ x)
ψ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x) →L[𝕜] E₃ (b x)
w : (x : M) → E₂ (b x)
hψ :
  Continuous[inst✝⁸,
      ContinuousLinearMap.topologicalSpaceTotalSpace (RingHom.id 𝕜) F₁ E₁ (F₂ →L[𝕜] F₃) fun x ↦ E₂ x →L[𝕜] E₃ x]
    fun m ↦ TotalSpace.mk' (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (b m) (ψ m)
hv : Continuous[inst✝⁸, inst✝²³] fun m ↦ TotalSpace.mk' F₁ (b m) (v m)
hw : Continuous[inst✝⁸, inst✝¹⁷] fun m ↦ TotalSpace.mk' F₂ (b m) (w m)
⊢ Continuous[inst✝⁸, inst✝¹¹] fun m ↦ TotalSpace.mk' F₃ (b m) (((ψ m) (v m)) (w m))

Tactic:
simp only [← continuousOn_univ] at hψ hv hw ⊢
  exact hψ.clm_bundle_apply₂ hv hw

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
g : G
V : (g : G) → TangentSpace I g
⊢ mulInvariantVectorField (V 1) g = mpullback I I (fun x ↦ g⁻¹ * x) V g

Tactic:
have A : 1 = g⁻¹ * g := by simp

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
g : G
V : (g : G) → TangentSpace I g
A : 1 = g⁻¹ * g
⊢ mulInvariantVectorField (V 1) g = mpullback I I (fun x ↦ g⁻¹ * x) V g
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case hxV
𝕜 : 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 V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hxV : V₁ x = V x
hW : W₁ =ᶠ[𝓝[s] x] W
hxW : W₁ x = W x
I1 : NormedAddCommGroup (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := ⋯
_I2 : NormedSpace 𝕜 (TangentSpace 𝓘(𝕜, E) (↑(extChartAt I x) x)) := inst✝²
⊢ mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V₁ (range ↑I) (↑(extChartAt I x) x) =
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I) (↑(extChartAt I x) x)

Tactic:
simp only [mpullbackWithin_apply]
    congr 1
    convert! hxV <;> exact extChartAt_to_inv x

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

Goal state before:
pp: case hV
𝕜 : 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
v w : GroupLieAlgebra I G
g : G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField v x⟩) (g⁻¹ * g)

pp: case hW
𝕜 : 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
v w : GroupLieAlgebra I G
g : G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField w x⟩) (g⁻¹ * g)

pp: case hf
𝕜 : 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
v w : GroupLieAlgebra I G
g : G
⊢ ContMDiffAt I I (minSmoothness 𝕜 3) (fun x ↦ g⁻¹ * x) g

pp: case hn
𝕜 : 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
v w : GroupLieAlgebra I G
g : G
⊢ minSmoothness 𝕜 2 ≤ minSmoothness 𝕜 3

Tactic:
· exact mdifferentiableAt_mulInvariantVectorField _

Goal state after:
case hW
𝕜 : 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
v w : GroupLieAlgebra I G
g : G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField w x⟩) (g⁻¹ * g)

case hf
𝕜 : 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
v w : GroupLieAlgebra I G
g : G
⊢ ContMDiffAt I I (minSmoothness 𝕜 3) (fun x ↦ g⁻¹ * x) g

case hn
𝕜 : 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
v w : GroupLieAlgebra I G
g : G
⊢ minSmoothness 𝕜 2 ≤ minSmoothness 𝕜 3