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 ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).num -
      Polynomial.C ((algebraMap K[X] K⟮X⟯) (generator E).num) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (g E)) *
        Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.map Polynomial.C (f E)) -
      Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (f E)) *
        Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.map Polynomial.C (g E))

Tactic:
map_C,

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 ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).num -
      Polynomial.C ((algebraMap K[X] K⟮X⟯) (generator E).num) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom =
    Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
        Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.map Polynomial.C (f E)) -
      Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (f E)) *
        Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.map Polynomial.C (g E))
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 ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).num -
      Polynomial.C ((algebraMap K[X] K⟮X⟯) (generator E).num) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom =
    Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
        Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.map Polynomial.C (f E)) -
      Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (f E)) *
        Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.map Polynomial.C (g E))

Tactic:
map_C,

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 ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).num -
      Polynomial.C ((algebraMap K[X] K⟮X⟯) (generator E).num) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom =
    Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
        Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.map Polynomial.C (f E)) -
      Polynomial.C ((algebraMap K[X] K⟮X⟯) (f E)) *
        Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.map Polynomial.C (g E))
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
this :
  (algebraMap K[X] F[X]) (g E) * Polynomial.C ((aeval α) (f E)) -
      (algebraMap K[X] F[X]) (f E) * Polynomial.C ((aeval α) (g E)) =
    0
⊢ (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))

Tactic:
algebraMap_def,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
this :
  (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) -
      (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E)) =
    0
⊢ (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
this :
  Polynomial.map (algebraMap K F) (g E) * Polynomial.C ((aeval α) (f E)) -
      Polynomial.map (algebraMap K F) (f E) * Polynomial.C ((aeval α) (g E)) =
    0
⊢ (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))

Tactic:
sub_eq_zero,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
this :
  Polynomial.map (algebraMap K F) (g E) * Polynomial.C ((aeval α) (f E)) =
    Polynomial.map (algebraMap K F) (f E) * Polynomial.C ((aeval α) (g E))
⊢ (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))
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₁ s₂ : AffineSubspace 𝕜 P
inst✝⁴ : Nonempty ↥s₁
inst✝³ : Nonempty ↥s₂
inst✝² : s₁.direction.HasOrthogonalProjection
inst✝¹ : s₂.direction.HasOrthogonalProjection
p : P
h : ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)
inst✝ : (s₁ ⊔ s₂).direction.HasOrthogonalProjection
⊢ p -ᵥ ↑((orthogonalProjection s₁) p) ∈ (s₁ ⊔ s₂).directionᗮ

Tactic:
rw [direction_sup_eq_sup_direction (orthogonalProjection_mem p) (h ▸ orthogonalProjection_mem p),
    ← Submodule.inf_orthogonal]

Goal state after:
𝕜 : 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₁ s₂ : AffineSubspace 𝕜 P
inst✝⁴ : Nonempty ↥s₁
inst✝³ : Nonempty ↥s₂
inst✝² : s₁.direction.HasOrthogonalProjection
inst✝¹ : s₂.direction.HasOrthogonalProjection
p : P
h : ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)
inst✝ : (s₁ ⊔ s₂).direction.HasOrthogonalProjection
⊢ p -ᵥ ↑((orthogonalProjection s₁) p) ∈ s₁.directionᗮ ⊓ 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
⊢ #{i}ᶜ = n - 1 + 1

Tactic:
card_compl,

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
⊢ Fintype.card (Fin (n + 1)) - #{i} = n - 1 + 1
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case refine_1
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ (o.kahler x.1) x.2 ≠ 0

pp: case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ContinuousAt (fun y ↦ (o.kahler y.1) y.2) x

Tactic:
· exact o.kahler_ne_zero hx1 hx2

Goal state after:
case refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ContinuousAt (fun y ↦ (o.kahler y.1) y.2) x
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case mpr
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)
p : P
⊢ p ≠ s.points i ∧
      p -ᵥ s.points i ∈ vectorSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ →
    vectorSpan ℝ {p, s.points i} = (s.altitude i).direction

Tactic:
· rintro ⟨hne, h⟩
    rw [← Submodule.mem_inf, _root_.inf_comm, ← direction_altitude] at h
    rw [vectorSpan_eq_span_vsub_set_left_ne ℝ (Set.mem_insert _ _),
      Set.insert_sdiff_of_mem _ (Set.mem_singleton _),
      Set.sdiff_singleton_eq_self fun h => hne (Set.mem_singleton_iff.1 h), Set.image_singleton]
    refine Submodule.eq_of_le_of_finrank_eq ?_ ?_
    · rw [Submodule.span_le]
      simpa using h
    · rw [finrank_direction_altitude, finrank_span_set_eq_card]
      · simp
      · exact .singleton <| by simpa using hne

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
⊢ LinearIndependent ℝ ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ↔ AffineIndependent ℝ ![p₁, p₂, p₃]

Tactic:
affineIndependent_iff_linearIndependent_vsub ℝ _ (1 : Fin 3),

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
⊢ LinearIndependent ℝ ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ↔ LinearIndependent ℝ fun i ↦ ![p₁, p₂, p₃] ↑i -ᵥ ![p₁, p₂, p₃] 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
⊢ ∡ p₁ p₂ p₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ ↑π ↔ AffineIndependent ℝ ![p₁, p₂, p₃]

Tactic:
by
  rw [oangle, o.oangle_ne_zero_and_ne_pi_iff_linearIndependent,
    affineIndependent_iff_linearIndependent_vsub ℝ _ (1 : Fin 3), ←
    linearIndependent_equiv (finSuccAboveEquiv (1 : Fin 3))]
  convert! Iff.rfl
  ext i
  fin_cases i <;> rfl

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₁₂₄₅ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₄, p₅]
h₃₂₆₅ : line[ℝ, p₃, p₂] ∥ line[ℝ, p₆, p₅]
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₄ p₅ p₆

Tactic:
rw [AffineSubspace.affineSpan_pair_parallel_iff_vectorSpan_eq] at h₁₂₄₅ h₃₂₆₅
  exact two_zsmul_oangle_of_vectorSpan_eq h₁₂₄₅ h₃₂₆₅

Goal state after:
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
⊢ ‖x‖ / Real.cos (angle x (x + y)) = ‖x + y‖

Tactic:
rw [cos_angle_add_of_inner_eq_zero h]
  rcases h0 with (h0 | h0)
  · rw [div_div_eq_mul_div, mul_comm, div_eq_mul_inv, mul_inv_cancel_right₀ (norm_ne_zero_iff.2 h0)]
  · simp [h0]

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

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ o.oangle (x + r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r⁻¹)

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj, ←
    neg_neg ((π / 2 : ℝ) : Real.Angle), ← rotation_neg_orientation_eq_neg, add_comm]

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
⊢ (-o).oangle (r • ((-o).rotation (-↑(π / 2))) x) (r • ((-o).rotation (-↑(π / 2))) x + x) = ↑(Real.arctan r⁻¹)
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
c p₁ p₂ : P
⊢ ⟪2⁻¹ • (c -ᵥ p₁ + (c -ᵥ p₂)), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪((c -ᵥ p₁) +ᵥ c) -ᵥ p₂, p₂ -ᵥ p₁⟫ = 0

Tactic:
real_inner_smul_left,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ 2⁻¹ * ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪((c -ᵥ p₁) +ᵥ c) -ᵥ p₂, p₂ -ᵥ p₁⟫ = 0
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
p₁ p₂ : P
⊢ midpoint ℝ p₁ p₂ ∈ perpBisector p₁ p₂

Tactic:
by
  simp [mem_perpBisector_iff_inner_eq_zero]

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p q : P
⊢ |⟪‖v‖⁻¹ • v, q -ᵥ p⟫| = ‖q -ᵥ p‖ ↔ ∃ a, a • v = q -ᵥ p

