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

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
inst✝ : NeZero n
i j : Fin (n + 1)
h : i ≠ j
⊢ ⟪s.points i -ᵥ s.points j, s.points i -ᵥ s.altitudeFoot i⟫ = s.height i ^ 2

Tactic:
suffices ⟪s.points j -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫ = 0 by
    rwa [height, inner_vsub_vsub_left_eq_dist_sq_right_iff, inner_vsub_left_eq_zero_symm]
  exact s.inner_vsub_altitudeFoot_vsub_altitudeFoot_eq_zero h

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

Goal state before:
pp: case a
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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| ≤ s.height i * s.height j

Tactic:
convert! abs_real_inner_le_norm _ _ using 1

Goal state after:
case e'_4
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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ s.height i * s.height j = ‖s.points i -ᵥ s.altitudeFoot i‖ * ‖s.points j -ᵥ s.altitudeFoot j‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

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
p₀ p : P
⊢ ∠ p₀ p₀ p = π / 2

Tactic:
angle_self_left

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₀ p : P
⊢ π / 2 = π / 2
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

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
p₁ p₂ p₃ : P
h : ∠ p₂ p₂ p₃ = π
heq : p₁ = p₂
⊢ False

Tactic:
angle_self_left

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : π / 2 = π
heq : p₁ = p₂
⊢ False
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case inr
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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ |(-⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫)| < s.height i * s.height j

Tactic:
abs_neg

Goal state after:
case inr
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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| < s.height i * s.height j
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle x z - o.oangle y z = o.oangle x y

Tactic:
by rw [sub_eq_iff_eq_add, o.oangle_add hx hy hz]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ |(o.oangle x y).toReal| = 0 ∨ |(o.oangle x y).toReal| = π

Tactic:
Real.Angle.sign_eq_zero_iff

Goal state after:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = 0 ∨ o.oangle x y = ↑π
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ |(o.oangle x y).toReal| = 0 ∨ |(o.oangle x y).toReal| = π
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x + y) y).sin = ‖x‖ / ‖x + y‖

Tactic:
by
  rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
  rw [add_comm]
  exact (-o).sin_oangle_add_right_of_oangle_eq_pi_div_two h

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ ‖x‖ / (o.oangle x (x + y)).cos = ‖x + y‖

Tactic:
have hs : (o.oangle x (x + y)).sign = 1 := by
    rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
  rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    InnerProductGeometry.norm_div_cos_angle_add_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inl (o.left_ne_zero_of_oangle_eq_pi_div_two h))]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

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)
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
⊢ ∡ p₃ p₁ p₂ = 0

Tactic:
by
  rw [oangle_eq_zero_iff_oangle_rev_eq_zero, h.oangle₂₁₃_eq_zero]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

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)
p₁ p₂ p₃ : P
h₁₂ : p₁ ≠ p₂
h₃₂ : p₃ ≠ p₂
⊢ ∡ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) = ∡ p₁ p₂ p₃ + ↑π

Tactic:
have h₂₃' : (AffineEquiv.pointReflection ℝ p₂) p₃ ≠ p₂ := by
    conv_rhs => rw [← AffineEquiv.pointReflection_self ℝ p₂]
    rw [(AffineEquiv.pointReflection ℝ p₂).injective.ne_iff]
    exact h₃₂
  rw [← sub_eq_iff_eq_add', oangle_sub_left h₁₂ h₃₂ h₂₃']
  exact Sbtw.oangle₁₂₃_eq_pi <| sbtw_pointReflection_of_ne ℝ h₃₂.symm

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

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
v : V
p q : P
r : ℝ
h : 0 < r
⊢ ((signedDist (r • v)) p) q = ((signedDist v) p) q

Tactic:
simp [signedDist_smul, h]

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

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
v : V
p q : P
r : ℝ
h : r < 0
⊢ ((signedDist (r • v)) p) q = -((signedDist v) p) q

Tactic:
simp [signedDist_smul, h]

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

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
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ (-∑ i₁ ∈ s₁,
          ∑ i₂ ∈ s₂,
            w₁ i₁ * w₂ i₂ *
              (‖p₁ i₁ -ᵥ Classical.choice ⋯ - (p₂ i₂ -ᵥ Classical.choice ⋯)‖ *
                ‖p₁ i₁ -ᵥ Classical.choice ⋯ - (p₂ i₂ -ᵥ Classical.choice ⋯)‖)) /
      2 =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2

Tactic:
vsub_sub_vsub_cancel_right

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ (-∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * w₂ x_1 * (‖p₁ x -ᵥ p₂ x_1‖ * ‖p₁ x -ᵥ p₂ x_1‖)) / 2 =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: P : Type u_2
inst✝ : MetricSpace P
p : P
⊢ Cospherical {p}

Tactic:
by
  use p
  simp

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ dist p₁ p₂ = 2 * s.radius

Tactic:
by
  rw [← mem_sphere.1 h.left_mem, ← h.midpoint_eq_center, dist_left_midpoint]
  simp

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

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
⊢ s.orthRadius s.center = ⊤

