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

Goal state before:
pp: 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 = π
H5 : ¬angle y z = π
H6 :
  Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle x y) * Real.sin (angle y z) *
        ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
Hw : Real.sin (angle x y) * Real.sin (angle y z) ≠ 0
H8 : NormedSpace.normalize (ortho y x) = -NormedSpace.normalize (ortho y z)
H9 : ortho y x ≠ 0
H10 : ortho y z ≠ 0
H11 : ‖NormedSpace.normalize (ortho y x)‖ = 1
H12 : ‖NormedSpace.normalize (ortho y z)‖ = 1
⊢ 0 = Real.sin (angle y z) * (Real.sin (angle x y) * -1) + Real.sin (angle x y) * (Real.sin (angle z y) * 1)

Tactic:
grind [Real.sin_add, angle_comm]

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

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
y : V
hy left✝ : y ≠ 0
r : ℝ
hr : 0 < r
hxz₁ : ¬angle 0 (r • y) = π
hxz₂ : ¬angle 0 (r • y) = 0
h_sin_xz : Real.sin (angle 0 (r • y)) ≠ 0
⊢ y ∈ Submodule.span ℝ≥0 {0, r • y}

Tactic:
lift r to ℝ≥0 using hr.le

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
y : V
hy left✝ : y ≠ 0
r : ℝ≥0
hr : 0 < ↑r
hxz₁ : ¬angle 0 (↑r • y) = π
hxz₂ : ¬angle 0 (↑r • y) = 0
h_sin_xz : Real.sin (angle 0 (↑r • y)) ≠ 0
⊢ y ∈ Submodule.span ℝ≥0 {0, ↑r • y}
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : ¬x = 0
hxz₁ : ¬angle x 0 = π
hxz₂ : ¬angle x 0 = 0
h_sin_xz : Real.sin (angle x 0) ≠ 0
left✝ : x ≠ 0
r : ℝ
hr : 0 < r
hy : r • x ≠ 0
⊢ r • x ∈ Submodule.span ℝ≥0 {x, 0}

Tactic:
lift r to ℝ≥0 using hr.le

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : ¬x = 0
hxz₁ : ¬angle x 0 = π
hxz₂ : ¬angle x 0 = 0
h_sin_xz : Real.sin (angle x 0) ≠ 0
left✝ : x ≠ 0
r : ℝ≥0
hr : 0 < ↑r
hy : ↑r • x ≠ 0
⊢ ↑r • x ∈ Submodule.span ℝ≥0 {x, 0}
Module: Mathlib.Geometry.Euclidean.Circumcenter

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
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter
r₁ r₂ : ℝ
hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)
hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)
hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
h : s.points 0 ∈ span_s
hd₁ :
  r₁ * r₁ *
      ⟪p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p),
        p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)⟫ =
    r₂ * r₂ *
      ⟪p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p),
        p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)⟫
hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius
hp : p = ↑(s.orthogonalProjectionSpan p)
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) p₂

Tactic:
Simplex.orthogonalProjectionSpan

Goal state after:
case pos
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
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter
r₁ r₂ : ℝ
hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)
hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)
hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
h : s.points 0 ∈ span_s
hd₁ :
  r₁ * r₁ *
      ⟪p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p),
        p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)⟫ =
    r₂ * r₂ *
      ⟪p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p),
        p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)⟫
hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius
hp : p = ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) p₂
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case inr.inl
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₃
i : Fin (2 + 1)
h₁₂ : i₁ ≠ i
h₂₃ : i ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i i₁ + Simplex.touchpointWeights t {i₁} i i₃ = 1
⊢ Simplex.touchpointWeights t {i₁} i i =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i i₃) i

pp: case 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
i₁ i₂ : Fin 3
h₁₂ : i₁ ≠ i₂
i : Fin (2 + 1)
h₁₃ : i₁ ≠ i
h₂₃ : i₂ ≠ i
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i = 1
⊢ Simplex.touchpointWeights t {i₁} i₂ i =
    Finset.affineCombinationLineMapWeights i₁ i (Simplex.touchpointWeights t {i₁} i₂ i) i

