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), HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
have neg : ∀ (hy : ¬y = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle 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
⊢ o.oangle (-x) y = o.oangle x (-y)
have rw : o.oangle (-x) (- -y) = o.oangle x (- - -y)
Tactic: rw [← neg_neg y, oangle_neg_neg, neg_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
rw : o.oangle (-x) (- -y) = o.oangle x (- - -y)
⊢ o.oangle (-x) y = o.oangle x (-y)
have rw₁ : o.oangle x (-y) = o.oangle x (- - -y)
Tactic: rw [← neg_neg y, oangle_neg_neg, neg_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
rw : o.oangle (-x) (- -y) = o.oangle x (- - -y)
rw₁ : o.oangle x (-y) = o.oangle x (- - -y)
⊢ o.oangle (-x) y = o.oangle x (-y)
have rw₂ : o.oangle x (-y) = o.oangle x (-y)
Tactic: rw [← neg_neg y, oangle_neg_neg, neg_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 : V
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) x) = 0
have pos : ∀ (hx : x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) x) = 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 : V
pos : ∀ (hx : x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) x) = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) x) = 0
have neg : ∀ (hx : ¬x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) x) = 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 : V
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (-x)) = 0
have pos : ∀ (hx : x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (-x)) = 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 : V
pos : ∀ (hx : x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (-x)) = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (-x)) = 0
have neg : ∀ (hx : ¬x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (-x)) = 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
⊢ o.oangle (-x) y + o.oangle (-y) x = 0
have rw : o.oangle x (-y) + o.oangle (-y) x = 0
Tactic: rw [oangle_neg_left_eq_neg_right, oangle_rev, neg_add_cancel]
-- 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 : o.oangle x (-y) + o.oangle (-y) x = 0
⊢ o.oangle (-x) y + o.oangle (-y) x = 0
have rw₁ : -o.oangle (-y) x + o.oangle (-y) x = 0
Tactic: rw [oangle_neg_left_eq_neg_right, oangle_rev, neg_add_cancel]
-- 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 : o.oangle x (-y) + o.oangle (-y) x = 0
rw₁ : -o.oangle (-y) x + o.oangle (-y) x = 0
⊢ o.oangle (-x) y + o.oangle (-y) x = 0
have rw₂ : Eq (α := Real.Angle) 0 0
Tactic: rw [oangle_neg_left_eq_neg_right, oangle_rev, neg_add_cancel]
-- 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) + o.oangle y (-x) = 0
have rw : o.oangle x (-y) + -o.oangle (-x) y = 0
Tactic: rw [o.oangle_rev (-x), oangle_neg_left_eq_neg_right, add_neg_cancel]
-- 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 : o.oangle x (-y) + -o.oangle (-x) y = 0
⊢ o.oangle x (-y) + o.oangle y (-x) = 0
have rw₁ : o.oangle x (-y) + -o.oangle x (-y) = 0
Tactic: rw [o.oangle_rev (-x), oangle_neg_left_eq_neg_right, add_neg_cancel]
-- 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 : o.oangle x (-y) + -o.oangle (-x) y = 0
rw₁ : o.oangle x (-y) + -o.oangle x (-y) = 0
⊢ o.oangle x (-y) + o.oangle y (-x) = 0
have rw₂ : Eq (α := Real.Angle) 0 0
Tactic: rw [o.oangle_rev (-x), oangle_neg_left_eq_neg_right, add_neg_cancel]
-- 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 : ℝ
hr : r < 0
⊢ o.oangle (r • x) y = o.oangle (-x) y
have rw : o.oangle (- -r • x) y = o.oangle (-x) y
Tactic: rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_left_of_pos _ _ (neg_pos_of_neg 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 y : V
r : ℝ
hr : r < 0
rw : o.oangle (- -r • x) y = o.oangle (-x) y
⊢ o.oangle (r • x) y = o.oangle (-x) y
have rw₁ : o.oangle (-(-r • x)) y = o.oangle (-x) y
Tactic: rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_left_of_pos _ _ (neg_pos_of_neg 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 y : V
r : ℝ
hr : r < 0
rw : o.oangle (- -r • x) y = o.oangle (-x) y
rw₁ : o.oangle (-(-r • x)) y = o.oangle (-x) y
⊢ o.oangle (r • x) y = o.oangle (-x) y
have rw₂ : o.oangle (-r • -x) y = o.oangle (-x) y
Tactic: rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_left_of_pos _ _ (neg_pos_of_neg 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 y : V
r : ℝ
hr : r < 0
rw : o.oangle (- -r • x) y = o.oangle (-x) y
rw₁ : o.oangle (-(-r • x)) y = o.oangle (-x) y
rw₂ : o.oangle (-r • -x) y = o.oangle (-x) y
⊢ o.oangle (r • x) y = o.oangle (-x) y
have rw₃ : o.oangle (-x) y = o.oangle (-x) y
Tactic: rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_left_of_pos _ _ (neg_pos_of_neg 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 y : V
r : ℝ
hr : r < 0
⊢ o.oangle x (r • y) = o.oangle x (-y)
have rw : o.oangle x (- -r • y) = o.oangle x (-y)
Tactic: rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_right_of_pos _ _ (neg_pos_of_neg 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 y : V
r : ℝ
hr : r < 0
rw : o.oangle x (- -r • y) = o.oangle x (-y)
⊢ o.oangle x (r • y) = o.oangle x (-y)
have rw₁ : o.oangle x (-(-r • y)) = o.oangle x (-y)
Tactic: rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_right_of_pos _ _ (neg_pos_of_neg 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 y : V
r : ℝ
hr : r < 0
rw : o.oangle x (- -r • y) = o.oangle x (-y)
rw₁ : o.oangle x (-(-r • y)) = o.oangle x (-y)
⊢ o.oangle x (r • y) = o.oangle x (-y)
have rw₂ : o.oangle x (-r • -y) = o.oangle x (-y)
Tactic: rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_right_of_pos _ _ (neg_pos_of_neg 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 y : V
r : ℝ
hr : r < 0
rw : o.oangle x (- -r • y) = o.oangle x (-y)
rw₁ : o.oangle x (-(-r • y)) = o.oangle x (-y)
rw₂ : o.oangle x (-r • -y) = o.oangle x (-y)
⊢ o.oangle x (r • y) = o.oangle x (-y)
have rw₃ : o.oangle x (-y) = o.oangle x (-y)
Tactic: rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_right_of_pos _ _ (neg_pos_of_neg 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 : ℝ
hr : 0 ≤ r
⊢ o.oangle (r • x) x = 0
have inl : ∀ (h : 0 < r), o.oangle (r • x) x = 0
Tactic: rcases hr.lt_or_eq 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 : V
r : ℝ
hr : 0 ≤ r
inl : ∀ (h : 0 < r), o.oangle (r • x) x = 0
⊢ o.oangle (r • x) x = 0
have inr : ∀ (h : 0 = r), o.oangle (r • x) x = 0
Tactic: rcases hr.lt_or_eq 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 : V
r : ℝ
hr : 0 ≤ r
⊢ o.oangle x (r • x) = 0
have inl : ∀ (h : 0 < r), o.oangle x (r • x) = 0
Tactic: rcases hr.lt_or_eq 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 : V
r : ℝ
hr : 0 ≤ r
inl : ∀ (h : 0 < r), o.oangle x (r • x) = 0
⊢ o.oangle x (r • x) = 0
have inr : ∀ (h : 0 = r), o.oangle x (r • x) = 0
Tactic: rcases hr.lt_or_eq 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 : V
r₁ r₂ : ℝ
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
⊢ o.oangle (r₁ • x) (r₂ • x) = 0
have inl : ∀ (h : 0 < r₁), o.oangle (r₁ • x) (r₂ • x) = 0
Tactic: rcases hr₁.lt_or_eq 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 : V
r₁ r₂ : ℝ
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
inl : ∀ (h : 0 < r₁), o.oangle (r₁ • x) (r₂ • x) = 0
⊢ o.oangle (r₁ • x) (r₂ • x) = 0
have inr : ∀ (h : 0 = r₁), o.oangle (r₁ • x) (r₂ • x) = 0
Tactic: rcases hr₁.lt_or_eq 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
r : ℝ
hr : r ≠ 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
have inl : ∀ (h : r < 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
Tactic: rcases hr.lt_or_gt 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
r : ℝ
hr : r ≠ 0
inl : ∀ (h : r < 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
have inr : ∀ (h : 0 < r), HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
Tactic: rcases hr.lt_or_gt 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
r : ℝ
hr : r ≠ 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
have inl : ∀ (h : r < 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
Tactic: rcases hr.lt_or_gt 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
r : ℝ
hr : r ≠ 0
inl : ∀ (h : r < 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
have inr : ∀ (h : 0 < r), HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
Tactic: rcases hr.lt_or_gt 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 : V
r : ℝ
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) x) = 0
have inl : ∀ (h : r < 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) x) = 0
Tactic: rcases lt_or_ge r 0 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 : V
r : ℝ
inl : ∀ (h : r < 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) x) = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) x) = 0
have inr : ∀ (h : 0 ≤ r), HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) x) = 0
Tactic: rcases lt_or_ge r 0 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 : V
r : ℝ
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • x)) = 0
have inl : ∀ (h : r < 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • x)) = 0
Tactic: rcases lt_or_ge r 0 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 : V
r : ℝ
inl : ∀ (h : r < 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • x)) = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • x)) = 0
have inr : ∀ (h : 0 ≤ r), HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • x)) = 0
Tactic: rcases lt_or_ge r 0 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 : V
r₁ r₂ : ℝ
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (r₁ • x) (r₂ • x)) = 0
have pos : ∀ (h : r₁ = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (r₁ • x) (r₂ • x)) = 0
Tactic: by_cases h : r₁ = 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₁ r₂ : ℝ
pos : ∀ (h : r₁ = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (r₁ • x) (r₂ • x)) = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (r₁ • x) (r₂ • x)) = 0
have neg : ∀ (h : ¬r₁ = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (r₁ • x) (r₂ • x)) = 0
Tactic: by_cases h : r₁ = 0
-- 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 z : V
h : Eq (α := Submodule ℝ V) (ℝ ∙ x) (ℝ ∙ y)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x z) = HSMul.hSMul (α := ℤ) 2 (o.oangle y z)
have h₁ : ∃ (z : ℝˣ), z • x = y
Tactic: rw [Submodule.span_singleton_eq_span_singleton] 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 z : V
h : ∃ (z : ℝˣ), z • x = y
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x z) = HSMul.hSMul (α := ℤ) 2 (o.oangle y z)
have rcases : ∀ (r : ℝˣ), HSMul.hSMul (α := ℤ) 2 (o.oangle x z) = HSMul.hSMul (α := ℤ) 2 (o.oangle (r • x) z)
Tactic: rcases h with ⟨r, rfl⟩
Cleared hypotheses: y, 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 z : V
h : Eq (α := Submodule ℝ V) (ℝ ∙ y) (ℝ ∙ z)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x z)
have h₁ : ∃ (z_1 : ℝˣ), z_1 • y = z
Tactic: rw [Submodule.span_singleton_eq_span_singleton] 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 z : V
h : ∃ (z_1 : ℝˣ), z_1 • y = z
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x z)
have rcases : ∀ (r : ℝˣ), HSMul.hSMul (α := ℤ) 2 (o.oangle x y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x (r • y))
Tactic: rcases h with ⟨r, rfl⟩
Cleared hypotheses: z, 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
hwx : Eq (α := Submodule ℝ V) (ℝ ∙ w) (ℝ ∙ x)
hyz : Eq (α := Submodule ℝ V) (ℝ ∙ y) (ℝ ∙ z)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle w y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x z)
have rw : HSMul.hSMul (α := ℤ) 2 (o.oangle x y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x z)
Tactic: rw [o.two_zsmul_oangle_left_of_span_eq y hwx, o.two_zsmul_oangle_right_of_span_eq x hyz]
-- 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
hwx : Eq (α := Submodule ℝ V) (ℝ ∙ w) (ℝ ∙ x)
hyz : Eq (α := Submodule ℝ V) (ℝ ∙ y) (ℝ ∙ z)
rw : HSMul.hSMul (α := ℤ) 2 (o.oangle x y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x z)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle w y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x z)
have rw₁ : HSMul.hSMul (α := ℤ) 2 (o.oangle x z) = HSMul.hSMul (α := ℤ) 2 (o.oangle x z)
Tactic: rw [o.two_zsmul_oangle_left_of_span_eq y hwx, o.two_zsmul_oangle_right_of_span_eq x hyz]
-- 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 y x = 0
have rw : -o.oangle y x = 0 ↔ o.oangle y x = 0
Tactic: rw [oangle_rev, neg_eq_zero]
-- 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 : -o.oangle y x = 0 ↔ o.oangle y x = 0
⊢ o.oangle x y = 0 ↔ o.oangle y x = 0
have rw₁ : o.oangle y x = 0 ↔ o.oangle y x = 0
Tactic: rw [oangle_rev, neg_eq_zero]
-- 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 ↔ SameRay ℝ x y
have rw : 0 ≤
      ((↑⟪x, y⟫ : ℂ) +
          HSMul.hSMul (α := ℝ) ((((o.areaForm : (a : V) → V →ₗ[ℝ] ℝ) x : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) y : ℝ) I).re ∧
    ((↑⟪x, y⟫ : ℂ) +
          HSMul.hSMul (α := ℝ) ((((o.areaForm : (a : V) → V →ₗ[ℝ] ℝ) x : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) y : ℝ) I).im =
      0 ↔
  SameRay ℝ x y
Tactic: rw [oangle, kahler_apply_apply, Complex.arg_coe_angle_eq_iff_eq_toReal, Real.Angle.toReal_zero,
    Complex.arg_eq_zero_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
⊢ o.oangle x y = (↑π : Real.Angle) ↔ o.oangle y x = (↑π : Real.Angle)
have rw : -o.oangle y x = (↑π : Real.Angle) ↔ o.oangle y x = (↑π : Real.Angle)
Tactic: rw [oangle_rev, neg_eq_iff_eq_neg, Real.Angle.neg_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
rw : -o.oangle y x = (↑π : Real.Angle) ↔ o.oangle y x = (↑π : Real.Angle)
⊢ o.oangle x y = (↑π : Real.Angle) ↔ o.oangle y x = (↑π : Real.Angle)
have rw₁ : o.oangle y x = -(↑π : Real.Angle) ↔ o.oangle y x = (↑π : Real.Angle)
Tactic: rw [oangle_rev, neg_eq_iff_eq_neg, Real.Angle.neg_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
rw : -o.oangle y x = (↑π : Real.Angle) ↔ o.oangle y x = (↑π : Real.Angle)
rw₁ : o.oangle y x = -(↑π : Real.Angle) ↔ o.oangle y x = (↑π : Real.Angle)
⊢ o.oangle x y = (↑π : Real.Angle) ↔ o.oangle y x = (↑π : Real.Angle)
have rw₂ : o.oangle y x = (↑π : Real.Angle) ↔ o.oangle y x = (↑π : Real.Angle)
Tactic: rw [oangle_rev, neg_eq_iff_eq_neg, Real.Angle.neg_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
⊢ o.oangle x y = (↑π : Real.Angle) ↔ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)
have rw : o.oangle x y = (↑π : Real.Angle) ↔ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
Tactic: rw [← o.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
⊢ o.oangle x y = (↑π : Real.Angle) ↔ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
have mp : o.oangle x y = (↑π : Real.Angle) → x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
Tactic: constructor