mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃) + ↑π
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}

Tactic:
have hs := t.excenter_eq_incenter_or_excenter_singleton_of_ne signs h₁₂ h₁₃ h₂₃

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃) + ↑π
hs :
  excenter t signs = incenter t ∨
    excenter t signs = excenter t {i₁} ∨ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case h.left.right
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
p₁ : P
hp₁ : p₁ ∈ insert p ps
⊢ p₁ ∈ Metric.sphere { center := cc₂, radius := cr₂ }.center { center := cc₂, radius := cr₂ }.radius

Tactic:
rw [Sphere.mem_coe, mem_sphere, ← mul_self_inj_of_nonneg dist_nonneg (Real.sqrt_nonneg _),
        Real.mul_self_sqrt (add_nonneg (mul_self_nonneg _) (mul_self_nonneg _))]

Goal state after:
case h.left.right
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
p₁ : P
hp₁ : p₁ ∈ insert p ps
⊢ dist p₁ { center := cc₂, radius := cr₂ }.center * dist p₁ { center := cc₂, radius := cr₂ }.center =
    cr * cr + ycc₂ * ycc₂
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)
⊢ s.excenter signs ≠ s.points i

Tactic:
have hf := h.excenter_notMem_affineSpan_face (fs := {i}) (m := 0) (by simp) (NeZero.ne' _)

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)
hf : s.excenter signs ∉ affineSpan ℝ (Set.range (s.face ⋯).points)
⊢ s.excenter signs ≠ s.points i
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
inst✝ : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
⊢ s.excenter signs ∉ line[ℝ, s.points i, s.points j]

Tactic:
by
  by_cases hij : i = j
  · simp only [hij, Set.mem_singleton_iff, Set.insert_eq_of_mem,
      AffineSubspace.mem_affineSpan_singleton]
    exact h.excenter_ne_point j
  · convert!
    h.excenter_notMem_affineSpan_face (fs := { i, j }) (m := 1) (by simp_all)
      Nat.AtLeastTwo.ne_one.symm
    simp [Set.image_insert_eq]

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

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ (1 + (∡ p₂ p₁ s.center).tan ^ 2) * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ +
      ‖(∡ p₂ p₁ s.center).tan‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * (‖(∡ p₂ p₁ s.center).tan‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖)

Tactic:
conv_rhs =>
      rw [← mul_assoc, mul_comm _ ‖Real.Angle.tan _‖, ← mul_assoc, Real.norm_eq_abs,
        abs_mul_abs_self]

Goal state after:
V : Type u_3
P : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ (1 + (∡ p₂ p₁ s.center).tan ^ 2) * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ +
      (∡ p₂ p₁ s.center).tan * (∡ p₂ p₁ s.center).tan * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖
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
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
r : ℝ
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
⊢ p = s.circumcenter

Tactic:
have h := s.circumsphere_unique_dist_eq.2 ⟨p, r⟩

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
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
r : ℝ
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
h :
  { center := p, radius := r }.center ∈ affineSpan ℝ (Set.range s.points) ∧
      Set.range s.points ⊆ Metric.sphere { center := p, radius := r }.center { center := p, radius := r }.radius →
    { center := p, radius := r } = s.circumsphere
⊢ p = s.circumcenter
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
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
r : ℝ
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
⊢ r = s.circumradius

Tactic:
have h := s.circumsphere_unique_dist_eq.2 ⟨p, r⟩

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
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
r : ℝ
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
h :
  { center := p, radius := r }.center ∈ affineSpan ℝ (Set.range s.points) ∧
      Set.range s.points ⊆ Metric.sphere { center := p, radius := r }.center { center := p, radius := r }.radius →
    { center := p, radius := r } = s.circumsphere
⊢ r = s.circumradius
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
inst✝ : n.AtLeastTwo
i : Fin (n + 1)
h : {i} = ∅ ∨ {i} = Finset.univ
⊢ False

Tactic:
simp at h

Goal state after:
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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
this : Nonempty ↥S
⊢ s.circumcenter = ↑(s.restrict S hS).circumcenter

Tactic:
exact (s.restrict S hS).circumcenter_map S.subtypeₐᵢ

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

