mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num - Polynomial.C Polynomial.X * Polynomial.map (algebraMap K K[X]) f.denom
φ_map : (mapEquiv e.toRingEquiv) φ = f.minpolyX ↥K[f]
this : φ = Bivariate.swap (Polynomial.C f.num - Polynomial.X * Polynomial.C f.denom)
⊢ Irreducible φ

Tactic:
this,

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
e : K[X] ≃ₐ[K] ↥K[f] := Polynomial.algEquivOfTranscendental K f ⋯
φ : K[X][X] :=
  Polynomial.map (algebraMap K K[X]) f.num - Polynomial.C Polynomial.X * Polynomial.map (algebraMap K K[X]) f.denom
φ_map : (mapEquiv e.toRingEquiv) φ = f.minpolyX ↥K[f]
this : φ = Bivariate.swap (Polynomial.C f.num - Polynomial.X * Polynomial.C f.denom)
⊢ Irreducible (Bivariate.swap (Polynomial.C f.num - Polynomial.X * Polynomial.C f.denom))
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: case h
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ generator E = (algebraMap K[X] K⟮X⟯) ((Φ E).coeff (generatorIndex h)) / (algebraMap K[X] K⟮X⟯) (c E).num

Tactic:
rw [Φ_coeff_generatorIndex h,
    mul_div_cancel_left₀ _ (algebraMap_ne_zero (num_ne_zero (c_ne_zero h)))]

Goal state after:
Module: Mathlib.Geometry.Convex.Hull

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
x : X
hs : (convexHull R) s = {x}
⊢ s ⊆ (convexHull R) s

Tactic:
exact subset_convexHull_self

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.map Polynomial.C (Q₂ h) = Q₁ h

Tactic:
have := eq_C_of_natDegree_eq_zero (swap_Q₁_natDegree h)
  apply_fun Bivariate.swap at this
  rw [Bivariate.swap_swap_apply, Bivariate.swap_C] at this
  exact this.symm

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

Goal state before:
pp: case mp
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ ↑((orthogonalProjection s) p) ∈ s ∧ p -ᵥ ↑((orthogonalProjection s) p) ∈ s.directionᗮ

Tactic:
exact ⟨orthogonalProjection_mem _, vsub_orthogonalProjection_mem_direction_orthogonal _ _⟩

Goal state after:
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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ s.altitude i = AffineSubspace.map S.subtype ((s.restrict S hS).altitude i)

Tactic:
convert! (s.restrict S hS).altitude_map S.subtypeₐᵢ i

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ nndist p ↑((orthogonalProjection s) p) = Metric.infNndist p ↑s

Tactic:
by
  rw [← NNReal.coe_inj]
  simp [dist_orthogonalProjection_eq_infDist]

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

Goal state before:
pp: case mp
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
hx : x ≠ 0
θ : Real.Angle
⊢ (o.rotation θ) x = x → θ = 0

Tactic:
intro h
    rw [eq_comm]
    simpa [hx, h] using o.oangle_rotation_right hx hx θ

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

Goal state before:
pp: case refine_1
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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂
⊢ (AffineMap.lineMap p₁ p₃) (1 / (1 - r)) = p₂

Tactic:
rw [AffineMap.lineMap_apply, hp₃p₂, vadd_vsub_assoc, ← neg_vsub_eq_vsub_rev p₂ p₁, smul_neg, ←
      neg_smul, smul_add, smul_smul, ← add_smul, eq_comm, eq_vadd_iff_vsub_eq]

Goal state after:
case refine_1
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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂
⊢ p₂ -ᵥ p₁ = (1 / (1 - r) * -r + 1 / (1 - r)) • (p₂ -ᵥ p₁)
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
h0 : x = 0 ∨ y ≠ 0
⊢ 0 < angle x (x + y)

Tactic:
rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_pos,
    norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖x‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
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 p₂).sign = 0
⊢ p₁ = p ∨ p₂ = p ∨ ∠ p₁ p p₂ = 0 ∨ ∠ p₁ p p₂ = π

Tactic:
by
  convert! o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero h <;> simp

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₂ p₃ = ↑(-π / 2)
⊢ ∠ p₁ p₂ p₃ = π / 2

Tactic:
rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
  exact o.inner_eq_zero_of_oangle_eq_neg_pi_div_two 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₁ w₂ : ι → ℝ
