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)
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 ≠ π
⊢ o.oangle w x = o.oangle y z
have h0wx : w = 0 ∨ x = 0
Tactic: have h0wx : w = 0 ∨ x = 0 := by
      have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hswx
      simpa [hwx, Real.pi_pos.ne.symm, hpi] using 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
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
⊢ y = 0 ∨ z = 0
have h0' : y = 0 ∨ z = 0 ∨ InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π
Tactic: have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero 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
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 ≠ π
h0wx : w = 0 ∨ x = 0
⊢ o.oangle w x = o.oangle y z
have h0yz : y = 0 ∨ z = 0
Tactic: have h0yz : y = 0 ∨ z = 0 := by
      have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hsyz
      simpa [hyz, Real.pi_pos.ne.symm, hpi] using 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
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
h0yz : y = 0 ∨ z = 0
⊢ o.oangle w x = o.oangle y z
have pos : ∀ (h0wx : w = 0), o.oangle w x = o.oangle y z
Tactic: rcases h0wx with (h0wx | h0wx)
Cleared hypotheses: h0wx
-- 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 ≠ π
h0wx : w = 0 ∨ x = 0
h0yz : y = 0 ∨ z = 0
pos : ∀ (h0wx : w = 0), o.oangle w x = o.oangle y z
⊢ o.oangle w x = o.oangle y z
have pos₁ : ∀ (h0wx : x = 0), o.oangle w x = o.oangle y z
Tactic: rcases h0wx with (h0wx | h0wx)
Cleared hypotheses: h0wx
-- 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 ≠ π
h0yz : y = 0 ∨ z = 0
h0wx : w = 0
⊢ o.oangle w x = o.oangle y z
have pos : ∀ (h0yz : y = 0), o.oangle w x = o.oangle y z
Tactic: rcases h0yz with (h0yz | h0yz)
Cleared hypotheses: h0yz
-- 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 ≠ π
h0yz : y = 0 ∨ z = 0
h0wx : w = 0
pos : ∀ (h0yz : y = 0), o.oangle w x = o.oangle y z
⊢ o.oangle w x = o.oangle y z
have pos₁ : ∀ (h0yz : z = 0), o.oangle w x = o.oangle y z
Tactic: rcases h0yz with (h0yz | h0yz)
Cleared hypotheses: h0yz
-- 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 ≠ π
h0yz : y = 0 ∨ z = 0
h0wx : x = 0
⊢ o.oangle w x = o.oangle y z
have pos : ∀ (h0yz : y = 0), o.oangle w x = o.oangle y z
Tactic: rcases h0yz with (h0yz | h0yz)
Cleared hypotheses: h0yz
-- 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 ≠ π
h0yz : y = 0 ∨ z = 0
h0wx : x = 0
pos : ∀ (h0yz : y = 0), o.oangle w x = o.oangle y z
⊢ o.oangle w x = o.oangle y z
have pos₁ : ∀ (h0yz : z = 0), o.oangle w x = o.oangle y z
Tactic: rcases h0yz with (h0yz | h0yz)
Cleared hypotheses: h0yz
-- 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 = o.oangle y z
have neg : |(o.oangle w x).toReal| = |(o.oangle y z).toReal|
Tactic: rw [Real.Angle.eq_iff_abs_toReal_eq_of_sign_eq 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
⊢ |(o.oangle w x).toReal| = |(o.oangle y z).toReal|
have neg : ∀ (h : |(o.oangle w x).toReal| = 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).toReal| = |(o.oangle y z).toReal|
Tactic: rwa [o.angle_eq_abs_oangle_toReal h0.1.1 h0.1.2,
      o.angle_eq_abs_oangle_toReal h0.2.1 h0.2.2] at h
Cleared hypotheses: 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
neg :
  ∀ (h : |(o.oangle w x).toReal| = 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).toReal| = |(o.oangle y z).toReal|
⊢ |(o.oangle w x).toReal| = |(o.oangle y z).toReal|
have neg₁ : ∀ (h : |(o.oangle w x).toReal| = |(o.oangle y z).toReal|) (hs : (o.oangle w x).sign = (o.oangle y z).sign)
  (h0 : (w ≠ 0 ∧ x ≠ 0) ∧ y ≠ 0 ∧ z ≠ 0), |(o.oangle w x).toReal| = |(o.oangle y z).toReal|
Tactic: rwa [o.angle_eq_abs_oangle_toReal h0.1.1 h0.1.2,
      o.angle_eq_abs_oangle_toReal h0.2.1 h0.2.2] at h
Cleared hypotheses: 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
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = (o.oangle y z).sign
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle y z
have refine : ∀ (h : o.oangle w x = o.oangle y z), InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
Tactic: refine ⟨fun h => o.oangle_eq_of_angle_eq_of_sign_eq h hs, fun 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
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = (o.oangle y z).sign
h : o.oangle w x = o.oangle y z
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
have rw : |(o.oangle w x).toReal| = InnerProductGeometry.angle y z
Tactic: rw [o.angle_eq_abs_oangle_toReal hw hx, o.angle_eq_abs_oangle_toReal hy hz, 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
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = (o.oangle y z).sign
h : o.oangle w x = o.oangle y z
rw : |(o.oangle w x).toReal| = InnerProductGeometry.angle y z
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
have rw₁ : |(o.oangle w x).toReal| = |(o.oangle y z).toReal|
Tactic: rw [o.angle_eq_abs_oangle_toReal hw hx, o.angle_eq_abs_oangle_toReal hy hz, 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
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = (o.oangle y z).sign
h : o.oangle w x = o.oangle y z
rw : |(o.oangle w x).toReal| = InnerProductGeometry.angle y z
rw₁ : |(o.oangle w x).toReal| = |(o.oangle y z).toReal|
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
have rw₂ : |(o.oangle y z).toReal| = |(o.oangle y z).toReal|
Tactic: rw [o.angle_eq_abs_oangle_toReal hw hx, o.angle_eq_abs_oangle_toReal hy hz, 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 rw : o.oangle w x = o.oangle z y
Tactic: rw [← oangle_rev]
-- 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
⊢ o.oangle w x = o.oangle z y
have hs₁ : (o.oangle w x).sign = (o.oangle z y).sign
Tactic: rw [← Real.Angle.sign_neg, ← oangle_rev] at hs
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 z y).sign
⊢ o.oangle w x = o.oangle z y
have h₁ : InnerProductGeometry.angle w x = InnerProductGeometry.angle z y
Tactic: nth_rw 2 [InnerProductGeometry.angle_comm] at h
Cleared hypotheses: h, 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
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = -(o.oangle y z).sign
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = -o.oangle y z
have rw : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle z y
Tactic: rw [← oangle_rev]
-- 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
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = -(o.oangle y z).sign
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle z y
have hs₁ : (o.oangle w x).sign = (o.oangle z y).sign
Tactic: rw [← Real.Angle.sign_neg, ← oangle_rev] at hs
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
hw : w ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
hs : (o.oangle w x).sign = (o.oangle z y).sign
⊢ InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle z y
have nth_rw : InnerProductGeometry.angle w x = InnerProductGeometry.angle z y ↔ o.oangle w x = o.oangle z y
Tactic: nth_rw 2 [InnerProductGeometry.angle_comm]
-- 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 = 1
⊢ o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
have pos : ∀ (hx : x = 0), o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
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 = 1
pos : ∀ (hx : x = 0), o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
have neg : ∀ (hx : ¬x = 0), o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
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 = 1
hx : ¬x = 0
⊢ o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
have pos : ∀ (hy : y = 0), o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
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 = 1
hx : ¬x = 0
pos : ∀ (hy : y = 0), o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
have neg : ∀ (hy : ¬y = 0), o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
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 = 1
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
have neg : ¬o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
Tactic: refine (o.oangle_eq_angle_or_eq_neg_angle hx hy).resolve_right ?_
-- 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 = 1
hx : ¬x = 0
hy : ¬y = 0
hxy : o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ False
have h₁ : ¬0 ≤ (↑(InnerProductGeometry.angle x y) : Real.Angle).sign
Tactic: rw [hxy, Real.Angle.sign_neg, neg_eq_iff_eq_neg, ← SignType.neg_iff, ← not_le] at h
Cleared hypotheses: h, hx, hy, hxy
-- 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 = -1
⊢ o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
have pos : ∀ (hx : x = 0), o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
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 = -1
pos : ∀ (hx : x = 0), o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
have neg : ∀ (hx : ¬x = 0), o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
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 = -1
hx : ¬x = 0
⊢ o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
have pos : ∀ (hy : y = 0), o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
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 = -1
hx : ¬x = 0
pos : ∀ (hy : y = 0), o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
have neg : ∀ (hy : ¬y = 0), o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
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 = -1
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
have neg : ¬o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
Tactic: refine (o.oangle_eq_angle_or_eq_neg_angle hx hy).resolve_left ?_
-- 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 = -1
hx : ¬x = 0
hy : ¬y = 0
hxy : o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ False
have h₁ : ¬0 ≤ (↑(InnerProductGeometry.angle x y) : Real.Angle).sign
Tactic: rw [hxy, ← SignType.neg_iff, ← not_le] at h
Cleared hypotheses: h, hx, hy, hxy
-- 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
⊢ o.oangle x y = 0 ↔ InnerProductGeometry.angle x y = 0
have refine_1 : ∀ (h : o.oangle x y = 0), InnerProductGeometry.angle x y = 0
Tactic: refine ⟨fun h => ?_, fun 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
refine_1 : ∀ (h : o.oangle x y = 0), InnerProductGeometry.angle x y = 0
⊢ o.oangle x y = 0 ↔ InnerProductGeometry.angle x y = 0
have refine_2 : ∀ (h : InnerProductGeometry.angle x y = 0), o.oangle x y = 0
Tactic: refine ⟨fun h => ?_, fun 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)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h : InnerProductGeometry.angle x y = 0
⊢ o.oangle x y = 0
have ha : o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle) ∨
  o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
Tactic: have ha := o.oangle_eq_angle_or_eq_neg_angle 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
hx : x ≠ 0
hy : y ≠ 0
h : InnerProductGeometry.angle x y = 0
ha :
  o.oangle x y = (↑(InnerProductGeometry.angle x y) : Real.Angle) ∨
    o.oangle x y = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ o.oangle x y = 0
have ha₁ : o.oangle x y = (↑0 : Real.Angle) ∨ o.oangle x y = -(↑0 : Real.Angle)
Tactic: rw [h] at ha
Cleared hypotheses: ha
-- 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
⊢ o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π
have pos : ∀ (hx : x = 0), o.oangle x y = (↑π : Real.Angle) ↔ 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
pos : ∀ (hx : x = 0), o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π
⊢ o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π
have neg : ∀ (hx : ¬x = 0), o.oangle x y = (↑π : Real.Angle) ↔ 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
hx : ¬x = 0
⊢ o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π
have pos : ∀ (hy : y = 0), o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π
Tactic: by_cases hy : y = 0