awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
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₄)
pos :
  ∀ (hc : Collinear ℝ (P := P) {p₁, p₂, p₄}),
    Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
have neg : ∀ (hc : ¬Collinear ℝ (P := P) {p₁, p₂, p₄}),
  Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
Tactic: by_cases hc : Collinear ℝ ({p₁, p₂, p₄} : Set P)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
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₄}
have pos : ∀ (he : p₁ = p₄), Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
Tactic: by_cases he : p₁ = p₄
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
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₄}
pos : ∀ (he : p₁ = p₄), Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
have neg : ∀ (he : ¬p₁ = p₄), Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
Tactic: by_cases he : p₁ = p₄
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
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₄
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
have pos : Cospherical (P := P) {p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₂, p₃, p₄}
Tactic: rw [he, Set.insert_eq_self.2
        (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_singleton _)))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
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₄
⊢ Cospherical (P := P) {p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₂, p₃, p₄}
have pos : ∀ (hl : Collinear ℝ (P := P) {p₂, p₃, p₄}), Cospherical (P := P) {p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₂, p₃, p₄}
Tactic: by_cases hl : Collinear ℝ ({p₂, p₃, p₄} : Set P)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
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₄
pos : ∀ (hl : Collinear ℝ (P := P) {p₂, p₃, p₄}), Cospherical (P := P) {p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₂, p₃, p₄}
⊢ Cospherical (P := P) {p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₂, p₃, p₄}
have neg : ∀ (hl : ¬Collinear ℝ (P := P) {p₂, p₃, p₄}), Cospherical (P := P) {p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₂, p₃, p₄}
Tactic: by_cases hl : Collinear ℝ ({p₂, p₃, p₄} : Set P)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
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₄}
⊢ Cospherical (P := P) {p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₂, p₃, p₄}
have neg : Cospherical (P := P) {p₂, p₃, p₄}
Tactic: rw [or_iff_left hl]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
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 := ⋯ }
⊢ Cospherical (P := P) {p₂, p₃, p₄}
have neg : ∃ (s : Sphere P), {p₂, p₃, p₄} ⊆ Metric.sphere s.center s.radius
Tactic: rw [cospherical_iff_exists_sphere]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
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
have neg : {p₂, p₃, p₄} ⊆ Metric.sphere (Affine.Simplex.circumsphere t).center (Affine.Simplex.circumsphere t).radius
Tactic: refine ⟨t.circumsphere, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
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₂, p₃, p₄} ⊆ Metric.sphere (Affine.Simplex.circumsphere t).center (Affine.Simplex.circumsphere t).radius
have 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
Tactic: simp_rw [Set.insert_subset_iff, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
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₄
⊢ Cospherical (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
have hc' : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
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₄}
have neg : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
Tactic: refine Or.inr ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
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₃, p₄}
have hc₁ : Collinear ℝ (P := P) {p₂, p₁, p₄}
Tactic: rw [Set.insert_comm p₁ p₂] at hc
Cleared hypotheses: hc, he, hc'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
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₃, p₄}
have neg : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
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₄)
⊢ Concyclic (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
have inl : ∀ (hc : Cospherical (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)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
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₄}
⊢ Concyclic (P := P) {p₁, p₂, p₃, p₄} ∨ Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
have inr : ∀ (hc : 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)
-- 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
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)
⊢ ContinuousAt (Y := ℝ) (fun (y : P × P × P) ↦ ∠ y.1 y.2.1 y.2.2) x
have hf1 : (f x).1 ≠ 0
Tactic: have hf1 : (f x).1 ≠ 0 := by simp [f, hx12]
-- 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
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
⊢ ContinuousAt (Y := ℝ) (fun (y : P × P × P) ↦ ∠ y.1 y.2.1 y.2.2) x
have hf2 : (f x).2 ≠ 0
Tactic: have hf2 : (f x).2 ≠ 0 := by simp [f, hx32]
-- 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
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
⊢ 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₃
have 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₂)
Tactic: simp_rw [angle, ← AffineIsometry.map_vsub, LinearIsometry.angle_map]
-- 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
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₂)
⊢ 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₃
have 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₂)
Tactic: simp_rw [angle, ← AffineIsometry.map_vsub, LinearIsometry.angle_map]
-- 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₃ : P
r : ℝ
h : r ≠ 0
⊢ ∠ (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₃
have simp_rw : InnerProductGeometry.angle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
Tactic: simp_rw [angle, ← AffineMap.linearMap_vsub, AffineMap.homothety_linear, LinearMap.smul_apply,
    LinearMap.id_coe, id_eq]
-- 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₃ : P
r : ℝ
h : r ≠ 0
⊢ InnerProductGeometry.angle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
have inl : ∀ (hlt : r < 0),
  InnerProductGeometry.angle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
Tactic: rcases h.lt_or_gt with hlt | hlt
-- 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₃ : P
r : ℝ
h : r ≠ 0
inl :
  ∀ (hlt : r < 0),
    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₂)
have inr : ∀ (hlt : 0 < r),
  InnerProductGeometry.angle (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
Tactic: rcases h.lt_or_gt with hlt | hlt
-- 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
⊢ InnerProductGeometry.angle (p₀ -ᵥ p₀) (p -ᵥ p₀) = π / 2
have rw : InnerProductGeometry.angle 0 (p -ᵥ p₀) = π / 2
Tactic: rw [vsub_self]
-- 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 p₀ p₀ = π / 2
have rw : ∠ p₀ p₀ p = π / 2
Tactic: rw [angle_comm, angle_self_left]
-- 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
rw : ∠ p₀ p₀ p = π / 2
⊢ ∠ p p₀ p₀ = π / 2
have rw₁ : π / 2 = π / 2
Tactic: rw [angle_comm, angle_self_left]
-- 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 : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π
⊢ ∠ p₂ p₁ p₃ = 0
have h₁ : p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
Tactic: rw [angle_eq_pi_iff] 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₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ ∠ p₂ p₁ p₃ = 0
have rcases : ∀ (hp₁p₂ : p₁ -ᵥ p₂ ≠ 0) (r : ℝ) (hr : r < 0) (hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)), ∠ p₂ p₁ p₃ = 0
Tactic: rcases h with ⟨hp₁p₂, ⟨r, ⟨hr, hpr⟩⟩⟩
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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₃ -ᵥ p₁) = 0
have rw : p₂ -ᵥ p₁ ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ p₃ -ᵥ p₁ = r • (p₂ -ᵥ p₁)
Tactic: rw [angle_eq_zero_iff]
-- 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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ p₂ -ᵥ p₁ ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ p₃ -ᵥ p₁ = r • (p₂ -ᵥ p₁)
have rw : ∀ (hp₁p₂ : p₂ -ᵥ p₁ ≠ 0) (r : ℝ) (hr : r < 0) (hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)),
  p₂ -ᵥ p₁ ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ p₃ -ᵥ p₁ = r • (p₂ -ᵥ p₁)
Tactic: rw [← neg_vsub_eq_vsub_rev, neg_ne_zero] at hp₁p₂
Cleared hypotheses: hp₁p₂, r, hr, hpr
-- 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
hp₁p₂ : p₂ -ᵥ p₁ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ p₂ -ᵥ p₁ ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ p₃ -ᵥ p₁ = r • (p₂ -ᵥ p₁)
have right : p₃ -ᵥ p₁ = (-r + 1) • (p₂ -ᵥ p₁)
Tactic: use hp₁p₂, -r + 1, add_pos (neg_pos_of_neg hr) zero_lt_one
-- 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
hp₁p₂ : p₂ -ᵥ p₁ ≠ 0
r : ℝ
hr : r < 0
hpr : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ p₃ -ᵥ p₁ = (-r + 1) • (p₂ -ᵥ p₁)
have right : p₃ -ᵥ p₁ = -(-r • (p₁ -ᵥ p₂)) + HSMul.hSMul (α := ℝ) 1 (-(p₁ -ᵥ p₂))
Tactic: rw [add_smul, ← neg_vsub_eq_vsub_rev p₁ p₂, smul_neg]
-- 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₃ = π
⊢ ∠ p₂ p₃ p₁ = 0
have h₁ : ∠ p₃ p₂ p₁ = π
Tactic: rw [angle_comm] 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₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
have rcases : p₂ -ᵥ p₃ ≠ 0 →
  ∀ (r : ℝ) (hr : r < 0) (hpr : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)),
    InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
Tactic: rcases angle_eq_pi_iff.1 h with ⟨_, ⟨r, ⟨hr, hpr⟩⟩⟩
-- 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₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
left : p₂ -ᵥ p₃ ≠ 0
r : ℝ
hr : r < 0
hpr : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
have rw : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
Tactic: rw [eq_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₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
left : p₂ -ᵥ p₃ ≠ 0
r : ℝ
hr : r < 0
hpr : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
have h₁ : p₄ -ᵥ p₂ = (-r + 1) • (p₃ -ᵥ p₂)
Tactic: convert! angle_smul_right_of_pos (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) (add_pos (neg_pos_of_neg hr) zero_lt_one)
-- 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₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
left : p₂ -ᵥ p₃ ≠ 0
r : ℝ
hr : r < 0
hpr : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)
⊢ p₄ -ᵥ p₂ = (-r + 1) • (p₃ -ᵥ p₂)
have h₁ : p₄ -ᵥ p₂ = - -(p₄ -ᵥ p₃) + HSMul.hSMul (α := ℝ) 1 (-(p₂ -ᵥ p₃))
Tactic: rw [add_smul, ← neg_vsub_eq_vsub_rev p₂ p₃, smul_neg, neg_smul, ← hpr]
-- 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₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
⊢ ∠ p₁ p₃ p₂ + ∠ p₁ p₃ p₄ = π
have rw : ∠ p₂ p₃ p₁ + ∠ p₄ p₃ p₁ = π
Tactic: rw [angle_comm p₁ p₃ p₂, angle_comm p₁ p₃ p₄]
-- 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₄ p₅ : P
hapc : ∠ p₁ p₅ p₃ = π
hbpd : ∠ p₂ p₅ p₄ = π
⊢ ∠ p₁ p₅ p₂ = ∠ p₃ p₅ p₄
have linarith : ∠ p₁ p₅ p₂ < ∠ p₃ p₅ p₄ →
  ∠ p₁ p₅ p₂ - ∠ p₃ p₅ p₄ + -(∠ p₁ p₅ p₂ + ∠ p₁ p₅ p₄ - π) + -(∠ p₄ p₅ p₁ - ∠ p₁ p₅ p₄) +
        (∠ p₄ p₅ p₁ + ∠ p₄ p₅ p₃ - π) +
      -(∠ p₄ p₅ p₃ - ∠ p₃ p₅ p₄) =
    0
Tactic: linarith [angle_add_angle_eq_pi_of_angle_eq_pi p₁ hbpd, angle_comm p₄ p₅ p₁,
    angle_add_angle_eq_pi_of_angle_eq_pi p₄ hapc, angle_comm p₄ p₅ p₃]