Tactic:
· simp [h₁₂.symm, h₂₃]

Goal state after:
case 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
i₁ i₂ : Fin 3
h₁₂ : i₁ ≠ i₂
i : Fin (2 + 1)
h₁₃ : i₁ ≠ i
h₂₃ : i₂ ≠ i
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i = 1
⊢ Simplex.touchpointWeights t {i₁} i₂ i =
    Finset.affineCombinationLineMapWeights i₁ i (Simplex.touchpointWeights t {i₁} i₂ i) i
Module: Mathlib.Geometry.Euclidean.NinePointCircle

Goal state before:
pp: case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
hn : ¬n = 0
⊢ s.points i -ᵥ s.mongePoint - (↑n)⁻¹ • (s.points i -ᵥ s.mongePoint) = ((↑n - 1) / ↑n) • (s.points i -ᵥ s.mongePoint)

Tactic:
rw [sub_div, div_self (by simpa using hn), one_div, sub_smul, one_smul]

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
⊢ (n + 1) • (s.mongePoint -ᵥ s.circumcenter) = ∑ i, (s.points i -ᵥ s.circumcenter)

Tactic:
rw [mongePoint_eq_smul_vsub_vadd_circumcenter, vadd_vsub, ← smul_assoc]

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 + 2)
⊢ ((n + 1) • (↑(n + 2 + 1) / ↑(n + 2 - 1))) • (Finset.centroid ℝ univ s.points -ᵥ s.circumcenter) =
    ∑ i, (s.points i -ᵥ s.circumcenter)
