awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₂.center s₁.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
neg :
  Membership.mem (α := P) s₁
    ((AffineMap.lineMap s₂.center s₁.center : (a : ℝ) → P) (s₂.radius / (s₂.radius - s₁.radius)) : P)
neg₁ :
  Membership.mem (α := P) s₂
    ((AffineMap.lineMap s₂.center s₁.center : (a : ℝ) → P) (s₂.radius / (s₂.radius - s₁.radius)) : P)
⊢ s₁.IsIntTangent s₂
have neg₂ : Wbtw ℝ s₂.center s₁.center ((AffineMap.lineMap s₂.center s₁.center : (a : ℝ) → P) (s₂.radius / (s₂.radius - s₁.radius)))
Tactic: refine ⟨AffineMap.lineMap s₂.center s₁.center (s₂.radius / (s₂.radius - s₁.radius)),
              ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₂.center s₁.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
⊢ Membership.mem (α := P) s₁
    ((AffineMap.lineMap s₂.center s₁.center : (a : ℝ) → P) (s₂.radius / (s₂.radius - s₁.radius)) : P)
have neg : s₁.radius / (s₂.radius - s₁.radius) * (s₂.radius - s₁.radius) = s₁.radius
Tactic: simp only [mem_sphere, dist_lineMap_right, Real.norm_eq_abs, h, one_sub_div hr0, abs_div,
          sub_sub_cancel_left, abs_neg, abs_of_nonneg h₁, ha]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₂.center s₁.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
⊢ Membership.mem (α := P) s₂
    ((AffineMap.lineMap s₂.center s₁.center : (a : ℝ) → P) (s₂.radius / (s₂.radius - s₁.radius)) : P)
have neg : s₂.radius / (s₂.radius - s₁.radius) * (s₂.radius - s₁.radius) = s₂.radius
Tactic: simp only [mem_sphere, dist_lineMap_left, norm_div, Real.norm_eq_abs, h, ha,
          abs_of_nonneg h₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₂.center s₁.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
⊢ Wbtw ℝ s₂.center s₁.center
    ((AffineMap.lineMap s₂.center s₁.center : (a : ℝ) → P) (s₂.radius / (s₂.radius - s₁.radius)))
have neg : s₂.center = s₁.center ∨
  Membership.mem.{u_2, u_2} (α := P) (γ := Set P)
    (Set.image (α := ℝ) (⇑(AffineMap.lineMap s₂.center s₁.center) : (a : ℝ) → P) (Set.Ici 1))
    ((AffineMap.lineMap s₂.center s₁.center : (a : ℝ) → P) (s₂.radius / (s₂.radius - s₁.radius)) : P)
Tactic: rw [wbtw_iff_left_eq_or_right_mem_image_Ici]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₂.center s₁.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
⊢ s₂.center = s₁.center ∨
    Membership.mem.{u_2, u_2} (α := P) (γ := Set P)
      (Set.image (α := ℝ) (⇑(AffineMap.lineMap s₂.center s₁.center) : (a : ℝ) → P) (Set.Ici 1))
      ((AffineMap.lineMap s₂.center s₁.center : (a : ℝ) → P) (s₂.radius / (s₂.radius - s₁.radius)) : P)
have neg : 1 ≤ s₂.radius / (s₂.radius - s₁.radius)
Tactic: simp only [Ne.symm h0, Set.mem_image, Set.mem_Ici, AffineMap.lineMap_eq_lineMap_iff,
          false_or, exists_eq_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₂.center s₁.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
⊢ 1 ≤ s₂.radius / (s₂.radius - s₁.radius)
have neg : s₂.radius - s₁.radius ≤ s₂.radius
Tactic: rw [one_le_div]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₂.center s₁.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
neg : s₂.radius - s₁.radius ≤ s₂.radius
⊢ 1 ≤ s₂.radius / (s₂.radius - s₁.radius)
have neg₁ : 0 < s₂.radius - s₁.radius
Tactic: rw [one_le_div]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₂.center s₁.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
⊢ s₂.radius - s₁.radius ≤ s₂.radius
have linarith : s₂.radius < s₂.radius - s₁.radius → 0 - s₁.radius + (s₂.radius - (s₂.radius - s₁.radius)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
inst_4 : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₂.center s₁.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
⊢ 0 < s₂.radius - s₁.radius
have neg : 0 < dist s₂.center s₁.center
Tactic: rw [← 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
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y)
have rw : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖))
Tactic: rw [show 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y) = 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖)) by ring,
    cos_angle_mul_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, ←
    real_inner_self_eq_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, real_inner_sub_sub_self,
    sub_add_eq_add_sub]
-- 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
rw : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖))
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y)
have rw₁ : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
Tactic: rw [show 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y) = 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖)) by ring,
    cos_angle_mul_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, ←
    real_inner_self_eq_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, real_inner_sub_sub_self,
    sub_add_eq_add_sub]
-- 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
rw : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖))
rw₁ : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y)
have rw₂ : ⟪x - y, x - y⟫ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
Tactic: rw [show 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y) = 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖)) by ring,
    cos_angle_mul_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, ←
    real_inner_self_eq_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, real_inner_sub_sub_self,
    sub_add_eq_add_sub]
-- 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
rw : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖))
rw₁ : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
rw₂ : ⟪x - y, x - y⟫ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y)
have rw₃ : ⟪x - y, x - y⟫ = ⟪x, x⟫ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
Tactic: rw [show 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y) = 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖)) by ring,
    cos_angle_mul_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, ←
    real_inner_self_eq_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, real_inner_sub_sub_self,
    sub_add_eq_add_sub]
-- 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
rw : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖))
rw₁ : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
rw₂ : ⟪x - y, x - y⟫ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
rw₃ : ⟪x - y, x - y⟫ = ⟪x, x⟫ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y)
have rw₄ : ⟪x - y, x - y⟫ = ⟪x, x⟫ + ⟪y, y⟫ - 2 * ⟪x, y⟫
Tactic: rw [show 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y) = 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖)) by ring,
    cos_angle_mul_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, ←
    real_inner_self_eq_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, real_inner_sub_sub_self,
    sub_add_eq_add_sub]
-- 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
rw : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖))
rw₁ : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
rw₂ : ⟪x - y, x - y⟫ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
rw₃ : ⟪x - y, x - y⟫ = ⟪x, x⟫ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
rw₄ : ⟪x - y, x - y⟫ = ⟪x, x⟫ + ⟪y, y⟫ - 2 * ⟪x, y⟫
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y)
have rw₅ : ⟪x, x⟫ - 2 * ⟪x, y⟫ + ⟪y, y⟫ = ⟪x, x⟫ + ⟪y, y⟫ - 2 * ⟪x, y⟫
Tactic: rw [show 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y) = 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖)) by ring,
    cos_angle_mul_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, ←
    real_inner_self_eq_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, real_inner_sub_sub_self,
    sub_add_eq_add_sub]
-- 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
rw : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖))
rw₁ : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
rw₂ : ⟪x - y, x - y⟫ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
rw₃ : ⟪x - y, x - y⟫ = ⟪x, x⟫ + ‖y‖ * ‖y‖ - 2 * ⟪x, y⟫
rw₄ : ⟪x - y, x - y⟫ = ⟪x, x⟫ + ⟪y, y⟫ - 2 * ⟪x, y⟫
rw₅ : ⟪x, x⟫ - 2 * ⟪x, y⟫ + ⟪y, y⟫ = ⟪x, x⟫ + ⟪y, y⟫ - 2 * ⟪x, y⟫
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y)
have rw₆ : ⟪x, x⟫ + ⟪y, y⟫ - 2 * ⟪x, y⟫ = ⟪x, x⟫ + ⟪y, y⟫ - 2 * ⟪x, y⟫
Tactic: rw [show 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y) = 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖)) by ring,
    cos_angle_mul_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, ←
    real_inner_self_eq_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, real_inner_sub_sub_self,
    sub_add_eq_add_sub]
