mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Incenter

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
n : ℕ
inst✝¹ : NeZero n
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : ¬i = j
⊢ s.excenter signs ∉ line[ℝ, s.points i, s.points j]

Tactic:
·

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
n : ℕ
inst✝¹ : NeZero n
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : ¬i = j
⊢ s.excenter signs ∉ line[ℝ, s.points i, s.points j]
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case H
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ι : Type u_3
hne : Nonempty ι
inst✝ : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val✝ : Fintype ι
m : ℕ
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P},
    AffineIndependent ℝ p →
      ∀ (val : Fintype ι),
        Fintype.card ι = m + 1 →
          ∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x // x ≠ i }
⊢ ∀ (x : ι), x ∈ {x | x ≠ i} ↔ x ≠ i

Tactic:
·

Goal state after:
case H
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ι : Type u_3
hne : Nonempty ι
inst✝ : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val✝ : Fintype ι
m : ℕ
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P},
    AffineIndependent ℝ p →
      ∀ (val : Fintype ι),
        Fintype.card ι = m + 1 →
          ∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x // x ≠ i }
⊢ ∀ (x : ι), x ∈ {x | x ≠ i} ↔ x ≠ i
Module: Mathlib.Geometry.Euclidean.Incenter

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : s.excenterWeights signs₁ = s.excenterWeights signs₂
⊢ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ
⊢ s.excenterWeights signs₁ = s.excenterWeights signs₂

Tactic:
·

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : s.excenterWeights signs₁ = s.excenterWeights signs₂
⊢ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ
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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ / (1 / √(1 + (∡ p₂ p₁ s.center).tan ^ 2)) =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁ + (∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖

pp: case h
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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0

Tactic:
·

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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ / (1 / √(1 + (∡ p₂ p₁ s.center).tan ^ 2)) =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁ + (∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
y : V
hy : y ≠ 0
hx : -y ≠ 0
⊢ Real.cos (angle (-y) y) = Real.cos (angle (-y) (-y + y) + angle y (y + -y))

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
⊢ Real.cos (angle x y) = Real.cos (angle x (x + y) + angle y (y + x))

Tactic:
·

Goal state after:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
y : V
hy : y ≠ 0
hx : -y ≠ 0
⊢ Real.cos (angle (-y) y) = Real.cos (angle (-y) (-y + y) + angle y (y + -y))
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
⊢ Real.cos (angle x y) = Real.cos (angle x (x + y) + angle y (y + x))

Tactic:
·

Goal state after:
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
⊢ Real.cos (angle x y) = Real.cos (angle x (x + y) + angle y (y + x))
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case refine_1.inl
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₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : s.excenterWeights signs₁ = s.excenterWeights signs₂
hi :
  ∀ (i : Fin (n + 1)),
    SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₁ i) =
      SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₂ i)
hn₁ : ∑ i, s.excenterWeightsUnnorm signs₁ i ≠ 0
hn₂ : ∑ i, s.excenterWeightsUnnorm signs₂ i ≠ 0
hs : SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ = SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹
⊢ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ

pp: case refine_1.inr
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₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : s.excenterWeights signs₁ = s.excenterWeights signs₂
hi :
  ∀ (i : Fin (n + 1)),
    SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₁ i) =
      SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₂ i)
hn₁ : ∑ i, s.excenterWeightsUnnorm signs₁ i ≠ 0
hn₂ : ∑ i, s.excenterWeightsUnnorm signs₂ i ≠ 0
hs : SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ = -SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹
⊢ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ

Tactic:
·

Goal state after:
case refine_1.inl
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₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : s.excenterWeights signs₁ = s.excenterWeights signs₂
hi :
  ∀ (i : Fin (n + 1)),
    SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₁ i) =
      SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₂ i)
hn₁ : ∑ i, s.excenterWeightsUnnorm signs₁ i ≠ 0
hn₂ : ∑ i, s.excenterWeightsUnnorm signs₂ i ≠ 0
hs : SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ = SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹
⊢ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ
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, y⟫ * ‖x + y‖ ^ 2 = ⟪x, x + y⟫ * ⟪y, x + y⟫ - (⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
simp only [← real_inner_self_eq_norm_sq, inner_add_right, inner_add_left, real_inner_comm]

Goal state after:
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, y⟫ * (⟪x, x⟫ + ⟪x, y⟫ + (⟪x, y⟫ + ⟪y, y⟫)) =
    (⟪x, x⟫ + ⟪x, y⟫) * (⟪x, y⟫ + ⟪y, y⟫) - (⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
y : V
hy : y ≠ 0
hx : -y ≠ 0
⊢ Real.sin (angle (-y) y) = Real.sin (angle (-y) (-y + y) + angle y (y + -y))

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
⊢ Real.sin (angle x y) = Real.sin (angle x (x + y) + angle y (y + x))

Tactic:
·

Goal state after:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
y : V
hy : y ≠ 0
hx : -y ≠ 0
⊢ Real.sin (angle (-y) y) = Real.sin (angle (-y) (-y + y) + angle y (y + -y))
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
⊢ Real.sin (angle x y) = Real.sin (angle x (x + y) + angle y (y + x))

Tactic:
·

Goal state after:
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
⊢ Real.sin (angle x y) = Real.sin (angle x (x + y) + angle y (y + x))
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: case h
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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0

Tactic:
·

Goal state after:
case h
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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case refine_1.inr
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₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : s.excenterWeights signs₁ = s.excenterWeights signs₂
hi :
  ∀ (i : Fin (n + 1)),
    SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₁ i) =
      SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₂ i)
hn₁ : ∑ i, s.excenterWeightsUnnorm signs₁ i ≠ 0
hn₂ : ∑ i, s.excenterWeightsUnnorm signs₂ i ≠ 0
hs : SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ = -SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹
⊢ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ

Tactic:
·

Goal state after:
case refine_1.inr
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₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : s.excenterWeights signs₁ = s.excenterWeights signs₂
hi :
  ∀ (i : Fin (n + 1)),
    SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₁ i) =
      SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₂ i)
hn₁ : ∑ i, s.excenterWeightsUnnorm signs₁ i ≠ 0
hn₂ : ∑ i, s.excenterWeightsUnnorm signs₂ i ≠ 0
hs : SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ = -SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹
⊢ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ
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 + y‖ ^ 2 =
    √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) * ⟪y, x + y⟫ + ⟪x, x + y⟫ * √(⟪y, y⟫ * ⟪x, x⟫ - ⟪y, x⟫ * ⟪y, x⟫)

Tactic:
simp only [← real_inner_self_eq_norm_sq, inner_add_right, inner_add_left, real_inner_comm]

Goal state after:
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⟫)
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
y : V
hy : y ≠ 0
⊢ angle 0 y = angle 0 (0 + y) + angle y (0 + y)

pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
⊢ angle x y = angle x (x + y) + angle y (x + y)

Tactic:
·

Goal state after:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
y : V
hy : y ≠ 0
⊢ angle 0 y = angle 0 (0 + y) + angle y (0 + y)
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
this✝ : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
this : (r₁ + r₂ - 1) • (x + y) = 0
h✝ : r₁ + r₂ - 1 = 0
⊢ False

pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
this✝ : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
this : (r₁ + r₂ - 1) • (x + y) = 0
h✝ : x + y = 0
⊢ False

Tactic:
·

Goal state after:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
this✝ : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
this : (r₁ + r₂ - 1) • (x + y) = 0
h✝ : r₁ + r₂ - 1 = 0
⊢ False
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
this✝ : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
this : (r₁ + r₂ - 1) • (x + y) = 0
h✝ : x + y = 0
⊢ False

Tactic:
·

