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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
      (Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
          (Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).num) -
        Polynomial.C
            (((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
              ((algebraMap ↥K[generator E] ↥K⟮generator E⟯) ⟨generator E, ⋯⟩)) *
          Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
            (Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).denom)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
RingHom.coe_comp,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
      (Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
          (Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).num) -
        Polynomial.C
            ((⇑(algebraMap (↥E) K⟮X⟯) ∘ ⇑(algebraMap ↥K⟮generator E⟯ ↥E))
              ((algebraMap ↥K[generator E] ↥K⟮generator E⟯) ⟨generator E, ⋯⟩)) *
          Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
            (Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).denom)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: case mpr
𝕜 : 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 q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
hq : q ∈ mk' p s.directionᗮ
⊢ q ∈ ↑s ∩ ↑(mk' p s.directionᗮ)

Tactic:
simp only [Set.mem_inter_iff, SetLike.mem_coe]

Goal state after:
case mpr
𝕜 : 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 q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
hq : q ∈ mk' p s.directionᗮ
⊢ q ∈ s ∧ q ∈ mk' p s.directionᗮ
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 : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
h :
  finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
⊢ Fintype.card (Fin (n + 1)) - 1 = n - 1 + 1

Tactic:
Fintype.card_fin,

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)
h :
  finrank ℝ ↥(vectorSpan ℝ (s.points '' {i}ᶜ)) +
      finrank ℝ ↥((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)) =
    finrank ℝ ↥(vectorSpan ℝ (Set.range s.points))
hn : n - 1 + 1 = n
⊢ n + 1 - 1 = n - 1 + 1
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 : V
r : ℝ
hr : r ≠ 0
⊢ 2 • o.oangle (r • x) y = 2 • o.oangle x y

Tactic:
rcases hr.lt_or_gt with (h | h)

Goal state after:
case inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
hr : r ≠ 0
h : r < 0
⊢ 2 • o.oangle (r • x) y = 2 • o.oangle x y

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
r : ℝ
hr : r ≠ 0
h : 0 < r
⊢ 2 • o.oangle (r • x) y = 2 • o.oangle x y
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 : V
r : ℝ
hr : r ≠ 0
⊢ 2 • o.oangle x (r • y) = 2 • o.oangle x y

Tactic:
rcases hr.lt_or_gt with (h | h)

Goal state after:
case inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
hr : r ≠ 0
h : r < 0
⊢ 2 • o.oangle x (r • y) = 2 • o.oangle x y

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
r : ℝ
hr : r ≠ 0
h : 0 < r
⊢ 2 • o.oangle x (r • y) = 2 • o.oangle x y
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case a.refine_2
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)
⊢ s.points j -ᵥ s.altitudeFoot j ∈ ↑(vectorSpan ℝ (Set.range s.points))ᗮ

Tactic:
· rw [SetLike.mem_coe]
      have hk : ∃ k, k ≠ i ∧ k ≠ j := Fin.exists_ne_and_ne_of_two_lt i j
        (by linarith only [Nat.AtLeastTwo.one_lt (n := n)])
      have hs : vectorSpan ℝ (Set.range s.points) =
          vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔
            vectorSpan ℝ (Set.range (s.faceOpposite j).points) := by
        rcases hk with ⟨k, hki, hkj⟩
        have hki' : s.points k ∈ Set.range (s.faceOpposite i).points := by
          rw [range_faceOpposite_points]
          exact Set.mem_image_of_mem _ hki
        have hkj' : s.points k ∈ Set.range (s.faceOpposite j).points := by
          rw [range_faceOpposite_points]
          exact Set.mem_image_of_mem _ hkj
        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
        convert! AffineSubspace.vectorSpan_union_of_mem_of_mem ℝ hki' hkj'
      rw [hs, ← Submodule.inf_orthogonal, Submodule.mem_inf]
      refine ⟨?_, ?_⟩
      · rw [h, ← direction_affineSpan]
        exact Submodule.smul_mem _ _ (vsub_orthogonalProjection_mem_direction_orthogonal _ _)
      · rw [← direction_affineSpan]
        exact vsub_orthogonalProjection_mem_direction_orthogonal _ _

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₁ -ᵥ p₃‖
⊢ o.oangle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) = o.oangle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃)

Tactic:
← vsub_sub_vsub_cancel_left p₂ 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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ o.oangle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) = o.oangle (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃)
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 : ¬0 ≤ (↑(InnerProductGeometry.angle x y)).sign
hx : ¬x = 0
hy : ¬y = 0
hxy : o.oangle x y = -↑(InnerProductGeometry.angle x y)
⊢ False

Tactic:
exact h (Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi (InnerProductGeometry.angle_nonneg _ _)
    (InnerProductGeometry.angle_le_pi _ _))

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 : ¬0 ≤ (↑(InnerProductGeometry.angle x y)).sign
hx : ¬x = 0
hy : ¬y = 0
hxy : o.oangle x y = ↑(InnerProductGeometry.angle x y)
⊢ False

Tactic:
exact h (Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi (InnerProductGeometry.angle_nonneg _ _)
    (InnerProductGeometry.angle_le_pi _ _))

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

Goal state before:
pp: case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x = 0
⊢ o.oangle x y = ↑π ↔ InnerProductGeometry.angle x y = π

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
hx : ¬x = 0
⊢ o.oangle x y = ↑π ↔ InnerProductGeometry.angle x y = π

Tactic:
· simp [hx, Real.Angle.pi_ne_zero.symm, div_eq_mul_inv,
      Real.pi_ne_zero]

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
hx : ¬x = 0
⊢ o.oangle x y = ↑π ↔ InnerProductGeometry.angle x y = π
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ r₃ r₄ : ℝ
hr₁ : r₁ = 0
⊢ (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign

Tactic:
rw [hr₁, zero_smul, zero_mul, zero_add, zero_sub, Left.sign_neg,
      oangle_sign_smul_left, add_comm, oangle_sign_smul_add_smul_right, oangle_rev,
      Real.Angle.sign_neg, sign_mul, mul_neg, mul_neg, neg_mul, mul_assoc]

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

Tactic:
simpa [*] using (signedDist_smul v p q r).symm

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

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 : P
h_sbtw : Sbtw ℝ a b c
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c) t = b
ht0 : 0 < t
ht1 : t < 1
hb : b -ᵥ a = t • (c -ᵥ a)
⊢ dist p b < dist p c

Tactic:
have hpc : ⟪p -ᵥ a, c -ᵥ a⟫ = 0 := by simpa [ht0.ne', hb, inner_smul_right] using h_inner

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 : P
h_sbtw : Sbtw ℝ a b c
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c) t = b
ht0 : 0 < t
ht1 : t < 1
hb : b -ᵥ a = t • (c -ᵥ a)
hpc : ⟪p -ᵥ a, c -ᵥ a⟫ = 0
⊢ dist p b < dist p c
Module: Mathlib.Geometry.Euclidean.PerpBisector

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 : P
h_sbtw : Sbtw ℝ a b c
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c) t = b
ht0 : 0 < t
ht1 : t < 1
hb : b -ᵥ a = t • (c -ᵥ a)
hpc : ⟪p -ᵥ a, c -ᵥ a⟫ = 0
h_sq_ineq : dist p b ^ 2 < dist p c ^ 2
⊢ dist p b < dist p c

Tactic:
simpa only [Real.sqrt_sq dist_nonneg] using Real.sqrt_lt_sqrt (sq_nonneg _) h_sq_ineq

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
p q : P
⊢ ((signedDist (q -ᵥ p)) p) q = dist p q

Tactic:
apply signedDist_vsub_self

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

Tactic:
rw [dist_eq_norm_vsub V _ p₂, ← real_inner_self_eq_norm_mul_norm, vadd_vsub_assoc,
    real_inner_add_add_self, real_inner_smul_left, real_inner_smul_left, real_inner_smul_right]
  ring

Goal state after:
Module: Mathlib.Geometry.Euclidean.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 : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
⊢ Fintype.card (Fin 2) = finrank ℝ ↥s.direction

Tactic:
Fintype.card_fin,

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 : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
⊢ 2 = finrank ℝ ↥s.direction
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

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 : Sphere P
as : AffineSubspace ℝ P
⊢ s.radius = 0 ∧ s.center ∈ as → s.IsTangentAt s.center as

Tactic:
· rintro ⟨hr, hm⟩
    refine ⟨?_, hm, ?_⟩
    · rw [center_mem_iff, hr]
    · simp

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

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

Tactic:
← vsub_sub_vsub_cancel_right p₁ p₂ s.center,

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₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ s.center - (p₂ -ᵥ s.center), p₁ -ᵥ s.center⟫
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
as : AffineSubspace ℝ P
h : s.IsTangent as
⊢ Metric.infDist s.center ↑as = s.radius

Tactic:
obtain ⟨p, h⟩ := h
  refine le_antisymm ?_ ?_
  · convert! Metric.infDist_le_dist_of_mem h.mem_space
    rw [mem_sphere'.1 h.mem_sphere]
  · rw [Metric.infDist_eq_iInf]
    have : Nonempty as := ⟨⟨p, h.mem_space⟩⟩
    refine le_ciInf fun x ↦ ?_
    rw [dist_comm]
    exact h.isTangent.radius_le_dist_center x.property

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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(s.orthRadius p).direction
hv : ∀ (w : ↥(s.orthRadius p).direction), ∃ c, c • v = w
hv0 : ↑v ≠ 0
⊢ ¬√(s.radius ^ 2 - dist p s.center ^ 2) = 0

Tactic:
have hvp : 0 < √(s.radius ^ 2 - dist p s.center ^ 2) := by
      rw [Real.sqrt_pos, sub_pos, sq_lt_sq, abs_of_nonneg dist_nonneg]
      exact lt_abs.2 (.inl hp)

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(s.orthRadius p).direction
hv : ∀ (w : ↥(s.orthRadius p).direction), ∃ c, c • v = w
hv0 : ↑v ≠ 0
hvp : 0 < √(s.radius ^ 2 - dist p s.center ^ 2)
⊢ ¬√(s.radius ^ 2 - dist p s.center ^ 2) = 0
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

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
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
⊢ 2 • o.oangle (x - y) (x - z) = 2 • o.oangle (y - x) (z - x)

Tactic:
rw [← oangle_neg_neg, neg_sub, neg_sub]

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
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)
⊢ -⟪p₃ -ᵥ o, p₃ -ᵥ o⟫_ℝ + -⟪p₃ -ᵥ o, o -ᵥ p₂⟫_ℝ + (⟪p₃ -ᵥ o, o -ᵥ p₂⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ) = 0 ↔
    dist s.center p₂ = s.radius

Tactic:
ring_nf

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)
⊢ -⟪p₃ -ᵥ o, p₃ -ᵥ o⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ = 0 ↔ 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)⁻¹ -
      ∑ j with j ≠ i,
        -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) *
          (s.height j)⁻¹ =
    0

Tactic:
neg_mul

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 with x ≠ i,
        -(⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ / (s.height i * s.height x) *
            (s.height x)⁻¹) =
    0
Module: Mathlib.Geometry.Euclidean.Incenter

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 : ℕ
inst✝¹ : NeZero n
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
h : j ∈ {k | k ≠ i}
⊢ s.excenterWeightsUnnorm {i} j = (s.height j)⁻¹

Tactic:
Finset.mem_filter_univ

Goal state after:
case a
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 j : Fin (n + 1)
h : j ≠ i
⊢ s.excenterWeightsUnnorm {i} j = (s.height j)⁻¹
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₄ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₄ : ‖p₄ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ 2 • «o».oangle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) = 2 • «o».oangle (p₁ -ᵥ p₃) (p₄ -ᵥ p₃)

Tactic:
← vsub_sub_vsub_cancel_right p₁ p₂ s.center,

Goal state after:
V : Type u_3
P : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ p₄ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₄ : ‖p₄ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ 2 • «o».oangle (p₁ -ᵥ s.center - (p₂ -ᵥ s.center)) (p₄ -ᵥ p₂) = 2 • «o».oangle (p₁ -ᵥ p₃) (p₄ -ᵥ p₃)
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case inr.inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
hxy : x ≠ y
h_sin : ∀ (x y : V), x ≠ 0 → y ≠ 0 → Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)
hsub : x - y ≠ 0
⊢ √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ ^ 2) = √(⟪y, y⟫ * (⟪x, x⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪y, y⟫)) - (⟪x, y⟫ - ⟪y, y⟫) ^ 2)

Tactic:
ring_nf

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.incenter ∈ s.interior

Tactic:
by
  have h := s.excenterExists_empty.sum_excenterWeights_eq_one
  rw [incenter_eq_affineCombination, s.affineCombination_mem_interior_iff h]
  intro i
  refine ⟨s.excenterWeights_empty_pos i, ?_⟩
  by_contra! hp
  obtain ⟨j, hj⟩ := exists_ne i
  rw [← Finset.sum_add_sum_compl {j, i}, Finset.sum_pair hj] at h
  revert h
  apply ne_of_gt
  nth_rw 2 [add_comm]
  grw [hp]
  rw [add_assoc, lt_add_iff_pos_right]
  exact add_pos_of_pos_of_nonneg (s.excenterWeights_empty_pos j)
    (Finset.sum_nonneg fun k _ ↦ (s.excenterWeights_empty_pos k).le)

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

Goal state before:
pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
this : x + y ≠ 0
⊢ √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) * (⟪x, x⟫ + ⟪x, y⟫ + (⟪x, y⟫ + ⟪y, y⟫)) =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) * (⟪x, y⟫ + ⟪y, y⟫) + (⟪x, x⟫ + ⟪x, y⟫) * √(⟪y, y⟫ * ⟪x, x⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
ring_nf

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
s : Simplex ℝ P 1
⊢ Set.univ.Pairwise fun i j ↦
    dist (s.points i) (Finset.centroid ℝ univ s.points) = dist (s.points j) (Finset.centroid ℝ univ s.points)

Tactic:
intro i hi j hj hij

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 : Simplex ℝ P 1
i : Fin 2
hi : i ∈ Set.univ
j : Fin 2
hj : j ∈ Set.univ
hij : i ≠ j
⊢ dist (s.points i) (Finset.centroid ℝ univ s.points) = dist (s.points j) (Finset.centroid ℝ univ s.points)
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ ∑ j, pointWeightsWithCircumcenter i j = 1

Tactic:
convert! sum_ite_eq' univ (pointIndex i) (Function.const _ (1 : ℝ)) with j
  · cases j <;> simp [pointWeightsWithCircumcenter]
  · simp

Goal state after: