awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
c p₁ p₂ : P
rw : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = dist c p₂
rw₁ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = ‖c -ᵥ p₂‖
rw₂ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), c -ᵥ p₁ - (c -ᵥ p₂)⟫ = 0
rw₃ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0
rw₄ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ + ⟪c -ᵥ p₂, p₂ -ᵥ p₁⟫ = 0
rw₅ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = -⟪c -ᵥ p₂, p₂ -ᵥ p₁⟫
rw₆ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, -(p₂ -ᵥ p₁)⟫
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ dist c p₁ = dist c p₂
have rw₇ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← real_inner_add_sub_eq_zero_iff,
    vsub_sub_vsub_cancel_left, inner_add_left, add_eq_zero_iff_eq_neg, ← inner_neg_right,
    neg_vsub_eq_vsub_rev, mem_perpBisector_iff_inner_eq_inner]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
c p₁ p₂ : P
rw : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = dist c p₂
rw₁ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ‖c -ᵥ p₁‖ = ‖c -ᵥ p₂‖
rw₂ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), c -ᵥ p₁ - (c -ᵥ p₂)⟫ = 0
rw₃ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0
rw₄ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ + ⟪c -ᵥ p₂, p₂ -ᵥ p₁⟫ = 0
rw₅ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = -⟪c -ᵥ p₂, p₂ -ᵥ p₁⟫
rw₆ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, -(p₂ -ᵥ p₁)⟫
rw₇ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔ dist c p₁ = dist c p₂
have rw₈ : ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫
Tactic: rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← real_inner_add_sub_eq_zero_iff,
    vsub_sub_vsub_cancel_left, inner_add_left, add_eq_zero_iff_eq_neg, ← inner_neg_right,
    neg_vsub_eq_vsub_rev, mem_perpBisector_iff_inner_eq_inner]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
⊢ Eq (α := AffineSubspace ℝ P) (perpBisector p₁ p₂) (perpBisector p₂ p₁)
have h : ∀ (c : P),
  Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c ↔
    Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₂ p₁) c
Tactic: ext c
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) p₁ ↔ p₁ = p₂
have rw : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₂ p₁) p₁ ↔ p₁ = p₂
Tactic: rw [perpBisector_comm, right_mem_perpBisector, eq_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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 : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₂ p₁) p₁ ↔ p₁ = p₂
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) p₁ ↔ p₁ = p₂
have rw₁ : p₂ = p₁ ↔ p₁ = p₂
Tactic: rw [perpBisector_comm, right_mem_perpBisector, eq_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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 : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₂ p₁) p₁ ↔ p₁ = p₂
rw₁ : p₂ = p₁ ↔ p₁ = p₂
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) p₁ ↔ p₁ = p₂
have rw₂ : p₁ = p₂ ↔ p₁ = p₂
Tactic: rw [perpBisector_comm, right_mem_perpBisector, eq_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
⊢ Eq (α := AffineSubspace ℝ P) (perpBisector p₁ p₂) ⊤ ↔ p₁ = p₂
have refine : ∀ (h : Eq (α := AffineSubspace ℝ P) (perpBisector p₁ p₂) ⊤), p₁ = p₂
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h ▸ perpBisector_self _⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
h : Eq (α := AffineSubspace ℝ P) (perpBisector p₁ p₂) ⊤
⊢ p₁ = p₂
have rw : Membership.mem (γ := AffineSubspace ℝ P) ⊤ p₁
Tactic: rw [← left_mem_perpBisector, h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
⊢ Ne (α := AffineSubspace ℝ P) (perpBisector p₁ p₂) ⊥
have rw : (↑(perpBisector p₁ p₂) : Set P).Nonempty
Tactic: rw [← nonempty_iff_ne_bot]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_sbtw : Sbtw ℝ a b c
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
⊢ dist p b < dist p c
have obtain : ∀ (t : ℝ) (hb_eq : (AffineMap.lineMap a c : (a : ℝ) → P) t = b) (ht0 : 0 < t) (ht1 : t < 1), dist p b < dist p c
Tactic: obtain ⟨t, ⟨ht0, ht1⟩, hb_eq⟩ := h_sbtw.mem_image_Ioo
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_sbtw : Sbtw ℝ a b c
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c : (a : ℝ) → P) t = b
ht0 : 0 < t
ht1 : t < 1
⊢ dist p b < dist p c
have hb : b -ᵥ a = t • (c -ᵥ a)
Tactic: have hb : b -ᵥ a = t • (c -ᵥ a) := by simp [← hb_eq, AffineMap.lineMap_apply]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_sbtw : Sbtw ℝ a b c
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c : (a : ℝ) → P) t = b
ht0 : 0 < t
ht1 : t < 1
hb : b -ᵥ a = t • (c -ᵥ a)
⊢ dist p b < dist p c
have hpc : ⟪p -ᵥ a, c -ᵥ a⟫ = 0
Tactic: have hpc : ⟪p -ᵥ a, c -ᵥ a⟫ = 0 := by simpa [ht0.ne', hb, inner_smul_right] using h_inner
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_sbtw : Sbtw ℝ a b c
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c : (a : ℝ) → P) t = b
ht0 : 0 < t
ht1 : t < 1
hb : b -ᵥ a = t • (c -ᵥ a)
hpc : ⟪p -ᵥ a, c -ᵥ a⟫ = 0
⊢ HPow.hPow (β := ℕ) (dist p b) 2 < HPow.hPow (β := ℕ) (dist p c) 2
have rw : HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a c) 2 <
  HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) (dist a c) 2
