awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
r : ℝ
hr0 : 0 ≤ r
hr : (r + 1) • y = x
⊢ |(o.oangle (y - x) y).toReal| < π / 2
have h₁ : r = 0
Tactic: rw [← hr, norm_smul, Real.norm_eq_abs, abs_of_pos (Left.add_pos_of_nonneg_of_pos hr0 one_pos),
      mul_left_eq_self₀, or_iff_left (norm_ne_zero_iff.2 hy), add_eq_right] at h
Cleared hypotheses: h, hr0, hr
-- 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
hn : ¬x = y
hy : y ≠ 0
r : ℝ
h : r = 0
hr0 : 0 ≤ r
hr : (r + 1) • y = x
⊢ |(o.oangle (y - x) y).toReal| < π / 2
have hr₁ : y = x
Tactic: rw [h, zero_add, one_smul] at hr
Cleared hypotheses: 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 z : V
hx : x ≠ 0
hz : z ≠ 0
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
have pos : ∀ (hy : y = 0),
  InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
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 z : V
hx : x ≠ 0
hz : z ≠ 0
pos :
  ∀ (hy : y = 0),
    InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
have neg : ∀ (hy : ¬y = 0),
  InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
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 z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
have pos : ∀ (hr : SameRay ℝ x z),
  InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
Tactic: by_cases hr : SameRay ℝ 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
hz : z ≠ 0
hy : ¬y = 0
pos :
  ∀ (hr : SameRay ℝ x z),
    InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
have neg : ∀ (hr : ¬SameRay ℝ x z),
  InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
Tactic: by_cases hr : SameRay ℝ 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
hz : z ≠ 0
hy : ¬y = 0
hr : SameRay ℝ x z
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
have pos : ∀ (r : ℝ) (hrp : 0 < r) (hz : r • x ≠ 0) (hr : SameRay ℝ x (r • x)),
  InnerProductGeometry.angle x y = InnerProductGeometry.angle y (r • x) ↔
    o.oangle x y = o.oangle y (r • x) ∨ SameRay ℝ x (r • x)
Tactic: obtain ⟨r, hrp, rfl⟩ := hr.exists_pos_left hx hz
Cleared hypotheses: z, hz, 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 z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z ∨ SameRay ℝ x z
have neg : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z
Tactic: simp only [hr, or_false]
-- 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
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z
have pos : ∀ (hs : (o.oangle x y).sign = (o.oangle y z).sign),
  InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z
Tactic: by_cases hs : (o.oangle x y).sign = (o.oangle y z).sign
-- 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
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
pos :
  ∀ (hs : (o.oangle x y).sign = (o.oangle y z).sign),
    InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z
have neg : ∀ (hs : ¬(o.oangle x y).sign = (o.oangle y z).sign),
  InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z
