mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
x y : M
a b : R
hF : F.IsFaceOf C
hx : x ∈ C
hy : y ∈ C
ha : 0 < a
hb : 0 < b
h : a • x + b • y ∈ F
⊢ y ∈ F

Tactic:
apply hF.2 hy (smul_mem _ ha.le hx) hb; rwa [add_comm]

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
x y : M
a b : R
hF : F.IsFaceOf C
hx : x ∈ C
hy : y ∈ C
ha : 0 < a
hb : 0 < b
h : a • x + b • y ∈ F
⊢ y ∈ F

Tactic:
by
  apply hF.2 hy (smul_mem _ ha.le hx) hb; rwa [add_comm]

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
hF : F.IsFaceOf C
x y : M
hx : x ∈ C
hy : y ∈ C
⊢ x + y ∈ F ↔ x ∈ F ∧ y ∈ F

Tactic:
refine ⟨?_, fun ⟨hx, hy⟩ ↦ F.add_mem hx hy⟩
  exact fun h ↦ ⟨mem_of_add_mem_left hF hx hy h, mem_of_add_mem_right hF hx hy h⟩

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

Tactic:
← mul_assoc,

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)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).num -
      Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
          Polynomial.C
            ↑((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)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ 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.map Polynomial.C (Q₂ h) * Φ E = θ E

Tactic:
by
  rw [Q₂_map h, Q₁_mul_Φ h]

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 ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
eq :
  (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))
⊢ IsUnit (Polynomial.C ((aeval α) (f E))) ∧ IsUnit (Polynomial.C ((aeval α) (g E)))

Tactic:
rw [Polynomial.isUnit_C, isUnit_iff_ne_zero, Polynomial.isUnit_C, isUnit_iff_ne_zero]
    obtain (H | H) := aeval_ne_zero_of_isCoprime (generator E).isCoprime_num_denom α
    · refine ⟨H, Polynomial.C_injective.ne_iff.mp ?_⟩
      rw [map_zero, ← mul_ne_zero_iff_left <| Polynomial.map_ne_zero <|
        num_ne_zero (generator_ne_zero h)]
      exact eq ▸ mul_ne_zero (Polynomial.map_ne_zero (generator E).denom_ne_zero) <|
        Polynomial.C_ne_zero.mpr H
    · refine ⟨Polynomial.C_injective.ne_iff.mp ?_, H⟩
      rw [map_zero, ← mul_ne_zero_iff_left <| Polynomial.map_ne_zero (generator E).denom_ne_zero]
      exact eq ▸ mul_ne_zero (Polynomial.map_ne_zero (num_ne_zero (generator_ne_zero h))) <|
        Polynomial.C_ne_zero.mpr H

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
i : Fin (n + 1)
⊢ (mk' (s.points i) (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ).direction ⊓
      (affineSpan ℝ (Set.range s.points)).direction =
    (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)

Tactic:
direction_mk',

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
i : Fin (n + 1)
⊢ (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ ⊓ (affineSpan ℝ (Set.range s.points)).direction =
    (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
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✝ : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₂ : p₂ ∈ s
⊢ dist p₁ ↑((orthogonalProjection s) p₁) = dist p₁ p₂ ↔ ↑((orthogonalProjection s) p₁) = p₂

Tactic:
have : Nonempty s := ⟨p₂, hp₂⟩

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 : AffineSubspace 𝕜 P
inst✝ : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₂ : p₂ ∈ s
this : Nonempty ↥s
⊢ dist p₁ ↑((orthogonalProjection s) p₁) = dist p₁ p₂ ↔ ↑((orthogonalProjection s) p₁) = p₂
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ p₄ : P
h : ∠ p₂ p₃ p₄ = π
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₄

Tactic:
unfold angle at *

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₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ dist p₁ p₂ ≠ 0

Tactic:
by
  by_contra heq
  rw [dist_eq_zero] at heq
  rw [heq, angle_self_left] at h
  exact Real.pi_ne_zero (by linarith)

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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ 0 < |s.height i * s.height j|

Tactic:
by simp [height]

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 : ℕ
inst✝ : n.AtLeastTwo
s : Simplex ℝ P n
i j : Fin (n + 1)
⊢ 0 < s.height i * s.height j

Tactic:
by simp [height]

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‖ * ‖x‖ + ‖y‖ * ‖y‖ ≠ 0

Tactic:
ne_comm

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
⊢ 0 ≠ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
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
⊢ ‖y‖ / Real.tan (angle x (x + y)) = ‖x‖

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

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 : Wbtw ℝ p₁ p₂ p₃
⊢ ∡ p₂ p₁ p₃ = 0

Tactic:
by_cases hp₂p₁ : 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 : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : p₂ = p₁
⊢ ∡ p₂ p₁ p₃ = 0

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 : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : ¬p₂ = p₁
⊢ ∡ p₂ p₁ p₃ = 0
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ o.oangle (x - y) x = ↑(Real.arctan (‖y‖ / ‖x‖))

Tactic:
by
  rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
  exact (-o).oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two h

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₂
h₃₂ : p₃ ≠ p₂
| p₂

Tactic:
rw [← AffineEquiv.pointReflection_self ℝ 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₂
h₃₂ : p₃ ≠ p₂
| (AffineEquiv.pointReflection ℝ p₂) p₂
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ‖y‖ / ((-o).oangle x (x - y)).tan = ‖x‖

Tactic:
exact (-o).norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two h

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

Goal state before:
pp: 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 (-(o.rotation ↑(π / 2)) x) = -↑(π / 2)

Tactic:
o.oangle_neg_right h,

Goal state after:
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 ((o.rotation ↑(π / 2)) x) + ↑π = -↑(π / 2)

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.rotation ↑(π / 2)) x ≠ 0
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Projection

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
s : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ ↑((orthogonalProjection s) p)
⊢ 2 • ∡ p' (↑((orthogonalProjection s) p)) p = ↑π

Tactic:
by
  rw [Real.Angle.two_zsmul_eq_pi_iff]
  exact oangle_orthogonalProjection_self p hp h hp'

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
r₁ r₂ r₃ r₄ : ℝ
hr₁ : ¬r₁ = 0
⊢ SignType.sign (-r₃ / r₁ * r₂ + r₄) * (SignType.sign r₁ * (o.oangle x y).sign) =
    SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign

Tactic:
← mul_assoc,

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
r₁ r₂ r₃ r₄ : ℝ
hr₁ : ¬r₁ = 0
⊢ SignType.sign (-r₃ / r₁ * r₂ + r₄) * SignType.sign r₁ * (o.oangle x y).sign =
    SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

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₁).cos = dist p₃ p₂ / dist p₁ p₃

Tactic:
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
  rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    cos_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

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
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
⊢ ∠ p₁ p₂ p₃ = ∠ p₃ p₂ p₄ ↔ ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ ∨ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁

Tactic:
simp_rw [angle, oangle,
    o.angle_eq_iff_oangle_eq_or_sameRay (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₄)]
  apply or_congr_right
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · obtain ⟨r, hr, he⟩ := h.exists_pos_left (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₄)
    rw [← vsub_vadd p₁ p₂, ← vsub_vadd p₄ p₂, ← he]
    nth_rw 1 4 [← one_smul ℝ (p₁ -ᵥ p₂)]
    exact wbtw_or_wbtw_smul_vadd_of_nonneg _ _ zero_le_one hr.le
  · rcases h with h | h
    · exact h.sameRay_vsub_left
    · exact h.sameRay_vsub_left.symm

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : 2 • ∡ p₂ p₁ p = 2 • ∡ p p₁ p₃
h' : ↑((orthogonalProjection line[ℝ, p₁, p₃]) p) = p₁
⊢ 2 • ∡ p₃ p₁ p = 2 • ∡ p p₁ p₂

Tactic:
rw [oangle_rev, smul_neg, ← h, oangle_rev, smul_neg, neg_neg]

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 : r * ⟪p -ᵥ s.center, p -ᵥ s.center⟫ - r * (r * ⟪p -ᵥ s.center, p -ᵥ s.center⟫) = 0
⊢ p = q ∨ q = s.center

Tactic:
← mul_assoc,

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 : r * ⟪p -ᵥ s.center, p -ᵥ s.center⟫ - r * r * ⟪p -ᵥ s.center, p -ᵥ s.center⟫ = 0
⊢ p = q ∨ q = s.center
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

Goal state before:
pp: case e'_8
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h : dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
ho : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
hs : ↑((orthogonalProjection (line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃])) p) = ↑((orthogonalProjection line[ℝ, p₁, p₂]) p)
hinf : line[ℝ, p₁, p₂] ⊓ line[ℝ, p₁, p₃] = affineSpan ℝ {p₁}
⊢ {p₁, p₂} ∪ {p₁, p₃} = Set.range ![p₁, p₂, p₃]

Tactic:
simp
        grind

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
s : Sphere P
p q : P
⊢ (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ).direction = (mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ).direction ∧
      (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ = ⊥ ↔ mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ = ⊥) ↔
    ∃ r, r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)