Goal state after:
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
this✝ : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
this : (r₁ + r₂ - 1) • (x + y) = 0
h✝ : x + y = 0
⊢ False
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h✝ : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
h : angle x y + n • (2 * π) = angle x (x + y) + angle y (x + y)
this✝ : -1 < n
this : n < 1
⊢ n = 0

Tactic:
by lia

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

Goal state before:
pp: 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
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ ↑π
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : o.oangle x (x - y) = o.oangle (y - x) y
⊢ ‖x‖ = ‖y‖

pp: 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
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ ↑π
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : o.oangle x (x - y) = o.oangle (y - x) y + ↑π
⊢ ‖x‖ = ‖y‖

Tactic:
·

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
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ ↑π
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : o.oangle x (x - y) = o.oangle (y - x) y
⊢ ‖x‖ = ‖y‖
Module: Mathlib.Geometry.Euclidean.Incenter

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ
⊢ s.excenterWeights signs₁ = s.excenterWeights signs₂

Tactic:
·

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ
⊢ s.excenterWeights signs₁ = s.excenterWeights signs₂
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: 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
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ ↑π
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : angle x (x - y) = angle y (y - x)
⊢ angle x y ≠ π

Tactic:
rw [ne_eq, ← o.oangle_eq_pi_iff_angle_eq_pi]

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
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ ↑π
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : angle x (x - y) = angle y (y - x)
⊢ ¬o.oangle x y = ↑π
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: 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
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ ↑π
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : o.oangle x (x - y) = o.oangle (y - x) y + ↑π
⊢ ‖x‖ = ‖y‖

Tactic:
·

Goal state after:
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
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ ↑π
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : o.oangle x (x - y) = o.oangle (y - x) y + ↑π
⊢ ‖x‖ = ‖y‖
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case refine_2.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs₁ : Finset (Fin (n + 1))
h₁ h₂ : s.ExcenterExists signs₁
⊢ s.excenterWeights signs₁ = s.excenterWeights signs₁

pp: case refine_2.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs₂ : Finset (Fin (n + 1))
h₂ : s.ExcenterExists signs₂
h₁ : s.ExcenterExists signs₂ᶜ
⊢ s.excenterWeights signs₂ᶜ = s.excenterWeights signs₂

Tactic:
·

Goal state after:
case refine_2.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs₁ : Finset (Fin (n + 1))
h₁ h₂ : s.ExcenterExists signs₁
⊢ s.excenterWeights signs₁ = s.excenterWeights signs₁
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case refine_2.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs₂ : Finset (Fin (n + 1))
h₂ : s.ExcenterExists signs₂
h₁ : s.ExcenterExists signs₂ᶜ
⊢ s.excenterWeights signs₂ᶜ = s.excenterWeights signs₂

Tactic:
·

Goal state after:
case refine_2.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs₂ : Finset (Fin (n + 1))
h₂ : s.ExcenterExists signs₂
h₁ : s.ExcenterExists signs₂ᶜ
⊢ s.excenterWeights signs₂ᶜ = s.excenterWeights signs₂
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case e'_5.e'_3
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₁ -ᵥ p₃ = p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)

pp: case e'_6.e'_3
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₁ -ᵥ p₃ = p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)

Tactic:
·

Goal state after:
case e'_5.e'_3
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₁ -ᵥ p₃ = p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case e'_6.e'_3
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₁ -ᵥ p₃ = p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)

Tactic:
·

Goal state after:
case e'_6.e'_3
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₁ -ᵥ p₃ = p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case e'_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₃ -ᵥ p₂ = p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)

pp: case e'_3
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₂ -ᵥ p₃ = p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)

Tactic:
·

Goal state after:
case e'_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₃ -ᵥ p₂ = p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case e'_3
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₂ -ᵥ p₃ = p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)

Tactic:
·

Goal state after:
case e'_3
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ p₂ -ᵥ p₃ = p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)