awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : p₁ = p₄
hl : ¬Collinear ℝ (P := P) {p₂, p₃, p₄}
neg : Cospherical (P := P) {p₂, p₃, p₄}
⊢ Cospherical (P := P) {p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₂, p₃, p₄}

Tactic:
rw [or_iff_left hl]

Premises used: or_iff_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : p₁ = p₄
hl : ¬Collinear ℝ (P := P) {p₂, p₃, p₄}
t : Affine.Triangle ℝ P := { points := ![p₂, p₃, p₄], independent := ⋯ }
neg : ∃ (s : Sphere P), {p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius
⊢ Cospherical (P := P) {p₂, p₃, p₄}

Tactic:
rw [cospherical_iff_exists_sphere]

Premises used: EuclideanGeometry.cospherical_iff_exists_sphere
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : p₁ = p₄
hl : ¬Collinear ℝ (P := P) {p₂, p₃, p₄}
t : Affine.Triangle ℝ P := { points := ![p₂, p₃, p₄], independent := ⋯ }
⊢ ∃ (s : Sphere P), {p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius

Tactic:
⟨t.circumsphere, ?_⟩

Premises used: Affine.Simplex.circumsphere, Exists.intro
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : p₁ = p₄
hl : ¬Collinear ℝ (P := P) {p₂, p₃, p₄}
t : Affine.Triangle ℝ P := { points := ![p₂, p₃, p₄], independent := ⋯ }
neg : {p₂, p₃, p₄} ⊆ Metric.sphere (Affine.Simplex.circumsphere t).center (Affine.Simplex.circumsphere t).radius
⊢ ∃ (s : Sphere P), {p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius

Tactic:
refine ⟨t.circumsphere, ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : p₁ = p₄
hl : ¬Collinear ℝ (P := P) {p₂, p₃, p₄}
t : Affine.Triangle ℝ P := { points := ![p₂, p₃, p₄], independent := ⋯ }
neg :
  p₂ ∈ Metric.sphere (Affine.Simplex.circumsphere t).center (Affine.Simplex.circumsphere t).radius ∧
    p₃ ∈ Metric.sphere (Affine.Simplex.circumsphere t).center (Affine.Simplex.circumsphere t).radius ∧
      p₄ ∈ Metric.sphere (Affine.Simplex.circumsphere t).center (Affine.Simplex.circumsphere t).radius
⊢ {p₂, p₃, p₄} ⊆ Metric.sphere (Affine.Simplex.circumsphere t).center (Affine.Simplex.circumsphere t).radius

Tactic:
simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Set.insert_subset_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : p₁ = p₄
hl : ¬Collinear ℝ (P := P) {p₂, p₃, p₄}
t : Affine.Triangle ℝ P := { points := ![p₂, p₃, p₄], independent := ⋯ }
⊢ p₂ ∈ Metric.sphere (Affine.Simplex.circumsphere t).center (Affine.Simplex.circumsphere t).radius ∧
    p₃ ∈ Metric.sphere (Affine.Simplex.circumsphere t).center (Affine.Simplex.circumsphere t).radius ∧
      p₄ ∈ Metric.sphere (Affine.Simplex.circumsphere t).center (Affine.Simplex.circumsphere t).radius

Tactic:
⟨t.mem_circumsphere 0, t.mem_circumsphere 1, t.mem_circumsphere 2⟩

Premises used: Affine.Simplex.mem_circumsphere, And.intro, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : p₁ = p₄
hl : ¬Collinear ℝ (P := P) {p₂, p₃, p₄}
t : Affine.Triangle ℝ P := { points := ![p₂, p₃, p₄], independent := ⋯ }
⊢ p₂ ∈ Metric.sphere (Affine.Simplex.circumsphere t).center (Affine.Simplex.circumsphere t).radius ∧
    p₃ ∈ Metric.sphere (Affine.Simplex.circumsphere t).center (Affine.Simplex.circumsphere t).radius ∧
      p₄ ∈ Metric.sphere (Affine.Simplex.circumsphere t).center (Affine.Simplex.circumsphere t).radius

Tactic:
exact ⟨t.mem_circumsphere 0, t.mem_circumsphere 1, t.mem_circumsphere 2⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : ¬p₁ = p₄
rwa rwa₁ rwa₂ rwa₃ : Collinear ℝ (P := P) {p₁, p₂, p₄}
⊢ Collinear ℝ (P := P) {p₁, p₃, p₄}

Tactic:
rwa [← collinear_iff_of_two_zsmul_oangle_eq h]

Premises used: EuclideanGeometry.collinear_iff_of_two_zsmul_oangle_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : ¬p₁ = p₄
⊢ Collinear ℝ (P := P) {p₁, p₃, p₄}

Tactic:
have hc' : Collinear ℝ ({p₁, p₃, p₄} : Set P) := by
      rwa [← collinear_iff_of_two_zsmul_oangle_eq h]
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : ¬p₁ = p₄
hc' : Collinear ℝ (P := P) {p₁, p₃, p₄}
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}

Tactic:
Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : ¬p₁ = p₄
hc' : Collinear ℝ (P := P) {p₁, p₃, p₄}
neg : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}

Tactic:
refine Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : ¬p₁ = p₄
hc' : Collinear ℝ (P := P) {p₁, p₃, p₄}
⊢ Collinear ℝ (P := P) {p₂, p₁, p₄}

Tactic:
rw [Set.insert_comm p₁ p₂] at hc

Premises used: Set.insert_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : ¬p₁ = p₄
hc' : Collinear ℝ (P := P) {p₁, p₃, p₄}
hc₁ : Collinear ℝ (P := P) {p₂, p₁, p₄}
⊢ ¬p₁ = p₄

Tactic:
rw [Set.insert_comm p₁ p₂] at hc

Premises used: Set.insert_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₄}
he : ¬p₁ = p₄
hc' : Collinear ℝ (P := P) {p₁, p₃, p₄}
hc₁ : Collinear ℝ (P := P) {p₂, p₁, p₄}
he₁ : ¬p₁ = p₄
⊢ Collinear ℝ (P := P) {p₁, p₃, p₄}

Tactic:
rw [Set.insert_comm p₁ p₂] at hc

Premises used: Set.insert_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₂, p₁, p₄}
he : ¬p₁ = p₄
hc' : Collinear ℝ (P := P) {p₁, p₃, p₄}
neg : Collinear ℝ (P := P) {p₂, p₁, p₃, p₄}
neg₁ neg₂ neg₃ neg₄ : Collinear ℝ (P := P) {p₂, p₁, p₄}
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}

Tactic:
rwa [Set.insert_comm p₁ p₂, hc'.collinear_insert_iff_of_ne (Set.mem_insert _ _)
      (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _))) he]

Premises used: Set.mem_singleton, Set.mem_insert_of_mem, Set.insert_comm, Set.mem_insert, Collinear.collinear_insert_iff_of_ne
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}

Tactic:
Or.inl (cospherical_of_two_zsmul_oangle_eq_of_not_collinear h hc)

Premises used: EuclideanGeometry.cospherical_of_two_zsmul_oangle_eq_of_not_collinear, Or.inl
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}

Tactic:
exact Or.inl (cospherical_of_two_zsmul_oangle_eq_of_not_collinear h hc)

Premises used: EuclideanGeometry.cospherical_of_two_zsmul_oangle_eq_of_not_collinear, Or.inl
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
inl :
  ∀ (hc : Cospherical (P := P) {p₁, p₂, p₃, p₄}),
    Concyclic (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
inr :
  ∀ (hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}),
    Concyclic (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
⊢ Concyclic (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}

Tactic:
rcases cospherical_or_collinear_of_two_zsmul_oangle_eq h with (hc | hc)

Premises used: EuclideanGeometry.cospherical_or_collinear_of_two_zsmul_oangle_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Cospherical (P := P) {p₁, p₂, p₃, p₄}
⊢ Concyclic (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}

Tactic:
Or.inl ⟨hc, coplanar_of_fact_finrank_eq_two _⟩

Premises used: coplanar_of_fact_finrank_eq_two, Or.inl, EuclideanGeometry.Concyclic.mk
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Cospherical (P := P) {p₁, p₂, p₃, p₄}
⊢ Concyclic (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}

Tactic:
exact Or.inl ⟨hc, coplanar_of_fact_finrank_eq_two _⟩

Premises used: Or.inl
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
⊢ Concyclic (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}

Tactic:
Or.inr hc

Premises used: Or.inr
-- Module: Mathlib.Geometry.Euclidean.Angle.Sphere
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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₄) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₃ p₄)
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
⊢ Concyclic (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}

Tactic:
exact Or.inr hc

Premises used: 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
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
f : P × P × P → V × V := fun (y : P × P × P) ↦ (y.1 -ᵥ y.2.1, y.2.2 -ᵥ y.2.1)
⊢ (f x).1 ≠ 0

Tactic:
simp [f, hx12]
-- 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
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
f : P × P × P → V × V := fun (y : P × P × P) ↦ (y.1 -ᵥ y.2.1, y.2.2 -ᵥ y.2.1)
⊢ (f x).1 ≠ 0

Tactic:
have hf1 : (f x).1 ≠ 0 := by simp [f, hx12]
-- 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
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
f : P × P × P → V × V := fun (y : P × P × P) ↦ (y.1 -ᵥ y.2.1, y.2.2 -ᵥ y.2.1)
hf1 : (f x).1 ≠ 0
⊢ (f x).2 ≠ 0

Tactic:
simp [f, hx32]
-- 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
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
f : P × P × P → V × V := fun (y : P × P × P) ↦ (y.1 -ᵥ y.2.1, y.2.2 -ᵥ y.2.1)
hf1 : (f x).1 ≠ 0
⊢ (f x).2 ≠ 0

Tactic:
have hf2 : (f x).2 ≠ 0 := by simp [f, hx32]
-- 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
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
f : P × P × P → V × V := fun (y : P × P × P) ↦ (y.1 -ᵥ y.2.1, y.2.2 -ᵥ y.2.1)
hf1 : (f x).1 ≠ 0
hf2 : (f x).2 ≠ 0
⊢ ContinuousAt f x

Tactic:
fun_prop
-- 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
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
f : P × P × P → V × V := fun (y : P × P × P) ↦ (y.1 -ᵥ y.2.1, y.2.2 -ᵥ y.2.1)
hf1 : (f x).1 ≠ 0
hf2 : (f x).2 ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (y : P × P × P) ↦ ∠ y.1 y.2.1 y.2.2) x

Tactic:
exact (InnerProductGeometry.continuousAt_angle hf1 hf2).comp (by fun_prop)

Premises used: ContinuousAt.comp, InnerProductGeometry.continuousAt_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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[ℝ] P₂
p₁ p₂ p₃ : P
simp_rw :
  InnerProductGeometry.angle (VSub.vsub.{u_3, u_4} (P := P₂) ((f : (a : P) → P₂) p₁ : P₂) ((f : (a : P) → P₂) p₂ : P₂))
      (VSub.vsub.{u_3, u_4} (P := P₂) ((f : (a : P) → P₂) p₃ : P₂) ((f : (a : P) → P₂) p₂ : P₂)) =
    InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
simp_rw₁ :
  InnerProductGeometry.angle.{u_3} (V := V₂) ((f.linearIsometry : (a : V) → V₂) (p₁ -ᵥ p₂) : V₂)
      ((f.linearIsometry : (a : V) → V₂) (p₃ -ᵥ p₂) : V₂) =
    InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
⊢ angle.{u_3, u_4} (P := P₂) ((f : (a : P) → P₂) p₁ : P₂) ((f : (a : P) → P₂) p₂ : P₂) ((f : (a : P) → P₂) p₃ : P₂) =
    ∠ p₁ p₂ p₃

Tactic:
simp_rw [angle, ← AffineIsometry.map_vsub, LinearIsometry.angle_map]

Premises used: AffineIsometry.map_vsub, EuclideanGeometry.angle, LinearIsometry.angle_map
-- 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
s : AffineSubspace ℝ P
p₁ p₂ p₃ : ↥s
⊢ ∠ (↑p₁ : P) (↑p₂ : P) (↑p₃ : P) = ∠ p₁ p₂ p₃

Tactic:
haveI : Nonempty s := ⟨p₁⟩
  s.subtypeₐᵢ.angle_map p₁ p₂ p₃

Premises used: Set.Mem, setOf, AffineSubspace.subtypeₐᵢ, AffineIsometry.angle_map
-- 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₃ : P
r : ℝ
h : r ≠ 0
simp_rw :
  InnerProductGeometry.angle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
⊢ ∠ (P := P) ((AffineMap.homothety p r : (a : P) → P) p₁ : P) ((AffineMap.homothety p r : (a : P) → P) p₂ : P)
      ((AffineMap.homothety p r : (a : P) → P) p₃ : P) =
    ∠ p₁ p₂ p₃

