awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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
h : Wbtw ℝ p₁ p₂ p₃ ∨ Wbtw ℝ p₂ p₃ p₁ ∨ Wbtw ℝ p₃ p₁ p₂
h₁₂ : ¬p₁ = p₂
h₃₂ : ¬p₃ = p₂
neg : ∀ (h : Wbtw ℝ p₁ p₂ p₃), ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
neg₁ : ∀ (h : Wbtw ℝ p₂ p₃ p₁), ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
⊢ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
have neg₂ : ∀ (h : Wbtw ℝ p₃ p₁ p₂), ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
Tactic: rcases h with (h | h | h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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
h : p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}
have refine_2 : Collinear ℝ (P := P) {p₁, p₁, p₃}
Tactic: rcases h with (rfl | rfl | h | h)
Cleared hypotheses: p₂, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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
h : p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
refine_2 : Collinear ℝ (P := P) {p₁, p₁, p₃}
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}
have refine_2₁ : Collinear ℝ (P := P) {p₁, p₃, p₃}
Tactic: rcases h with (rfl | rfl | h | h)
Cleared hypotheses: p₂, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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
h : p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
refine_2 : Collinear ℝ (P := P) {p₁, p₁, p₃}
refine_2₁ : Collinear ℝ (P := P) {p₁, p₃, p₃}
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}
have refine_2₂ : ∀ (h : ∠ p₁ p₂ p₃ = 0), Collinear ℝ (P := P) {p₁, p₂, p₃}
Tactic: rcases h with (rfl | rfl | h | h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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
h : p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
refine_2 : Collinear ℝ (P := P) {p₁, p₁, p₃}
refine_2₁ : Collinear ℝ (P := P) {p₁, p₃, p₃}
refine_2₂ : ∀ (h : ∠ p₁ p₂ p₃ = 0), Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}
have refine_2₃ : ∀ (h : ∠ p₁ p₂ p₃ = π), Collinear ℝ (P := P) {p₁, p₂, p₃}
Tactic: rcases h with (rfl | rfl | h | h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (hypothesis)
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
h : ∠ p₁ p₂ p₃ = 0
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}
have h₁ : p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
Tactic: rw [angle_eq_zero_iff_ne_and_wbtw] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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
h : p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}
have refine_2 : ∀ (h : Wbtw ℝ p₂ p₁ p₃), Collinear ℝ (P := P) {p₁, p₂, p₃}
Tactic: rcases h with (⟨-, h⟩ | ⟨-, h⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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
h : p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
refine_2 : ∀ (h : Wbtw ℝ p₂ p₁ p₃), Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}
have refine_2₁ : ∀ (h : Wbtw ℝ p₂ p₃ p₁), Collinear ℝ (P := P) {p₁, p₂, p₃}
Tactic: rcases h with (⟨-, h⟩ | ⟨-, h⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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
h : Wbtw ℝ p₂ p₁ p₃
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}
have refine_2 : Collinear ℝ (P := P) {p₂, p₁, p₃}
Tactic: rw [Set.insert_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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
h : Wbtw ℝ p₂ p₃ p₁
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}
have refine_2 : Collinear ℝ (P := P) {p₂, p₃, p₁}
Tactic: rw [Set.insert_comm, Set.pair_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (hypothesis)
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
h : ∠ p₁ p₂ p₃ = π
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}
have h₁ : Sbtw ℝ p₁ p₂ p₃
Tactic: rw [angle_eq_pi_iff_sbtw] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃} ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ sin (∠ p₁ p₂ p₃) = 0
have rw : Collinear ℝ (P := P) {p₁, p₂, p₃} ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
Tactic: rw [sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi,
    collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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
rw : Collinear ℝ (P := P) {p₁, p₂, p₃} ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃} ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ sin (∠ p₁ p₂ p₃) = 0
have rw₁ : p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
Tactic: rw [sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi,
    collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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
h : sin (∠ p₁ p₂ p₃) = 0
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}
have revert : ∀ (h : sin (∠ p₁ p₂ p₃) = 0), Collinear ℝ (P := P) {p₁, p₂, p₃}
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine (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
⊢ ∀ (h : sin (∠ p₁ p₂ p₃) = 0), Collinear ℝ (P := P) {p₁, p₂, p₃}
have contrapose : ¬Collinear ℝ (P := P) {p₁, p₂, p₃} → ¬sin (∠ p₁ p₂ p₃) = 0
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (y : V × V) ↦ arccos (⟪y.1, y.2⟫ / (‖y.1‖ * ‖y.2‖))) x
have funProp : ‖x.1‖ * ‖x.2‖ ≠ 0
Tactic: fun_prop (disch := simp [*])
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (hypothesis)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
⊢ angle (c • x) (c • y) = angle x y
have this : c * c ≠ 0
Tactic: have : c * c ≠ 0 := mul_ne_zero hc hc
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
⊢ angle (c • x) (c • y) = angle x y
have rw : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = angle x y
Tactic: rw [angle, angle, real_inner_smul_left, inner_smul_right, norm_smul, norm_smul, Real.norm_eq_abs,
    mul_mul_mul_comm _ ‖x‖, abs_mul_abs_self, ← mul_assoc c c, mul_div_mul_left _ _ this]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