Tactic:
simp [orthRadius]

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

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 q : P
as : AffineSubspace ℝ P
hp : s.IsTangentAt p as
hq : s.IsTangentAt q as
hqp : ⟪p -ᵥ q, p -ᵥ s.center - (q -ᵥ s.center)⟫ = 0
hpq : ⟪p -ᵥ q, q -ᵥ s.center⟫ = 0
⊢ p = q

Tactic:
vsub_sub_vsub_cancel_right

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
p q : P
as : AffineSubspace ℝ P
hp : s.IsTangentAt p as
hq : s.IsTangentAt q as
hqp : ⟪p -ᵥ q, p -ᵥ q⟫ = 0
hpq : ⟪p -ᵥ q, q -ᵥ s.center⟫ = 0
⊢ p = q
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case refine_1.refine_1
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : Sphere P
as : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥as
inst✝ : as.direction.HasOrthogonalProjection
h : dist s.center ↑((orthogonalProjection as) s.center) = s.radius
⊢ ↑((orthogonalProjection as) s.center) ∈ s

Tactic:
rwa [mem_sphere']

Goal state after:
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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
p : P
hp : p ∈ affineSpan ℝ (Set.range s.points)
i₁ : Fin (n + 1)
h :
  ∀ (i₂ : Fin (n + 1)),
    i₂ ≠ i₁ →
      ∃ p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points),
        p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points) ∧
          ∠ p p' ↑((s.faceOpposite i₁).orthogonalProjectionSpan p) =
            ∠ p p' ↑((s.faceOpposite i₂).orthogonalProjectionSpan p)
⊢ ∃ signs, s.ExcenterExists signs ∧ p = s.excenter signs

Tactic:
by
  rw [← s.exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter hp]
  refine ⟨dist p ((s.faceOpposite i₁).orthogonalProjectionSpan p), ?_⟩
  intro i
  by_cases hi : i = i₁
  · rw [hi]
  obtain ⟨p', hp'₁, hp'₂, ha⟩ := h i hi
  exact ((dist_orthogonalProjection_eq_iff_angle_eq hp'₁ hp'₂).2 ha).symm

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

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
inst✝ : Nontrivial V
s : Sphere P
⊢ (∃ p, s.IsIntTangentAt s p) ↔ 0 ≤ s.radius

Tactic:
isIntTangentAt_self_iff_mem

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : Nontrivial V
s : Sphere P
⊢ (∃ p, p ∈ s) ↔ 0 ≤ s.radius
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))
⊢ ∑ i, s.excenterWeights signs i = 1 ↔ s.ExcenterExists signs

Tactic:
classical
  simp [sum_excenterWeights]

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

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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hr : s.radius ≠ 0
h : ∠ p₁ s.center p₂ = 0
⊢ InnerProductGeometry.angle (p₁ -ᵥ ?m.42) (p₂ -ᵥ ?m.42) = 0

Tactic:
by simpa [angle] using h

Goal state after:
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
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : s.excenter signs ∈ affineSpan ℝ (s.points '' ↑fs)
⊢ ∃ i, i ∉ ↑fs

Tactic:
simp only [SetLike.mem_coe]
    have hc : #fs < #(Finset.univ : Finset (Fin (n + 1))) := by
      have : m + 1 ≤ #fs := hfs.ge
      grw [fs.subset_univ] at this
      simp only [Finset.card_univ, Fintype.card_fin] at *
      lia
    obtain ⟨i, -, hi⟩ := Finset.exists_mem_notMem_of_card_lt_card hc
    exact ⟨i, hi⟩

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

Goal state before:
pp: case inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ ↑π
hs : (o.oangle x y).sign = 0
h : o.oangle x (x - y) = o.oangle (y - x) y + ↑π
⊢ ‖x‖ = ‖y‖

Tactic:
Real.Angle.sign_eq_zero_iff

Goal state after:
case inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ ↑π
hs : o.oangle x y = 0 ∨ o.oangle x y = ↑π
h : o.oangle x (x - y) = o.oangle (y - x) y + ↑π
⊢ ‖x‖ = ‖y‖
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)
⊢ (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SSameSide
      ((Finset.affineCombination ℝ Finset.univ s.points) (s.excenterWeights signs)) (s.points i) ↔
    0 < s.excenterWeights signs i

Tactic:
s.sSameSide_affineSpan_faceOpposite_point_right_iff h.sum_excenterWeights_eq_one

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)
⊢ 0 < s.excenterWeights signs i ↔ 0 < s.excenterWeights signs i
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.circumcenter = (affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter n)

Tactic:
rw [← pointsWithCircumcenter_eq_circumcenter]

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
⊢ s.pointsWithCircumcenter circumcenterIndex =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter n)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ x = ⟪y, x⟫ • y + (‖x - ⟪y, x⟫ • y‖⁻¹ * (1 ^ 2 - ⟪y, x⟫ ^ 2)) • ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)

Tactic:
mul_smul,

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ x = ⟪y, x⟫ • y + ‖x - ⟪y, x⟫ • y‖⁻¹ • (1 ^ 2 - ⟪y, x⟫ ^ 2) • ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
this : s.excenter signs -ᵥ s.touchpoint signs i ∈ (vectorSpan ℝ (Set.range s.points))ᗮ
h' : s.excenter signs -ᵥ s.touchpoint signs i ∈ vectorSpan ℝ (Set.range s.points)
⊢ False

Tactic:
have h0 : s.excenter signs -ᵥ s.touchpoint signs i = 0 := by
        rw [← Submodule.mem_bot ℝ,
          ← Submodule.inf_orthogonal_eq_bot (vectorSpan ℝ (Set.range s.points))]
        exact ⟨h', this⟩

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
this : s.excenter signs -ᵥ s.touchpoint signs i ∈ (vectorSpan ℝ (Set.range s.points))ᗮ
h' : s.excenter signs -ᵥ s.touchpoint signs i ∈ vectorSpan ℝ (Set.range s.points)
h0 : s.excenter signs -ᵥ s.touchpoint signs i = 0
⊢ False
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
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
⊢ ∃ r, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r

Tactic:
by
  rw [cospherical_iff_exists_mem_of_finiteDimensional h] at hc
  rcases hc with ⟨c, hc, r, hcr⟩
  use r
  intro sx hsxps
  have hsx : affineSpan ℝ (Set.range sx.points) = s := by
    refine
      sx.independent.affineSpan_eq_of_le_of_card_eq_finrank_add_one
        (affineSpan_le_of_subset_coe (hsxps.trans h)) ?_
    simp [hd]
  have hc : c ∈ affineSpan ℝ (Set.range sx.points) := hsx.symm ▸ hc
  exact
    (sx.eq_circumradius_of_dist_eq hc fun i =>
        hcr (sx.points i) (hsxps (Set.mem_range_self i))).symm

Goal state after:
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 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
h3 : Real.sin (π - ∠ a b c) ≤ Real.sin (∠ a c b)
h5 : π - ∠ a b c < π / 2
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
⊢ ∠ b a c > 0

Tactic:
rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at 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
a b c : P
h : ¬Collinear ℝ {b, a, 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 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
h3 : Real.sin (π - ∠ a b c) ≤ Real.sin (∠ a c b)
h5 : π - ∠ a b c < π / 2
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ a c b + ∠ c a b = π
⊢ ∠ b a c > 0
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
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
⊢ sx₁.circumradius = sx₂.circumradius

Tactic:
rcases exists_circumradius_eq_of_cospherical hd hc with ⟨r, hr⟩
  rw [hr sx₁ hsx₁, hr sx₂ hsx₂]

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

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 : ℕ
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
⊢ False

Tactic:
· suffices s.excenter signs -ᵥ s.touchpoint signs i ∈ (vectorSpan ℝ (Set.range s.points))ᗮ by
      have h' : s.excenter signs -ᵥ s.touchpoint signs i ∈ (vectorSpan ℝ (Set.range s.points)) := by
        rw [← direction_affineSpan]
        exact AffineSubspace.vsub_mem_direction h.excenter_mem_affineSpan_range
          (s.touchpoint_mem_affineSpan_simplex _ _)
      have h0 : s.excenter signs -ᵥ s.touchpoint signs i = 0 := by
        rw [← Submodule.mem_bot ℝ,
          ← Submodule.inf_orthogonal_eq_bot (vectorSpan ℝ (Set.range s.points))]
        exact ⟨h', this⟩
      rw [← norm_eq_zero, ← dist_eq_norm_vsub, h.dist_excenter] at h0
      exact h.exradius_pos.ne' h0
    obtain ⟨k, hki, hkj⟩ : ∃ k, k ≠ i ∧ k ≠ j := Fin.exists_ne_and_ne_of_two_lt i j (by lia)
    have hu : Set.range s.points =
        Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points := by
      simp only [range_faceOpposite_points, ← Set.image_union, ← Set.compl_inter]
      convert! Set.image_univ.symm
      simp [Ne.symm hne]
    rw [hu, range_faceOpposite_points, range_faceOpposite_points,
      AffineSubspace.vectorSpan_union_of_mem_of_mem ℝ (p := s.points k)
        (Set.mem_image_of_mem _ (by simp [hki])) (Set.mem_image_of_mem _ (by simp [hkj])),
      ← Submodule.inf_orthogonal]
    refine ⟨?_, ?_⟩
    · rw [← direction_affineSpan, ← range_faceOpposite_points]
      exact vsub_orthogonalProjection_mem_direction_orthogonal _ _
    · rw [hij, ← direction_affineSpan, ← range_faceOpposite_points]
      exact vsub_orthogonalProjection_mem_direction_orthogonal _ _

Goal state after:
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}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
h2 : ∠ a b c = ∠ a c b
⊢ ∠ b a c ≠ π

Tactic:
rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at 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
a b c : P
h : ¬Collinear ℝ {b, a, c}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
h2 : ∠ a b c = ∠ a c b
⊢ ∠ b a c ≠ π
Module: Mathlib.Geometry.Euclidean.Triangle

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

Tactic:
angle_self_left

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : p₂ = p₁
⊢ π / 3 ≤ π / 2