Goal state before:
pp: α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
⊢ univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

Tactic:
ext x

Goal state after:
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
x : PointsWithCircumcenterIndex n
⊢ x ∈ univ ↔ x ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
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}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : ∠ a b c ≤ π / 2
h3 : Real.sin (∠ a c b) < Real.sin (∠ a b c)
w : dist a c ≤ dist a b
⊢ Real.sin (∠ a c b) * dist a c < Real.sin (∠ a b c) * dist a b

Tactic:
exact mul_lt_mul h3 w hac hsinabc

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

Goal state before:
pp: case left
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ⟪x, y⟫ = 1
⊢ x - ⟪x, y⟫ • y = 0

Tactic:
inner_eq_one_iff_of_norm_eq_one hx hy

Goal state after:
case left
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : x = y
⊢ x - ⟪x, y⟫ • y = 0
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

Goal state after:
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
x : P
⊢ x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c ↑(perpBisector c (inversion c R y))
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
⊢ -(∑ i,
            ∑ i₂_1,
              mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ (pointIndex i) *
                  (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
                (dist (s.pointsWithCircumcenter (pointIndex i)) (s.pointsWithCircumcenter i₂_1) *
                  dist (s.pointsWithCircumcenter (pointIndex i)) (s.pointsWithCircumcenter i₂_1)) +
          ∑ i₂_1,
            mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ circumcenterIndex *
                (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
              (dist (s.pointsWithCircumcenter circumcenterIndex) (s.pointsWithCircumcenter i₂_1) *
                dist (s.pointsWithCircumcenter circumcenterIndex) (s.pointsWithCircumcenter i₂_1))) /
      2 =
    0

Tactic:
pointsWithCircumcenter_eq_circumcenter

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
⊢ -(∑ i,
            ∑ i₂_1,
              mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ (pointIndex i) *
                  (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i₂_1 *
                (dist (s.pointsWithCircumcenter (pointIndex i)) (s.pointsWithCircumcenter i₂_1) *
                  dist (s.pointsWithCircumcenter (pointIndex i)) (s.pointsWithCircumcenter i₂_1)) +
          ∑ i₂_1,
            mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ circumcenterIndex *
                (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.MongePoint

Goal state before:
pp: case left
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 : Fin (n + 3)
hi : i ∉ fs
⊢ i ≠ i₁

Tactic:
intro hj; simp [fs, ← hj] at hi

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

Goal state before:
pp: case right
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 : Fin (n + 3)
hi : i ∉ fs
⊢ i ≠ i₂

Tactic:
intro hj; simp [fs, ← hj] at hi

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)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (Submodule.span ℝ (⋃ i, {s.points i₁ -ᵥ s.points ↑i}))ᗮ
⊢ ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x ↦ s.points i₁ -ᵥ s.points x) '' (Set.univ \ {i₁})

Tactic:
ext x

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)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (Submodule.span ℝ (⋃ i, {s.points i₁ -ᵥ s.points ↑i}))ᗮ
x : V
⊢ x ∈ ⋃ i, {s.points i₁ -ᵥ s.points ↑i} ↔ x ∈ (fun x ↦ s.points i₁ -ᵥ s.points x) '' (Set.univ \ {i₁})
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' : P
⊢ Collinear ℝ {p, p', s.secondInter p (p' -ᵥ p)}

Tactic:
by
  rw [Set.pair_comm, Set.insert_comm]
  exact
    (collinear_insert_iff_of_mem_affineSpan (s.secondInter_vsub_mem_affineSpan _ _)).2
      (collinear_pair ℝ _ _)

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
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)
⊢ (∀ (i_1 : Fin (n + 1)), ¬i_1 = i → 0 < r * (w i_1 - Pi.single i 1 i_1) + Pi.single i 1 i_1) ∧ r * (w i - 1) + 1 = 0

Tactic:
refine ⟨fun j hj ↦ ?_, by grind⟩

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)
j : Fin (n + 1)
hj : ¬j = i
⊢ 0 < r * (w j - Pi.single i 1 j) + Pi.single i 1 j
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case right
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ t₁.points i₁ ∈ affineSpan ℝ (Set.range t₂.points) ∧
    t₁.points i₁ -ᵥ t₁.points i₂ ∈ (affineSpan ℝ (t₂.points '' {j₂}ᶜ)).directionᗮ

Tactic:
have he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points) := by
    refine ext_of_direction_eq ?_
      ⟨t₁.points i₃, mem_affineSpan ℝ ⟨j₃, h₃⟩, mem_affineSpan ℝ (Set.mem_range_self _)⟩
    refine Submodule.eq_of_le_of_finrank_eq (direction_le (affineSpan_le_of_subset_coe ?_))
      ?_
    · have hu : (Set.univ : Set (Fin 3)) = {j₁, j₂, j₃} := by grind
      rw [← Set.image_univ, hu, Set.image_insert_eq, Set.image_insert_eq, Set.image_singleton, h₁,
        h₂, h₃, Set.insert_subset_iff, Set.insert_subset_iff, Set.singleton_subset_iff]
      exact
        ⟨t₁.orthocenter_mem_affineSpan, mem_affineSpan ℝ (Set.mem_range_self _),
          mem_affineSpan ℝ (Set.mem_range_self _)⟩
    · rw [direction_affineSpan, direction_affineSpan,
        t₁.independent.finrank_vectorSpan (Fintype.card_fin _),
        t₂.independent.finrank_vectorSpan (Fintype.card_fin _)]

Goal state after:
case right
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
he : affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)
⊢ t₁.points i₁ ∈ affineSpan ℝ (Set.range t₂.points) ∧
    t₁.points i₁ -ᵥ t₁.points i₂ ∈ (affineSpan ℝ (t₂.points '' {j₂}ᶜ)).directionᗮ
Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
E'' : Type u_7
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝¹⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace H'' N'
n : ℕ∞ω
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : ContMDiffMul I' n G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : ContMDiffMul I'' n G''
φ : G' →* G''
hφ : ContMDiff I' I'' n ⇑φ
f g : C^n⟮I, N; I', G'⟯
⊢ ⟨⇑φ ∘ ⇑(f * g), ⋯⟩ = ⟨⇑φ ∘ ⇑f, ⋯⟩ * ⟨⇑φ ∘ ⇑g, ⋯⟩

Tactic:
ext x

Goal state after:
𝕜 : Type u_1
inst✝²¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝²⁰ : NormedAddCommGroup E
inst✝¹⁹ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁴ : TopologicalSpace N
inst✝¹³ : ChartedSpace H N
E'' : Type u_7
inst✝¹² : NormedAddCommGroup E''
inst✝¹¹ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝¹⁰ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁹ : TopologicalSpace N'
inst✝⁸ : ChartedSpace H'' N'
n : ℕ∞ω
G' : Type u_10
inst✝⁷ : Monoid G'
inst✝⁶ : TopologicalSpace G'
inst✝⁵ : ChartedSpace H' G'
inst✝⁴ : ContMDiffMul I' n G'
G'' : Type u_11
inst✝³ : Monoid G''
inst✝² : TopologicalSpace G''
inst✝¹ : ChartedSpace H'' G''
inst✝ : ContMDiffMul I'' n G''
φ : G' →* G''
hφ : ContMDiff I' I'' n ⇑φ
f g : C^n⟮I, N; I', G'⟯
x : N
⊢ ⟨⇑φ ∘ ⇑(f * g), ⋯⟩ x = (⟨⇑φ ∘ ⇑f, ⋯⟩ * ⟨⇑φ ∘ ⇑g, ⋯⟩) x
Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝¹¹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝¹⁰ : TopologicalSpace N
inst✝⁹ : ChartedSpace H N
E'' : Type u_7
inst✝⁸ : NormedAddCommGroup E''
inst✝⁷ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁶ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace H'' N'
n : ℕ∞ω
R : Type u_10
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : ChartedSpace H' R
inst✝ : ContMDiffRing I' n R
a b c : C^n⟮I, N; I', R⟯
⊢ a * (b + c) = a * b + a * c

Tactic:
by ext; exact left_distrib _ _ _

Goal state after: