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

Goal state before:
pp: case mp
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
h : Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)
hr : 0 ≤ s.radius
h' : ∀ (q' : P), q' -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖q' -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2 ↔ q' = q
hq' : q -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖q -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
hq'' : (-(q -ᵥ p) +ᵥ p) -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖(-(q -ᵥ p) +ᵥ p) -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
hqq : -(q -ᵥ p) +ᵥ p = q
⊢ q = p ∧ dist p s.center = s.radius

Tactic:
eq_comm,

Goal state after:
case mp
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
h : Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)
hr : 0 ≤ s.radius
h' : ∀ (q' : P), q' -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖q' -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2 ↔ q' = q
hq' : q -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖q -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
hq'' : (-(q -ᵥ p) +ᵥ p) -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖(-(q -ᵥ p) +ᵥ p) -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
hqq : q = -(q -ᵥ p) +ᵥ p
⊢ q = p ∧ dist p s.center = s.radius
Module: Mathlib.Geometry.Euclidean.Sphere.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
s : Sphere P
p₁ p₂ : P
x✝ : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
⊢ (s.center -ᵥ p₁) +ᵥ s.center = p₂

Tactic:
eq_comm,

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₁ p₂ : P
x✝ : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
⊢ p₂ = (s.center -ᵥ p₁) +ᵥ s.center
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
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
s : Sphere P
p : P
hp : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr0 : r ≠ 0
hr' : s.radius = |r| * s.radius
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)

Tactic:
right_eq_mul₀ hrad

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
s : Sphere P
p : P
hp : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr0 : r ≠ 0
hr' : |r| = 1
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)
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
p : P
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
this : FiniteDimensional ℝ V
ha : ℝ ∙ (p -ᵥ s.center) = ⊤
hpo : p' = p
⊢ ¬0 = s.radius ^ 2 - dist p s.center ^ 2

Tactic:
eq_comm,

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 : P
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
this : FiniteDimensional ℝ V
ha : ℝ ∙ (p -ᵥ s.center) = ⊤
hpo : p' = p
⊢ ¬s.radius ^ 2 - dist p s.center ^ 2 = 0
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
p : P
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
this : FiniteDimensional ℝ V
ha : ℝ ∙ (p -ᵥ s.center) = ⊤
hpo : p' = p
⊢ ¬s.radius ^ 2 = dist p s.center ^ 2

Tactic:
eq_comm,

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 : P
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
this : FiniteDimensional ℝ V
ha : ℝ ∙ (p -ᵥ s.center) = ⊤
hpo : p' = p
⊢ ¬dist p s.center ^ 2 = s.radius ^ 2
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: case inl.inr.inl
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
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : ℝ ∙ (p -ᵥ s.center) = ⊤
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V

pp: case inl.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : ℝ ∙ (p -ᵥ s.center) ≠ ⊤
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V

Tactic:
· have hb' := hb
        rw [Submodule.span_singleton_eq_top_iff] at hb'
        have hf := finrank_eq_one_iff'.2 ⟨p -ᵥ s.center, vsub_ne_zero.2 hp, hb'⟩
        simpa [hf] using inter_orthRadius_eq_empty_of_finrank_eq_one hp h.ne

Goal state after:
case inl.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : ℝ ∙ (p -ᵥ s.center) ≠ ⊤
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅ ↔ Module.finrank ℝ V = 1 ∨ Subsingleton V
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
p : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : ℝ ∙ (p -ᵥ s.center) ≠ ⊤
hn : ¬Subsingleton V
v : V
hv0 : v ≠ 0
hv : ∀ (w : V), ∃ c, c • v = w
hc : 0 = p -ᵥ s.center
⊢ False

Tactic:
eq_comm,

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 : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : ℝ ∙ (p -ᵥ s.center) ≠ ⊤
hn : ¬Subsingleton V
v : V
hv0 : v ≠ 0
hv : ∀ (w : V), ∃ c, c • v = w
hc : p -ᵥ s.center = 0
⊢ False
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

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
inst✝ : Nontrivial V
s₁ s₂ : Sphere P
h : 0 = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.center = s₂.center
⊢ s₁.IsIntTangent s₂

Tactic:
eq_comm,

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
inst✝ : Nontrivial V
s₁ s₂ : Sphere P
h : s₂.radius - s₁.radius = 0
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.center = s₂.center
⊢ s₁.IsIntTangent s₂
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₃
p : P
h₁ : 2 • ∡ (t.points i₂) (t.points i₁) p = 2 • ∡ p (t.points i₁) (t.points i₃)
h₂ : 2 • ∡ (t.points i₃) (t.points i₂) p = 2 • ∡ p (t.points i₂) (t.points i₁)
⊢ ∃ signs, p = excenter t signs

Tactic:
by
  rw [← dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃] at h₁
  rw [← dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq h₂₃ h₁₂.symm h₁₃.symm]
    at h₂
  have hp : p ∈ affineSpan ℝ (Set.range t.points) := by
    convert! AffineSubspace.mem_top ℝ V p
    rw [t.independent.affineSpan_eq_top_iff_card_eq_finrank_add_one]
    simp [hd2.out]
  have hr : ∃ r : ℝ, ∀ i, dist p ((t.faceOpposite i).orthogonalProjectionSpan p) = r := by
    refine ⟨dist p ((faceOpposite t i₃).orthogonalProjectionSpan p), ?_⟩
    intro i
    have h : i = i₁ ∨ i = i₂ ∨ i = i₃ := by clear! p t; decide +revert
    rcases h with rfl | rfl | rfl <;> grind
  obtain ⟨signs, -, hp⟩ :=
    (t.exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter hp).1 hr
  exact ⟨signs, hp⟩

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

Goal state before:
pp: case e'_3
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
i : Fin (n + 1)
hi : i ≠ 0
⊢ 0 =
    (s.height 0)⁻¹ ^ 2 * ⟪s.points i -ᵥ s.points 0, s.points 0 -ᵥ s.altitudeFoot 0⟫ +
      (s.height i)⁻¹ ^ 2 * s.height i ^ 2

Tactic:
← neg_vsub_eq_vsub_rev,

Goal state after:
case e'_3
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
i : Fin (n + 1)
hi : i ≠ 0
⊢ 0 =
    (s.height 0)⁻¹ ^ 2 * ⟪-(s.points 0 -ᵥ s.points i), s.points 0 -ᵥ s.altitudeFoot 0⟫ +
      (s.height i)⁻¹ ^ 2 * s.height i ^ 2
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
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₂ p₃ p₁
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ 2 • o.oangle (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) = 2 • o.oangle (p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) (p₂ -ᵥ p₁)

Tactic:
eq_comm,

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✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₂ p₃ p₁
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ 2 • o.oangle (p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) (p₂ -ᵥ p₁) = 2 • o.oangle (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁))
Module: Mathlib.Geometry.Euclidean.Triangle

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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ a b c = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
hp : ∠ b p c = π
hp' : ∠ c p b = π
⊢ ∠ b a p + ∠ p a c = ∠ b a c

Tactic:
angle_comm a b c

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
a b c p : P
hb : a ≠ b
hc : a ≠ c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ c b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
hp : ∠ b p c = π
hp' : ∠ c p b = π
⊢ ∠ b a p + ∠ p a c = ∠ b a c
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))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : ∑ i, w i = 1
hp : (Finset.affineCombination ℝ Finset.univ s.points) w ∈ affineSpan ℝ (Set.range s.points)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) = (if i ∈ signs then -1 else 1) * r
i : Fin (n + 1)
h' : w i * dist (s.points i) (s.altitudeFoot i) = (if i ∈ signs then -1 else 1) * r
⊢ w i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)

Tactic:
← height,

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))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : ∑ i, w i = 1
hp : (Finset.affineCombination ℝ Finset.univ s.points) w ∈ affineSpan ℝ (Set.range s.points)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) = (if i ∈ signs then -1 else 1) * r
i : Fin (n + 1)
h' : w i * s.height i = (if i ∈ signs then -1 else 1) * r
⊢ w i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)
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
H : 1 - ⟪x, y⟫ ^ 2 ≠ 0
H0 : ⟪x - ⟪x, y⟫ • y, x - ⟪x, y⟫ • y⟫ = 1 - ⟪x, y⟫ ^ 2
⊢ x = ⟪x, y⟫ • y + ((1 - ⟪x, y⟫ ^ 2) / (1 - ⟪x, y⟫ ^ 2)) • (x - ⟪x, y⟫ • y)

Tactic:
simp [H]

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

Goal state before:
pp: case neg.refine_1
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
⊢ s.excenter signs -ᵥ s.touchpoint signs i ∈ ↑(vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ

pp: case neg.refine_2
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
⊢ s.excenter signs -ᵥ s.touchpoint signs i ∈ ↑(vectorSpan ℝ (s.points '' {j}ᶜ))ᗮ

Tactic:
· rw [← direction_affineSpan, ← range_faceOpposite_points]
      exact vsub_orthogonalProjection_mem_direction_orthogonal _ _

Goal state after:
case neg.refine_2
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
⊢ s.excenter signs -ᵥ s.touchpoint signs i ∈ ↑(vectorSpan ℝ (s.points '' {j}ᶜ))ᗮ
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
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ (s.reindex e).touchpointWeights signs i =
    s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm i) ∘ ⇑e.symm

Tactic:
eq_comm,

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm i) ∘ ⇑e.symm =
    (s.reindex e).touchpointWeights signs 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
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ (Finset.affineCombination ℝ Finset.univ (s.points ∘ ⇑e.symm))
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm i) ∘ ⇑e.symm) =
    (Finset.affineCombination ℝ Finset.univ s.points)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm i))

Tactic:
rw [← Equiv.coe_toEmbedding, ← Finset.affineCombination_map]

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ (Finset.affineCombination ℝ (Finset.map e.symm.toEmbedding Finset.univ) s.points)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm.toEmbedding i)) =
    (Finset.affineCombination ℝ Finset.univ s.points)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm.toEmbedding i))
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ¬x = 0
hy : y = 0
⊢ angle x z ≤ angle x y + angle y z

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ¬x = 0
hy : ¬y = 0
⊢ angle x z ≤ angle x y + angle y z

Tactic:
· simpa [hy] using angle_le_pi x z

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ¬x = 0
hy : ¬y = 0
⊢ angle x z ≤ angle x y + angle y z
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)
he : s.touchpoint signs i = s.points j
⊢ False

Tactic:
eq_comm,

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
inst✝ : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : s.points j = s.touchpoint signs i
⊢ False
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)
he : Pi.single j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : 0 = SignType.sign (s.touchpointWeights signs i k)
⊢ False

Tactic:
eq_comm,

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
inst✝ : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : Pi.single j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : SignType.sign (s.touchpointWeights signs i k) = 0
⊢ False
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case 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
⊢ Simplex.excenter t ∅ = Simplex.incenter t ∨ ∃ i, Simplex.excenter t ∅ = Simplex.excenter t {i}

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
⊢ Simplex.excenter t Finset.univ = Simplex.incenter t ∨ ∃ i, Simplex.excenter t Finset.univ = Simplex.excenter t {i}

pp: case inr.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 : Fin 3
⊢ Simplex.excenter t {i} = Simplex.incenter t ∨ ∃ i_1, Simplex.excenter t {i} = Simplex.excenter t {i_1}

pp: case inr.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 : Fin 3
⊢ Simplex.excenter t {i}ᶜ = Simplex.incenter t ∨ ∃ i_1, Simplex.excenter t {i}ᶜ = Simplex.excenter t {i_1}

Tactic:
· exact .inl rfl

Goal state after:
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
⊢ Simplex.excenter t Finset.univ = Simplex.incenter t ∨ ∃ i, Simplex.excenter t Finset.univ = Simplex.excenter t {i}

case inr.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 : Fin 3
⊢ Simplex.excenter t {i} = Simplex.incenter t ∨ ∃ i_1, Simplex.excenter t {i} = Simplex.excenter t {i_1}

case inr.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 : Fin 3
⊢ Simplex.excenter t {i}ᶜ = Simplex.incenter t ∨ ∃ i_1, Simplex.excenter t {i}ᶜ = Simplex.excenter t {i_1}
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₂ i₃ : Fin (2 + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∠ (t.points i₁) (t.points i₂) (t.points i₃) < π / 2

Tactic:
fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ <;> simp [*] at *

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

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
s : Sphere P
p : P
v : V
hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p
hv : ¬v = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0

Tactic:
eq_comm,

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
s : Sphere P
p : P
v : V
hp : p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
hv : ¬v = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0