Tactic:
simp_rw [angle, ← AffineMap.linearMap_vsub, AffineMap.homothety_linear, LinearMap.smul_apply,
    LinearMap.id_coe, id_eq]

Premises used: LinearMap.smul_apply, LinearMap.id_coe, AffineMap.linearMap_vsub, AffineMap.homothety_linear, EuclideanGeometry.angle, id_eq
-- 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₃ : P
r : ℝ
h : r ≠ 0
inl :
  ∀ (hlt : r < 0),
    InnerProductGeometry.angle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
inr :
  ∀ (hlt : 0 < r),
    InnerProductGeometry.angle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
⊢ InnerProductGeometry.angle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

Tactic:
rcases h.lt_or_gt with hlt | hlt

Premises used: Ne.lt_or_gt
-- 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₃ : P
r : ℝ
h : r ≠ 0
hlt : r < 0
⊢ InnerProductGeometry.angle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

Tactic:
simp [hlt, -neg_vsub_eq_vsub_rev]

Premises used: neg_vsub_eq_vsub_rev
-- 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₃ : P
r : ℝ
h : r ≠ 0
hlt : 0 < r
⊢ InnerProductGeometry.angle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

Tactic:
simp [hlt, -neg_vsub_eq_vsub_rev]

Premises used: neg_vsub_eq_vsub_rev
-- 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
v : V
p₁ p₂ p₃ : P
⊢ ∠ (v +ᵥ p₁) (v +ᵥ p₂) (v +ᵥ p₃) = ∠ p₁ p₂ p₃

Tactic:
(AffineIsometryEquiv.constVAdd ℝ P v).toAffineIsometry.angle_map _ _ _

Premises used: Real, AffineIsometryEquiv.constVAdd, AffineIsometryEquiv.toAffineIsometry, AffineIsometry.angle_map
-- 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
v₁ v₂ v₃ : V
p : P
⊢ ∠ (v₁ +ᵥ p) (v₂ +ᵥ p) (v₃ +ᵥ p) = ∠ v₁ v₂ v₃

Tactic:
(AffineIsometryEquiv.vaddConst ℝ p).toAffineIsometry.angle_map _ _ _

Premises used: Real, AffineIsometryEquiv.toAffineIsometry, AffineIsometryEquiv.vaddConst, AffineIsometry.angle_map
-- 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₃ : P
⊢ ∠ (p -ᵥ p₁) (p -ᵥ p₂) (p -ᵥ p₃) = ∠ p₁ p₂ p₃

Tactic:
(AffineIsometryEquiv.constVSub ℝ p).toAffineIsometry.angle_map _ _ _

Premises used: Real, AffineIsometryEquiv.toAffineIsometry, AffineIsometryEquiv.constVSub, AffineIsometry.angle_map
-- 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 : P
⊢ ∠ (p₁ -ᵥ p) (p₂ -ᵥ p) (p₃ -ᵥ p) = ∠ p₁ p₂ p₃

Tactic:
(AffineIsometryEquiv.vaddConst ℝ p).symm.toAffineIsometry.angle_map _ _ _

Premises used: Real, AffineIsometryEquiv.toAffineIsometry, AffineIsometryEquiv.symm, AffineIsometryEquiv.vaddConst, AffineIsometry.angle_map
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
v₁ v₂ v₃ v : V
⊢ ∠ (v₁ + v) (v₂ + v) (v₃ + v) = ∠ v₁ v₂ v₃

Tactic:
angle_vadd_const _ _ _ _

Premises used: EuclideanGeometry.angle_vadd_const
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
v v₁ v₂ v₃ : V
⊢ ∠ (v + v₁) (v + v₂) (v + v₃) = ∠ v₁ v₂ v₃

Tactic:
angle_const_vadd _ _ _ _

Premises used: EuclideanGeometry.angle_const_vadd
-- Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
v₁ v₂ v₃ v : V
⊢ ∠ (v₁ - v) (v₂ - v) (v₃ - v) = ∠ v₁ v₂ v₃

Tactic:
simpa only [vsub_eq_sub] using angle_vsub_const v₁ v₂ v₃ v

Premises used: EuclideanGeometry.angle_vsub_const, vsub_eq_sub