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
mp : o.oangle x y = (↑π : Real.Angle) → x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
⊢ o.oangle x y = (↑π : Real.Angle) ↔ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
have mpr : x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0 → o.oangle x y = (↑π : Real.Angle)
Tactic: constructor
-- 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 = (↑π : Real.Angle)
⊢ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
have pos : ∀ (hx : x = 0), x ≠ 0 ∧ y ≠ 0 ∧ o.oangle 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
h : o.oangle x y = (↑π : Real.Angle)
pos : ∀ (hx : x = 0), x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
⊢ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
have neg : ∀ (hx : ¬x = 0), x ≠ 0 ∧ y ≠ 0 ∧ o.oangle 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
h : o.oangle x y = (↑π : Real.Angle)
hx : ¬x = 0
⊢ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
have pos : ∀ (hy : y = 0), x ≠ 0 ∧ y ≠ 0 ∧ o.oangle 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
h : o.oangle x y = (↑π : Real.Angle)
hx : ¬x = 0
pos : ∀ (hy : y = 0), x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
⊢ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
have neg : ∀ (hy : ¬y = 0), x ≠ 0 ∧ y ≠ 0 ∧ o.oangle 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
h : o.oangle x y = (↑π : Real.Angle)
hx : ¬x = 0
hy : ¬y = 0
⊢ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
have neg : o.oangle x (-y) = 0
Tactic: refine ⟨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 = (↑π : Real.Angle)
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle x (-y) = 0
have neg : o.oangle x y + (↑π : Real.Angle) = 0
Tactic: rw [o.oangle_neg_right hx hy, h, Real.Angle.coe_pi_add_coe_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
h : o.oangle x y = (↑π : Real.Angle)
hx : ¬x = 0
hy : ¬y = 0
neg : o.oangle x y + (↑π : Real.Angle) = 0
⊢ o.oangle x (-y) = 0
have neg₁ : (↑π : Real.Angle) + (↑π : Real.Angle) = 0
Tactic: rw [o.oangle_neg_right hx hy, h, Real.Angle.coe_pi_add_coe_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
h : o.oangle x y = (↑π : Real.Angle)
hx : ¬x = 0
hy : ¬y = 0
neg : o.oangle x y + (↑π : Real.Angle) = 0
neg₁ : (↑π : Real.Angle) + (↑π : Real.Angle) = 0
⊢ o.oangle x (-y) = 0
have neg₂ : Eq (α := Real.Angle) 0 0
Tactic: rw [o.oangle_neg_right hx hy, h, Real.Angle.coe_pi_add_coe_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
h : o.oangle x (-y) = 0
⊢ o.oangle x y = (↑π : Real.Angle)
have mpr : ∀ (h : o.oangle x y + (↑π : Real.Angle) = 0), o.oangle x y = (↑π : Real.Angle)
Tactic: rwa [o.oangle_neg_right hx hy, ← Real.Angle.sub_coe_pi_eq_add_coe_pi, sub_eq_zero] at 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
hx : x ≠ 0
hy : y ≠ 0
h : o.oangle x (-y) = 0
mpr : ∀ (h : o.oangle x y + (↑π : Real.Angle) = 0), o.oangle x y = (↑π : Real.Angle)
⊢ o.oangle x y = (↑π : Real.Angle)
have mpr₁ : ∀ (h : o.oangle x y - (↑π : Real.Angle) = 0), o.oangle x y = (↑π : Real.Angle)
Tactic: rwa [o.oangle_neg_right hx hy, ← Real.Angle.sub_coe_pi_eq_add_coe_pi, sub_eq_zero] at 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
hx : x ≠ 0
hy : y ≠ 0
h : o.oangle x (-y) = 0
mpr : ∀ (h : o.oangle x y + (↑π : Real.Angle) = 0), o.oangle x y = (↑π : Real.Angle)
mpr₁ : ∀ (h : o.oangle x y - (↑π : Real.Angle) = 0), o.oangle x y = (↑π : Real.Angle)
⊢ o.oangle x y = (↑π : Real.Angle)
have mpr₂ : ∀ (h : o.oangle x y = (↑π : Real.Angle)), o.oangle x y = (↑π : Real.Angle)
Tactic: rwa [o.oangle_neg_right hx hy, ← Real.Angle.sub_coe_pi_eq_add_coe_pi, sub_eq_zero] at 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
⊢ o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle) ↔ ¬LinearIndependent ℝ ![x, y]
have rw : SameRay ℝ x y ∨ o.oangle x y = (↑π : Real.Angle) ↔ ¬LinearIndependent ℝ ![x, y]
Tactic: rw [oangle_eq_zero_iff_sameRay, oangle_eq_pi_iff_sameRay_neg,
    sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent]
-- 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
rw : SameRay ℝ x y ∨ o.oangle x y = (↑π : Real.Angle) ↔ ¬LinearIndependent ℝ ![x, y]
⊢ o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle) ↔ ¬LinearIndependent ℝ ![x, y]
have rw₁ : SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y) ↔ ¬LinearIndependent ℝ ![x, y]
Tactic: rw [oangle_eq_zero_iff_sameRay, oangle_eq_pi_iff_sameRay_neg,
    sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent]
-- 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
rw : SameRay ℝ x y ∨ o.oangle x y = (↑π : Real.Angle) ↔ ¬LinearIndependent ℝ ![x, y]
rw₁ : SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y) ↔ ¬LinearIndependent ℝ ![x, y]
⊢ o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle) ↔ ¬LinearIndependent ℝ ![x, y]
have rw₂ : ¬LinearIndependent ℝ ![x, y] ↔ ¬LinearIndependent ℝ ![x, y]
Tactic: rw [oangle_eq_zero_iff_sameRay, oangle_eq_pi_iff_sameRay_neg,
    sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent]
-- 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 = 0 ∨ o.oangle x y = (↑π : Real.Angle) ↔ x = 0 ∨ ∃ (r : ℝ), y = r • x
have rw : SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y) ↔ x = 0 ∨ ∃ (r : ℝ), y = r • x
Tactic: rw [oangle_eq_zero_iff_sameRay, oangle_eq_pi_iff_sameRay_neg]
-- 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
⊢ SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y) ↔ x = 0 ∨ ∃ (r : ℝ), y = r • x
have refine_1 : ∀ (h : SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)), x = 0 ∨ ∃ (r : ℝ), y = r • x
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
refine_1 : ∀ (h : SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)), x = 0 ∨ ∃ (r : ℝ), y = r • x
⊢ SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y) ↔ x = 0 ∨ ∃ (r : ℝ), y = r • x
have refine_2 : ∀ (h : x = 0 ∨ ∃ (r : ℝ), y = r • x), SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ 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
h : SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x
have refine_1 : ∀ (h : SameRay ℝ x y), x = 0 ∨ ∃ (r : ℝ), y = r • x
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 : SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)
refine_1 : ∀ (h : SameRay ℝ x y), x = 0 ∨ ∃ (r : ℝ), y = r • x
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x
have refine_1₁ : ∀ (h : SameRay ℝ x (-y)), x = 0 ∨ ∃ (r : ℝ), y = r • x
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 : SameRay ℝ x y
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x
have pos : ∀ (hx : x = 0), x = 0 ∨ ∃ (r : ℝ), y = r • x
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 : SameRay ℝ x y
pos : ∀ (hx : x = 0), x = 0 ∨ ∃ (r : ℝ), y = r • x
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x
have neg : ∀ (hx : ¬x = 0), x = 0 ∨ ∃ (r : ℝ), y = r • x
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 : SameRay ℝ x y
hx : ¬x = 0
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x
have neg : ∀ (r : ℝ) (h : SameRay ℝ x (r • x)), x = 0 ∨ ∃ (r_1 : ℝ), r • x = r_1 • x
Tactic: obtain ⟨r, -, rfl⟩ := h.exists_nonneg_left hx
Cleared hypotheses: y, 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 : SameRay ℝ x (-y)
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x
have pos : ∀ (hx : x = 0), x = 0 ∨ ∃ (r : ℝ), y = r • x
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 : SameRay ℝ x (-y)
pos : ∀ (hx : x = 0), x = 0 ∨ ∃ (r : ℝ), y = r • x
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x
have neg : ∀ (hx : ¬x = 0), x = 0 ∨ ∃ (r : ℝ), y = r • x
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 : SameRay ℝ x (-y)
hx : ¬x = 0
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x
have neg : ∀ (r : ℝ) (hy : r • x = -y), x = 0 ∨ ∃ (r : ℝ), y = r • x
Tactic: obtain ⟨r, -, hy⟩ := h.exists_nonneg_left hx
-- 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 : SameRay ℝ x (-y)
hx : ¬x = 0
r : ℝ
hy : r • x = -y
⊢ x = 0 ∨ ∃ (r : ℝ), y = r • x
have neg : y = -r • x
Tactic: refine Or.inr ⟨-r, ?_⟩
-- 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 : x = 0 ∨ ∃ (r : ℝ), y = r • x
⊢ SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)
have refine_2 : SameRay ℝ 0 y ∨ Ne.{u_1 + 1} (α := V) 0 0 ∧ y ≠ 0 ∧ SameRay ℝ 0 (-y)
Tactic: rcases h with (rfl | ⟨r, rfl⟩)
Cleared hypotheses: x, 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 : x = 0 ∨ ∃ (r : ℝ), y = r • x
refine_2 : SameRay ℝ 0 y ∨ Ne.{u_1 + 1} (α := V) 0 0 ∧ y ≠ 0 ∧ SameRay ℝ 0 (-y)
⊢ SameRay ℝ x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)
have refine_2₁ : ∀ (r : ℝ), SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
Tactic: rcases h with (rfl | ⟨r, rfl⟩)
Cleared hypotheses: y, 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 : V
r : ℝ
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
have pos : ∀ (hx : x = 0), SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
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 : V
r : ℝ
pos : ∀ (hx : x = 0), SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
have neg : ∀ (hx : ¬x = 0), SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
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 : V
r : ℝ
hx : ¬x = 0
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
have neg : ∀ (hr : r < 0), SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
Tactic: rcases lt_trichotomy r 0 with (hr | hr | hr)
-- 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 : V
r : ℝ
hx : ¬x = 0
neg : ∀ (hr : r < 0), SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
have neg₁ : ∀ (hr : r = 0), SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
Tactic: rcases lt_trichotomy r 0 with (hr | hr | hr)
-- 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 : V
r : ℝ
hx : ¬x = 0
neg : ∀ (hr : r < 0), SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
neg₁ : ∀ (hr : r = 0), SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
have neg₂ : ∀ (hr : 0 < r), SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
Tactic: rcases lt_trichotomy r 0 with (hr | hr | hr)
-- 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 : V
r : ℝ
hx : ¬x = 0
hr : r < 0
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
have neg : SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-r • x)
Tactic: rw [← neg_smul]
-- 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 ≠ 0 ∧ o.oangle x y ≠ (↑π : Real.Angle) ↔ LinearIndependent ℝ ![x, y]
have contrapose! : o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle) ↔ ¬LinearIndependent ℝ ![x, y]
Tactic: contrapose! +distrib
-- 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 = y ↔ ‖x‖ = ‖y‖ ∧ o.oangle x y = 0
have rw : x = y ↔ ‖x‖ = ‖y‖ ∧ SameRay ℝ x y
Tactic: rw [oangle_eq_zero_iff_sameRay]
-- 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 = y ↔ ‖x‖ = ‖y‖ ∧ SameRay ℝ x y
have mp : x = y → ‖x‖ = ‖y‖ ∧ SameRay ℝ x y
Tactic: constructor
-- 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
mp : x = y → ‖x‖ = ‖y‖ ∧ SameRay ℝ x y
⊢ x = y ↔ ‖x‖ = ‖y‖ ∧ SameRay ℝ x y
have mpr : ‖x‖ = ‖y‖ ∧ SameRay ℝ x y → x = y
Tactic: constructor
-- 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 : V
⊢ ‖x‖ = ‖x‖ ∧ SameRay ℝ x x
have mp : SameRay ℝ x x
Tactic: simp
-- 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‖ = ‖y‖ ∧ SameRay ℝ x y → x = y
have mpr : ‖x‖ = norm.{u_1} (E := V) 0 ∧ SameRay ℝ x 0 → x = 0
Tactic: rcases eq_or_ne y 0 with (rfl | hy)
Cleared hypotheses: 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
mpr : ‖x‖ = norm.{u_1} (E := V) 0 ∧ SameRay ℝ x 0 → x = 0
⊢ ‖x‖ = ‖y‖ ∧ SameRay ℝ x y → x = y
have mpr₁ : ∀ (hy : y ≠ 0), ‖x‖ = ‖y‖ ∧ SameRay ℝ x y → x = y
Tactic: rcases eq_or_ne y 0 with (rfl | 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
hy : y ≠ 0
h₁ : ‖x‖ = ‖y‖
h₂ : SameRay ℝ x y
⊢ x = y
have mpr : ∀ (r : ℝ) (hr : 0 ≤ r) (h₁ : ‖r • y‖ = ‖y‖) (h₂ : SameRay ℝ (r • y) y), r • y = y
Tactic: obtain ⟨r, hr, rfl⟩ := h₂.exists_nonneg_right hy
Cleared hypotheses: x, h₁, 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)
y : V
hy : y ≠ 0
r : ℝ
hr : 0 ≤ r
h₁ : ‖r • y‖ = ‖y‖
h₂ : SameRay ℝ (r • y) y
⊢ r • y = y
have this : ‖y‖ ≠ 0
Tactic: have : ‖y‖ ≠ 0 := by simpa using 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)
y : V
hy : y ≠ 0
r : ℝ
hr : 0 ≤ r
h₁ : ‖r • y‖ = ‖y‖
h₂ : SameRay ℝ (r • y) y
this : ‖y‖ ≠ 0
⊢ r = 1
have apply : r * ‖y‖ = 1 * ‖y‖
Tactic: apply mul_right_cancel₀ this
-- 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)
y : V
hy : y ≠ 0
r : ℝ
hr : 0 ≤ r
h₁ : ‖r • y‖ = ‖y‖
h₂ : SameRay ℝ (r • y) y
this : ‖y‖ ≠ 0
⊢ r • y = y
have mpr : ∀ (hr : LE.le (α := ℝ) 0 1) (h₁ : ‖HSMul.hSMul (α := ℝ) 1 y‖ = ‖y‖) (h₂ : SameRay ℝ (HSMul.hSMul (α := ℝ) 1 y) y),
  HSMul.hSMul (α := ℝ) 1 y = y
Tactic: obtain rfl : r = 1 := by
      apply mul_right_cancel₀ this
      simpa [norm_smul, abs_of_nonneg hr] using h₁
Cleared hypotheses: r, hr, 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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) +
      (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) y : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z)) : Real.Angle)
have rw : (↑(HMul.hMul (β := ℂ) (HPow.hPow (β := ℕ) (↑‖y‖ : ℂ) 2)
          ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z : ℂ)).arg :
    Real.Angle) =
  (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z)) : Real.Angle)
Tactic: rw [← Complex.arg_mul_coe_angle, o.kahler_mul y x z]
-- 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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
rw :
  (↑(HMul.hMul (β := ℂ) (HPow.hPow (β := ℕ) (↑‖y‖ : ℂ) 2)
            ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z : ℂ)).arg :
      Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z)) : Real.Angle)
⊢ (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) +
      (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) y : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z)) : Real.Angle)
have hx₁ : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)
Tactic: rw [← Complex.arg_mul_coe_angle, o.kahler_mul y x z]
-- 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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
rw :
  (↑(HMul.hMul (β := ℂ) (HPow.hPow (β := ℕ) (↑‖y‖ : ℂ) 2)
            ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z : ℂ)).arg :
      Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z)) : Real.Angle)
hx₁ : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)
⊢ (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) +
      (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) y : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z)) : Real.Angle)
have hy₁ : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) y : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z : ℂ) (0 : ℂ)
Tactic: rw [← Complex.arg_mul_coe_angle, o.kahler_mul y x z]