Tactic: by_cases hs : (o.oangle x y).sign = (o.oangle y z).sign
-- 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
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : (o.oangle x y).sign = (o.oangle y z).sign
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z
have pos : o.oangle x y = o.oangle y z ↔ o.oangle x y = o.oangle y z
Tactic: rw [o.angle_eq_iff_oangle_eq_of_sign_eq hx hy hy hz 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)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z
have hn : o.oangle x y ≠ o.oangle y z
Tactic: have hn : o.oangle x y ≠ o.oangle y z := by grind
-- 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
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
⊢ InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔ o.oangle x y = o.oangle y z
have neg : ¬InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
Tactic: simp only [hn, iff_false]
-- 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
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
⊢ False
have neg : SameRay ℝ x z
Tactic: apply 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 z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
⊢ SameRay ℝ x z
have pos : ∀ (hs' : (o.oangle x y).sign = -(o.oangle y z).sign), SameRay ℝ x z
Tactic: by_cases hs' : (o.oangle x y).sign = -(o.oangle y z).sign
-- 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
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
pos : ∀ (hs' : (o.oangle x y).sign = -(o.oangle y z).sign), SameRay ℝ x z
⊢ SameRay ℝ x z
have neg : ∀ (hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign), SameRay ℝ x z
Tactic: by_cases hs' : (o.oangle x y).sign = -(o.oangle y z).sign
-- 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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : (o.oangle x y).sign = -(o.oangle y z).sign
⊢ SameRay ℝ x z
have he₁ : o.oangle x y = -o.oangle y z
Tactic: rw [o.angle_eq_iff_oangle_eq_neg_of_sign_eq_neg hx hy hy hz hs'] at he
Cleared hypotheses: he, 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)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : o.oangle x y = -o.oangle y z
hs' : (o.oangle x y).sign = -(o.oangle y z).sign
⊢ SameRay ℝ x z
have pos : o.oangle x y + o.oangle y z = 0
Tactic: rw [← o.oangle_eq_zero_iff_sameRay, ← o.oangle_add hx hy hz]
-- 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
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
⊢ (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
have revert : ∀ (hs : ¬(o.oangle x y).sign = (o.oangle y z).sign) (hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign),
  (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
Tactic: revert hs hs'
Cleared hypotheses: hs, 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)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
⊢ ∀ (hs : ¬(o.oangle x y).sign = (o.oangle y z).sign) (hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign),
    (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
have generalize : ∀ (sxy : SignType) (hs : ¬sxy = (o.oangle y z).sign) (hs' : ¬sxy = -(o.oangle y z).sign),
  sxy = 0 ∨ (o.oangle y z).sign = 0
Tactic: generalize (o.oangle x y).sign = sxy
-- 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
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
sxy : SignType
⊢ ∀ (hs : ¬sxy = (o.oangle y z).sign) (hs' : ¬sxy = -(o.oangle y z).sign), sxy = 0 ∨ (o.oangle y z).sign = 0
have generalize : ∀ (syz : SignType) (hs : ¬sxy = syz) (hs' : ¬sxy = -syz), sxy = 0 ∨ syz = 0
Tactic: generalize (o.oangle y z).sign = syz
-- 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
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
⊢ SameRay ℝ x z
have h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
Tactic: have h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0 := by
        revert hs hs'
        generalize (o.oangle x y).sign = sxy
        generalize (o.oangle y z).sign = syz
        decide +revert
-- 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
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
⊢ InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π
have inl : ∀ (h0 : (o.oangle x y).sign = 0), InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π
Tactic: rcases h0 with h0 | h0
Cleared hypotheses: 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)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
inl : ∀ (h0 : (o.oangle x y).sign = 0), InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π
⊢ InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π
have inr : ∀ (h0 : (o.oangle y z).sign = 0), InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π
Tactic: rcases h0 with h0 | h0
Cleared hypotheses: 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)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
⊢ SameRay ℝ x z
have h0' : InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π
Tactic: have h0' : InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π := by
        rcases h0 with h0 | h0
          <;> simpa [*] using o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero 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)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π
⊢ SameRay ℝ x z
have neg : ∀ (h0' : InnerProductGeometry.angle y z = 0), SameRay ℝ x z
Tactic: rcases h0' with h0' | h0'
Cleared hypotheses: 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)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = 0 ∨ InnerProductGeometry.angle y z = π
neg : ∀ (h0' : InnerProductGeometry.angle y z = 0), SameRay ℝ x z
⊢ SameRay ℝ x z
have neg₁ : ∀ (h0' : InnerProductGeometry.angle y z = π), SameRay ℝ x z
Tactic: rcases h0' with h0' | h0'
Cleared hypotheses: 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)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = 0
⊢ SameRay ℝ x z
have he₁ : InnerProductGeometry.angle x y = 0
Tactic: rw [h0'] at he
Cleared hypotheses: he, hs', h0, 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)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = 0
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = 0
⊢ SameRay ℝ x z
have neg : ∀ (r : ℝ) (hr0 : 0 < r) (hz : r • y ≠ 0) (hr : ¬SameRay ℝ x (r • y))
  (hs : ¬(o.oangle x y).sign = (o.oangle y (r • y)).sign) (hn : o.oangle x y ≠ o.oangle y (r • y))
  (hs' : ¬(o.oangle x y).sign = -(o.oangle y (r • y)).sign)
  (h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y (r • y)).sign = 0) (h0' : InnerProductGeometry.angle y (r • y) = 0),
  SameRay ℝ x (r • y)
Tactic: obtain ⟨-, r, hr0, rfl⟩ := InnerProductGeometry.angle_eq_zero_iff.1 h0'
Cleared hypotheses: z, hz, hr, hs, hn, hs', h0, 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)
x y : V
hx : x ≠ 0
hy : ¬y = 0
he : InnerProductGeometry.angle x y = 0
r : ℝ
hr0 : 0 < r
hz : r • y ≠ 0
hr : ¬SameRay ℝ x (r • y)
hs : ¬(o.oangle x y).sign = (o.oangle y (r • y)).sign
hn : o.oangle x y ≠ o.oangle y (r • y)
hs' : ¬(o.oangle x y).sign = -(o.oangle y (r • y)).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y (r • y)).sign = 0
h0' : InnerProductGeometry.angle y (r • y) = 0
⊢ SameRay ℝ x (r • y)
have neg : ∀ (r' : ℝ) (hr'0 : 0 < r') (hy : ¬r' • x = 0) (he : InnerProductGeometry.angle x (r' • x) = 0) (hz : r • r' • x ≠ 0)
  (hr : ¬SameRay ℝ x (r • r' • x)) (hs : ¬(o.oangle x (r' • x)).sign = (o.oangle (r' • x) (r • r' • x)).sign)
  (hn : o.oangle x (r' • x) ≠ o.oangle (r' • x) (r • r' • x))
  (hs' : ¬(o.oangle x (r' • x)).sign = -(o.oangle (r' • x) (r • r' • x)).sign)
  (h0 : (o.oangle x (r' • x)).sign = 0 ∨ (o.oangle (r' • x) (r • r' • x)).sign = 0)
  (h0' : InnerProductGeometry.angle (r' • x) (r • r' • x) = 0), SameRay ℝ x (r • r' • x)
Tactic: obtain ⟨-, r', hr'0, rfl⟩ := InnerProductGeometry.angle_eq_zero_iff.1 he
Cleared hypotheses: y, hy, he, hz, hr, hs, hn, hs', h0, 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)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = InnerProductGeometry.angle y z
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = π
⊢ SameRay ℝ x z
have he₁ : InnerProductGeometry.angle x y = π
Tactic: rw [h0'] at he
Cleared hypotheses: he, hs', h0, 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)
x y z : V
hx : x ≠ 0
hz : z ≠ 0
hy : ¬y = 0
hr : ¬SameRay ℝ x z
hs : ¬(o.oangle x y).sign = (o.oangle y z).sign
hn : o.oangle x y ≠ o.oangle y z
he : InnerProductGeometry.angle x y = π
hs' : ¬(o.oangle x y).sign = -(o.oangle y z).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y z).sign = 0
h0' : InnerProductGeometry.angle y z = π
⊢ SameRay ℝ x z
have neg : ∀ (r : ℝ) (hr0 : r < 0) (hz : r • y ≠ 0) (hr : ¬SameRay ℝ x (r • y))
  (hs : ¬(o.oangle x y).sign = (o.oangle y (r • y)).sign) (hn : o.oangle x y ≠ o.oangle y (r • y))
  (hs' : ¬(o.oangle x y).sign = -(o.oangle y (r • y)).sign)
  (h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y (r • y)).sign = 0) (h0' : InnerProductGeometry.angle y (r • y) = π),
  SameRay ℝ x (r • y)
Tactic: obtain ⟨-, r, hr0, rfl⟩ := InnerProductGeometry.angle_eq_pi_iff.1 h0'
Cleared hypotheses: z, hz, hr, hs, hn, hs', h0, 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)
x y : V
hx : x ≠ 0
hy : ¬y = 0
he : InnerProductGeometry.angle x y = π
r : ℝ
hr0 : r < 0
hz : r • y ≠ 0
hr : ¬SameRay ℝ x (r • y)
hs : ¬(o.oangle x y).sign = (o.oangle y (r • y)).sign
hn : o.oangle x y ≠ o.oangle y (r • y)
hs' : ¬(o.oangle x y).sign = -(o.oangle y (r • y)).sign
h0 : (o.oangle x y).sign = 0 ∨ (o.oangle y (r • y)).sign = 0
h0' : InnerProductGeometry.angle y (r • y) = π
⊢ SameRay ℝ x (r • y)
have neg : ∀ (r' : ℝ) (hr'0 : r' < 0) (hy : ¬r' • x = 0) (he : InnerProductGeometry.angle x (r' • x) = π) (hz : r • r' • x ≠ 0)
  (hr : ¬SameRay ℝ x (r • r' • x)) (hs : ¬(o.oangle x (r' • x)).sign = (o.oangle (r' • x) (r • r' • x)).sign)
  (hn : o.oangle x (r' • x) ≠ o.oangle (r' • x) (r • r' • x))
  (hs' : ¬(o.oangle x (r' • x)).sign = -(o.oangle (r' • x) (r • r' • x)).sign)
  (h0 : (o.oangle x (r' • x)).sign = 0 ∨ (o.oangle (r' • x) (r • r' • x)).sign = 0)
  (h0' : InnerProductGeometry.angle (r' • x) (r • r' • x) = π), SameRay ℝ x (r • r' • x)
Tactic: obtain ⟨-, r', hr'0, rfl⟩ := InnerProductGeometry.angle_eq_pi_iff.1 he
Cleared hypotheses: y, hy, he, hz, hr, hs, hn, hs', h0, h0'