Tactic:
real_inner_smul_left,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p q : P
⊢ |‖v‖⁻¹ * ⟪v, q -ᵥ p⟫| = ‖q -ᵥ p‖ ↔ ∃ a, a • v = q -ᵥ p
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
c p₁ p₂ : P
⊢ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ - ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = dist p₁ p₂ ^ 2 / 2

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
c p₁ p₂ : P
⊢ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = dist p₁ p₂ ^ 2 / 2
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
c p₁ p₂ : P
⊢ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪2⁻¹ • (p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = dist p₁ p₂ ^ 2 / 2

Tactic:
real_inner_smul_left,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = 2⁻¹ * ⟪p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = dist p₁ p₂ ^ 2 / 2
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
⊢ ⟪r • v, r • v⟫ + 2 * ⟪r • v, p₁ -ᵥ p₂⟫ + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ =
    ⟪v, v⟫ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫

Tactic:
real_inner_smul_left,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
r : ℝ
v : V
p₁ p₂ : P
⊢ r * ⟪v, r • v⟫ + 2 * ⟪r • v, p₁ -ᵥ p₂⟫ + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ =
    ⟪v, v⟫ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫
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
⊢ r * ⟪v, r • v⟫ + 2 * ⟪r • v, p₁ -ᵥ p₂⟫ + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ =
    ⟪v, v⟫ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫

Tactic:
real_inner_smul_left,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
r : ℝ
v : V
p₁ p₂ : P
⊢ r * ⟪v, r • v⟫ + 2 * (r * ⟪v, p₁ -ᵥ p₂⟫) + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫ =
    ⟪v, v⟫ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫
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:
by
  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.Sphere.Basic

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

Tactic:
rintro rfl; exact isDiameter_ofDiameter _ _

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

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
s : Sphere P
p q : P
h : s.orthRadius p ≤ s.orthRadius q
h' : (ℝ ∙ (p -ᵥ s.center))ᗮ ≤ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : ⟪p -ᵥ s.center, r • (p -ᵥ s.center)⟫ - ⟪r • (p -ᵥ s.center), r • (p -ᵥ s.center)⟫ = 0
⊢ p = q ∨ q = s.center

Tactic:
real_inner_smul_left,

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
s : Sphere P
p q : P
h : s.orthRadius p ≤ s.orthRadius q
h' : (ℝ ∙ (p -ᵥ s.center))ᗮ ≤ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : ⟪p -ᵥ s.center, r • (p -ᵥ s.center)⟫ - r * ⟪p -ᵥ s.center, r • (p -ᵥ s.center)⟫ = 0
⊢ p = q ∨ q = s.center
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 = 0

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 : 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
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
c : ℝ
hc : c • v = p -ᵥ s.center
hc0 : c ≠ 0
c' : ℝ
⊢ (c' / c) • (p -ᵥ s.center) = c' • v

Tactic:
simp [← hc, smul_smul, hc0]

Goal state after:
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 : s₂.radius - s₁.radius = 0
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : s₁.center = s₂.center
⊢ s₁.IsIntTangent s₂

Tactic:
sub_eq_zero,

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
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:
rw [← dist_orthogonalProjectionSpan_faceOpposite_eq_iff_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃] 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
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.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 ⋯).excenterWeights = s.excenterWeights

Tactic:
by
  ext
  simp [excenterWeights]

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).excenterWeights = s.excenterWeights

Tactic:
by
  ext
  simp [excenterWeights]

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₁ : ∡ (t.points i₂) (t.points i₁) p = ∡ p (t.points i₁) (t.points i₃) + ↑π
h₂ : ∡ (t.points i₃) (t.points i₂) p = ∡ p (t.points i₂) (t.points i₁) + ↑π
⊢ 2 • ∡ (t.points i₂) (t.points i₁) ?m.162 = 2 • ∡ ?m.162 (t.points i₁) (t.points i₃)

Tactic:
rw [h₁]; simp

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:
have h := s.excenterExists_empty.sum_excenterWeights_eq_one

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
h : ∑ i, s.excenterWeights ∅ i = 1
⊢ s.incenter ∈ s.interior