rw : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = angle x y
⊢ angle (c • x) (c • y) = angle x y
have rw₁ : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Tactic: rw [angle, angle, real_inner_smul_left, inner_smul_right, norm_smul, norm_smul, Real.norm_eq_abs,
    mul_mul_mul_comm _ ‖x‖, abs_mul_abs_self, ← mul_assoc c c, mul_div_mul_left _ _ this]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
rw : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = angle x y
rw₁ : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
⊢ angle (c • x) (c • y) = angle x y
have rw₂ : arccos (c * ⟪x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Tactic: rw [angle, angle, real_inner_smul_left, inner_smul_right, norm_smul, norm_smul, Real.norm_eq_abs,
    mul_mul_mul_comm _ ‖x‖, abs_mul_abs_self, ← mul_assoc c c, mul_div_mul_left _ _ this]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
rw : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = angle x y
rw₁ : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₂ : arccos (c * ⟪x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
⊢ angle (c • x) (c • y) = angle x y
have rw₃ : arccos (c * (c * ⟪x, y⟫) / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Tactic: rw [angle, angle, real_inner_smul_left, inner_smul_right, norm_smul, norm_smul, Real.norm_eq_abs,
    mul_mul_mul_comm _ ‖x‖, abs_mul_abs_self, ← mul_assoc c c, mul_div_mul_left _ _ this]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
rw : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = angle x y
rw₁ : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₂ : arccos (c * ⟪x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₃ : arccos (c * (c * ⟪x, y⟫) / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
⊢ angle (c • x) (c • y) = angle x y
have rw₄ : arccos (c * (c * ⟪x, y⟫) / (‖c‖ * ‖x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Tactic: rw [angle, angle, real_inner_smul_left, inner_smul_right, norm_smul, norm_smul, Real.norm_eq_abs,
    mul_mul_mul_comm _ ‖x‖, abs_mul_abs_self, ← mul_assoc c c, mul_div_mul_left _ _ this]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
rw : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = angle x y
rw₁ : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₂ : arccos (c * ⟪x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₃ : arccos (c * (c * ⟪x, y⟫) / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₄ : arccos (c * (c * ⟪x, y⟫) / (‖c‖ * ‖x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
⊢ angle (c • x) (c • y) = angle x y
have rw₅ : arccos (c * (c * ⟪x, y⟫) / (‖c‖ * ‖x‖ * (‖c‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Tactic: rw [angle, angle, real_inner_smul_left, inner_smul_right, norm_smul, norm_smul, Real.norm_eq_abs,
    mul_mul_mul_comm _ ‖x‖, abs_mul_abs_self, ← mul_assoc c c, mul_div_mul_left _ _ this]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
rw : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = angle x y
rw₁ : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₂ : arccos (c * ⟪x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₃ : arccos (c * (c * ⟪x, y⟫) / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₄ : arccos (c * (c * ⟪x, y⟫) / (‖c‖ * ‖x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₅ : arccos (c * (c * ⟪x, y⟫) / (‖c‖ * ‖x‖ * (‖c‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
⊢ angle (c • x) (c • y) = angle x y
have rw₆ : arccos (c * (c * ⟪x, y⟫) / (|c| * ‖x‖ * (|c| * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Tactic: rw [angle, angle, real_inner_smul_left, inner_smul_right, norm_smul, norm_smul, Real.norm_eq_abs,
    mul_mul_mul_comm _ ‖x‖, abs_mul_abs_self, ← mul_assoc c c, mul_div_mul_left _ _ this]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
rw : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = angle x y
rw₁ : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₂ : arccos (c * ⟪x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₃ : arccos (c * (c * ⟪x, y⟫) / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₄ : arccos (c * (c * ⟪x, y⟫) / (‖c‖ * ‖x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₅ : arccos (c * (c * ⟪x, y⟫) / (‖c‖ * ‖x‖ * (‖c‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₆ : arccos (c * (c * ⟪x, y⟫) / (|c| * ‖x‖ * (|c| * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
⊢ angle (c • x) (c • y) = angle x y
have rw₇ : arccos (c * (c * ⟪x, y⟫) / (|c| * |c| * (‖x‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Tactic: rw [angle, angle, real_inner_smul_left, inner_smul_right, norm_smul, norm_smul, Real.norm_eq_abs,
    mul_mul_mul_comm _ ‖x‖, abs_mul_abs_self, ← mul_assoc c c, mul_div_mul_left _ _ this]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
rw : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = angle x y
rw₁ : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₂ : arccos (c * ⟪x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₃ : arccos (c * (c * ⟪x, y⟫) / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₄ : arccos (c * (c * ⟪x, y⟫) / (‖c‖ * ‖x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₅ : arccos (c * (c * ⟪x, y⟫) / (‖c‖ * ‖x‖ * (‖c‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₆ : arccos (c * (c * ⟪x, y⟫) / (|c| * ‖x‖ * (|c| * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₇ : arccos (c * (c * ⟪x, y⟫) / (|c| * |c| * (‖x‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
⊢ angle (c • x) (c • y) = angle x y
have rw₈ : arccos (c * (c * ⟪x, y⟫) / (c * c * (‖x‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Tactic: rw [angle, angle, real_inner_smul_left, inner_smul_right, norm_smul, norm_smul, Real.norm_eq_abs,
    mul_mul_mul_comm _ ‖x‖, abs_mul_abs_self, ← mul_assoc c c, mul_div_mul_left _ _ this]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
rw : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = angle x y
rw₁ : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₂ : arccos (c * ⟪x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₃ : arccos (c * (c * ⟪x, y⟫) / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₄ : arccos (c * (c * ⟪x, y⟫) / (‖c‖ * ‖x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₅ : arccos (c * (c * ⟪x, y⟫) / (‖c‖ * ‖x‖ * (‖c‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₆ : arccos (c * (c * ⟪x, y⟫) / (|c| * ‖x‖ * (|c| * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₇ : arccos (c * (c * ⟪x, y⟫) / (|c| * |c| * (‖x‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₈ : arccos (c * (c * ⟪x, y⟫) / (c * c * (‖x‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
⊢ angle (c • x) (c • y) = angle x y
have rw₉ : arccos (c * c * ⟪x, y⟫ / (c * c * (‖x‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Tactic: rw [angle, angle, real_inner_smul_left, inner_smul_right, norm_smul, norm_smul, Real.norm_eq_abs,
    mul_mul_mul_comm _ ‖x‖, abs_mul_abs_self, ← mul_assoc c c, mul_div_mul_left _ _ this]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
this : c * c ≠ 0
rw : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = angle x y
rw₁ : arccos (⟪c • x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₂ : arccos (c * ⟪x, c • y⟫ / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₃ : arccos (c * (c * ⟪x, y⟫) / (‖c • x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₄ : arccos (c * (c * ⟪x, y⟫) / (‖c‖ * ‖x‖ * ‖c • y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₅ : arccos (c * (c * ⟪x, y⟫) / (‖c‖ * ‖x‖ * (‖c‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₆ : arccos (c * (c * ⟪x, y⟫) / (|c| * ‖x‖ * (|c| * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₇ : arccos (c * (c * ⟪x, y⟫) / (|c| * |c| * (‖x‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₈ : arccos (c * (c * ⟪x, y⟫) / (c * c * (‖x‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
rw₉ : arccos (c * c * ⟪x, y⟫ / (c * c * (‖x‖ * ‖y‖))) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
⊢ angle (c • x) (c • y) = angle x y
have rw₁₀ : arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
Tactic: rw [angle, angle, real_inner_smul_left, inner_smul_right, norm_smul, norm_smul, Real.norm_eq_abs,
    mul_mul_mul_comm _ ‖x‖, abs_mul_abs_self, ← mul_assoc c c, mul_div_mul_left _ _ this]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →ₗᵢ[ℝ] F
u v : E
⊢ angle.{u_3} (V := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = angle u v
have rw : arccos
    (inner.{0, u_3} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) /
      (Norm.norm.{u_3} (E := F) ((f : (a : E) → F) u : F) * Norm.norm.{u_3} (E := F) ((f : (a : E) → F) v : F))) =
  angle u v
Tactic: rw [angle, angle, f.inner_map_map, f.norm_map, f.norm_map]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →ₗᵢ[ℝ] F
u v : E
rw :
  arccos
      (inner.{0, u_3} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) /
        (Norm.norm.{u_3} (E := F) ((f : (a : E) → F) u : F) * Norm.norm.{u_3} (E := F) ((f : (a : E) → F) v : F))) =
    angle u v
⊢ angle.{u_3} (V := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = angle u v
have rw₁ : arccos
    (inner.{0, u_3} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) /
      (Norm.norm.{u_3} (E := F) ((f : (a : E) → F) u : F) * Norm.norm.{u_3} (E := F) ((f : (a : E) → F) v : F))) =
  arccos (⟪u, v⟫ / (‖u‖ * ‖v‖))
Tactic: rw [angle, angle, f.inner_map_map, f.norm_map, f.norm_map]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →ₗᵢ[ℝ] F
u v : E
rw :
  arccos
      (inner.{0, u_3} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) /
        (Norm.norm.{u_3} (E := F) ((f : (a : E) → F) u : F) * Norm.norm.{u_3} (E := F) ((f : (a : E) → F) v : F))) =
    angle u v
rw₁ :
  arccos
      (inner.{0, u_3} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) /
        (Norm.norm.{u_3} (E := F) ((f : (a : E) → F) u : F) * Norm.norm.{u_3} (E := F) ((f : (a : E) → F) v : F))) =
    arccos (⟪u, v⟫ / (‖u‖ * ‖v‖))
⊢ angle.{u_3} (V := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = angle u v
have rw₂ : arccos
    (⟪u, v⟫ /
      (Norm.norm.{u_3} (E := F) ((f : (a : E) → F) u : F) * Norm.norm.{u_3} (E := F) ((f : (a : E) → F) v : F))) =
  arccos (⟪u, v⟫ / (‖u‖ * ‖v‖))
Tactic: rw [angle, angle, f.inner_map_map, f.norm_map, f.norm_map]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →ₗᵢ[ℝ] F
u v : E
rw :
  arccos
      (inner.{0, u_3} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) /
        (Norm.norm.{u_3} (E := F) ((f : (a : E) → F) u : F) * Norm.norm.{u_3} (E := F) ((f : (a : E) → F) v : F))) =
    angle u v
rw₁ :
  arccos
      (inner.{0, u_3} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) /
        (Norm.norm.{u_3} (E := F) ((f : (a : E) → F) u : F) * Norm.norm.{u_3} (E := F) ((f : (a : E) → F) v : F))) =
    arccos (⟪u, v⟫ / (‖u‖ * ‖v‖))
rw₂ :
  arccos
      (⟪u, v⟫ /
        (Norm.norm.{u_3} (E := F) ((f : (a : E) → F) u : F) * Norm.norm.{u_3} (E := F) ((f : (a : E) → F) v : F))) =
    arccos (⟪u, v⟫ / (‖u‖ * ‖v‖))
⊢ angle.{u_3} (V := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = angle u v
have rw₃ : arccos (⟪u, v⟫ / (‖u‖ * Norm.norm.{u_3} (E := F) ((f : (a : E) → F) v : F))) = arccos (⟪u, v⟫ / (‖u‖ * ‖v‖))
Tactic: rw [angle, angle, f.inner_map_map, f.norm_map, f.norm_map]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →ₗᵢ[ℝ] F
u v : E
rw :
  arccos
      (inner.{0, u_3} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) /
        (Norm.norm.{u_3} (E := F) ((f : (a : E) → F) u : F) * Norm.norm.{u_3} (E := F) ((f : (a : E) → F) v : F))) =
    angle u v
rw₁ :
  arccos
      (inner.{0, u_3} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) /
        (Norm.norm.{u_3} (E := F) ((f : (a : E) → F) u : F) * Norm.norm.{u_3} (E := F) ((f : (a : E) → F) v : F))) =
    arccos (⟪u, v⟫ / (‖u‖ * ‖v‖))
rw₂ :
  arccos
      (⟪u, v⟫ /
        (Norm.norm.{u_3} (E := F) ((f : (a : E) → F) u : F) * Norm.norm.{u_3} (E := F) ((f : (a : E) → F) v : F))) =
    arccos (⟪u, v⟫ / (‖u‖ * ‖v‖))
rw₃ : arccos (⟪u, v⟫ / (‖u‖ * Norm.norm.{u_3} (E := F) ((f : (a : E) → F) v : F))) = arccos (⟪u, v⟫ / (‖u‖ * ‖v‖))
⊢ angle.{u_3} (V := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = angle u v
have rw₄ : arccos (⟪u, v⟫ / (‖u‖ * ‖v‖)) = arccos (⟪u, v⟫ / (‖u‖ * ‖v‖))
Tactic: rw [angle, angle, f.inner_map_map, f.norm_map, f.norm_map]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = arccos (⟪y, x⟫ / (‖y‖ * ‖x‖))
have rw : arccos (⟪y, x⟫ / (‖x‖ * ‖y‖)) = arccos (⟪y, x⟫ / (‖y‖ * ‖x‖))
Tactic: rw [real_inner_comm, mul_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
rw : arccos (⟪y, x⟫ / (‖x‖ * ‖y‖)) = arccos (⟪y, x⟫ / (‖y‖ * ‖x‖))
⊢ arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = arccos (⟪y, x⟫ / (‖y‖ * ‖x‖))
have rw₁ : arccos (⟪y, x⟫ / (‖y‖ * ‖x‖)) = arccos (⟪y, x⟫ / (‖y‖ * ‖x‖))
Tactic: rw [real_inner_comm, mul_comm]