mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
H5 : angle y z = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
H5 : ¬angle y z = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
·

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
H5 : angle y z = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
Module: Mathlib.Geometry.Euclidean.Triangle

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
⊢ π / 3 ≤ ∠ p₁ p₂ p₃

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
⊢ π / 3 ≤ ∠ p₁ p₂ p₃
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case refine_1.h
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
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : r ∈ Set.Icc 0 1
t : ℝ
ht : t ∈ Set.Icc 0 1
h0 : |(s.signedInfDist j) ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) t)| = 0
⊢ (AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) t ∈ affineSpan ℝ (Set.range s.points)

Tactic:
·

Goal state after:
case refine_1.h
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
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : r ∈ Set.Icc 0 1
t : ℝ
ht : t ∈ Set.Icc 0 1
h0 : |(s.signedInfDist j) ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) t)| = 0
⊢ (AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) t ∈ affineSpan ℝ (Set.range s.points)
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 : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : r ∈ Set.Icc 0 1
t : ℝ
ht : t ∈ Set.Icc 0 1
⊢ Continuous ⇑(AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i))

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 : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : r ∈ Set.Icc 0 1
t : ℝ
ht : t ∈ Set.Icc 0 1
⊢ Continuous ⇑(AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i))
Module: Mathlib.Geometry.Euclidean.Triangle

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : p₂ = p₁
⊢ π / 3 < ∠ p₁ p₂ p₃

pp: case neg
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₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
·

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : p₂ = p₁
⊢ π / 3 < ∠ p₁ p₂ p₃
Module: Mathlib.Geometry.Euclidean.Triangle

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
⊢ π / 3 < ∠ p₁ p₂ p₃

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
⊢ π / 3 < ∠ p₁ p₂ p₃
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case mp
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))
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
hw : ∑ j, w j = 1
⊢ (Finset.affineCombination ℝ Finset.univ s.points) w = s.touchpoint signs i → w = s.touchpointWeights signs i

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
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
hw : ∑ j, w j = 1
⊢ w = s.touchpointWeights signs i → (Finset.affineCombination ℝ Finset.univ s.points) w = s.touchpoint signs i

Tactic:
·

Goal state after:
case mp
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))
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
hw : ∑ j, w j = 1
⊢ (Finset.affineCombination ℝ Finset.univ s.points) w = s.touchpoint signs i → w = s.touchpointWeights signs i
Module: Mathlib.Geometry.Euclidean.Incenter

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
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
hw : ∑ j, w j = 1
⊢ w = s.touchpointWeights signs i → (Finset.affineCombination ℝ Finset.univ s.points) w = s.touchpoint signs i

Tactic:
·

Goal state after:
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
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
hw : ∑ j, w j = 1
⊢ w = s.touchpointWeights signs i → (Finset.affineCombination ℝ Finset.univ s.points) w = s.touchpoint signs i
Module: Mathlib.Geometry.Euclidean.Incenter

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
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
hw : ∑ j, w j = 1
⊢ w = s.touchpointWeights signs i → (Finset.affineCombination ℝ Finset.univ s.points) w = s.touchpoint signs i

Tactic:
· rintro rfl
    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
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
hw : ∑ j, w j = 1
⊢ (Finset.affineCombination ℝ Finset.univ s.points) w = s.touchpoint signs i ↔ w = s.touchpointWeights signs i

Tactic:
by
  constructor
  · rw [← s.affineCombination_touchpointWeights]
    exact fun h ↦ (affineIndependent_iff_eq_of_fintype_affineCombination_eq ℝ s.points).1
      s.independent _ _ hw (s.sum_touchpointWeights _ _) h
  · rintro rfl
    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
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ (Finset.affineCombination ℝ Finset.univ (s.reindex e).points)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm i) ∘ ⇑e.symm) =
    (s.reindex e).touchpoint signs i

pp: V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ ∑ j, (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm i) ∘ ⇑e.symm) j = 1

Tactic:
·

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ (Finset.affineCombination ℝ Finset.univ (s.reindex e).points)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm i) ∘ ⇑e.symm) =
    (s.reindex e).touchpoint signs i
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
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ ∑ j, (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm i) ∘ ⇑e.symm) j = 1

Tactic:
·

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ ∑ j, (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm i) ∘ ⇑e.symm) j = 1
Module: Mathlib.Geometry.Euclidean.Triangle

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃
h : p₂ = p₁
⊢ ∠ p₁ p₂ p₃ ≤ π / 3

pp: case neg
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₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃
h : ¬p₂ = p₁
⊢ ∠ p₁ p₂ p₃ ≤ π / 3

Tactic:
·

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃
h : p₂ = p₁
⊢ ∠ p₁ p₂ p₃ ≤ π / 3
Module: Mathlib.Geometry.Euclidean.Triangle

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃
h : ¬p₂ = p₁
⊢ ∠ p₁ p₂ p₃ ≤ π / 3

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃
h : ¬p₂ = p₁
⊢ ∠ p₁ p₂ p₃ ≤ π / 3
Module: Mathlib.Geometry.Euclidean.Triangle

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : p₂ = p₁
⊢ ∠ p₁ p₂ p₃ < π / 3

pp: case neg
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₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
·

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : p₂ = p₁
⊢ ∠ p₁ p₂ p₃ < π / 3
Module: Mathlib.Geometry.Euclidean.Triangle

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
p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂
h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂
hne : ∠ p₂ p₂ p₃ ≠ ∠ p₂ p₃ p₂ ∨ ∠ p₂ p₂ p₃ ≠ ∠ p₃ p₂ p₂ ∨ ∠ p₂ p₃ p₂ ≠ ∠ p₃ p₂ p₂
h₂₃ : p₂ = p₃
⊢ ∠ p₂ p₂ p₃ < π / 3

pp: case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂
h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂
hne : ∠ p₂ p₂ p₃ ≠ ∠ p₂ p₃ p₂ ∨ ∠ p₂ p₂ p₃ ≠ ∠ p₃ p₂ p₂ ∨ ∠ p₂ p₃ p₂ ≠ ∠ p₃ p₂ p₂
h₂₃ : ¬p₂ = p₃
⊢ ∠ p₂ p₂ p₃ < π / 3

Tactic:
·

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
p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂
h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂
hne : ∠ p₂ p₂ p₃ ≠ ∠ p₂ p₃ p₂ ∨ ∠ p₂ p₂ p₃ ≠ ∠ p₃ p₂ p₂ ∨ ∠ p₂ p₃ p₂ ≠ ∠ p₃ p₂ p₂
h₂₃ : p₂ = p₃
⊢ ∠ p₂ p₂ p₃ < π / 3
Module: Mathlib.Geometry.Euclidean.Triangle

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
p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂
h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂
hne : ∠ p₂ p₂ p₃ ≠ ∠ p₂ p₃ p₂ ∨ ∠ p₂ p₂ p₃ ≠ ∠ p₃ p₂ p₂ ∨ ∠ p₂ p₃ p₂ ≠ ∠ p₃ p₂ p₂
h₂₃ : ¬p₂ = p₃
⊢ ∠ p₂ p₂ p₃ < π / 3

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
p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂
h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂
hne : ∠ p₂ p₂ p₃ ≠ ∠ p₂ p₃ p₂ ∨ ∠ p₂ p₂ p₃ ≠ ∠ p₃ p₂ p₂ ∨ ∠ p₂ p₃ p₂ ≠ ∠ p₃ p₂ p₂
h₂₃ : ¬p₂ = p₃
⊢ ∠ p₂ p₂ p₃ < π / 3
Module: Mathlib.Geometry.Euclidean.Triangle

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
⊢ ∠ p₁ p₂ p₃ < π / 3

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
⊢ ∠ p₁ p₂ p₃ < π / 3
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : x = 0
⊢ angle x z ≤ angle x y + angle y z

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ¬x = 0
⊢ angle x z ≤ angle x y + angle y z

Tactic:
·

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : x = 0
⊢ angle x z ≤ angle x y + angle y z
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ¬x = 0
hy : y = 0
⊢ angle x z ≤ angle x y + angle y z

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ¬x = 0
hy : ¬y = 0
⊢ angle x z ≤ angle x y + angle y z

Tactic:
·

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ¬x = 0
hy : y = 0
⊢ angle x z ≤ angle x y + angle y z
Module: Mathlib.Topology.MetricSpace.Congruence

Goal state before:
pp: case pos
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
h : Pairwise fun i₁ i₂ ↦ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
i₁ i₂ : ι
hi : i₁ = i₂
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

pp: case neg
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
h : Pairwise fun i₁ i₂ ↦ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
i₁ i₂ : ι
hi : ¬i₁ = i₂
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

Tactic:
·

Goal state after:
case pos
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
h : Pairwise fun i₁ i₂ ↦ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
i₁ i₂ : ι
hi : i₁ = i₂
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
Module: Mathlib.Topology.MetricSpace.Congruence

Goal state before:
pp: case neg
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
h : Pairwise fun i₁ i₂ ↦ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
i₁ i₂ : ι
hi : ¬i₁ = i₂
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

Tactic:
·

Goal state after:
case neg
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
h : Pairwise fun i₁ i₂ ↦ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
i₁ i₂ : ι
hi : ¬i₁ = i₂
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ¬x = 0
hy : ¬y = 0
hz : z = 0
⊢ angle x z ≤ angle x y + angle y z

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ¬x = 0
hy : ¬y = 0
hz : ¬z = 0
⊢ angle x z ≤ angle x y + angle y z

Tactic:
·

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ¬x = 0
hy : ¬y = 0
hz : z = 0
⊢ angle x z ≤ angle x y + angle y z
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

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

pp: case inl.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kz : ℝ≥0
hy : 0 • x + kz • z ≠ 0
hkz : 0 < kz
⊢ angle x z = angle x (0 • x + kz • z) + angle (0 • x + kz • z) z

pp: case inr.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx : ℝ≥0
hkx : 0 < kx
hy : kx • x + 0 • z ≠ 0
⊢ angle x z = angle x (kx • x + 0 • z) + angle (kx • x + 0 • z) z

pp: case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
⊢ angle x z = angle x (kx • x + kz • z) + angle (kx • x + kz • z) z

Tactic:
·

Goal state after:
case inl.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
hy : 0 • x + 0 • z ≠ 0
⊢ angle x z = angle x (0 • x + 0 • z) + angle (0 • x + 0 • z) z
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case inl.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kz : ℝ≥0
hy : 0 • x + kz • z ≠ 0
hkz : 0 < kz
⊢ angle x z = angle x (0 • x + kz • z) + angle (0 • x + kz • z) z

pp: case inr.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx : ℝ≥0
hkx : 0 < kx
hy : kx • x + 0 • z ≠ 0
⊢ angle x z = angle x (kx • x + 0 • z) + angle (kx • x + 0 • z) z

pp: case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
⊢ angle x z = angle x (kx • x + kz • z) + angle (kx • x + kz • z) z

Tactic:
·

Goal state after:
case inl.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kz : ℝ≥0
hy : 0 • x + kz • z ≠ 0
hkz : 0 < kz
⊢ angle x z = angle x (0 • x + kz • z) + angle (0 • x + kz • z) z
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case inr.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx : ℝ≥0
hkx : 0 < kx
hy : kx • x + 0 • z ≠ 0
⊢ angle x z = angle x (kx • x + 0 • z) + angle (kx • x + 0 • z) z

pp: case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
⊢ angle x z = angle x (kx • x + kz • z) + angle (kx • x + kz • z) z

Tactic:
·

Goal state after:
case inr.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx : ℝ≥0
hkx : 0 < kx
hy : kx • x + 0 • z ≠ 0
⊢ angle x z = angle x (kx • x + 0 • z) + angle (kx • x + 0 • z) z
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
⊢ angle x z = angle x (kx • x + kz • z) + angle (kx • x + kz • z) z

Tactic:
·

Goal state after:
case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
⊢ angle x z = angle x (kx • x + kz • z) + angle (kx • x + kz • z) z