awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : angle x y + n • (2 * π) = angle x (x + y) + angle y (x + y)
⊢ angle x y = angle x (x + y) + angle y (x + y)
have this : -1 < n
Tactic: have : -1 < n := by
    replace h := h.ge
    contrapose! h
    grw [h, neg_smul, one_smul, angle_le_pi, ← angle_nonneg, ← angle_nonneg]
    linear_combination Real.pi_pos
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : angle x y + n • (2 * π) = angle x (x + y) + angle y (x + y)
this : -1 < n
⊢ n < 1
have h₁ : angle x y + n • (2 * π) ≤ angle x (x + y) + angle y (x + y)
Tactic: replace h := h.le
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : angle x y + n • (2 * π) ≤ angle x (x + y) + angle y (x + y)
⊢ n < 1
have by_contra! : ∀ (hn : 1 ≤ n), False
Tactic: by_contra! hn
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : angle x y + n • (2 * π) ≤ angle x (x + y) + angle y (x + y)
hn : 1 ≤ n
⊢ False
have h₁ : π + π ≤ angle x (x + y) + angle y (x + y)
Tactic: grw [← hn, one_smul, ← angle_nonneg x y, zero_add, two_mul] at h
Cleared hypotheses: h, hn
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : π + π ≤ angle x (x + y) + angle y (x + y)
hn : 1 ≤ n
⊢ False
have h' : π + π ≤ angle y (x + y) + angle x (x + y)
Tactic: have h' := h.trans_eq (add_comm _ _)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : π + π ≤ angle x (x + y) + angle y (x + y)
hn : 1 ≤ n
h' : π + π ≤ angle y (x + y) + angle x (x + y)
⊢ False
have h₁ : π + π ≤ π + angle y (x + y)
Tactic: grw [angle_le_pi] at h' h
Cleared hypotheses: h, hn, h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : π + π ≤ angle x (x + y) + angle y (x + y)
hn : 1 ≤ n
h' : π + π ≤ angle y (x + y) + angle x (x + y)
h₁ : π + π ≤ π + angle y (x + y)
hn₁ : 1 ≤ n
⊢ False
have h'₁ : π + π ≤ π + angle x (x + y)
Tactic: grw [angle_le_pi] at h' h
Cleared hypotheses: h, hn, h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : π + π ≤ π + angle y (x + y)
hn : 1 ≤ n
h' : π + π ≤ π + angle x (x + y)
⊢ False
have h₁ : x + y ≠ 0 ∧ ∃ r < 0, y = r • (x + y)
Tactic: rw [add_le_add_iff_left, (angle_le_pi _ _).ge_iff_eq, angle_comm, angle_eq_pi_iff] at h' h
Cleared hypotheses: h, hn, h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : π + π ≤ π + angle y (x + y)
hn : 1 ≤ n
h' : π + π ≤ π + angle x (x + y)
h₁ : x + y ≠ 0 ∧ ∃ r < 0, y = r • (x + y)
hn₁ : 1 ≤ n
⊢ False
have h'₁ : x + y ≠ 0 ∧ ∃ r < 0, x = r • (x + y)
Tactic: rw [add_le_add_iff_left, (angle_le_pi _ _).ge_iff_eq, angle_comm, angle_eq_pi_iff] at h' h
Cleared hypotheses: h, hn, h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : x + y ≠ 0 ∧ ∃ r < 0, y = r • (x + y)
hn : 1 ≤ n
h' : x + y ≠ 0 ∧ ∃ r < 0, x = r • (x + y)
⊢ False
have obtain : ∀ (hxy : x + y ≠ 0) (r₁ : ℝ) (r₁_pos : r₁ < 0) (hr₁ : x = r₁ • (x + y)), False
Tactic: obtain ⟨hxy, r₁, r₁_pos, hr₁⟩ := h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
h : x + y ≠ 0 ∧ ∃ r < 0, y = r • (x + y)
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
⊢ False
have obtain : ∀ (r₂ : ℝ) (r₂_pos : r₂ < 0) (hr₂ : y = r₂ • (x + y)), False
Tactic: obtain ⟨-, r₂, r₂_pos, hr₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
⊢ (r₁ + r₂ - 1) • (x + y) = 0
have rw : (r₁ + r₂) • (x + y) - HSMul.hSMul (α := ℝ) 1 (x + y) = 0
Tactic: rw [sub_smul, add_smul, one_smul, ← hr₁, ← hr₂, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
rw : (r₁ + r₂) • (x + y) - HSMul.hSMul (α := ℝ) 1 (x + y) = 0
⊢ (r₁ + r₂ - 1) • (x + y) = 0
have rw₁ : r₁ • (x + y) + r₂ • (x + y) - HSMul.hSMul (α := ℝ) 1 (x + y) = 0
Tactic: rw [sub_smul, add_smul, one_smul, ← hr₁, ← hr₂, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
rw : (r₁ + r₂) • (x + y) - HSMul.hSMul (α := ℝ) 1 (x + y) = 0
rw₁ : r₁ • (x + y) + r₂ • (x + y) - HSMul.hSMul (α := ℝ) 1 (x + y) = 0
⊢ (r₁ + r₂ - 1) • (x + y) = 0
have rw₂ : r₁ • (x + y) + r₂ • (x + y) - (x + y) = 0
Tactic: rw [sub_smul, add_smul, one_smul, ← hr₁, ← hr₂, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
rw : (r₁ + r₂) • (x + y) - HSMul.hSMul (α := ℝ) 1 (x + y) = 0
rw₁ : r₁ • (x + y) + r₂ • (x + y) - HSMul.hSMul (α := ℝ) 1 (x + y) = 0
rw₂ : r₁ • (x + y) + r₂ • (x + y) - (x + y) = 0
⊢ (r₁ + r₂ - 1) • (x + y) = 0
have rw₃ : x + r₂ • (x + y) - (x + y) = 0
Tactic: rw [sub_smul, add_smul, one_smul, ← hr₁, ← hr₂, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
rw : (r₁ + r₂) • (x + y) - HSMul.hSMul (α := ℝ) 1 (x + y) = 0
rw₁ : r₁ • (x + y) + r₂ • (x + y) - HSMul.hSMul (α := ℝ) 1 (x + y) = 0
rw₂ : r₁ • (x + y) + r₂ • (x + y) - (x + y) = 0
rw₃ : x + r₂ • (x + y) - (x + y) = 0
⊢ (r₁ + r₂ - 1) • (x + y) = 0
have rw₄ : x + y - (x + y) = 0
Tactic: rw [sub_smul, add_smul, one_smul, ← hr₁, ← hr₂, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
rw : (r₁ + r₂) • (x + y) - HSMul.hSMul (α := ℝ) 1 (x + y) = 0
rw₁ : r₁ • (x + y) + r₂ • (x + y) - HSMul.hSMul (α := ℝ) 1 (x + y) = 0
rw₂ : r₁ • (x + y) + r₂ • (x + y) - (x + y) = 0
rw₃ : x + r₂ • (x + y) - (x + y) = 0
rw₄ : x + y - (x + y) = 0
⊢ (r₁ + r₂ - 1) • (x + y) = 0
have rw₅ : x + y = x + y
Tactic: rw [sub_smul, add_smul, one_smul, ← hr₁, ← hr₂, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
⊢ False
have this₁ : (r₁ + r₂ - 1) • (x + y) = 0
Tactic: have : (r₁ + r₂ - 1) • (x + y) = 0 := by
      rw [sub_smul, add_smul, one_smul, ← hr₁, ← hr₂, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this_1 : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
this : (r₁ + r₂ - 1) • (x + y) = 0
⊢ False
have inl : r₁ + r₂ - 1 = 0 → False
Tactic: cases smul_eq_zero.1 this
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
this_1 : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
this : (r₁ + r₂ - 1) • (x + y) = 0
h_1 : r₁ + r₂ - 1 = 0
⊢ False
have linarith : -1 + (r₁ - 0) + (r₂ - 0) + -(r₁ + r₂ - 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : angle x y + n • (2 * π) = angle x (x + y) + angle y (x + y)
this : -1 < n
⊢ angle x y = angle x (x + y) + angle y (x + y)
have this₁ : n < 1
Tactic: have : n < 1 := by
    replace h := h.le
    by_contra! hn
    grw [← hn, one_smul, ← angle_nonneg x y, zero_add, two_mul] at h
    have h' := h.trans_eq (add_comm _ _)
    grw [angle_le_pi] at h' h
    rw [add_le_add_iff_left, (angle_le_pi _ _).ge_iff_eq, angle_comm, angle_eq_pi_iff] at h' h
    obtain ⟨hxy, r₁, r₁_pos, hr₁⟩ := h'
    obtain ⟨-, r₂, r₂_pos, hr₂⟩ := h
    have : (r₁ + r₂ - 1) • (x + y) = 0 := by
      rw [sub_smul, add_smul, one_smul, ← hr₁, ← hr₂, sub_eq_zero]
    cases smul_eq_zero.1 this
    · linarith
    · contradiction
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : angle x y + n • (2 * π) = angle x (x + y) + angle y (x + y)
this_1 : -1 < n
this : n < 1
⊢ angle x y = angle x (x + y) + angle y (x + y)
have h₁ : angle x y + HSMul.hSMul (α := ℤ) 0 (2 * π) = angle x (x + y) + angle y (x + y)
Tactic: obtain rfl : n = 0 := by lia
Cleared hypotheses: n, h, this_1, this
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : angle x y + n • (2 * π) = angle x (x + y) + angle y (x + y)
this_1 : -1 < n
this : n < 1
h₁ : angle x y + HSMul.hSMul (α := ℤ) 0 (2 * π) = angle x (x + y) + angle y (x + y)
⊢ angle x y = angle x (x + y) + angle y (x + y)
have this₁ : LT.lt (α := ℤ) (-1) 0
Tactic: obtain rfl : n = 0 := by lia
Cleared hypotheses: n, h, this_1, this
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h_1 : (↑(angle x y) : Real.Angle) = (↑(angle x (x + y) + angle y (x + y)) : Real.Angle)
n : ℤ
h : angle x y + n • (2 * π) = angle x (x + y) + angle y (x + y)
this_1 : -1 < n
this : n < 1
h₁ : angle x y + HSMul.hSMul (α := ℤ) 0 (2 * π) = angle x (x + y) + angle y (x + y)
this₁ : LT.lt (α := ℤ) (-1) 0
⊢ angle x y = angle x (x + y) + angle y (x + y)
have this₂ : LT.lt (α := ℤ) 0 1
Tactic: obtain rfl : n = 0 := by lia
Cleared hypotheses: n, h, this_1, this
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
⊢ angle x y + angle x (x - y) + angle y (y - x) = π
have h : angle (x - y) y = angle (x - y) (x - y + y) + angle y (x - y + y)
Tactic: have h := angle_eq_angle_add_add_angle_add (x - y) hy
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
h : angle (x - y) y = angle (x - y) (x - y + y) + angle y (x - y + y)
⊢ angle x y + angle x (x - y) + angle y (y - x) = π
have h₁ : angle (x - y) y = angle (x - y) x + angle y x
Tactic: rw [sub_add_cancel] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
h : angle (x - y) y = angle (x - y) x + angle y x
⊢ angle x y + angle x (x - y) + angle y (y - x) = π
have rw : angle x y + angle x (x - y) + (π - angle y (x - y)) = π
Tactic: rw [← neg_sub x y, angle_neg_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
h : angle (x - y) y = angle (x - y) x + angle y x
⊢ angle x y + angle x (x - y) + (π - angle y (x - y)) = π
have h₁ : angle y (x - y) = angle x (x - y) + angle x y
Tactic: simp only [angle_comm] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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 : HSMul.hSMul (α := ℤ) 2 (o.oangle x (x - y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
⊢ ‖x‖ = ‖y‖
have hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
Tactic: have hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign := by simp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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 : HSMul.hSMul (α := ℤ) 2 (o.oangle x (x - y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
⊢ ‖x‖ = ‖y‖
have h₁ : o.oangle x (x - y) = o.oangle (y - x) y ∨ o.oangle x (x - y) = o.oangle (y - x) y + (↑π : Real.Angle)
Tactic: rw [Real.Angle.two_zsmul_eq_iff] at h
Cleared hypotheses: h, h0, hpi, hs
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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 (x - y) = o.oangle (y - x) y ∨ o.oangle x (x - y) = o.oangle (y - x) y + (↑π : Real.Angle)
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
⊢ ‖x‖ = ‖y‖
have inl : ∀ (h : o.oangle x (x - y) = o.oangle (y - x) y), ‖x‖ = ‖y‖
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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 (x - y) = o.oangle (y - x) y ∨ o.oangle x (x - y) = o.oangle (y - x) y + (↑π : Real.Angle)
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
inl : ∀ (h : o.oangle x (x - y) = o.oangle (y - x) y), ‖x‖ = ‖y‖
⊢ ‖x‖ = ‖y‖
have inr : ∀ (h : o.oangle x (x - y) = o.oangle (y - x) y + (↑π : Real.Angle)), ‖x‖ = ‖y‖
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : o.oangle x (x - y) = o.oangle (y - x) y
⊢ ‖x‖ = ‖y‖
have h₁ : angle x (x - y) = angle y (y - x)
Tactic: rw [← o.angle_eq_iff_oangle_eq_of_sign_eq (o.left_ne_zero_of_oangle_ne_zero h0)
      (sub_ne_zero_of_ne (o.ne_of_oangle_ne_zero h0))
      (sub_ne_zero_of_ne (o.ne_of_oangle_ne_zero h0).symm)
      (o.right_ne_zero_of_oangle_ne_zero h0) hs, angle_comm (y - x)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : angle x (x - y) = angle y (y - x)
⊢ ‖x‖ = ‖y‖
have inl : angle x y ≠ π
Tactic: refine norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi h ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : angle x (x - y) = angle y (y - x)
⊢ angle x y ≠ π
have inl : ¬o.oangle x y = (↑π : Real.Angle)
Tactic: rw [ne_eq, ← o.oangle_eq_pi_iff_angle_eq_pi]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (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
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ (↑π : Real.Angle)
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : o.oangle x (x - y) = o.oangle (y - x) y + (↑π : Real.Angle)
⊢ ‖x‖ = ‖y‖
have hs₁ : o.oangle x y = 0 ∨ o.oangle x y = (↑π : Real.Angle)
Tactic: rw [h, Real.Angle.sign_add_pi, SignType.neg_eq_self_iff, oangle_sign_sub_left_swap,
      o.oangle_rev, Real.Angle.sign_neg, SignType.neg_eq_zero_iff,
      Real.Angle.sign_eq_zero_iff] at hs
Cleared hypotheses: hs, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ dist p₁ p₃ * dist p₁ p₃ =
    dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ - 2 * dist p₁ p₂ * dist p₃ p₂ * Real.cos (∠ p₁ p₂ p₃)
have rw : ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ =
  ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ - 2 * ‖p₁ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ * Real.cos (∠ p₁ p₂ p₃)
Tactic: rw [dist_eq_norm_vsub V p₁ p₃, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₃ p₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ =
    ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ -
      2 * ‖p₁ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖ * Real.cos (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂))
have h : p₁ -ᵥ p₃ = p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)
Tactic: convert!
    norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle (p₁ -ᵥ p₂ : V)
      (p₃ -ᵥ p₂ : V)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ Real.sin (∠ p₁ p₂ p₃) * dist p₂ p₃ = Real.sin (∠ p₃ p₁ p₂) * dist p₃ p₁
have simp : Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) * dist p₃ p₂ =
  Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁)) * dist p₃ p₁
Tactic: simp only [dist_comm p₂ p₃, angle]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) * dist p₃ p₂ =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁)) * dist p₃ p₁
have rw : Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₁)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁)) ∨
  ‖p₃ -ᵥ p₁‖ = 0
Tactic: rw [dist_eq_norm_vsub V p₃ p₂, dist_eq_norm_vsub V p₃ p₁, InnerProductGeometry.angle_comm,
    sin_angle_mul_norm_eq_sin_angle_mul_norm, vsub_sub_vsub_cancel_right, mul_eq_mul_right_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₁)) =
      Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁)) ∨
    ‖p₃ -ᵥ p₁‖ = 0
have h : Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₁)) =
  Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁))
Tactic: left
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Triangle (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₁)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁))
have h : Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
  Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁))
Tactic: rw [InnerProductGeometry.angle_comm, ← neg_vsub_eq_vsub_rev p₁ p₂, angle_neg_right,
    Real.sin_pi_sub]