mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case mpr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
y : V
hy : y ≠ 0
r : ℝ
hr : 0 ≤ r
h₁ : ‖r • y‖ = ‖y‖
h₂ : SameRay ℝ (r • y) y
⊢ r • y = y

Tactic:
have : ‖y‖ ≠ 0 := by simpa using hy

Goal state after:
case mpr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
y : V
hy : y ≠ 0
r : ℝ
hr : 0 ≤ r
h₁ : ‖r • y‖ = ‖y‖
h₂ : SameRay ℝ (r • y) y
this : ‖y‖ ≠ 0
⊢ r • y = y
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case inl.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hsyz : (o.oangle y z).sign = 0
h : InnerProductGeometry.angle 0 x = InnerProductGeometry.angle y z
hs : (o.oangle 0 x).sign = (o.oangle y z).sign
hswx : (o.oangle 0 x).sign = 0
⊢ InnerProductGeometry.angle 0 x = π / 2 ∧ InnerProductGeometry.angle y z = π / 2

pp: case inl.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w y z : V
hsyz : (o.oangle y z).sign = 0
h : InnerProductGeometry.angle w 0 = InnerProductGeometry.angle y z
hs : (o.oangle w 0).sign = (o.oangle y z).sign
hswx : (o.oangle w 0).sign = 0
⊢ InnerProductGeometry.angle w 0 = π / 2 ∧ InnerProductGeometry.angle y z = π / 2

pp: case inr.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x z : V
hswx : (o.oangle w x).sign = 0
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle 0 z
hs : (o.oangle w x).sign = (o.oangle 0 z).sign
hsyz : (o.oangle 0 z).sign = 0
⊢ InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle 0 z = π / 2

pp: case inr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y : V
hswx : (o.oangle w x).sign = 0
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y 0
hs : (o.oangle w x).sign = (o.oangle y 0).sign
hsyz : (o.oangle y 0).sign = 0
⊢ InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y 0 = π / 2

Tactic:
· simpa using h.symm

Goal state after:
case inl.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w y z : V
hsyz : (o.oangle y z).sign = 0
h : InnerProductGeometry.angle w 0 = InnerProductGeometry.angle y z
hs : (o.oangle w 0).sign = (o.oangle y z).sign
hswx : (o.oangle w 0).sign = 0
⊢ InnerProductGeometry.angle w 0 = π / 2 ∧ InnerProductGeometry.angle y z = π / 2

case inr.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x z : V
hswx : (o.oangle w x).sign = 0
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle 0 z
hs : (o.oangle w x).sign = (o.oangle 0 z).sign
hsyz : (o.oangle 0 z).sign = 0
⊢ InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle 0 z = π / 2

case inr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y : V
hswx : (o.oangle w x).sign = 0
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y 0
hs : (o.oangle w x).sign = (o.oangle y 0).sign
hsyz : (o.oangle y 0).sign = 0
⊢ InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y 0 = π / 2
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case inl.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w y z : V
hsyz : (o.oangle y z).sign = 0
h : InnerProductGeometry.angle w 0 = InnerProductGeometry.angle y z
hs : (o.oangle w 0).sign = (o.oangle y z).sign
hswx : (o.oangle w 0).sign = 0
⊢ InnerProductGeometry.angle w 0 = π / 2 ∧ InnerProductGeometry.angle y z = π / 2

pp: case inr.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x z : V
hswx : (o.oangle w x).sign = 0
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle 0 z
hs : (o.oangle w x).sign = (o.oangle 0 z).sign
hsyz : (o.oangle 0 z).sign = 0
⊢ InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle 0 z = π / 2

pp: case inr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y : V
hswx : (o.oangle w x).sign = 0
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y 0
hs : (o.oangle w x).sign = (o.oangle y 0).sign
hsyz : (o.oangle y 0).sign = 0
⊢ InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y 0 = π / 2

Tactic:
· simpa using h.symm

Goal state after:
case inr.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x z : V
hswx : (o.oangle w x).sign = 0
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle 0 z
hs : (o.oangle w x).sign = (o.oangle 0 z).sign
hsyz : (o.oangle 0 z).sign = 0
⊢ InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle 0 z = π / 2

case inr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y : V
hswx : (o.oangle w x).sign = 0
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y 0
hs : (o.oangle w x).sign = (o.oangle y 0).sign
hsyz : (o.oangle y 0).sign = 0
⊢ InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y 0 = π / 2
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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
h' : InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y z = π / 2
⊢ o.oangle w x = o.oangle y z

Tactic:
rcases h' with ⟨hwx, hyz⟩

Goal state after:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
⊢ o.oangle w x = o.oangle y z
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case refine_2.inr.inr.inl
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₃ = 0
⊢ Collinear ℝ {p₁, p₂, p₃}

Tactic:
rw [angle_eq_zero_iff_ne_and_wbtw] at h
      rcases h with (⟨-, h⟩ | ⟨-, h⟩)
      · rw [Set.insert_comm]
        exact h.collinear
      · rw [Set.insert_comm, Set.pair_comm]
        exact h.collinear

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)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w ≠ 0 ∧ x ≠ 0) ∧ y ≠ 0 ∧ z ≠ 0
⊢ |(o.oangle w x).toReal| = |(o.oangle y z).toReal|

Tactic:
rwa [o.angle_eq_abs_oangle_toReal h0.1.1 h0.1.2,
      o.angle_eq_abs_oangle_toReal h0.2.1 h0.2.2] at 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 y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x + y) y).cos = ‖y‖ / ‖x + y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
  rw [add_comm]
  exact (-o).cos_oangle_add_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 y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x + y) y).sin * ‖x + y‖ = ‖x‖

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

Goal state after:
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 : ℝ
⊢ (o.oangle (r • x) y).sign = SignType.sign r * (o.oangle x y).sign

Tactic:
rcases lt_trichotomy r 0 with (h | 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 : ℝ
h : r < 0
⊢ (o.oangle (r • x) y).sign = SignType.sign r * (o.oangle x y).sign

case inr.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 : ℝ
h : r = 0
⊢ (o.oangle (r • x) y).sign = SignType.sign r * (o.oangle x y).sign

case inr.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 : ℝ
h : 0 < r
⊢ (o.oangle (r • x) y).sign = SignType.sign r * (o.oangle x y).sign
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 : ℝ
⊢ (o.oangle x (r • y)).sign = SignType.sign r * (o.oangle x y).sign

Tactic:
rcases lt_trichotomy r 0 with (h | 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 : ℝ
h : r < 0
⊢ (o.oangle x (r • y)).sign = SignType.sign r * (o.oangle x y).sign

case inr.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 : ℝ
h : r = 0
⊢ (o.oangle x (r • y)).sign = SignType.sign r * (o.oangle x y).sign

case inr.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 : ℝ
h : 0 < r
⊢ (o.oangle x (r • y)).sign = SignType.sign r * (o.oangle x y).sign
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ : P
h : p₁ ≠ p₂
r : ℝ
⊢ ⟪2⁻¹ • -(p₂ -ᵥ p₁) - r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁), 2⁻¹ • -(p₂ -ᵥ p₁) - r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁)⟫ =
    ⟪2⁻¹ • (p₂ -ᵥ p₁) - r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁), 2⁻¹ • (p₂ -ᵥ p₁) - r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁)⟫

Tactic:
inner_sub_sub_self

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ : P
h : p₁ ≠ p₂
r : ℝ
⊢ ⟪2⁻¹ • -(p₂ -ᵥ p₁), 2⁻¹ • -(p₂ -ᵥ p₁)⟫ - ⟪2⁻¹ • -(p₂ -ᵥ p₁), r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁)⟫ -
        ⟪r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁), 2⁻¹ • -(p₂ -ᵥ p₁)⟫ +
      ⟪r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁), r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁)⟫ =
    ⟪2⁻¹ • (p₂ -ᵥ p₁), 2⁻¹ • (p₂ -ᵥ p₁)⟫ - ⟪2⁻¹ • (p₂ -ᵥ p₁), r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁)⟫ -
        ⟪r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁), 2⁻¹ • (p₂ -ᵥ p₁)⟫ +
      ⟪r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁), r • (o.rotation ↑(π / 2)) (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
r₁ r₂ r₃ r₄ : ℝ
hr₁ : ¬r₁ = 0
⊢ SignType.sign ((-r₃ / r₁ * r₂ + r₄) * r₁) * (o.oangle x y).sign =
    SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign

Tactic:
add_mul,

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₁ + r₄ * r₁) * (o.oangle x y).sign =
    SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign
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 z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z

Tactic:
by_cases hs : (o.oangle x y).sign = (o.oangle y z).sign

Goal state after:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : (o.oangle x y).sign = (o.oangle y z).sign
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

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✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
hc : Collinear ℝ {p', ↑((orthogonalProjection s₁) p), ↑((orthogonalProjection s₂) p)}
⊢ False

Tactic:
have h₁ : (orthogonalProjection s₁ p : P) ∈ line[ℝ, p', (orthogonalProjection s₂ p : P)] :=
      hc.mem_affineSpan_of_mem_of_ne (by grind) (by grind) (by grind) (by grind)

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✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
hc : Collinear ℝ {p', ↑((orthogonalProjection s₁) p), ↑((orthogonalProjection s₂) p)}
h₁ : ↑((orthogonalProjection s₁) p) ∈ line[ℝ, p', ↑((orthogonalProjection s₂) p)]
⊢ False
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
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = 2
c₁ c₂ p₁ p₂ p : P
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₂
⊢ finrank ℝ ↥⊤.direction = 2

Tactic:
rw [direction_top, finrank_top]
    exact hd

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
⊢ ‖q -ᵥ s.center‖ * ‖q -ᵥ s.center‖ = ‖p -ᵥ s.center‖ * ‖p -ᵥ s.center‖ + ‖q -ᵥ p‖ * ‖q -ᵥ p‖ ↔ q ∈ s.orthRadius p

Tactic:
rw [← vsub_add_vsub_cancel q p s.center]

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
⊢ ‖q -ᵥ p + (p -ᵥ s.center)‖ * ‖q -ᵥ p + (p -ᵥ s.center)‖ = ‖p -ᵥ s.center‖ * ‖p -ᵥ s.center‖ + ‖q -ᵥ p‖ * ‖q -ᵥ p‖ ↔
    q ∈ s.orthRadius p
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
h : dist q s.center ^ 2 = dist p s.center ^ 2 + dist q p ^ 2
⊢ q ∈ s ↔ 0 ≤ s.radius ∧ dist q p ^ 2 = s.radius ^ 2 - dist p s.center ^ 2

Tactic:
rw [← sub_eq_iff_eq_add'] at h

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p q : P
h : dist q s.center ^ 2 - dist p s.center ^ 2 = dist q p ^ 2
⊢ q ∈ s ↔ 0 ≤ s.radius ∧ dist q p ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
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
inst✝¹ : Nonempty ↥as
inst✝ : as.direction.HasOrthogonalProjection
⊢ dist s.center ↑((orthogonalProjection as) s.center) = s.radius ↔ s.IsTangent as

Tactic:
dist_orthogonalProjection_eq_radius_iff_isTangent

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
as : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥as
inst✝ : as.direction.HasOrthogonalProjection
⊢ s.IsTangent as ↔ s.IsTangent as
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case neg.refine_3
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
h : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
⊢ s₁.center = s₂.center ∨ s₁.radius / (s₁.radius + s₂.radius) ∈ Set.Icc 0 1

Tactic:
refine .inr ⟨?_, ?_⟩

Goal state after:
case neg.refine_3.refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
h : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
⊢ 0 ≤ s₁.radius / (s₁.radius + s₂.radius)

case neg.refine_3.refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
h : dist s₁.center s₂.center = s₁.radius + s₂.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.radius + s₂.radius = 0
⊢ s₁.radius / (s₁.radius + s₂.radius) ≤ 1
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
pp: case inr.inl
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₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ : ∡ (t.points i₃) (t.points i₂) (excenter t signs) = ∡ (excenter t signs) (t.points i₂) (t.points i₁)
h₁' : excenter t signs = excenter t {i₁}
h₂' : excenter t signs = incenter t
⊢ excenter t signs = incenter t

Tactic:
exact h₂'

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))
inst✝ : Decidable (s.ExcenterExists signs)
⊢ ∑ i, s.excenterWeights signs i = if s.ExcenterExists signs then 1 else 0

Tactic:
by
  simp_rw [ExcenterExists, excenterWeights]
  split_ifs with h
  · simp [← Finset.mul_sum, h]
  · simp only [ne_eq, not_not] at h
    simp [h]

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

Goal state before:
pp: case inl.inr
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₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ : ∡ (t.points i₃) (t.points i₂) (excenter t signs) = ∡ (excenter t signs) (t.points i₂) (t.points i₁) + ↑π
h₁' : excenter t signs = incenter t
h₂' : excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₁}

Tactic:
exact h₂'

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

Goal state before:
pp: case inl.inl
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₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃) + ↑π
h₂ : ∡ (t.points i₃) (t.points i₂) (excenter t signs) = ∡ (excenter t signs) (t.points i₂) (t.points i₁) + ↑π
h₁' : excenter t signs = excenter t {i₂}
h₂' : excenter t signs = excenter t {i₃}
⊢ excenter t signs = excenter t {i₃}

Tactic:
exact h₂'

Goal state after: