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✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hki' : s.points k ∈ Set.range (s.faceOpposite i).points
hkj' : s.points k ∈ Set.range (s.faceOpposite j).points
⊢ vectorSpan ℝ (Set.range s.points) =
    vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points)

Tactic:
have hs :
            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]
          simp_rw [← Set.image_univ, ← Set.compl_inter]
          rw [Set.inter_singleton_eq_empty.mpr ?_, Set.compl_empty]
          simpa using hij.symm

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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hki' : s.points k ∈ Set.range (s.faceOpposite i).points
hkj' : s.points k ∈ Set.range (s.faceOpposite j).points
hs : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
⊢ vectorSpan ℝ (Set.range s.points) =
    vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points)
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 : SameRay ℝ x (-y)
hx : ¬x = 0
r : ℝ
hy : r • x = -y
⊢ x = 0 ∨ ∃ r, y = r • x

Tactic:
refine Or.inr ⟨-r, ?_⟩

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 : SameRay ℝ x (-y)
hx : ¬x = 0
r : ℝ
hy : r • x = -y
⊢ y = -r • x
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ Real.cos (angle x (x + y)) * ‖x + y‖ = ‖x‖

Tactic:
rw [cos_angle_add_of_inner_eq_zero h]
  by_cases hxy : ‖x + y‖ = 0
  · have h' := norm_add_sq_eq_norm_sq_add_norm_sq_real h
    rw [hxy, zero_mul, eq_comm,
      add_eq_zero_iff_of_nonneg (mul_self_nonneg ‖x‖) (mul_self_nonneg ‖y‖), mul_self_eq_zero] at h'
    simp [h'.1]
  · exact div_mul_cancel₀ _ hxy

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₄ p₅ p₆ : P
h₂ : p₂ ∉ line[ℝ, p₁, p₃]
h₄ : p₄ ∈ line[ℝ, p₁, p₃]
h₆ : p₆ ∈ line[ℝ, p₁, p₃]
h₁₂₄₅ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₄, p₅]
h₃₂₆₅ : line[ℝ, p₃, p₂] ∥ line[ℝ, p₆, p₅]
hd : line[ℝ, p₆, p₄].direction ≤ line[ℝ, p₃, p₁].direction
⊢ o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = o.oangle (p₄ -ᵥ p₅) (p₆ -ᵥ p₅)

Tactic:
obtain ⟨r, hr, h₅₄, h₆₅, -⟩ := exists_eq_smul_of_parallel h₂ h₁₂₄₅
    (Set.pair_comm p₃ p₂ ▸ Set.pair_comm p₆ p₅ ▸ h₃₂₆₅).direction_eq.symm.le hd

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)
p₁ p₂ p₃ p₄ p₅ p₆ : P
h₂ : p₂ ∉ line[ℝ, p₁, p₃]
h₄ : p₄ ∈ line[ℝ, p₁, p₃]
h₆ : p₆ ∈ line[ℝ, p₁, p₃]
h₁₂₄₅ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₄, p₅]
h₃₂₆₅ : line[ℝ, p₃, p₂] ∥ line[ℝ, p₆, p₅]
hd : line[ℝ, p₆, p₄].direction ≤ line[ℝ, p₃, p₁].direction
r : ℝ
hr : r ≠ 0
h₅₄ : p₅ -ᵥ p₄ = r • (p₂ -ᵥ p₁)
h₆₅ : p₆ -ᵥ p₅ = r • (p₃ -ᵥ p₂)
⊢ o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = o.oangle (p₄ -ᵥ p₅) (p₆ -ᵥ p₅)
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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π * 2 = π
⊢ False

pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 = π
⊢ 2 ≠ 0

Tactic:
← sub_eq_zero,

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π * 2 - π = 0
⊢ False

V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 = π
⊢ 2 ≠ 0
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
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃

Tactic:
by_cases h : p₃ = p₂

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : p₃ = p₂
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃

case neg
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₂
⊢ ∡ p₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃
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 : ℝ
⊢ ⟪NormedSpace.normalize (r • v), q -ᵥ p⟫ = ↑(SignType.sign r) * ⟪NormedSpace.normalize v, q -ᵥ p⟫

Tactic:
rw [normalize_smul, real_inner_smul_left]

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
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
| ⟪v, v⟫ * (r * r) + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ = dist p₁ p₂ * dist p₁ p₂

Tactic:
← sub_eq_zero,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
| ⟪v, v⟫ * (r * r) + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ - dist p₁ p₂ * dist p₁ p₂ = 0
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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign

Tactic:
by
  by_cases h : p₁ = p₂; · simp [h]
  let sp : Set (P × P × P) := (fun p : P => (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}
  have hc : IsConnected sp :=
    (isConnected_setOfPred_sSameSide hp₃p₄.2.1 hp₃p₄.nonempty).image _ (by fun_prop)
  have hf : ContinuousOn (fun p : P × P × P => ∡ p.1 p.2.1 p.2.2) sp := by
    refine continuousOn_of_forall_continuousAt fun p hp => continuousAt_oangle ?_ ?_
    all_goals
      simp_rw [sp, Set.mem_image, Set.mem_ofPred] at hp
      obtain ⟨p', hp', rfl⟩ := hp
      dsimp only
      rintro rfl
    · exact hp'.2.2 hp₁
    · exact hp'.2.2 hp₂
  have hsp : ∀ p : P × P × P, p ∈ sp → ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ π := by
    intro p hp
    simp_rw [sp, Set.mem_image, Set.mem_ofPred] at hp
    obtain ⟨p', hp', rfl⟩ := hp
    dsimp only
    rw [oangle_ne_zero_and_ne_pi_iff_affineIndependent]
    exact affineIndependent_of_ne_of_mem_of_notMem_of_mem h hp₁ hp'.2.2 hp₂
  have hp₃ : (p₁, p₃, p₂) ∈ sp :=
    Set.mem_image_of_mem _ (sSameSide_self_iff.2 ⟨hp₃p₄.nonempty, hp₃p₄.2.1⟩)
  have hp₄ : (p₁, p₄, p₂) ∈ sp := Set.mem_image_of_mem _ hp₃p₄
  convert! Real.Angle.sign_eq_of_continuousOn hc hf hsp hp₃ hp₄

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
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p x : P
h : x ∈ affineSpan ℝ (insert p ↑s)
⊢ |(s.signedInfDist p) x| = dist x ↑((orthogonalProjection s) x)

Tactic:
rw [mem_affineSpan_insert_iff (orthogonalProjection s p).property] 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
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p x : P
h : ∃ r, ∃ p0 ∈ s, x = r • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ p0
⊢ |(s.signedInfDist p) x| = dist x ↑((orthogonalProjection s) x)
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 : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : Fin 3 → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
hf0' : (f 0 • v +ᵥ p 0) -ᵥ p 0 = 0
⊢ f 0 = 0

Tactic:
vadd_vsub,

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 : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : Fin 3 → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
hf0' : f 0 • v = 0
⊢ f 0 = 0
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ Function.Injective ![p₁, p₂, p₃]

Tactic:
simp only [Matrix.vecCons, Fin.cons_injective_iff]

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ p₁ ∉ Set.range (Fin.cons p₂ (Fin.cons p₃ ![])) ∧
    p₂ ∉ Set.range (Fin.cons p₃ ![]) ∧ p₃ ∉ Set.range ![] ∧ Function.Injective ![]
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 : ⟪q -ᵥ p, p -ᵥ s.center⟫ = 0
⊢ p = q

Tactic:
have hpq := hq.inner_left_eq_zero_of_mem hp.mem_space

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 : ⟪q -ᵥ p, p -ᵥ s.center⟫ = 0
hpq : ⟪p -ᵥ q, q -ᵥ s.center⟫ = 0
⊢ p = q
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⟫ = ⟪p -ᵥ q, q -ᵥ s.center⟫
hpq : ⟪p -ᵥ q, q -ᵥ s.center⟫ = 0
⊢ p = q

Tactic:
← sub_eq_zero,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
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⟫ - ⟪p -ᵥ q, q -ᵥ s.center⟫ = 0
hpq : ⟪p -ᵥ q, q -ᵥ s.center⟫ = 0
⊢ p = q
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

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
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂

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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂

Tactic:
· exact Or.inr h

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₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫ ∨ p₁ = p₂
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case neg.refine_2.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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖p₁ -ᵥ s.center‖
⊢ ¬‖p₁ -ᵥ s.center‖ • (p₂ -ᵥ s.center) = ‖p₁ -ᵥ s.center‖ • (p₁ -ᵥ s.center)

Tactic:
← sub_eq_zero,

Goal state after:
case neg.refine_2.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₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖p₁ -ᵥ s.center‖
⊢ ¬‖p₁ -ᵥ s.center‖ • (p₂ -ᵥ s.center) - ‖p₁ -ᵥ s.center‖ • (p₁ -ᵥ s.center) = 0
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
⊢ midpoint ℝ p₁ p₂ = s.center

Tactic:
rw [midpoint_eq_iff, AffineEquiv.pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq]

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 = s.center -ᵥ p₁
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
⊢ s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂

Tactic:
by
  refine ⟨fun h ↦ ⟨h.left_mem, h.right_mem, h.wbtw⟩, fun ⟨h₁, h₂, hr⟩ ↦ ?_⟩
  have hd := hr.dist_add_dist
  rw [mem_sphere.1 h₁, mem_sphere'.1 h₂, ← two_mul, eq_comm] at hd
  exact isDiameter_iff_mem_and_mem_and_dist.2 ⟨h₁, h₂, hd⟩

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
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:
← dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq 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₃
p : P
h₁ : dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₂).orthogonalProjectionSpan p)
h₂ : 2 • ∡ (t.points i₃) (t.points i₂) p = 2 • ∡ p (t.points i₂) (t.points i₁)
⊢ ∃ signs, p = excenter t signs
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case h.left.right.inr
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₁ ∈ ps
⊢ cr * cr + ‖cc₂ -ᵥ cc‖ * ‖cc₂ -ᵥ cc‖ = cr * cr + ycc₂ * ycc₂

Tactic:
vadd_vsub,

Goal state after:
case h.left.right.inr
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₁ ∈ ps
⊢ cr * cr + ‖(ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p))‖ * ‖(ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p))‖ =
    cr * cr + ycc₂ * ycc₂
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
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
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)
cc₃ : P
cr₃ : ℝ
hcc₃ : cc₃ ∈ affineSpan ℝ (insert p ↑s)
hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃
t₃ : ℝ
hcc₃' : cc ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
hcr₃' : ∀ p₁ ∈ ps, dist p₁ ↑⟨cc, hcc₃'⟩ = cr
p0 : P
hp0 : p0 ∈ ps
h' : ↑⟨cc, hcc₃'⟩ = cc
⊢ cr * cr +
      ‖(t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc) -ᵥ cc‖ *
        ‖(t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc) -ᵥ cc‖ =
    cr * cr + t₃ * y * (t₃ * y)

Tactic:
vadd_vsub,

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 : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
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)
cc₃ : P
cr₃ : ℝ
hcc₃ : cc₃ ∈ affineSpan ℝ (insert p ↑s)
hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃
t₃ : ℝ
hcc₃' : cc ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
hcr₃' : ∀ p₁ ∈ ps, dist p₁ ↑⟨cc, hcc₃'⟩ = cr
p0 : P
hp0 : p0 ∈ ps
h' : ↑⟨cc, hcc₃'⟩ = cc
⊢ cr * cr + ‖t₃ • (p -ᵥ ↑((orthogonalProjection s) p))‖ * ‖t₃ • (p -ᵥ ↑((orthogonalProjection s) p))‖ =
    cr * cr + t₃ * y * (t₃ * 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
V₂ : Type u_3
P₂ : Type u_4
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
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).excenter signs = f (s.excenter signs)

Tactic:
simp [excenter, exsphere, ← AffineIsometry.coe_toAffineMap, h.sum_excenterWeights_eq_one,
    Finset.map_affineCombination]

Goal state after: