awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h0 : 0 ≤ InnerProductGeometry.angle x y
⊢ InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
have hpi : InnerProductGeometry.angle x y ≤ π
Tactic: have hpi := InnerProductGeometry.angle_le_pi x y
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h0 : 0 ≤ InnerProductGeometry.angle x y
hpi : InnerProductGeometry.angle x y ≤ π
⊢ InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
have inl : ∀ (h : o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)),
  InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
Tactic: rcases o.oangle_eq_angle_or_eq_neg_angle hx hy with (h | h)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h0 : 0 ≤ InnerProductGeometry.angle x y
hpi : InnerProductGeometry.angle x y ≤ π
inl :
  ∀ (h : o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)),
    InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
⊢ InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
have inr : ∀ (h : o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)),
  InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
Tactic: rcases o.oangle_eq_angle_or_eq_neg_angle hx hy with (h | h)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h0 : 0 ≤ InnerProductGeometry.angle x y
hpi : InnerProductGeometry.angle x y ≤ π
h : o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
have inl : 0 ≤ InnerProductGeometry.angle x y ∧ InnerProductGeometry.angle x y ≤ π
Tactic: rw [h, eq_comm, Real.Angle.abs_toReal_coe_eq_self_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h0 : 0 ≤ InnerProductGeometry.angle x y
hpi : InnerProductGeometry.angle x y ≤ π
h : o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
have inr : 0 ≤ InnerProductGeometry.angle x y ∧ InnerProductGeometry.angle x y ≤ π
Tactic: rw [h, eq_comm, Real.Angle.abs_toReal_neg_coe_eq_self_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign = 0
⊢ x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π
have pos : ∀ (hx : x = 0), x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign = 0
pos : ∀ (hx : x = 0), x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π
⊢ x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π
have neg : ∀ (hx : ¬x = 0), x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign = 0
hx : ¬x = 0
⊢ x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π
have pos : ∀ (hy : y = 0), x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign = 0
hx : ¬x = 0
pos : ∀ (hy : y = 0), x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π
⊢ x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π
have neg : ∀ (hy : ¬y = 0), x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π
have neg : x = 0 ∨ y = 0 ∨ |(o.oangle x y).toReal| = 0 ∨ |(o.oangle x y).toReal| = π
Tactic: rw [o.angle_eq_abs_oangle_toReal hx hy]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ |(o.oangle x y).toReal| = 0 ∨ |(o.oangle x y).toReal| = π
have h₁ : o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle)
Tactic: rw [Real.Angle.sign_eq_zero_iff] at h
Cleared hypotheses: h, hx, hy
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle)
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ |(o.oangle x y).toReal| = 0 ∨ |(o.oangle x y).toReal| = π
have neg : ∀ (h : o.oangle x y = 0), x = 0 ∨ y = 0 ∨ |(o.oangle x y).toReal| = 0 ∨ |(o.oangle x y).toReal| = π
Tactic: rcases h with (h | h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle)
hx : ¬x = 0
hy : ¬y = 0
neg : ∀ (h : o.oangle x y = 0), x = 0 ∨ y = 0 ∨ |(o.oangle x y).toReal| = 0 ∨ |(o.oangle x y).toReal| = π
⊢ x = 0 ∨ y = 0 ∨ |(o.oangle x y).toReal| = 0 ∨ |(o.oangle x y).toReal| = π
have neg₁ : ∀ (h : o.oangle x y = (↑π : Real.Angle)), x = 0 ∨ y = 0 ∨ |(o.oangle x y).toReal| = 0 ∨ |(o.oangle x y).toReal| = π
Tactic: rcases h with (h | h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
⊢ o.oangle w x = o.oangle y z
have pos : ∀ (h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0), o.oangle w x = o.oangle y z
Tactic: by_cases! h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
pos : ∀ (h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0), o.oangle w x = o.oangle y z
⊢ o.oangle w x = o.oangle y z
have neg : ∀ (h0 : (w ≠ 0 ∧ x ≠ 0) ∧ y ≠ 0 ∧ z ≠ 0), o.oangle w x = o.oangle y z
Tactic: by_cases! h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
have inl : ∀ (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
Tactic: rcases h0 with ((rfl | rfl) | rfl | rfl)
Cleared hypotheses: w, h, hs, h0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
inl :
  ∀ (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
⊢ (o.oangle w x).sign = 0 ∧ (o.oangle y z).sign = 0
have inl₁ : ∀ (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: rcases h0 with ((rfl | rfl) | rfl | rfl)
Cleared hypotheses: x, h, hs, h0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
inl :
  ∀ (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
inl₁ :
  ∀ (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
⊢ (o.oangle w x).sign = 0 ∧ (o.oangle y z).sign = 0
have inr : ∀ (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
Tactic: rcases h0 with ((rfl | rfl) | rfl | rfl)
Cleared hypotheses: y, h, hs, h0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
inl :
  ∀ (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
inl₁ :
  ∀ (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
inr :
  ∀ (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
⊢ (o.oangle w x).sign = 0 ∧ (o.oangle y z).sign = 0
have inr₁ : ∀ (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
Tactic: rcases h0 with ((rfl | rfl) | rfl | rfl)
Cleared hypotheses: z, h, hs, h0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
have hs' : (o.oangle w x).sign = 0 ∧ (o.oangle y z).sign = 0
Tactic: have hs' : (o.oangle w x).sign = 0 ∧ (o.oangle y z).sign = 0 := by
      rcases h0 with ((rfl | rfl) | rfl | rfl)
      · simpa using hs.symm
      · simpa using hs.symm
      · simpa using hs
      · simpa using hs
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
hs' : (o.oangle w x).sign = 0 ∧ (o.oangle y z).sign = 0
⊢ o.oangle w x = o.oangle y z
have hswx : (o.oangle w x).sign = 0
Tactic: rcases hs' with ⟨hswx, hsyz⟩
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
hs' : (o.oangle w x).sign = 0 ∧ (o.oangle y z).sign = 0
hswx : (o.oangle w x).sign = 0
⊢ o.oangle w x = o.oangle y z
have hsyz : (o.oangle y z).sign = 0
Tactic: rcases hs' with ⟨hswx, hsyz⟩
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
have inl : ∀ (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
Tactic: rcases h0 with ((rfl | rfl) | rfl | rfl)
Cleared hypotheses: w, h, hs, h0, hswx
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
inl :
  ∀ (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
⊢ InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y z = π / 2
have inl₁ : ∀ (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
Tactic: rcases h0 with ((rfl | rfl) | rfl | rfl)
Cleared hypotheses: x, h, hs, h0, hswx
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
inl :
  ∀ (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
inl₁ :
  ∀ (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
⊢ InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y z = π / 2
have inr : ∀ (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
Tactic: rcases h0 with ((rfl | rfl) | rfl | rfl)
Cleared hypotheses: y, h, hs, h0, hsyz
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
inl :
  ∀ (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
inl₁ :
  ∀ (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
inr :
  ∀ (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
⊢ InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y z = π / 2
have inr₁ : ∀ (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: rcases h0 with ((rfl | rfl) | rfl | rfl)
Cleared hypotheses: z, h, hs, h0, hsyz
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
⊢ o.oangle w x = o.oangle y z
have h' : InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y z = π / 2
Tactic: have h' : InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y z = π / 2 := by
      rcases h0 with ((rfl | rfl) | rfl | rfl)
      · simpa using h.symm
      · simpa using h.symm
      · simpa using h
      · simpa using h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
have hwx : InnerProductGeometry.angle w x = π / 2
Tactic: rcases h' with ⟨hwx, hyz⟩
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
hwx : InnerProductGeometry.angle w x = π / 2
⊢ o.oangle w x = o.oangle y z
have hyz : InnerProductGeometry.angle y z = π / 2
Tactic: rcases h' with ⟨hwx, hyz⟩
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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 = π
⊢ False
have rw : ∀ (hpi : π = 0), False
Tactic: rw [div_eq_iff, eq_comm, ← sub_eq_zero, mul_two, add_sub_cancel_right] at hpi
Cleared hypotheses: hpi
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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 = π
rw : ∀ (hpi : π = 0), False
⊢ False
have rw₁ : Ne (α := ℝ) 2 0
Tactic: rw [div_eq_iff, eq_comm, ← sub_eq_zero, mul_two, add_sub_cancel_right] at hpi
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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
have hpi : π / 2 ≠ π
Tactic: have hpi : π / 2 ≠ π := by
      intro hpi
      rw [div_eq_iff, eq_comm, ← sub_eq_zero, mul_two, add_sub_cancel_right] at hpi
      · exact Real.pi_pos.ne.symm hpi
      · exact two_ne_zero
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : 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 ≠ π
⊢ w = 0 ∨ x = 0
have h0' : w = 0 ∨ x = 0 ∨ InnerProductGeometry.angle w x = 0 ∨ InnerProductGeometry.angle w x = π
Tactic: have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hswx