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
r : ℝ
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)
have h₁ : m 0 • x + m 1 • (r • x + y) = 0
Tactic: change m 0 • x + m 1 • (r • x + y) = 0 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
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • (r • x + y) = 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 0 + m 1 * r, m 1] 0 • ![x, y] 0 + ![m 0 + m 1 * r, m 1] 1 • ![x, y] 1 = 0 ∧
  (![m 0 + m 1 * r, m 1] 0 ≠ 0 ∨ ![m 0 + m 1 * r, m 1] 1 ≠ 0)
Tactic: refine ⟨![m 0 + m 1 * r, m 1], ?_⟩
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • (r • x + y) = 0
⊢ ![m 0 + m 1 * r, m 1] 0 • ![x, y] 0 + ![m 0 + m 1 * r, m 1] 1 • ![x, y] 1 = 0 ∧
    (![m 0 + m 1 * r, m 1] 0 ≠ 0 ∨ ![m 0 + m 1 * r, m 1] 1 ≠ 0)
have refine_1 : (m 0 + m 1 * r) • x + m 1 • y = 0 ∧ (m 0 + m 1 * r ≠ 0 ∨ m 1 ≠ 0)
Tactic: change (m 0 + m 1 * r) • x + m 1 • y = 0 ∧ (m 0 + m 1 * r ≠ 0 ∨ m 1 ≠ 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 : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • (r • x + y) = 0
⊢ (m 0 + m 1 * r) • x + m 1 • y = 0 ∧ (m 0 + m 1 * r ≠ 0 ∨ m 1 ≠ 0)
have h₁ : (m 0 + m 1 * r) • x + m 1 • y = 0
Tactic: rw [smul_add, smul_smul, ← add_assoc, ← add_smul] 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
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
⊢ (m 0 + m 1 * r) • x + m 1 • y = 0 ∧ (m 0 + m 1 * r ≠ 0 ∨ m 1 ≠ 0)
have refine_1 : ∀ (h0 : m 0 + m 1 * r = 0 ∧ m 1 = 0), False
Tactic: refine ⟨h, not_and_or.1 fun 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 : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 + m 1 * r = 0 ∧ m 1 = 0
⊢ False
have h0₁ : m 0 + m 1 * r = 0
Tactic: obtain ⟨h0, h1⟩ := 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 : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 + m 1 * r = 0 ∧ m 1 = 0
h0₁ : m 0 + m 1 * r = 0
⊢ False
have h1 : m 1 = 0
Tactic: obtain ⟨h0, h1⟩ := 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 : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 + m 1 * r = 0
h1 : m 1 = 0
⊢ False
have hm₁ : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
Tactic: rw [h1] at h0 hm
Cleared hypotheses: hm, h, h0, h1
-- 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
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 + m 1 * r = 0
h1 : m 1 = 0
hm₁ : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
h₁ : (m 0 + m 1 * r) • x + m 1 • y = 0
⊢ False
have h0₁ : m 0 + 0 * r = 0
Tactic: rw [h1] at h0 hm
Cleared hypotheses: hm, h, h0, h1
-- 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
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
h : (m 0 + m 1 * r) • x + m 1 • y = 0
h0 : m 0 + 0 * r = 0
h1 : m 1 = 0
⊢ False
have h0₁ : m 0 = 0
Tactic: rw [zero_mul, add_zero] at h0
Cleared hypotheses: h0, h1
-- 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, 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)
have refine_2 : ∀ (m : Fin (Nat.succ 0).succ → ℝ) (h : m 0 • ![x, y] 0 + m 1 • ![x, y] 1 = 0) (hm : m 0 ≠ 0 ∨ m 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: rcases h with ⟨m, h, hm⟩
Cleared hypotheses: 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
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
h : m 0 • ![x, y] 0 + m 1 • ![x, y] 1 = 0
hm : m 0 ≠ 0 ∨ m 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)
have h₁ : m 0 • x + m 1 • y = 0
Tactic: change m 0 • x + m 1 • y = 0 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
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 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)
have refine_2 : ![m 0 - m 1 * r, m 1] 0 • ![x, r • x + y] 0 + ![m 0 - m 1 * r, m 1] 1 • ![x, r • x + y] 1 = 0 ∧
  (![m 0 - m 1 * r, m 1] 0 ≠ 0 ∨ ![m 0 - m 1 * r, m 1] 1 ≠ 0)
Tactic: refine ⟨![m 0 - m 1 * r, m 1], ?_⟩
-- 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 : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
⊢ ![m 0 - m 1 * r, m 1] 0 • ![x, r • x + y] 0 + ![m 0 - m 1 * r, m 1] 1 • ![x, r • x + y] 1 = 0 ∧
    (![m 0 - m 1 * r, m 1] 0 ≠ 0 ∨ ![m 0 - m 1 * r, m 1] 1 ≠ 0)
have refine_2 : (m 0 - m 1 * r) • x + m 1 • (r • x + y) = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0)
Tactic: change (m 0 - m 1 * r) • x + m 1 • (r • x + y) = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 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
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
⊢ (m 0 - m 1 * r) • x + m 1 • (r • x + y) = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0)
have refine_2 : m 0 • x + m 1 • y = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0)
Tactic: rw [sub_smul, smul_add, smul_smul, ← add_assoc, sub_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
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
⊢ m 0 • x + m 1 • y = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0)
have refine_2 : ∀ (h0 : m 0 - m 1 * r = 0 ∧ m 1 = 0), False
Tactic: refine ⟨h, not_and_or.1 fun 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 : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 - m 1 * r = 0 ∧ m 1 = 0
⊢ False
have h0₁ : m 0 - m 1 * r = 0
Tactic: obtain ⟨h0, h1⟩ := 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 : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 - m 1 * r = 0 ∧ m 1 = 0
h0₁ : m 0 - m 1 * r = 0
⊢ False
have h1 : m 1 = 0
Tactic: obtain ⟨h0, h1⟩ := 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 : V
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 - m 1 * r = 0
h1 : m 1 = 0
⊢ False
have hm₁ : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
Tactic: rw [h1] at h0 hm
Cleared hypotheses: hm, h, h0, h1
-- 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
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ m 1 ≠ 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 - m 1 * r = 0
h1 : m 1 = 0
hm₁ : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
h₁ : m 0 • x + m 1 • y = 0
⊢ False
have h0₁ : m 0 - 0 * r = 0
Tactic: rw [h1] at h0 hm
Cleared hypotheses: hm, h, h0, h1
-- 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
r : ℝ
m : Fin (Nat.succ 0).succ → ℝ
hm : m 0 ≠ 0 ∨ Ne (α := ℝ) 0 0
h : m 0 • x + m 1 • y = 0
h0 : m 0 - 0 * r = 0
h1 : m 1 = 0
⊢ False
have h0₁ : m 0 = 0
Tactic: rw [zero_mul, sub_zero] at h0
Cleared hypotheses: h0, h1
-- 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)).sign = (o.oangle x y).sign
have pos : ∀ (h : o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle)), (o.oangle x (r • x + y)).sign = (o.oangle x y).sign
Tactic: by_cases h : o.oangle x y = 0 ∨ o.oangle x 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
r : ℝ
pos : ∀ (h : o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle)), (o.oangle x (r • x + y)).sign = (o.oangle x y).sign
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign
have neg : ∀ (h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))), (o.oangle x (r • x + y)).sign = (o.oangle x y).sign
Tactic: by_cases h : o.oangle x y = 0 ∨ o.oangle x 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
r : ℝ
h : o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle)
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign
have pos : (o.oangle x (r • x + y)).sign = 0
Tactic: rwa [Real.Angle.sign_eq_zero_iff.2 h, Real.Angle.sign_eq_zero_iff,
      oangle_smul_add_right_eq_zero_or_eq_pi_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
r : ℝ
h : o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle)
pos : (o.oangle x (r • x + y)).sign = 0
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign
have pos₁ : o.oangle x (r • x + y) = 0 ∨ o.oangle x (r • x + y) = (↑π : Real.Angle)
Tactic: rwa [Real.Angle.sign_eq_zero_iff.2 h, Real.Angle.sign_eq_zero_iff,
      oangle_smul_add_right_eq_zero_or_eq_pi_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
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
r' : ℝ
⊢ o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
have rwa : ∀ (h : ¬(o.oangle x (r' • x + y) = 0 ∨ o.oangle x (r' • x + y) = (↑π : Real.Angle))),
  o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
Tactic: rwa [← o.oangle_smul_add_right_eq_zero_or_eq_pi_iff r', not_or] 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
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
r' : ℝ
rwa :
  ∀ (h : ¬(o.oangle x (r' • x + y) = 0 ∨ o.oangle x (r' • x + y) = (↑π : Real.Angle))),
    o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
⊢ o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
have rwa₁ : ∀ (h : ¬o.oangle x (r' • x + y) = 0 ∧ ¬o.oangle x (r' • x + y) = (↑π : Real.Angle)),
  o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
Tactic: rwa [← o.oangle_smul_add_right_eq_zero_or_eq_pi_iff r', not_or] at h
Cleared hypotheses: 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
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign
have h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
Tactic: have h' : ∀ r' : ℝ, o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ π := by
    intro r'
    rwa [← o.oangle_smul_add_right_eq_zero_or_eq_pi_iff r', not_or] at 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
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign
have hc : IsConnected s
Tactic: have hc : IsConnected s := isConnected_univ.image _ (by fun_prop)
-- 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 : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
⊢ ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s
have refine_1 : ∀ (z : V × V) (hz : z ∈ s), z.1 ≠ 0
Tactic: refine continuousOn_of_forall_continuousAt fun z hz => o.continuousAt_oangle ?_ ?_
-- 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 : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
refine_1 : ∀ (z : V × V) (hz : z ∈ s), z.1 ≠ 0
⊢ ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s
have refine_2 : ∀ (z : V × V) (hz : z ∈ s), z.2 ≠ 0
Tactic: refine continuousOn_of_forall_continuousAt fun z hz => o.continuousAt_oangle ?_ ?_
-- 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
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
z : V × V
hz : z ∈ s
⊢ z.1 ≠ 0
have hz₁ : ∃ (x_1 : ℝ), Membership.mem (γ := Set ℝ) Set.univ x_1 ∧ (x, x_1 • x + y) = z
Tactic: simp_rw [s, Set.mem_image] at hz
Cleared hypotheses: 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 : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
z : V × V
hz : ∃ (x_1 : ℝ), Membership.mem (γ := Set ℝ) Set.univ x_1 ∧ (x, x_1 • x + y) = z
⊢ z.1 ≠ 0
have refine_1 : ∀ (r' : ℝ), (x, r' • x + y).1 ≠ 0
Tactic: obtain ⟨r', -, rfl⟩ := hz
Cleared hypotheses: z, 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 : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
r' : ℝ
⊢ (x, r' • x + y).1 ≠ 0
have refine_1 : x ≠ 0
Tactic: simp only
-- 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
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
z : V × V
hz : z ∈ s
⊢ z.2 ≠ 0
have hz₁ : ∃ (x_1 : ℝ), Membership.mem (γ := Set ℝ) Set.univ x_1 ∧ (x, x_1 • x + y) = z
Tactic: simp_rw [s, Set.mem_image] at hz
Cleared hypotheses: 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 : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
z : V × V
hz : ∃ (x_1 : ℝ), Membership.mem (γ := Set ℝ) Set.univ x_1 ∧ (x, x_1 • x + y) = z
⊢ z.2 ≠ 0
have refine_2 : ∀ (r' : ℝ), (x, r' • x + y).2 ≠ 0
Tactic: obtain ⟨r', -, rfl⟩ := hz
Cleared hypotheses: z, 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 : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
r' : ℝ
⊢ (x, r' • x + y).2 ≠ 0
have refine_2 : r' • x + y ≠ 0
Tactic: simp only
-- 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
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign
have hf : ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s
Tactic: have hf : ContinuousOn (fun z : V × V => o.oangle z.1 z.2) s := by
    refine continuousOn_of_forall_continuousAt fun z hz => o.continuousAt_oangle ?_ ?_
    all_goals
      simp_rw [s, Set.mem_image] at hz
      obtain ⟨r', -, rfl⟩ := hz
      simp only
      intro hz
    · simpa [hz] using (h' 0).1
    · simpa [hz] using (h' r').1
-- 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
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign
have hs : ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ (↑π : Real.Angle)
Tactic: have hs : ∀ z : V × V, z ∈ s → o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ π := 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 : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s
hs : ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ (↑π : Real.Angle)
⊢ (x, y) ∈ s
have h₁ : y = HSMul.hSMul (α := ℝ) 0 x + y
Tactic: convert! Set.mem_image_of_mem (fun r' : ℝ => (x, r' • x + y)) (Set.mem_univ 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 : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle))
h' : ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ (↑π : Real.Angle)
s : Set (V × V) := (fun (r' : ℝ) ↦ (x, r' • x + y)) '' Set.univ
hc : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (z : V × V) ↦ o.oangle z.1 z.2) s
hs : ∀ z ∈ s, o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ (↑π : Real.Angle)
⊢ (o.oangle x (r • x + y)).sign = (o.oangle x y).sign
have hx : (x, y) ∈ s
Tactic: have hx : (x, y) ∈ s := by
    convert! Set.mem_image_of_mem (fun r' : ℝ => (x, r' • x + y)) (Set.mem_univ 0)
    simp