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
r : ℝ
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r ≠ p₁
hr0' : r ≠ 0
hr0 : 0 < r
rw : p₃ -ᵥ p₁ = r⁻¹ • ((r • (p₃ -ᵥ p₁) +ᵥ p₁) -ᵥ p₁)
rw₁ : p₃ -ᵥ p₁ = r⁻¹ • (r • (p₃ -ᵥ p₁) + (p₁ -ᵥ p₁))
rw₂ : p₃ -ᵥ p₁ = r⁻¹ • (r • (p₃ -ᵥ p₁) + 0)
rw₃ : p₃ -ᵥ p₁ = r⁻¹ • r • (p₃ -ᵥ p₁)
rw₄ : p₃ -ᵥ p₁ = (r⁻¹ * r) • (p₃ -ᵥ p₁)
⊢ p₃ -ᵥ p₁ = r⁻¹ • ((AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁)
have rw₅ : p₃ -ᵥ p₁ = HSMul.hSMul (α := ℝ) 1 (p₃ -ᵥ p₁)
Tactic: rw [AffineMap.lineMap_apply, vadd_vsub_assoc, vsub_self, add_zero, smul_smul,
    inv_mul_cancel₀ hr0', one_smul]
-- 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
r : ℝ
hr1 : r ≤ 1
hp₂p₁ : (AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r ≠ p₁
hr0' : r ≠ 0
hr0 : 0 < r
rw : p₃ -ᵥ p₁ = r⁻¹ • ((r • (p₃ -ᵥ p₁) +ᵥ p₁) -ᵥ p₁)
rw₁ : p₃ -ᵥ p₁ = r⁻¹ • (r • (p₃ -ᵥ p₁) + (p₁ -ᵥ p₁))
rw₂ : p₃ -ᵥ p₁ = r⁻¹ • (r • (p₃ -ᵥ p₁) + 0)
rw₃ : p₃ -ᵥ p₁ = r⁻¹ • r • (p₃ -ᵥ p₁)
rw₄ : p₃ -ᵥ p₁ = (r⁻¹ * r) • (p₃ -ᵥ p₁)
rw₅ : p₃ -ᵥ p₁ = HSMul.hSMul (α := ℝ) 1 (p₃ -ᵥ p₁)
⊢ p₃ -ᵥ p₁ = r⁻¹ • ((AffineMap.lineMap p₁ p₃ : (a : ℝ) → P) r -ᵥ p₁)
have rw₆ : p₃ -ᵥ p₁ = p₃ -ᵥ p₁
Tactic: rw [AffineMap.lineMap_apply, vadd_vsub_assoc, vsub_self, add_zero, smul_smul,
    inv_mul_cancel₀ hr0', one_smul]
-- 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₃
hp₂p₁ : p₂ ≠ p₁
⊢ ∠ p₃ p₁ p₂ = 0
have rw : ∠ p₃ p₁ p₂ = ∠ p₂ p₁ p₃
Tactic: rw [← h.angle₂₁₃_eq_zero_of_ne hp₂p₁, angle_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₃
hp₂p₁ : p₂ ≠ p₁
rw : ∠ p₃ p₁ p₂ = ∠ p₂ p₁ p₃
⊢ ∠ p₃ p₁ p₂ = 0
have rw₁ : ∠ p₂ p₁ p₃ = ∠ p₂ p₁ p₃
Tactic: rw [← h.angle₂₁₃_eq_zero_of_ne hp₂p₁, angle_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₁ p₂ p₃ = 0 ↔ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
have mp : ∠ p₁ p₂ p₃ = 0 → p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
Tactic: constructor
-- 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
mp : ∠ p₁ p₂ p₃ = 0 → p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
⊢ ∠ p₁ p₂ p₃ = 0 ↔ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
have mpr : p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ → ∠ p₁ p₂ p₃ = 0
Tactic: constructor
-- 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₂ p₃ = 0 → p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
have mp : (p₁ -ᵥ p₂ ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)) → p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
Tactic: rw [angle, 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
have mp : ∀ (hr1 : 1 ≤ r), p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
Tactic: rcases le_or_gt 1 r with (hr1 | hr1)
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
mp : ∀ (hr1 : 1 ≤ r), p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
have mp₁ : ∀ (hr1 : r < 1), p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
Tactic: rcases le_or_gt 1 r with (hr1 | hr1)
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : 1 ≤ r
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
have mp : (AffineMap.lineMap p₂ p₃ : (a : ℝ) → P) r⁻¹ = p₁
Tactic: refine Or.inl ⟨vsub_ne_zero.1 hp₁p₂, r⁻¹, ⟨(inv_pos.2 hr0).le, inv_le_one_of_one_le₀ hr1⟩, ?_⟩
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : 1 ≤ r
⊢ (AffineMap.lineMap p₂ p₃ : (a : ℝ) → P) r⁻¹ = p₁
have mp : r⁻¹ • (p₃ -ᵥ p₂) +ᵥ p₂ = p₁
Tactic: rw [AffineMap.lineMap_apply, hp₃p₂, smul_smul, inv_mul_cancel₀ hr0.ne.symm, one_smul,
        vsub_vadd]
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : 1 ≤ r
mp : r⁻¹ • (p₃ -ᵥ p₂) +ᵥ p₂ = p₁
⊢ (AffineMap.lineMap p₂ p₃ : (a : ℝ) → P) r⁻¹ = p₁
have mp₁ : r⁻¹ • r • (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
Tactic: rw [AffineMap.lineMap_apply, hp₃p₂, smul_smul, inv_mul_cancel₀ hr0.ne.symm, one_smul,
        vsub_vadd]
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : 1 ≤ r
mp : r⁻¹ • (p₃ -ᵥ p₂) +ᵥ p₂ = p₁
mp₁ : r⁻¹ • r • (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
⊢ (AffineMap.lineMap p₂ p₃ : (a : ℝ) → P) r⁻¹ = p₁
have mp₂ : (r⁻¹ * r) • (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
Tactic: rw [AffineMap.lineMap_apply, hp₃p₂, smul_smul, inv_mul_cancel₀ hr0.ne.symm, one_smul,
        vsub_vadd]
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : 1 ≤ r
mp : r⁻¹ • (p₃ -ᵥ p₂) +ᵥ p₂ = p₁
mp₁ : r⁻¹ • r • (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
mp₂ : (r⁻¹ * r) • (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
⊢ (AffineMap.lineMap p₂ p₃ : (a : ℝ) → P) r⁻¹ = p₁
have mp₃ : HSMul.hSMul (α := ℝ) 1 (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
Tactic: rw [AffineMap.lineMap_apply, hp₃p₂, smul_smul, inv_mul_cancel₀ hr0.ne.symm, one_smul,
        vsub_vadd]
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : 1 ≤ r
mp : r⁻¹ • (p₃ -ᵥ p₂) +ᵥ p₂ = p₁
mp₁ : r⁻¹ • r • (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
mp₂ : (r⁻¹ * r) • (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
mp₃ : HSMul.hSMul (α := ℝ) 1 (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
⊢ (AffineMap.lineMap p₂ p₃ : (a : ℝ) → P) r⁻¹ = p₁
have mp₄ : (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
Tactic: rw [AffineMap.lineMap_apply, hp₃p₂, smul_smul, inv_mul_cancel₀ hr0.ne.symm, one_smul,
        vsub_vadd]
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : 1 ≤ r
mp : r⁻¹ • (p₃ -ᵥ p₂) +ᵥ p₂ = p₁
mp₁ : r⁻¹ • r • (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
mp₂ : (r⁻¹ * r) • (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
mp₃ : HSMul.hSMul (α := ℝ) 1 (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
mp₄ : (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
⊢ (AffineMap.lineMap p₂ p₃ : (a : ℝ) → P) r⁻¹ = p₁
have mp₅ : p₁ = p₁
Tactic: rw [AffineMap.lineMap_apply, hp₃p₂, smul_smul, inv_mul_cancel₀ hr0.ne.symm, one_smul,
        vsub_vadd]
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
have mp : p₃ ≠ p₂
Tactic: refine Or.inr ⟨?_, r, ⟨hr0.le, hr1.le⟩, ?_⟩
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
mp : p₃ ≠ p₂
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
have mp₁ : (AffineMap.lineMap p₂ p₁ : (a : ℝ) → P) r = p₃
Tactic: refine Or.inr ⟨?_, r, ⟨hr0.le, hr1.le⟩, ?_⟩
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
⊢ p₃ ≠ p₂
have mp : r ≠ 0 ∧ p₁ -ᵥ p₂ ≠ 0
Tactic: rw [← @vsub_ne_zero V, hp₃p₂, smul_ne_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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
⊢ (AffineMap.lineMap p₂ p₁ : (a : ℝ) → P) r = p₃
have mp : r • (p₁ -ᵥ p₂) +ᵥ p₂ = p₃
Tactic: rw [AffineMap.lineMap_apply, ← hp₃p₂, vsub_vadd]
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
mp : r • (p₁ -ᵥ p₂) +ᵥ p₂ = p₃
⊢ (AffineMap.lineMap p₂ p₁ : (a : ℝ) → P) r = p₃
have mp₁ : (p₃ -ᵥ p₂) +ᵥ p₂ = p₃
Tactic: rw [AffineMap.lineMap_apply, ← hp₃p₂, vsub_vadd]
-- 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 : ℝ
hr0 : 0 < r
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
hr1 : r < 1
mp : r • (p₁ -ᵥ p₂) +ᵥ p₂ = p₃
mp₁ : (p₃ -ᵥ p₂) +ᵥ p₂ = p₃
⊢ (AffineMap.lineMap p₂ p₁ : (a : ℝ) → P) r = p₃
have mp₂ : p₃ = p₃
Tactic: rw [AffineMap.lineMap_apply, ← hp₃p₂, vsub_vadd]
-- 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₂ p₃ = 0 ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
have rw : p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
Tactic: rw [angle_eq_zero_iff_ne_and_wbtw]
-- 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₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
have pos : ∀ (hp₁p₂ : p₁ = p₂),
  p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
Tactic: by_cases hp₁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
pos :
  ∀ (hp₁p₂ : p₁ = p₂),
    p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
have neg : ∀ (hp₁p₂ : ¬p₁ = p₂),
  p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
Tactic: by_cases hp₁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
hp₁p₂ : ¬p₁ = p₂
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
have pos : ∀ (hp₁p₃ : p₁ = p₃),
  p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
Tactic: by_cases hp₁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
hp₁p₂ : ¬p₁ = p₂
pos :
  ∀ (hp₁p₃ : p₁ = p₃),
    p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
have neg : ∀ (hp₁p₃ : ¬p₁ = p₃),
  p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
Tactic: by_cases hp₁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
hp₁p₂ : ¬p₁ = p₂
hp₁p₃ : ¬p₁ = p₃
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
have pos : ∀ (hp₃p₂ : p₃ = p₂),
  p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
Tactic: by_cases hp₃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
hp₁p₂ : ¬p₁ = p₂
hp₁p₃ : ¬p₁ = p₃
pos :
  ∀ (hp₃p₂ : p₃ = p₂),
    p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
have neg : ∀ (hp₃p₂ : ¬p₃ = p₂),
  p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
Tactic: by_cases hp₃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
h : Wbtw ℝ p₂ p₃ p
hp₃p₂ : p₃ ≠ p₂
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p
have pos : ∀ (hp₃p : p₃ = p), ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p
Tactic: by_cases hp₃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
h : Wbtw ℝ p₂ p₃ p
hp₃p₂ : p₃ ≠ p₂
pos : ∀ (hp₃p : p₃ = p), ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p
have neg : ∀ (hp₃p : ¬p₃ = p), ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p
Tactic: by_cases hp₃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₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = π - ∠ p₁ p₂ p₃
have pos : ∀ (h₃₂ : p₃ = p₂), ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = π - ∠ p₁ p₂ p₃
Tactic: by_cases! h₃₂ : 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
pos : ∀ (h₃₂ : p₃ = p₂), ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = π - ∠ p₁ p₂ p₃
⊢ ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = π - ∠ p₁ p₂ p₃
have neg : ∀ (h₃₂ : p₃ ≠ p₂), ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = π - ∠ p₁ p₂ p₃
Tactic: by_cases! h₃₂ : 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
h₃₂ : p₃ = p₂
⊢ ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = π - ∠ p₁ p₂ p₃
have pos : π / 2 = π - π / 2
Tactic: simp [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₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = π - ∠ p₁ p₂ p₃
have neg : ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) + ∠ p₁ p₂ p₃ = π
Tactic: rw [eq_sub_iff_add_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
h₃₂ : p₃ ≠ p₂
⊢ ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) + ∠ p₁ p₂ p₃ = π
have neg : ∠ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) p₂ p₃ = π
Tactic: apply EuclideanGeometry.angle_add_angle_eq_pi_of_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
⊢ Collinear ℝ (P := P) {p₁, p₂, p₃} ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
have refine_1 : ∀ (h : Collinear ℝ (P := P) {p₁, p₂, p₃}), p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
Tactic: refine ⟨fun h => ?_, fun 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
refine_1 : ∀ (h : 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₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
have refine_2 : ∀ (h : p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π), Collinear ℝ (P := P) {p₁, p₂, p₃}
Tactic: refine ⟨fun h => ?_, fun 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 : Collinear ℝ (P := P) {p₁, p₂, p₃}
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
have h₁ : Wbtw ℝ p₁ p₂ p₃ ∨ Wbtw ℝ p₂ p₃ p₁ ∨ Wbtw ℝ p₃ p₁ p₂
Tactic: replace h := h.wbtw_or_wbtw_or_wbtw
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₃ ∨ Wbtw ℝ p₂ p₃ p₁ ∨ Wbtw ℝ p₃ p₁ p₂
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
have pos : ∀ (h₁₂ : p₁ = p₂), p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
Tactic: by_cases h₁₂ : 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
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₃ = π
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
have neg : ∀ (h₁₂ : ¬p₁ = p₂), p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
Tactic: by_cases h₁₂ : 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
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₃ = π
have pos : ∀ (h₃₂ : p₃ = p₂), p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
Tactic: by_cases h₃₂ : 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
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₃ = π
⊢ p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
have neg : ∀ (h₃₂ : ¬p₃ = p₂), p₁ = p₂ ∨ p₃ = p₂ ∨ ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
Tactic: by_cases h₃₂ : 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
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₃ = π
have neg : ∠ p₁ p₂ p₃ = 0 ∨ ∠ p₁ p₂ p₃ = π
Tactic: rw [or_iff_right h₁₂, or_iff_right 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₃ ∨ Wbtw ℝ p₂ p₃ p₁ ∨ Wbtw ℝ p₃ p₁ p₂
h₁₂ : ¬p₁ = p₂
h₃₂ : ¬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 : 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₃ = π
⊢ ∠ 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