Module: Mathlib.Geometry.Euclidean.Similarity

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
h_not_col : ¬Collinear ℝ {a, b, c}
h₁ : ∠ a b c = ∠ a' b' c'
h₂ : ∠ b c a = ∠ b' c' a'
hne_pi_div_two : ∠ a b c ≠ Real.pi / 2 ∨ ∠ b c a ≠ Real.pi / 2
not_all_eq : a' ≠ b' ∨ b' ≠ c' ∨ a' ≠ c'
h_not_col' : ¬Collinear ℝ {a', b', c'}
h_pos1 : 0 < dist a b
h_pos1' : 0 < dist a' b'
h_pos2 : 0 < dist b c
h_pos2' : 0 < dist b' c'
h₃ : ∠ c a b = ∠ c' a' b'
h_sin_ne1 : Real.sin (∠ b c a) ≠ 0
h_sin_ne2 : Real.sin (∠ c a b) ≠ 0
h_sin1 : Real.sin (∠ c a b) * dist a b = Real.sin (∠ b c a) * dist b c
⊢ ![a, b, c] ∼ ![a', b', c']

Tactic:
have h_sin1' := law_sin c' a' b'

Goal state after:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
h_not_col : ¬Collinear ℝ {a, b, c}
h₁ : ∠ a b c = ∠ a' b' c'
h₂ : ∠ b c a = ∠ b' c' a'
hne_pi_div_two : ∠ a b c ≠ Real.pi / 2 ∨ ∠ b c a ≠ Real.pi / 2
not_all_eq : a' ≠ b' ∨ b' ≠ c' ∨ a' ≠ c'
h_not_col' : ¬Collinear ℝ {a', b', c'}
h_pos1 : 0 < dist a b
h_pos1' : 0 < dist a' b'
h_pos2 : 0 < dist b c
h_pos2' : 0 < dist b' c'
h₃ : ∠ c a b = ∠ c' a' b'
h_sin_ne1 : Real.sin (∠ b c a) ≠ 0
h_sin_ne2 : Real.sin (∠ c a b) ≠ 0
h_sin1 : Real.sin (∠ c a b) * dist a b = Real.sin (∠ b c a) * dist b c
h_sin1' : Real.sin (∠ c' a' b') * dist a' b' = Real.sin (∠ b' c' a') * dist b' c'
⊢ ![a, b, c] ∼ ![a', b', c']
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₁ s₂ : Simplex ℝ P n
h : Set.range s₁.points = Set.range s₂.points
⊢ (↑(n + 1) / ↑(n - 1)) • (Finset.centroid ℝ univ s₂.points -ᵥ s₁.circumcenter) +ᵥ s₁.circumcenter =
    (↑(n + 1) / ↑(n - 1)) • (Finset.centroid ℝ univ s₂.points -ᵥ s₂.circumcenter) +ᵥ s₂.circumcenter

Tactic:
circumcenter_eq_of_range_eq h

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
he : s.Equilateral
i₁ i₂ : Fin (n + 1)
⊢ ∀ (i₃ : Fin (n + 1)), i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → ∠ (s.points i₁) (s.points i₂) (s.points i₃) < π / 2

Tactic:
i₃

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
he : s.Equilateral
i₁ i₂ i₃ : Fin (n + 1)
⊢ i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → ∠ (s.points i₁) (s.points i₂) (s.points i₃) < π / 2
Module: Mathlib.Geometry.Euclidean.Simplex

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
x✝ :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₁ i₂ : Fin (2 + 1)
⊢ ∀ (i₃ : Fin (2 + 1)), i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → ∠ (t.points i₁) (t.points i₂) (t.points i₃) < π / 2

Tactic:
i₃

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

Goal state before:
pp: case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
⊢ -(∑ i,
            ∑ i₂_1,
              (if i = i₁ ∨ i = i₂ then (↑(n + 1))⁻¹ else 0) *
                  (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
                (dist (s.points i) (s.pointsWithCircumcenter i₂_1) *
                  dist (s.points i) (s.pointsWithCircumcenter i₂_1)) +
          ∑ i₂_1,
            -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
              (dist s.circumcenter (s.pointsWithCircumcenter i₂_1) *
                dist s.circumcenter (s.pointsWithCircumcenter i₂_1))) /
      2 =
    0

Tactic:
have hfs : ∀ i : Fin (n + 3), i ∉ fs → i ≠ i₁ ∧ i ≠ i₂ := by
    intro i hi
    constructor <;> · intro hj; simp [fs, ← hj] at hi

Goal state after:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ -(∑ i,
            ∑ i₂_1,
              (if i = i₁ ∨ i = i₂ then (↑(n + 1))⁻¹ else 0) *
                  (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
                (dist (s.points i) (s.pointsWithCircumcenter i₂_1) *
                  dist (s.points i) (s.pointsWithCircumcenter i₂_1)) +
          ∑ i₂_1,
            -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
              (dist s.circumcenter (s.pointsWithCircumcenter i₂_1) *
                dist s.circumcenter (s.pointsWithCircumcenter i₂_1))) /
      2 =
    0
Module: Mathlib.Geometry.Euclidean.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
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ {p₁, p, p₃}
⊢ Cospherical {p₁, p₂, p₃, p₄}

Tactic:
have hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂ := angle_eq_pi_iff_sbtw.mp hp₁p₂

Goal state after:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ {p₁, p, p₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
⊢ Cospherical {p₁, p₂, p₃, p₄}
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : Sphere P
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)
⊢ (Finset.univ.weightedVSub sx.points) (r • (w - Pi.single i 1)) +ᵥ
      (Finset.affineCombination ℝ Finset.univ sx.points) (Pi.single i 1) ∈
    (sx.faceOpposite i).interior

Tactic:
Finset.weightedVSub_vadd_affineCombination,

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)
⊢ (Finset.affineCombination ℝ Finset.univ sx.points) (r • (w - Pi.single i 1) + Pi.single i 1) ∈
    (sx.faceOpposite i).interior
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
⊢ ∀ᶠ (y : M) in 𝓝 c, ‖f y‖ = ‖f c‖

Tactic:
by
  set e := extChartAt I c
  have hI : range I = univ := ModelWithCorners.Boundaryless.range_eq_univ
  have H₁ : 𝓝[range I] (e c) = 𝓝 (e c) := by rw [hI, nhdsWithin_univ]
  have H₂ : map e.symm (𝓝 (e c)) = 𝓝 c := by
    rw [← map_extChartAt_symm_nhdsWithin_range (I := I) c, H₁]
  rw [← H₂, eventually_map]
  replace hd : ∀ᶠ y in 𝓝 (e c), DifferentiableAt ℂ (f ∘ e.symm) y := by
    have : e.target ∈ 𝓝 (e c) := H₁ ▸ extChartAt_target_mem_nhdsWithin c
    filter_upwards [this, Tendsto.eventually H₂.le hd] with y hyt hy₂
    have hys : e.symm y ∈ (chartAt H c).source := by
      rw [← extChartAt_source I c]
      exact (extChartAt I c).map_target hyt
    have hfy : f (e.symm y) ∈ (chartAt F (0 : F)).source := mem_univ _
    rw [mdifferentiableAt_iff_of_mem_source hys hfy, hI, differentiableWithinAt_univ,
      e.right_inv hyt] at hy₂
    exact hy₂.2
  convert! norm_eventually_eq_of_isLocalMax hd _
  · exact congr_arg f (extChartAt_to_inv _).symm
  · simpa only [e, IsLocalMax, IsMaxFilter, ← H₂, (· ∘ ·), extChartAt_to_inv] using! hc

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : NormedAddCommGroup F
inst✝¹⁹ : NormedSpace 𝕜 F
inst✝¹⁸ : TopologicalSpace (TotalSpace F E)
inst✝¹⁷ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
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✝⁸ : TopologicalSpace B
inst✝⁷ : ChartedSpace HB B
inst✝⁶ : FiberBundle F E
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module 𝕜 (E x)
inst✝³ : VectorBundle 𝕜 F E
inst✝² : ContMDiffVectorBundle 1 F E IB
e : Trivialization F TotalSpace.proj
inst✝¹ : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e'
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : MDiffAt[s] (TotalSpace.proj ∘ f) x₀
he'f : (MDiffAt[s] fun x ↦ (↑e (f x)).2) x₀
he : f x₀ ∈ e.source
he' : f x₀ ∈ e'.source
⊢ (MDiffAt[s] fun x ↦ (↑e' (f x)).2) x₀

Tactic:
Trivialization.mem_source

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
inst✝²⁰ : NormedAddCommGroup F
inst✝¹⁹ : NormedSpace 𝕜 F
inst✝¹⁸ : TopologicalSpace (TotalSpace F E)
inst✝¹⁷ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
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✝⁸ : TopologicalSpace B
inst✝⁷ : ChartedSpace HB B
inst✝⁶ : FiberBundle F E
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module 𝕜 (E x)
inst✝³ : VectorBundle 𝕜 F E
inst✝² : ContMDiffVectorBundle 1 F E IB
e : Trivialization F TotalSpace.proj
inst✝¹ : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e'
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : MDiffAt[s] (TotalSpace.proj ∘ f) x₀
he'f : (MDiffAt[s] fun x ↦ (↑e (f x)).2) x₀
he : (f x₀).proj ∈ e.baseSet
he' : (f x₀).proj ∈ e'.baseSet
⊢ (MDiffAt[s] fun x ↦ (↑e' (f x)).2) x₀
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)) s m₀
hv : ContinuousWithinAt (fun m ↦ { proj := b₁ m, snd := v m }) s m₀
hb₂ : ContinuousWithinAt b₂ s m₀
⊢ ContinuousWithinAt (fun m ↦ { proj := b₂ m, snd := (ϕ m) (v m) }) s m₀

Tactic:
← continuousWithinAt_insert_self

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 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₀