Tactic:
direction_mk',

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
⊢ (ℝ ∙ (p -ᵥ s.center))ᗮ = (ℝ ∙ (q -ᵥ s.center))ᗮ ∧
      (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ = ⊥ ↔ mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ = ⊥) ↔
    ∃ r, r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ 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 q : P
⊢ (∃ z, z • (p -ᵥ s.center) = q -ᵥ s.center) ∧ (mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ = ⊥ ↔ mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ = ⊥) ↔
    ∃ r, r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)

Tactic:
← coe_eq_bot_iff,

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
⊢ (∃ z, z • (p -ᵥ s.center) = q -ᵥ s.center) ∧
      (↑(mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ) = ∅ ↔ ↑(mk' q (ℝ ∙ (q -ᵥ s.center))ᗮ) = ∅) ↔
    ∃ r, r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)
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
p₁ p₂ p : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp : Sbtw ℝ p₁ p p₂
⊢ dist s.center p < s.radius

Tactic:
by
  set o := s.center
  obtain ⟨⟨t, ⟨ht₀, ht₁⟩, hpt⟩, hne₁, hne₂⟩ := hp
  have ht₀' : 0 < t := lt_of_le_of_ne ht₀ fun h => hne₁ <| by
    rw [← hpt, ← h, AffineMap.lineMap_apply_zero]
  have ht₁' : t < 1 := lt_of_le_of_ne ht₁ fun h => hne₂ <| by
    rw [← hpt, h, AffineMap.lineMap_apply_one]
  set u := p₁ -ᵥ o; set v := p₂ -ᵥ o
  have hu : ‖u‖ = s.radius := norm_vsub_center_eq_radius hp₁
  have hv : ‖v‖ = s.radius := norm_vsub_center_eq_radius hp₂
  have huv : u ≠ v := fun h => hne₁ <| by
    rw [← hpt, vsub_left_cancel h, AffineMap.lineMap_same, AffineMap.const_apply]
  have hpo : p -ᵥ o = (1 - t) • u + t • v := by
    rw [show p = (AffineMap.lineMap p₁ p₂) t from hpt.symm, AffineMap.lineMap_apply,
      vadd_vsub_assoc, show (p₂ -ᵥ p₁ : V) = v - u from
      (vsub_sub_vsub_cancel_right p₂ p₁ o).symm]
    module
  rw [dist_comm, dist_eq_norm_vsub, hpo]
  have hmem := (strictConvex_closedBall ℝ (0 : V) s.radius)
    (by simp [Metric.mem_closedBall, hu]) (by simp [Metric.mem_closedBall, hv])
    huv (sub_pos.mpr ht₁') ht₀' (sub_add_cancel 1 t)
  rwa [interior_closedBall _ (fun h : s.radius = 0 => huv <|
      (norm_eq_zero.mp (hu.trans h)).trans (norm_eq_zero.mp (hv.trans h)).symm),
    Metric.mem_ball, dist_zero_right] at hmem

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 : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
hu : ∃! cs, cs.center ∈ s ∧ ps ⊆ Metric.sphere cs.center cs.radius
⊢ ∃! cs₂, cs₂.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius

Tactic:
have : Nonempty s := Set.Nonempty.to_subtype (hnps.mono hps)

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
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
hu : ∃! cs, cs.center ∈ s ∧ ps ⊆ Metric.sphere cs.center cs.radius
this : Nonempty ↥s
⊢ ∃! cs₂, cs₂.center ∈ affineSpan ℝ (insert p ↑s) ∧ insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case e'_2.e'_6
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ∈ (Finset.univ.erase 0).erase i
⊢ ℝ ∙ (s.points i -ᵥ s.points 0) ≤ (affineSpan ℝ (Set.range (s.faceOpposite j).points)).direction

Tactic:
Submodule.span_singleton_le_iff_mem,

Goal state after:
case e'_2.e'_6
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ∈ (Finset.univ.erase 0).erase i
⊢ s.points i -ᵥ s.points 0 ∈ (affineSpan ℝ (Set.range (s.faceOpposite j).points)).direction
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₃
⊢ ⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫_ℝ = 0 ↔ dist s.center p₂ = s.radius

Tactic:
rw [← vsub_add_vsub_cancel p₁ o p₂, ← vsub_add_vsub_cancel p₃ o p₂,
    inner_add_left, inner_add_right, inner_add_right]

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