-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem _root_.Wbtw.oangle₂₁₃_eq_zero {p₁ p₂ p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) : ∡ p₂ p₁ p₃ = 0

Proof state:
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

Tactic:
simp [hp₂p₁]

Result:
no goals

Proof state:
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₁

Result:
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

Proof state:
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

Tactic:
by_cases hp₃p₁ : p₃ = p₁

Result:
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₁
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₁
hp₃p₁ : ¬p₃ = p₁
⊢ ∡ p₂ p₁ p₃ = 0

Proof state:
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₁
hp₃p₁ : p₃ = p₁
⊢ ∡ p₂ p₁ p₃ = 0

Tactic:
simp [hp₃p₁]

Result:
no goals

Proof state:
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₁
hp₃p₁ : ¬p₃ = p₁
⊢ ∠ p₂ p₁ p₃ = 0

Tactic:
exact h.angle₂₁₃_eq_zero_of_ne hp₂p₁

Result:
no goals

Proof state:
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₁
hp₃p₁ : ¬p₃ = p₁
⊢ ∡ p₂ p₁ p₃ = 0

Tactic:
rw [oangle_eq_zero_iff_angle_eq_zero hp₂p₁ hp₃p₁]

Result:
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₁
hp₃p₁ : ¬p₃ = p₁
⊢ ∠ p₂ p₁ p₃ = 0