Tactic: rw [← hb_eq, dist_sq_lineMap_of_inner_eq_zero t hpc, dist_sq_of_inner_eq_zero hpc]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_sbtw : Sbtw ℝ a b c
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c : (a : ℝ) → P) t = b
ht0 : 0 < t
ht1 : t < 1
hb : b -ᵥ a = t • (c -ᵥ a)
hpc : ⟪p -ᵥ a, c -ᵥ a⟫ = 0
⊢ HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a c) 2 <
    HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) (dist a c) 2
have hv_pos : 0 < HPow.hPow (β := ℕ) (dist a c) 2
Tactic: have hv_pos : 0 < dist a c ^ 2 := sq_pos_of_pos (dist_pos.mpr h_sbtw.left_ne_right)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_sbtw : Sbtw ℝ a b c
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c : (a : ℝ) → P) t = b
ht0 : 0 < t
ht1 : t < 1
hb : b -ᵥ a = t • (c -ᵥ a)
hpc : ⟪p -ᵥ a, c -ᵥ a⟫ = 0
hv_pos : 0 < HPow.hPow (β := ℕ) (dist a c) 2
⊢ HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a c) 2 <
    HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) (dist a c) 2
have ht_sq_lt : HPow.hPow (β := ℕ) t 2 < 1
Tactic: have ht_sq_lt : t ^ 2 < 1 := sq_lt_one_iff₀ ht0.le |>.mpr ht1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_sbtw : Sbtw ℝ a b c
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c : (a : ℝ) → P) t = b
ht0 : 0 < t
ht1 : t < 1
hb : b -ᵥ a = t • (c -ᵥ a)
hpc : ⟪p -ᵥ a, c -ᵥ a⟫ = 0
hv_pos : 0 < HPow.hPow (β := ℕ) (dist a c) 2
ht_sq_lt : HPow.hPow (β := ℕ) t 2 < 1
⊢ HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a c) 2 <
    HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) (dist a c) 2
have nlinarith : HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) (dist a c) 2 ≤
    HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a c) 2 →
  HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) (dist a c) 2 -
        (HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a c) 2) +
      (0 - (0 - HPow.hPow (β := ℕ) (dist a c) 2) * (HPow.hPow (β := ℕ) t 2 - 1)) =
    0
Tactic: nlinarith [sq_nonneg (dist p a), sq_nonneg (dist a c)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_sbtw : Sbtw ℝ a b c
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c : (a : ℝ) → P) t = b
ht0 : 0 < t
ht1 : t < 1
hb : b -ᵥ a = t • (c -ᵥ a)
hpc : ⟪p -ᵥ a, c -ᵥ a⟫ = 0
⊢ dist p b < dist p c
have h_sq_ineq : HPow.hPow (β := ℕ) (dist p b) 2 < HPow.hPow (β := ℕ) (dist p c) 2
Tactic: have h_sq_ineq : dist p b ^ 2 < dist p c ^ 2 := by
    rw [← hb_eq, dist_sq_lineMap_of_inner_eq_zero t hpc, dist_sq_of_inner_eq_zero hpc]
    have hv_pos : 0 < dist a c ^ 2 := sq_pos_of_pos (dist_pos.mpr h_sbtw.left_ne_right)
    have ht_sq_lt : t ^ 2 < 1 := sq_lt_one_iff₀ ht0.le |>.mpr ht1
    nlinarith [sq_nonneg (dist p a), sq_nonneg (dist a c)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_wbtw : Wbtw ℝ a b c
h_inner : ⟪p -ᵥ a, c -ᵥ a⟫ = 0
⊢ dist p b ≤ dist p c
have obtain : ∀ (t : ℝ) (hb_eq : (AffineMap.lineMap a c : (a : ℝ) → P) t = b) (ht0 : 0 ≤ t) (ht1 : t ≤ 1), dist p b ≤ dist p c
Tactic: obtain ⟨t, ⟨ht0, ht1⟩, hb_eq⟩ := h_wbtw
Cleared hypotheses: h_wbtw
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_inner : ⟪p -ᵥ a, c -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c : (a : ℝ) → P) t = b
ht0 : 0 ≤ t
ht1 : t ≤ 1
⊢ HPow.hPow (β := ℕ) (dist p b) 2 ≤ HPow.hPow (β := ℕ) (dist p c) 2
have rw : HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a c) 2 ≤
  HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) (dist a c) 2
Tactic: rw [← hb_eq, dist_sq_lineMap_of_inner_eq_zero t h_inner, dist_sq_of_inner_eq_zero h_inner]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_inner : ⟪p -ᵥ a, c -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c : (a : ℝ) → P) t = b
ht0 : 0 ≤ t
ht1 : t ≤ 1
⊢ HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a c) 2 ≤
    HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) (dist a c) 2
have ht_sq_le : HPow.hPow (β := ℕ) t 2 ≤ 1
Tactic: have ht_sq_le : t ^ 2 ≤ 1 := sq_le_one_iff₀ ht0 |>.mpr ht1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_inner : ⟪p -ᵥ a, c -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c : (a : ℝ) → P) t = b
ht0 : 0 ≤ t
ht1 : t ≤ 1
ht_sq_le : HPow.hPow (β := ℕ) t 2 ≤ 1
⊢ HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a c) 2 ≤
    HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) (dist a c) 2
have nlinarith : HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) (dist a c) 2 <
    HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a c) 2 →
  HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) (dist a c) 2 -
        (HPow.hPow (β := ℕ) (dist p a) 2 + HPow.hPow (β := ℕ) t 2 * HPow.hPow (β := ℕ) (dist a c) 2) +
      (0 - (0 - HPow.hPow (β := ℕ) (dist a c) 2) * (HPow.hPow (β := ℕ) t 2 - 1)) =
    0
Tactic: nlinarith [sq_nonneg (dist p a), sq_nonneg (dist a c)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_inner : ⟪p -ᵥ a, c -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c : (a : ℝ) → P) t = b
ht0 : 0 ≤ t
ht1 : t ≤ 1
⊢ dist p b ≤ dist p c
have h_sq_ineq : HPow.hPow (β := ℕ) (dist p b) 2 ≤ HPow.hPow (β := ℕ) (dist p c) 2
Tactic: have h_sq_ineq : dist p b ^ 2 ≤ dist p c ^ 2 := by
    rw [← hb_eq, dist_sq_lineMap_of_inner_eq_zero t h_inner, dist_sq_of_inner_eq_zero h_inner]
    have ht_sq_le : t ^ 2 ≤ 1 := sq_le_one_iff₀ ht0 |>.mpr ht1
    nlinarith [sq_nonneg (dist p a), sq_nonneg (dist a c)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_sbtw : Sbtw ℝ a b c
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
⊢ ⟪p -ᵥ midpoint ℝ a b, b -ᵥ midpoint ℝ a b⟫ = 0
have rw : ⟪p -ᵥ midpoint ℝ a b, HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ = 0
Tactic: rw [right_vsub_midpoint, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, invOf_eq_inv, mul_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_sbtw : Sbtw ℝ a b c
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
rw :
  ⟪p -ᵥ midpoint ℝ a b, HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
⊢ ⟪p -ᵥ midpoint ℝ a b, b -ᵥ midpoint ℝ a b⟫ = 0
have rw₁ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ = 0
Tactic: rw [right_vsub_midpoint, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, invOf_eq_inv, mul_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_sbtw : Sbtw ℝ a b c
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
rw :
  ⟪p -ᵥ midpoint ℝ a b, HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₁ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ = 0
⊢ ⟪p -ᵥ midpoint ℝ a b, b -ᵥ midpoint ℝ a b⟫ = 0
have rw₂ : HMul.hMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0 = 0
Tactic: rw [right_vsub_midpoint, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, invOf_eq_inv, mul_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_sbtw : Sbtw ℝ a b c
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
rw :
  ⟪p -ᵥ midpoint ℝ a b, HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₁ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ = 0
rw₂ : HMul.hMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0 = 0
⊢ ⟪p -ᵥ midpoint ℝ a b, b -ᵥ midpoint ℝ a b⟫ = 0
have rw₃ : HMul.hMul (α := ℝ) 2⁻¹ 0 = 0
Tactic: rw [right_vsub_midpoint, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, invOf_eq_inv, mul_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_sbtw : Sbtw ℝ a b c
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
rw :
  ⟪p -ᵥ midpoint ℝ a b, HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₁ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ = 0
rw₂ : HMul.hMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0 = 0
rw₃ : HMul.hMul (α := ℝ) 2⁻¹ 0 = 0
⊢ ⟪p -ᵥ midpoint ℝ a b, b -ᵥ midpoint ℝ a b⟫ = 0
have rw₄ : Eq (α := ℝ) 0 0
Tactic: rw [right_vsub_midpoint, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, invOf_eq_inv, mul_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b c p : P
h_wbtw : Wbtw ℝ a b c
hab : a ≠ b
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
⊢ ⟪p -ᵥ midpoint ℝ a b, c -ᵥ midpoint ℝ a b⟫ = 0
have rcases : ∀ (s : ℝ) (h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b : (a : ℝ) → P) s)),
  ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ midpoint ℝ a b⟫ = 0
Tactic: rcases h_wbtw.right_mem_image_Ici_of_left_ne hab with ⟨s, -, rfl⟩
Cleared hypotheses: c, h_wbtw
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b p : P
hab : a ≠ b
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b : (a : ℝ) → P) s)
⊢ ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ midpoint ℝ a b⟫ = 0
have rw : ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ a + (a -ᵥ midpoint ℝ a b)⟫ = 0
Tactic: rw [← vsub_add_vsub_cancel (AffineMap.lineMap a b s) a, AffineMap.lineMap_vsub_left,
        left_vsub_midpoint, ← neg_vsub_eq_vsub_rev b a, smul_neg, ← sub_eq_add_neg,
        inner_sub_right, inner_smul_right, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, mul_zero, mul_zero, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b p : P
hab : a ≠ b
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b : (a : ℝ) → P) s)
rw : ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ a + (a -ᵥ midpoint ℝ a b)⟫ = 0
⊢ ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ midpoint ℝ a b⟫ = 0
have rw₁ : ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a) + (a -ᵥ midpoint ℝ a b)⟫ = 0
Tactic: rw [← vsub_add_vsub_cancel (AffineMap.lineMap a b s) a, AffineMap.lineMap_vsub_left,
        left_vsub_midpoint, ← neg_vsub_eq_vsub_rev b a, smul_neg, ← sub_eq_add_neg,
        inner_sub_right, inner_smul_right, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, mul_zero, mul_zero, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b p : P
hab : a ≠ b
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b : (a : ℝ) → P) s)
rw : ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ a + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₁ : ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a) + (a -ᵥ midpoint ℝ a b)⟫ = 0
⊢ ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ midpoint ℝ a b⟫ = 0
have rw₂ : ⟪p -ᵥ midpoint ℝ a b,
    s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (a -ᵥ b)⟫ =
  0
Tactic: rw [← vsub_add_vsub_cancel (AffineMap.lineMap a b s) a, AffineMap.lineMap_vsub_left,
        left_vsub_midpoint, ← neg_vsub_eq_vsub_rev b a, smul_neg, ← sub_eq_add_neg,
        inner_sub_right, inner_smul_right, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, mul_zero, mul_zero, sub_self]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.PerpBisector (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
a b p : P
hab : a ≠ b
hp : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector a b) p
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b : (a : ℝ) → P) s)
rw : ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ a + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₁ : ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a) + (a -ᵥ midpoint ℝ a b)⟫ = 0
rw₂ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (a -ᵥ b)⟫ =
    0
⊢ ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ midpoint ℝ a b⟫ = 0
have rw₃ : ⟪p -ᵥ midpoint ℝ a b,
    s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-(b -ᵥ a))⟫ =
  0
Tactic: rw [← vsub_add_vsub_cancel (AffineMap.lineMap a b s) a, AffineMap.lineMap_vsub_left,
        left_vsub_midpoint, ← neg_vsub_eq_vsub_rev b a, smul_neg, ← sub_eq_add_neg,
        inner_sub_right, inner_smul_right, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, mul_zero, mul_zero, sub_self]