awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₂
pos : ∀ (h₁₂ : p₁ = p₂), p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
neg : ∀ (h₁₂ : ¬p₁ = p₂), p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
by_cases h₁₂ : p₁ = p₂
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₂
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
Or.inl h₁₂

Premises used: Or.inl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₂
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
exact Or.inl h₁₂

Premises used: Or.inl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₂
pos : ∀ (h₃₂ : p₃ = p₂), p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
neg : ∀ (h₃₂ : ¬p₃ = p₂), p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
by_cases h₃₂ : p₃ = p₂
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₂
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
Or.inr (Or.inl h₃₂)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₂
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
exact Or.inr (Or.inl h₃₂)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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 : ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
rw [or_iff_right h₁₂, or_iff_right h₃₂]

Premises used: or_iff_right
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₃ = π
neg₂ : ∀ (h : Wbtw ℝ p₃ p₁ p₂), ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
⊢ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
rcases h with (h | h | h)
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₂
h₃₂ : ¬p₃ = p₂
h : Wbtw ℝ p₁ p₂ p₃
⊢ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
Or.inr (angle_eq_pi_iff_sbtw.2 ⟨h, Ne.symm h₁₂, Ne.symm h₃₂⟩)

Premises used: Iff.mpr, Ne.symm, And.intro, Or.inr, EuclideanGeometry.angle_eq_pi_iff_sbtw
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₂
h₃₂ : ¬p₃ = p₂
h : Wbtw ℝ p₁ p₂ p₃
⊢ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
exact Or.inr (angle_eq_pi_iff_sbtw.2 ⟨h, Ne.symm h₁₂, Ne.symm h₃₂⟩)

Premises used: Iff.mpr, Ne.symm, And.intro, Or.inr, EuclideanGeometry.angle_eq_pi_iff_sbtw
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₂
h₃₂ : ¬p₃ = p₂
h : Wbtw ℝ p₂ p₃ p₁
⊢ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
Or.inl (h.angle₃₁₂_eq_zero_of_ne h₃₂)

Premises used: Wbtw.angle₃₁₂_eq_zero_of_ne, Or.inl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₂
h₃₂ : ¬p₃ = p₂
h : Wbtw ℝ p₂ p₃ p₁
⊢ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
exact Or.inl (h.angle₃₁₂_eq_zero_of_ne h₃₂)

Premises used: Wbtw.angle₃₁₂_eq_zero_of_ne, Or.inl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₂
h₃₂ : ¬p₃ = p₂
h : Wbtw ℝ p₃ p₁ p₂
⊢ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
Or.inl (h.angle₂₃₁_eq_zero_of_ne h₁₂)

Premises used: Wbtw.angle₂₃₁_eq_zero_of_ne, Or.inl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₂
h₃₂ : ¬p₃ = p₂
h : Wbtw ℝ p₃ p₁ p₂
⊢ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
exact Or.inl (h.angle₂₃₁_eq_zero_of_ne h₁₂)

Premises used: Wbtw.angle₂₃₁_eq_zero_of_ne, Or.inl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₃}
refine_2₃ : ∀ (h : ∠ p₁ p₂ p₃ = π), Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}

Tactic:
rcases h with (rfl | rfl | h | h)

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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
⊢ Collinear ℝ (P := P) {p₁, p₁, p₃}

Tactic:
simpa using collinear_pair ℝ p₁ p₃

Premises used: Real, collinear_pair
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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
⊢ Collinear ℝ (P := P) {p₁, p₃, p₃}

Tactic:
simpa using collinear_pair ℝ p₁ p₃

Premises used: Real, collinear_pair
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁

Tactic:
rw [angle_eq_zero_iff_ne_and_wbtw] at h

Premises used: EuclideanGeometry.angle_eq_zero_iff_ne_and_wbtw
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₃}
refine_2₁ : ∀ (h : Wbtw ℝ p₂ p₃ p₁), Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}

Tactic:
rcases h with (⟨-, h⟩ | ⟨-, h⟩)
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₃
refine_2 : Collinear ℝ (P := P) {p₂, p₁, p₃}
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}

Tactic:
rw [Set.insert_comm]

Premises used: Set.insert_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₃}

Tactic:
h.collinear

Premises used: Wbtw.collinear
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₃}

Tactic:
exact h.collinear

Premises used: Wbtw.collinear
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₁
refine_2 : Collinear ℝ (P := P) {p₂, p₃, p₁}
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}

Tactic:
rw [Set.insert_comm, Set.pair_comm]

Premises used: Set.insert_comm, Set.pair_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₁}

Tactic:
h.collinear

Premises used: Wbtw.collinear
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₁}

Tactic:
exact h.collinear

Premises used: Wbtw.collinear
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₃ = π
⊢ Sbtw ℝ p₁ p₂ p₃

Tactic:
rw [angle_eq_pi_iff_sbtw] at h

Premises used: EuclideanGeometry.angle_eq_pi_iff_sbtw
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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 : Sbtw ℝ p₁ p₂ p₃
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}

Tactic:
h.wbtw.collinear

Premises used: Wbtw.collinear, Sbtw.wbtw
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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 : Sbtw ℝ p₁ p₂ p₃
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}

Tactic:
exact h.wbtw.collinear

Premises used: Wbtw.collinear, Sbtw.wbtw
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₃}

Tactic:
collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi.2 <| Or.inr <| Or.inr <| Or.inl h

Premises used: Iff.mpr, EuclideanGeometry.collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, Or.inl, Or.inr
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₃}

Tactic:
collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi.2 <| Or.inr <| Or.inr <| Or.inr h

Premises used: Iff.mpr, EuclideanGeometry.collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, Or.inr
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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 : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ ∠ p₁ p₂ p₃ ≠ 0

Tactic:
mt collinear_of_angle_eq_zero h

Premises used: EuclideanGeometry.collinear_of_angle_eq_zero, mt
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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 : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ ∠ p₁ p₂ p₃ ≠ π

Tactic:
mt collinear_of_angle_eq_pi h

Premises used: mt, EuclideanGeometry.collinear_of_angle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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 : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ 0 < ∠ p₁ p₂ p₃

Tactic:
(angle_nonneg _ _ _).lt_of_ne (angle_ne_zero_of_not_collinear h).symm

Premises used: Ne.symm, LE.le.lt_of_ne, EuclideanGeometry.angle_ne_zero_of_not_collinear, EuclideanGeometry.angle_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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 : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ ∠ p₁ p₂ p₃ < π

Tactic:
(angle_le_pi _ _ _).lt_of_ne <| angle_ne_pi_of_not_collinear h

Premises used: EuclideanGeometry.angle_le_pi, EuclideanGeometry.angle_ne_pi_of_not_collinear, LE.le.lt_of_ne
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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
⊢ cos (∠ p₁ p₂ p₃) = 1 ↔ ∠ p₁ p₂ p₃ = 0

Tactic:
cos_eq_one_iff_angle_eq_zero

Premises used: InnerProductGeometry.cos_eq_one_iff_angle_eq_zero, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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
⊢ cos (∠ p₁ p₂ p₃) = 0 ↔ ∠ p₁ p₂ p₃ = π / 2

Tactic:
cos_eq_zero_iff_angle_eq_pi_div_two

Premises used: InnerProductGeometry.cos_eq_zero_iff_angle_eq_pi_div_two, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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
⊢ cos (∠ p₁ p₂ p₃) = -1 ↔ ∠ p₁ p₂ p₃ = π

Tactic:
cos_eq_neg_one_iff_angle_eq_pi

Premises used: InnerProductGeometry.cos_eq_neg_one_iff_angle_eq_pi, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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
⊢ sin (∠ p₁ p₂ p₃) = 0 ↔ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π

Tactic:
sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi

Premises used: InnerProductGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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
⊢ sin (∠ p₁ p₂ p₃) = 1 ↔ ∠ p₁ p₂ p₃ = π / 2

Tactic:
sin_eq_one_iff_angle_eq_pi_div_two

Premises used: InnerProductGeometry.sin_eq_one_iff_angle_eq_pi_div_two, EuclideanGeometry.angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₃ = π
rw₁ rw₂ : p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ 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

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]

Premises used: EuclideanGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi, EuclideanGeometry.collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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 : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ 0 < sin (∠ p₁ p₂ p₃)

Tactic:
Real.sin_pos_of_pos_of_lt_pi (angle_pos_of_not_collinear h) (angle_lt_pi_of_not_collinear h)

Premises used: EuclideanGeometry.angle_pos_of_not_collinear, Real.sin_pos_of_pos_of_lt_pi, EuclideanGeometry.angle_lt_pi_of_not_collinear
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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 : ¬Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ sin (∠ p₁ p₂ p₃) ≠ 0

Tactic:
ne_of_gt (sin_pos_of_not_collinear h)

Premises used: ne_of_gt, EuclideanGeometry.sin_pos_of_not_collinear
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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
revert : ∀ (h : sin (∠ p₁ p₂ p₃) = 0), Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃}

Tactic:
revert h
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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
contrapose : ¬Collinear ℝ (P := P) {p₁, p₂, p₃} → ¬sin (∠ p₁ p₂ p₃) = 0
⊢ ∀ (h : sin (∠ p₁ p₂ p₃) = 0), Collinear ℝ (P := P) {p₁, p₂, p₃}

Tactic:
contrapose
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₃} → ¬sin (∠ p₁ p₂ p₃) = 0

Tactic:
sin_ne_zero_of_not_collinear

Premises used: EuclideanGeometry.sin_ne_zero_of_not_collinear
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
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₃} → ¬sin (∠ p₁ p₂ p₃) = 0

Tactic:
exact sin_ne_zero_of_not_collinear

Premises used: EuclideanGeometry.sin_ne_zero_of_not_collinear
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ‖x.1‖ * ‖x.2‖ ≠ 0

Tactic:
simp [*]
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
funProp : ‖x.1‖ * ‖x.2‖ ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (y : V × V) ↦ arccos (⟪y.1, y.2⟫ / (‖y.1‖ * ‖y.2‖))) x

Tactic:
fun_prop (disch := simp [*])
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
⊢ c * c ≠ 0

Tactic:
have : c * c ≠ 0 := mul_ne_zero hc hc
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
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‖))
rw₁₀ rw₁₁ : arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = arccos (⟪x, y⟫ / (‖x‖ * ‖y‖))
⊢ angle (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]

Premises used: Norm.norm, norm_smul, mul_mul_mul_comm, InnerProductGeometry.angle, mul_assoc, inner_smul_right, mul_div_mul_left, abs_mul_abs_self, real_inner_smul_left, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
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‖))
rw₄ rw₅ : arccos (⟪u, v⟫ / (‖u‖ * ‖v‖)) = 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

Tactic:
rw [angle, angle, f.inner_map_map, f.norm_map, f.norm_map]

Premises used: LinearIsometry.norm_map, InnerProductGeometry.angle, LinearIsometry.inner_map_map
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
s : Submodule ℝ V
x y : ↥s
⊢ angle (↑x : V) (↑y : V) = angle x y

Tactic:
s.subtypeₗᵢ.angle_map x y

Premises used: Set.Mem, Submodule.subtypeₗᵢ, LinearIsometry.angle_map
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) = ⟪x, y⟫ / (‖x‖ * ‖y‖)

Tactic:
Real.cos_arccos (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).1
    (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).2

Premises used: abs_le, InnerProductGeometry.angle, abs_real_inner_div_norm_mul_norm_le_one, Real.cos_arccos, And.right, And.left, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
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‖))
rw₁ rw₂ : arccos (⟪y, x⟫ / (‖y‖ * ‖x‖)) = arccos (⟪y, x⟫ / (‖y‖ * ‖x‖))
⊢ arccos (⟪x, y⟫ / (‖x‖ * ‖y‖)) = arccos (⟪y, x⟫ / (‖y‖ * ‖x‖))

Tactic:
rw [real_inner_comm, mul_comm]

Premises used: mul_comm, real_inner_comm