p : ι → P
h₁ : ∑ i ∈ s, w₁ i = 1
h₂ : ∑ i ∈ s, w₂ i = 1
⊢ ‖(Finset.affineCombination ℝ s p) w₁ -ᵥ (Finset.affineCombination ℝ s p) w₂‖ *
      ‖(Finset.affineCombination ℝ s p) w₁ -ᵥ (Finset.affineCombination ℝ s p) w₂‖ =
    (-∑ i₁ ∈ s, ∑ i₂ ∈ s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2

Tactic:
←
    @inner_self_eq_norm_mul_norm ℝ,

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₁ w₂ : ι → ℝ
p : ι → P
h₁ : ∑ i ∈ s, w₁ i = 1
h₂ : ∑ i ∈ s, w₂ i = 1
⊢ RCLike.re
      ⟪(Finset.affineCombination ℝ s p) w₁ -ᵥ (Finset.affineCombination ℝ s p) w₂,
        (Finset.affineCombination ℝ s p) w₁ -ᵥ (Finset.affineCombination ℝ s p) w₂⟫ =
    (-∑ i₁ ∈ s, ∑ i₂ ∈ s, (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (dist (p i₁) (p i₂) * dist (p i₁) (p i₂))) / 2
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
⊢ ((signedDist v) p) q = dist p q ↔ q -ᵥ p ∈ ℝ≥0 ∙ v

Tactic:
by
  rw [Submodule.mem_span_singleton]
  rw [signedDist_apply_apply, dist_eq_norm_vsub', NormedSpace.normalize, real_inner_smul_left]
  by_cases h : v = 0
  · simp [h, eq_comm (a := (0 : ℝ)), eq_comm (a := (0 : V))]
  rw [inv_mul_eq_iff_eq_mul₀ (by positivity)]
  rw [inner_eq_norm_mul_iff_real]
  simp only [smul_def]
  refine ⟨fun h => ?_, fun ⟨c, h⟩ => ?_⟩
  · simp only [NNReal.exists, coe_mk, exists_prop]
    use ‖v‖⁻¹ * ‖q -ᵥ p‖
    constructor
    · positivity
    · rw [← smul_smul, h, smul_smul, inv_mul_cancel₀ (by positivity), one_smul]
  · rw [← h, norm_smul, smul_smul, mul_comm]
    simp

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
n : ℕ
inst✝¹ : NeZero n
s : Simplex ℝ P n
m : ℕ
inst✝ : NeZero m
e : Fin (n + 1) ≃ Fin (m + 1)
j : Fin (m + 1)
⊢ (affineSpan ℝ (s.points '' ⇑e.symm '' {j}ᶜ)).signedInfDist ((s.points ∘ ⇑e.symm) j) =
    (affineSpan ℝ (s.points '' {e.symm j}ᶜ)).signedInfDist (s.points (e.symm j))

Tactic:
Set.image_compl_eq e.symm.bijective,

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
m : ℕ
inst✝ : NeZero m
e : Fin (n + 1) ≃ Fin (m + 1)
j : Fin (m + 1)
⊢ (affineSpan ℝ (s.points '' (⇑e.symm '' {j})ᶜ)).signedInfDist ((s.points ∘ ⇑e.symm) j) =
    (affineSpan ℝ (s.points '' {e.symm j}ᶜ)).signedInfDist (s.points (e.symm j))
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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
this : (∡ p₁ p₂ p₃).toReal = (∡ p₁ p₂ p₄).toReal / 2
⊢ |(∡ p₁ p₂ p₃).toReal| = |(∡ p₁ p₂ p₄).toReal| / 2

Tactic:
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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
this : (∡ p₁ p₂ p₃).toReal = (∡ p₁ p₂ p₄).toReal / 2
⊢ |(∡ p₁ p₂ p₄).toReal / 2| = |(∡ p₁ p₂ p₄).toReal| / 2
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: P : Type u_2
inst✝ : MetricSpace P
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ s.radius = dist p₂ s.center

Tactic:
mem_sphere.1 hp₂

Goal state after:
P : Type u_2
inst✝ : MetricSpace P
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ s.radius = s.radius
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

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

Tactic:
use p
  simp

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₁ s₂ : Sphere P
h : dist s₂.center s₁.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius = 0
⊢ False

Tactic:
rw [hr0, dist_eq_zero] 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
inst✝ : Nontrivial V
s₁ s₂ : Sphere P
h : s₂.center = s₁.center
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius = 0
⊢ 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
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
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).excenterWeightsUnnorm = s.excenterWeightsUnnorm

Tactic:
by
  ext
  simp [excenterWeightsUnnorm]

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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ (s.restrict S hS).excenterWeightsUnnorm = s.excenterWeightsUnnorm

Tactic:
by
  ext
  simp [excenterWeightsUnnorm]

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
i : Fin (n + 1)
⊢ (∑ i, s.excenterWeightsUnnorm signs i)⁻¹ ≠ 0

Tactic:
rw [ExcenterExists] 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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : ∑ i, s.excenterWeightsUnnorm signs i ≠ 0
i : Fin (n + 1)
⊢ (∑ i, s.excenterWeightsUnnorm signs i)⁻¹ ≠ 0
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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o)
⊢ dist p₃ o = dist o p₂ ↔ dist s.center p₂ = s.radius

Tactic:
mem_sphere.mp hd.right_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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o)
⊢ s.radius = dist o p₂ ↔ dist s.center p₂ = 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
i : Fin (n + 1)
⊢ (s.height i)⁻¹ +
      ∑ x ∈ Finset.univ.erase i,
        ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ / (s.height i * s.height x) * (s.height x)⁻¹ =
    0