-- 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
⊢ Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖
have inl : Real.sin (angle x 0) * ‖x‖ = Real.sin (angle 0 (x - 0)) * ‖x - 0‖
Tactic: obtain rfl | hy := eq_or_ne y 0
Cleared hypotheses: y
-- 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
inl : Real.sin (angle x 0) * ‖x‖ = Real.sin (angle 0 (x - 0)) * ‖x - 0‖
⊢ Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖
have inr : ∀ (hy : y ≠ 0), Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖
Tactic: obtain rfl | hy := eq_or_ne y 0
-- 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
⊢ Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖
have inr : Real.sin (angle 0 y) * norm.{u_1} (E := V) 0 = Real.sin (angle y (0 - y)) * ‖0 - y‖
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- 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
inr : Real.sin (angle 0 y) * norm.{u_1} (E := V) 0 = Real.sin (angle y (0 - y)) * ‖0 - y‖
⊢ Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖
have inr₁ : ∀ (hx : x ≠ 0), Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖
Tactic: obtain rfl | hx := eq_or_ne x 0
-- 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
⊢ Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖
have inr : ∀ (hy : x ≠ 0), Real.sin (angle x x) * ‖x‖ = Real.sin (angle x (x - x)) * ‖x - x‖
Tactic: obtain rfl | hxy := eq_or_ne x y
Cleared hypotheses: y, hy
-- 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
inr : ∀ (hy : x ≠ 0), Real.sin (angle x x) * ‖x‖ = Real.sin (angle x (x - x)) * ‖x - x‖
⊢ Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖
have inr₁ : ∀ (hxy : x ≠ y), Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖
Tactic: obtain rfl | hxy := eq_or_ne x y
-- 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
hxy : x ≠ y
⊢ Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖
have h_sin : ∀ (x y : V) (hx : x ≠ 0) (hy : y ≠ 0), Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)
Tactic: have h_sin (x y : V) (hx : x ≠ 0) (hy : y ≠ 0) :
      Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) := by
    simp [field, mul_assoc, sin_angle_mul_norm_mul_norm]
-- 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
hxy : x ≠ y
h_sin : ∀ (x y : V) (hx : x ≠ 0) (hy : y ≠ 0), Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)
⊢ Real.sin (angle x y) * ‖x‖ = Real.sin (angle y (x - y)) * ‖x - y‖
have inr : √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) * ‖x‖ =
  √(⟪y, y⟫ * ⟪x - y, x - y⟫ - ⟪y, x - y⟫ * ⟪y, x - y⟫) / (‖y‖ * ‖x - y‖) * ‖x - y‖
Tactic: rw [h_sin x y hx hy, h_sin y (x - y) hy (sub_ne_zero_of_ne hxy)]
-- 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
hxy : x ≠ y
h_sin : ∀ (x y : V) (hx : x ≠ 0) (hy : y ≠ 0), Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)
⊢ √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) * ‖x‖ =
    √(⟪y, y⟫ * ⟪x - y, x - y⟫ - ⟪y, x - y⟫ * ⟪y, x - y⟫) / (‖y‖ * ‖x - y‖) * ‖x - y‖
have inr : √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) * ‖x‖ =
  √(⟪y, y⟫ * (⟪x, x⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪y, y⟫)) - (⟪x, y⟫ - ⟪y, y⟫) * (⟪x, y⟫ - ⟪y, y⟫)) / (‖y‖ * ‖x - y‖) * ‖x - y‖
Tactic: simp only [inner_sub_left, inner_sub_right, real_inner_comm x y]
-- 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
hxy : x ≠ y
h_sin : ∀ (x y : V) (hx : x ≠ 0) (hy : y ≠ 0), Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)
⊢ √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) * ‖x‖ =
    √(⟪y, y⟫ * (⟪x, x⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪y, y⟫)) - (⟪x, y⟫ - ⟪y, y⟫) * (⟪x, y⟫ - ⟪y, y⟫)) / (‖y‖ * ‖x - y‖) *
      ‖x - y‖
have hsub : x - y ≠ 0
Tactic: have hsub : x - y ≠ 0 := sub_ne_zero_of_ne hxy
-- 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
hxy : x ≠ y
h_sin : ∀ (x y : V) (hx : x ≠ 0) (hy : y ≠ 0), Real.sin (angle x y) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖)
hsub : x - y ≠ 0
⊢ √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫) / (‖x‖ * ‖y‖) * ‖x‖ =
    √(⟪y, y⟫ * (⟪x, x⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪y, y⟫)) - (⟪x, y⟫ - ⟪y, y⟫) * (⟪x, y⟫ - ⟪y, y⟫)) / (‖y‖ * ‖x - y‖) *
      ‖x - y‖
have inr : √(⟪x, x⟫ * ⟪y, y⟫ - HPow.hPow (β := ℕ) ⟪x, y⟫ 2) =
  √(⟪y, y⟫ * (⟪x, x⟫ - ⟪x, y⟫ - (⟪x, y⟫ - ⟪y, y⟫)) - HPow.hPow (β := ℕ) (⟪x, y⟫ - ⟪y, y⟫) 2)
Tactic: field_simp
-- 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
h : ‖x‖ = ‖y‖
⊢ angle x (x - y) = angle y (y - x)
have refine : Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))
Tactic: refine Real.injOn_cos ⟨angle_nonneg _ _, angle_le_pi _ _⟩ ⟨angle_nonneg _ _, angle_le_pi _ _⟩ ?_
-- 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
h : ‖x‖ = ‖y‖
⊢ Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))
have rw : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = Real.cos (angle y (y - x))
Tactic: rw [cos_angle, cos_angle, h, ← neg_sub, norm_neg, neg_sub, inner_sub_right, inner_sub_right,
    real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_mul_norm, h, real_inner_comm x y]
-- 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
h : ‖x‖ = ‖y‖
rw : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = Real.cos (angle y (y - x))
⊢ Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))
have rw₁ : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
Tactic: rw [cos_angle, cos_angle, h, ← neg_sub, norm_neg, neg_sub, inner_sub_right, inner_sub_right,
    real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_mul_norm, h, real_inner_comm x y]
-- 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
h : ‖x‖ = ‖y‖
rw : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = Real.cos (angle y (y - x))
rw₁ : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
⊢ Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))
have rw₂ : ⟪x, x - y⟫ / (‖y‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
Tactic: rw [cos_angle, cos_angle, h, ← neg_sub, norm_neg, neg_sub, inner_sub_right, inner_sub_right,
    real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_mul_norm, h, real_inner_comm x y]
-- 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
h : ‖x‖ = ‖y‖
rw : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = Real.cos (angle y (y - x))
rw₁ : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₂ : ⟪x, x - y⟫ / (‖y‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
⊢ Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))
have rw₃ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖-(y - x)‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
Tactic: rw [cos_angle, cos_angle, h, ← neg_sub, norm_neg, neg_sub, inner_sub_right, inner_sub_right,
    real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_mul_norm, h, real_inner_comm x y]
-- 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
h : ‖x‖ = ‖y‖
rw : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = Real.cos (angle y (y - x))
rw₁ : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₂ : ⟪x, x - y⟫ / (‖y‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₃ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖-(y - x)‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
⊢ Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))
have rw₄ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
Tactic: rw [cos_angle, cos_angle, h, ← neg_sub, norm_neg, neg_sub, inner_sub_right, inner_sub_right,
    real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_mul_norm, h, real_inner_comm x y]
-- 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
h : ‖x‖ = ‖y‖
rw : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = Real.cos (angle y (y - x))
rw₁ : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₂ : ⟪x, x - y⟫ / (‖y‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₃ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖-(y - x)‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₄ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
⊢ Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))
have rw₅ : ⟪x, x - y⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
Tactic: rw [cos_angle, cos_angle, h, ← neg_sub, norm_neg, neg_sub, inner_sub_right, inner_sub_right,
    real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_mul_norm, h, real_inner_comm x y]
-- 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
h : ‖x‖ = ‖y‖
rw : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = Real.cos (angle y (y - x))
rw₁ : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₂ : ⟪x, x - y⟫ / (‖y‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₃ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖-(y - x)‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₄ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₅ : ⟪x, x - y⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
⊢ Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))
have rw₆ : (⟪x, x⟫ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
Tactic: rw [cos_angle, cos_angle, h, ← neg_sub, norm_neg, neg_sub, inner_sub_right, inner_sub_right,
    real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_mul_norm, h, real_inner_comm x y]
-- 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
h : ‖x‖ = ‖y‖
rw : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = Real.cos (angle y (y - x))
rw₁ : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₂ : ⟪x, x - y⟫ / (‖y‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₃ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖-(y - x)‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₄ : ⟪x, -(y - x)⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₅ : ⟪x, x - y⟫ / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
rw₆ : (⟪x, x⟫ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
⊢ Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))
have rw₇ : (⟪x, x⟫ - ⟪x, y⟫) / (‖y‖ * ‖y - x‖) = (⟪y, y⟫ - ⟪y, x⟫) / (‖y‖ * ‖y - x‖)
Tactic: rw [cos_angle, cos_angle, h, ← neg_sub, norm_neg, neg_sub, inner_sub_right, inner_sub_right,
    real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_mul_norm, h, real_inner_comm x y]