awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
pos : ∀ (hy : y = 0), o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π
⊢ o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π
have neg : ∀ (hy : ¬y = 0), o.oangle x y = (↑π : Real.Angle) ↔ 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
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π
have neg : ∀ (h : o.oangle x y = (↑π : Real.Angle)), InnerProductGeometry.angle x y = π
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
neg : ∀ (h : o.oangle x y = (↑π : Real.Angle)), InnerProductGeometry.angle x y = π
⊢ o.oangle x y = (↑π : Real.Angle) ↔ InnerProductGeometry.angle x y = π
have neg₁ : ∀ (h : InnerProductGeometry.angle x y = π), o.oangle x y = (↑π : Real.Angle)
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
h : o.oangle x y = (↑π : Real.Angle)
⊢ InnerProductGeometry.angle x y = π
have neg : |(↑π : Real.Angle).toReal| = π
Tactic: rw [o.angle_eq_abs_oangle_toReal hx hy, 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 = π
⊢ o.oangle x y = (↑π : Real.Angle)
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 = π
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 = (↑π : Real.Angle)
have ha₁ : o.oangle x y = (↑π : Real.Angle) ∨ o.oangle x y = -(↑π : 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
⊢ x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0
have pos : ∀ (hx : x = 0),
  x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0
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),
    x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0
⊢ x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0
have neg : ∀ (hx : ¬x = 0),
  x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0
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
⊢ x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0
have pos : ∀ (hy : y = 0),
  x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0
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
hx : ¬x = 0
pos :
  ∀ (hy : y = 0),
    x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0
⊢ x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0
have neg : ∀ (hy : ¬y = 0),
  x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0
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
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔ ⟪x, y⟫ = 0
have neg : o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔
  InnerProductGeometry.angle x y = π / 2
Tactic: rw [InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, or_iff_right hx, or_iff_right 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
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔
    InnerProductGeometry.angle x y = π / 2
have neg : ∀ (h : o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle)),
  InnerProductGeometry.angle x y = π / 2
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
neg :
  ∀ (h : o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle)),
    InnerProductGeometry.angle x y = π / 2
⊢ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle) ↔
    InnerProductGeometry.angle x y = π / 2
have neg₁ : ∀ (h : InnerProductGeometry.angle x y = π / 2),
  o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle)
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
h : o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle)
⊢ InnerProductGeometry.angle x y = π / 2
have neg : |(o.oangle x y).toReal| = π / 2
Tactic: rwa [o.angle_eq_abs_oangle_toReal hx hy, Real.Angle.abs_toReal_eq_pi_div_two_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
h : InnerProductGeometry.angle x y = π / 2
⊢ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle)
have h₁ : (↑(π / 2) : Real.Angle) = (↑(InnerProductGeometry.angle x y) : Real.Angle)
Tactic: convert! o.oangle_eq_angle_or_eq_neg_angle hx hy using 2
-- 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
h : InnerProductGeometry.angle x y = π / 2
h₁ : (↑(π / 2) : Real.Angle) = (↑(InnerProductGeometry.angle x y) : Real.Angle)
⊢ o.oangle x y = (↑(π / 2) : Real.Angle) ∨ o.oangle x y = (↑(-π / 2) : Real.Angle)
have h₂ : (↑(-π / 2) : Real.Angle) = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
Tactic: convert! o.oangle_eq_angle_or_eq_neg_angle hx hy using 2
-- 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
h : InnerProductGeometry.angle x y = π / 2
⊢ (↑(π / 2) : Real.Angle) = (↑(InnerProductGeometry.angle x y) : Real.Angle)
have h₁ : (↑(π / 2) : Real.Angle) = (↑(π / 2) : Real.Angle)
Tactic: rw [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
h : InnerProductGeometry.angle x y = π / 2
⊢ (↑(-π / 2) : Real.Angle) = -(↑(InnerProductGeometry.angle x y) : Real.Angle)
have h₁ : (↑(-π / 2) : Real.Angle) = -(↑(π / 2) : Real.Angle)
Tactic: rw [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 = (↑(π / 2) : Real.Angle)
⊢ ⟪y, x⟫ = 0
have rw : ⟪x, y⟫ = 0
Tactic: rw [real_inner_comm, o.inner_eq_zero_of_oangle_eq_pi_div_two 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 = (↑(π / 2) : Real.Angle)
rw : ⟪x, y⟫ = 0
⊢ ⟪y, x⟫ = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [real_inner_comm, o.inner_eq_zero_of_oangle_eq_pi_div_two 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 = (↑(-π / 2) : Real.Angle)
⊢ ⟪y, x⟫ = 0
have rw : ⟪x, y⟫ = 0
Tactic: rw [real_inner_comm, o.inner_eq_zero_of_oangle_eq_neg_pi_div_two 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 = (↑(-π / 2) : Real.Angle)
rw : ⟪x, y⟫ = 0
⊢ ⟪y, x⟫ = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [real_inner_comm, o.inner_eq_zero_of_oangle_eq_neg_pi_div_two 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
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign
have pos : ∀ (hx : x = 0), (o.oangle (-x) y).sign = -(o.oangle x y).sign
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).sign = -(o.oangle x y).sign
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign
have neg : ∀ (hx : ¬x = 0), (o.oangle (-x) y).sign = -(o.oangle x y).sign
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).sign = -(o.oangle x y).sign
have pos : ∀ (hy : y = 0), (o.oangle (-x) y).sign = -(o.oangle x y).sign
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
hx : ¬x = 0
pos : ∀ (hy : y = 0), (o.oangle (-x) y).sign = -(o.oangle x y).sign
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign
have neg : ∀ (hy : ¬y = 0), (o.oangle (-x) y).sign = -(o.oangle x y).sign
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
hx : ¬x = 0
hy : ¬y = 0
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign
have neg : (o.oangle x y + (↑π : Real.Angle)).sign = -(o.oangle x y).sign
Tactic: rw [o.oangle_neg_left hx hy, Real.Angle.sign_add_pi]
-- 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
neg : (o.oangle x y + (↑π : Real.Angle)).sign = -(o.oangle x y).sign
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign
have neg₁ : -(o.oangle x y).sign = -(o.oangle x y).sign
Tactic: rw [o.oangle_neg_left hx hy, Real.Angle.sign_add_pi]
-- 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)).sign = -(o.oangle x y).sign
have pos : ∀ (hx : x = 0), (o.oangle x (-y)).sign = -(o.oangle x y).sign
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)).sign = -(o.oangle x y).sign
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign
have neg : ∀ (hx : ¬x = 0), (o.oangle x (-y)).sign = -(o.oangle x y).sign
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)).sign = -(o.oangle x y).sign
have pos : ∀ (hy : y = 0), (o.oangle x (-y)).sign = -(o.oangle x y).sign
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
hx : ¬x = 0
pos : ∀ (hy : y = 0), (o.oangle x (-y)).sign = -(o.oangle x y).sign
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign
have neg : ∀ (hy : ¬y = 0), (o.oangle x (-y)).sign = -(o.oangle x y).sign
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
hx : ¬x = 0
hy : ¬y = 0
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign
have neg : (o.oangle x y + (↑π : Real.Angle)).sign = -(o.oangle x y).sign
Tactic: rw [o.oangle_neg_right hx hy, Real.Angle.sign_add_pi]
-- 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
neg : (o.oangle x y + (↑π : Real.Angle)).sign = -(o.oangle x y).sign
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign
have neg₁ : -(o.oangle x y).sign = -(o.oangle x y).sign
Tactic: rw [o.oangle_neg_right hx hy, Real.Angle.sign_add_pi]
-- 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
r : ℝ
⊢ (o.oangle (r • x) y).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
have inl : ∀ (h : r < 0),
  (o.oangle (r • x) y).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
Tactic: rcases lt_trichotomy r 0 with (h | 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
r : ℝ
inl :
  ∀ (h : r < 0),
    (o.oangle (r • x) y).sign =
      HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
⊢ (o.oangle (r • x) y).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
have inr : ∀ (h : r = 0),
  (o.oangle (r • x) y).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
Tactic: rcases lt_trichotomy r 0 with (h | 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
r : ℝ
inl :
  ∀ (h : r < 0),
    (o.oangle (r • x) y).sign =
      HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
inr :
  ∀ (h : r = 0),
    (o.oangle (r • x) y).sign =
      HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
⊢ (o.oangle (r • x) y).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
have inr₁ : ∀ (h : 0 < r),
  (o.oangle (r • x) y).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
Tactic: rcases lt_trichotomy r 0 with (h | 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
r : ℝ
⊢ (o.oangle x (r • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
have inl : ∀ (h : r < 0),
  (o.oangle x (r • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
Tactic: rcases lt_trichotomy r 0 with (h | 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
r : ℝ
inl :
  ∀ (h : r < 0),
    (o.oangle x (r • y)).sign =
      HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
⊢ (o.oangle x (r • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
have inr : ∀ (h : r = 0),
  (o.oangle x (r • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
Tactic: rcases lt_trichotomy r 0 with (h | 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
r : ℝ
inl :
  ∀ (h : r < 0),
    (o.oangle x (r • y)).sign =
      HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
inr :
  ∀ (h : r = 0),
    (o.oangle x (r • y)).sign =
      HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
⊢ (o.oangle x (r • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
have inr₁ : ∀ (h : 0 < r),
  (o.oangle x (r • y)).sign =
    HMul.hMul (α := SignType) ((SignType.sign : (a : ℝ) → SignType) r : SignType) (o.oangle x y).sign
Tactic: rcases lt_trichotomy r 0 with (h | 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
r : ℝ
⊢ o.oangle x (r • x + y) = 0 ∨ o.oangle x (r • x + y) = (↑π : Real.Angle) ↔
    o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle)
have simp_rw : (∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)) ↔
  ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
Tactic: simp_rw [oangle_eq_zero_or_eq_pi_iff_not_linearIndependent, Fintype.not_linearIndependent_iff,
    Fin.sum_univ_two, Fin.exists_fin_two]
-- 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
r : ℝ
⊢ (∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)) ↔
    ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
have refine_1 : ∀ (h : ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)),
  ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 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
r : ℝ
refine_1 :
  ∀
    (h :
      ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)),
    ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
⊢ (∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)) ↔
    ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
have refine_2 : ∀ (h : ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)),
  ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 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
r : ℝ
h : ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, r • x + y] 0 + g 1 • ![x, r • x + y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
⊢ ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
have refine_1 : ∀ (m : Fin (Nat.succ 0).succ → ℝ) (h : m 0 • ![x, r • x + y] 0 + m 1 • ![x, r • x + y] 1 = 0) (hm : m 0 ≠ 0 ∨ m 1 ≠ 0),
  ∃ (g : Fin (Nat.succ 0).succ → ℝ), g 0 • ![x, y] 0 + g 1 • ![x, y] 1 = 0 ∧ (g 0 ≠ 0 ∨ g 1 ≠ 0)
Tactic: rcases h with ⟨m, h, hm⟩
Cleared hypotheses: h