-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_eq_of_angle_eq_of_sign_eq {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) : o.oangle w x = o.oangle y z

Proof state:
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
⊢ InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y z = π / 2

Tactic:
rcases h0 with ((rfl | rfl) | rfl | rfl)

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

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

Proof state:
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 = o.oangle y z

Tactic:
push_neg at h0

Result:
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 = o.oangle y z

Proof state:
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
hpi : π / 2 ≠ π
h0' : w = 0 ∨ x = 0 ∨ InnerProductGeometry.angle w x = 0 ∨ InnerProductGeometry.angle w x = π
⊢ w = 0 ∨ x = 0

Tactic:
simpa [hwx, Real.pi_pos.ne.symm, hpi] using h0'

Result:
no goals

Proof state:
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
h : InnerProductGeometry.angle w 0 = InnerProductGeometry.angle y z
hs : (o.oangle w 0).sign = (o.oangle y z).sign
⊢ (o.oangle w 0).sign = 0 ∧ (o.oangle y z).sign = 0

Tactic:
simpa using hs.symm

Result:
no goals

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

Result:
no goals

Proof state:
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).sign = 0 ∧ (o.oangle y z).sign = 0

Tactic:
rcases h0 with ((rfl | rfl) | rfl | rfl)

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

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

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

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

Proof state:
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
hpi : π / 2 ≠ π
h0wx : w = 0 ∨ x = 0
h0' : y = 0 ∨ z = 0 ∨ InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π
⊢ y = 0 ∨ z = 0

Tactic:
simpa [hyz, Real.pi_pos.ne.symm, hpi] using h0'

Result:
no goals