Tactic:
Finset.sum_erase_eq_sub (Finset.mem_univ _),

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
i : Fin (n + 1)
⊢ (s.height i)⁻¹ +
      (∑ x,
          ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ / (s.height i * s.height x) *
            (s.height x)⁻¹ -
        ⟪s.points i -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫ / (s.height i * s.height i) * (s.height i)⁻¹) =
    0
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₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| = 2 * s.radius

Tactic:
by
  rw [← dist_div_sin_oangle_div_two_eq_radius hp₁ hp₂ hp₃ hp₁p₂ hp₁p₃ hp₂p₃,
    mul_div_cancel₀ _ (two_ne_zero' ℝ)]

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
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = dist p₁ p₃
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₃ p₂

Tactic:
dist_eq_norm_vsub V p₁ p₃

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 : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₃ p₂
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
p₁ p₂ p₃ : P
h : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)
hpi : InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₃ -ᵥ p₁) ≠ π
⊢ ‖p₁ -ᵥ p₂‖ = dist p₁ p₃

Tactic:
dist_eq_norm_vsub V p₁ p₃

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 : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)
hpi : InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₃ -ᵥ p₁) ≠ π
⊢ ‖p₁ -ᵥ 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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ ↑(s.restrict S hS).circumcenter = s.circumcenter

Tactic:
rw [eq_comm]
  have : Nonempty S := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
  exact (s.restrict S hS).circumcenter_map S.subtypeₐᵢ

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
hn' : ¬Collinear ℝ {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }
⊢ ∃ s, {p₁, p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius

Tactic:
refine ⟨t₂.circumsphere, ?_⟩

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
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
hn' : ¬Collinear ℝ {p₁, p₃, p₄}
t₁ : Affine.Triangle ℝ P := { points := ![p₁, p₂, p₄], independent := ⋯ }
t₂ : Affine.Triangle ℝ P := { points := ![p₁, p₃, p₄], independent := ⋯ }
⊢ {p₁, p₂, p₃, p₄} ⊆ Metric.sphere (Affine.Simplex.circumsphere t₂).center (Affine.Simplex.circumsphere t₂).radius
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : p₁ = p₄
⊢ Cospherical {p₂, p₃, p₄} ∨ Collinear ℝ {p₂, p₃, p₄}

Tactic:
by_cases hl : Collinear ℝ ({p₂, p₃, p₄} : Set 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₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : p₁ = p₄
hl : Collinear ℝ {p₂, p₃, p₄}
⊢ Cospherical {p₂, p₃, p₄} ∨ Collinear ℝ {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₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : p₁ = p₄
hl : ¬Collinear ℝ {p₂, p₃, p₄}
⊢ Cospherical {p₂, p₃, p₄} ∨ Collinear ℝ {p₂, p₃, p₄}
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
hf : Fact (Module.finrank ℝ V = n)
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ affineSpan ℝ (Set.range (s.faceOpposite i).points) = (s.exsphere signs).orthRadius (s.touchpoint signs i)

Tactic:
by
  refine (h.isTangentAt_touchpoint i).eq_orthRadius_of_finrank_add_one_eq (h.exradius_pos.ne') ?_
  rw [direction_affineSpan, (s.faceOpposite i).independent.finrank_vectorSpan_add_one,
    Fintype.card_fin, hf.out]
  have := NeZero.ne n
  lia

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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ x,
      ((if x ∈ {i₁, i₂} then ((↑2)⁻¹ + (↑2)⁻¹) • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
        else 0) -
        if x = i₁ ∨ x = i₂ then 1 • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) else 0) =
    0

Tactic:
convert! sum_const_zero

Goal state after:
case e'_2.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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
x✝ : Fin (n + 1)
a✝ : x✝ ∈ univ
⊢ ((if x✝ ∈ {i₁, i₂} then ((↑2)⁻¹ + (↑2)⁻¹) • (s.pointsWithCircumcenter (pointIndex x✝) -ᵥ Classical.choice ⋯) else 0) -
      if x✝ = i₁ ∨ x✝ = i₂ then 1 • (s.pointsWithCircumcenter (pointIndex x✝) -ᵥ Classical.choice ⋯) else 0) =
    0
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.reindex e).points)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm i) ∘ ⇑e.symm) =
    s.touchpoint (Finset.map e.symm.toEmbedding signs) (e.symm i)

Tactic:
← affineCombination_touchpointWeights,

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.univ (s.reindex e).points)
      (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))
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)
⊢ s.touchpoint ∅ i ∈ (s.face ⋯).interior

Tactic:
← affineCombination_touchpointWeights,

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
i : Fin (n + 1)
⊢ (Finset.affineCombination ℝ Finset.univ s.points) (s.touchpointWeights ∅ i) ∈ (s.face ⋯).interior