awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
⊢ (↑(perpBisector p₁ p₂) : Set P).Nonempty

Tactic:
exact perpBisector_nonempty

Premises used: AffineSubspace.perpBisector_nonempty
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
obtain :
  ∀ (t : ℝ) (hb_eq : (AffineMap.lineMap a c : (a : ℝ) → P) t = b) (ht0 : 0 < t) (ht1 : t < 1), dist p b < dist p c
⊢ dist p b < dist p c

Tactic:
obtain ⟨t, ⟨ht0, ht1⟩, hb_eq⟩ := h_sbtw.mem_image_Ioo

Premises used: Sbtw.mem_image_Ioo
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
⊢ b -ᵥ a = t • (c -ᵥ a)

Tactic:
simp [← hb_eq, AffineMap.lineMap_apply]

Premises used: AffineMap.lineMap_apply
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
⊢ b -ᵥ a = t • (c -ᵥ a)

Tactic:
have hb : b -ᵥ a = t • (c -ᵥ a) := by simp [← hb_eq, AffineMap.lineMap_apply]
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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)
⊢ ⟪p -ᵥ a, c -ᵥ a⟫ = 0

Tactic:
simpa [ht0.ne', hb, inner_smul_right] using h_inner

Premises used: LT.lt.ne', inner_smul_right
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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)
⊢ ⟪p -ᵥ a, c -ᵥ a⟫ = 0

Tactic:
have hpc : ⟪p -ᵥ a, c -ᵥ a⟫ = 0 := by simpa [ht0.ne', hb, inner_smul_right] using h_inner
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
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
⊢ HPow.hPow (β := ℕ) (dist p b) 2 < HPow.hPow (β := ℕ) (dist p c) 2

Tactic:
rw [← hb_eq, dist_sq_lineMap_of_inner_eq_zero t hpc, dist_sq_of_inner_eq_zero hpc]

Premises used: dist_sq_of_inner_eq_zero, dist_sq_lineMap_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
⊢ 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)
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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 (β := ℕ) t 2 < 1

Tactic:
have ht_sq_lt : t ^ 2 < 1 := sq_lt_one_iff₀ ht0.le |>.mpr ht1
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
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
⊢ 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:
nlinarith [sq_nonneg (dist p a), sq_nonneg (dist a c)]

Premises used: sq_nonneg, Dist.dist
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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

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)]
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
h_sq_ineq : HPow.hPow (β := ℕ) (dist p b) 2 < HPow.hPow (β := ℕ) (dist p c) 2
⊢ dist p b < dist p c

Tactic:
simpa only [Real.sqrt_sq dist_nonneg] using Real.sqrt_lt_sqrt (sq_nonneg _) h_sq_ineq

Premises used: dist_nonneg, sq_nonneg, Real.sqrt_sq, Real.sqrt_lt_sqrt
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
obtain :
  ∀ (t : ℝ) (hb_eq : (AffineMap.lineMap a c : (a : ℝ) → P) t = b) (ht0 : 0 ≤ t) (ht1 : t ≤ 1), dist p b ≤ dist p c
⊢ dist p b ≤ dist p c

Tactic:
obtain ⟨t, ⟨ht0, ht1⟩, hb_eq⟩ := h_wbtw
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
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
⊢ HPow.hPow (β := ℕ) (dist p b) 2 ≤ HPow.hPow (β := ℕ) (dist p c) 2

Tactic:
rw [← hb_eq, dist_sq_lineMap_of_inner_eq_zero t h_inner, dist_sq_of_inner_eq_zero h_inner]

Premises used: dist_sq_of_inner_eq_zero, dist_sq_lineMap_of_inner_eq_zero
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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 (β := ℕ) t 2 ≤ 1

Tactic:
have ht_sq_le : t ^ 2 ≤ 1 := sq_le_one_iff₀ ht0 |>.mpr ht1
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
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
⊢ 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:
nlinarith [sq_nonneg (dist p a), sq_nonneg (dist a c)]

Premises used: sq_nonneg, Dist.dist
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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

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)]
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
h_sq_ineq : HPow.hPow (β := ℕ) (dist p b) 2 ≤ HPow.hPow (β := ℕ) (dist p c) 2
⊢ dist p b ≤ dist p c

Tactic:
simpa only [Real.sqrt_sq dist_nonneg] using Real.sqrt_le_sqrt h_sq_ineq

Premises used: dist_nonneg, Real.sqrt_le_sqrt, Real.sqrt_sq
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
rw₄ rw₅ : Eq (α := ℝ) 0 0
⊢ ⟪p -ᵥ midpoint ℝ a b, b -ᵥ midpoint ℝ a b⟫ = 0

Tactic:
rw [right_vsub_midpoint, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, invOf_eq_inv, mul_zero]

Premises used: AffineSubspace.mem_perpBisector_iff_inner_eq_zero, MulZeroClass.mul_zero, inner_smul_right, Iff.mp, invOf_eq_inv, right_vsub_midpoint
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
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
⊢ ⟪p -ᵥ midpoint ℝ a b, c -ᵥ midpoint ℝ a b⟫ = 0

Tactic:
rcases h_wbtw.right_mem_image_Ici_of_left_ne hab with ⟨s, -, rfl⟩

Premises used: Wbtw.right_mem_image_Ici_of_left_ne, rfl
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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
rw₃ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-(b -ᵥ a))⟫ =
    0
rw₄ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) + -HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₅ :
  ⟪p -ᵥ midpoint ℝ a b,
      s • (b -ᵥ a) - HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₆ :
  ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a)⟫ -
      ⟪p -ᵥ midpoint ℝ a b,
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₇ :
  s * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ -
      ⟪p -ᵥ midpoint ℝ a b,
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (b -ᵥ a)⟫ =
    0
rw₈ :
  s * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ midpoint ℝ a b, b -ᵥ a⟫ =
    0
rw₉ : s * 0 - HMul.hMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0 = 0
rw₁₀ : 0 - HMul.hMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0 = 0
rw₁₁ : HSub.hSub (α := ℝ) 0 0 = 0
rw₁₂ rw₁₃ : Eq (α := ℝ) 0 0
⊢ ⟪p -ᵥ midpoint ℝ a b, (AffineMap.lineMap a b : (a : ℝ) → P) s -ᵥ 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]

Premises used: AffineMap.lineMap_vsub_left, sub_self, AffineSubspace.mem_perpBisector_iff_inner_eq_zero, AffineMap.lineMap, sub_eq_add_neg, vsub_add_vsub_cancel, smul_neg, MulZeroClass.mul_zero, inner_smul_right, inner_sub_right, neg_vsub_eq_vsub_rev, Iff.mp, DFunLike.coe, left_vsub_midpoint
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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₁ c₂ p₁ p₂ : P
hc₁ : dist p₁ c₁ = dist p₂ c₁
hc₂ : dist p₁ c₂ = dist p₂ c₂
rw : Membership.mem (γ := Submodule ℝ V) (direction (perpBisector p₁ p₂)) (c₂ -ᵥ c₁)
⊢ ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0

Tactic:
rw [← Submodule.mem_orthogonal_singleton_iff_inner_left, ← direction_perpBisector]

Premises used: Submodule.mem_orthogonal_singleton_iff_inner_left, AffineSubspace.direction_perpBisector
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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₁ c₂ p₁ p₂ : P
hc₁ : dist p₁ c₁ = dist p₂ c₁
hc₂ : dist p₁ c₂ = dist p₂ c₂
hp₁ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c₂
hp₂ : Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c₁
⊢ Membership.mem (γ := Submodule ℝ V) (direction (perpBisector p₁ p₂)) (c₂ -ᵥ c₁)

Tactic:
apply vsub_mem_direction

Premises used: AffineSubspace.vsub_mem_direction
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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₁ c₂ p₁ p₂ : P
hc₁ : dist p₁ c₁ = dist p₂ c₁
hc₂ hp₁ hp₂ hp₃ hp₄ : dist p₁ c₂ = dist p₂ c₂
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c₂

Tactic:
rwa [mem_perpBisector_iff_dist_eq']

Premises used: AffineSubspace.mem_perpBisector_iff_dist_eq'
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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₁ c₂ p₁ p₂ : P
hc₁ : dist p₁ c₁ = dist p₂ c₁
hc₂ : dist p₁ c₂ = dist p₂ c₂
hp₂ hp₃ hp₄ hp₅ : dist p₁ c₁ = dist p₂ c₁
⊢ Membership.mem (γ := AffineSubspace ℝ P) (perpBisector p₁ p₂) c₁

Tactic:
rwa [mem_perpBisector_iff_dist_eq']

Premises used: AffineSubspace.mem_perpBisector_iff_dist_eq'
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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'
h : Isometry f
p₁ p₂ : P
h₁ : ∀ (x : P), x ∈ f ⁻¹' (↑(perpBisector (f p₁) (f p₂)) : Set P') ↔ x ∈ (↑(perpBisector p₁ p₂) : Set P)
⊢ f ⁻¹' (↑(perpBisector (f p₁) (f p₂)) : Set P') = (↑(perpBisector p₁ p₂) : Set P)

Tactic:
ext x
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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'
h : Isometry f
p₁ p₂ x : P
⊢ x ∈ f ⁻¹' (↑(perpBisector (f p₁) (f p₂)) : Set P') ↔ x ∈ (↑(perpBisector p₁ p₂) : Set P)

Tactic:
simp [mem_perpBisector_iff_dist_eq, h.dist_eq]

Premises used: Isometry.dist_eq, AffineSubspace.mem_perpBisector_iff_dist_eq
-- Module: Mathlib.Geometry.Euclidean.PerpBisector
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'
h : Isometry f
p₁ p₂ : P
⊢ MapsTo f (↑(perpBisector p₁ p₂) : Set P) (↑(perpBisector (f p₁) (f p₂)) : Set P')

Tactic:
(h.preimage_perpBisector p₁ p₂).ge

Premises used: Isometry.preimage_perpBisector, Eq.ge, Set.Mem, setOf, Set.Subset, Set.preimage, Set.MapsTo
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ (orthogonalProjection s : (a : P) → ↥s) p =
    HVAdd.hVAdd (α := ↥s.direction) (β := ↥s)
      ((s.direction.orthogonalProjection : (a : V) → ↥s.direction) (p -ᵥ (↑(Classical.arbitrary ↥s) : P)) :
        ↥s.direction)
      (Classical.arbitrary ↥s)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (β := P)
      (↑((s.direction.orthogonalProjection : (a : V) → ↥s.direction) (p -ᵥ (↑(Classical.arbitrary ↥s) : P))) : V)
      (↑(Classical.arbitrary ↥s) : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p x : P
hx : x ∈ s
rw : (↑(Classical.arbitrary ↥s) : P) -ᵥ x ∈ s.direction
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) =
    HVAdd.hVAdd.{u_2, u_3, u_3} (α := V) (↑((s.direction.orthogonalProjection : (a : V) → ↥s.direction) (p -ᵥ x)) : V) x

Tactic:
rw [orthogonalProjection_apply, coe_vadd, vadd_eq_vadd_iff_sub_eq_vsub, ← Submodule.coe_sub,
    ← map_sub, vsub_sub_vsub_cancel_left, Submodule.coe_orthogonalProjection_apply,
    Submodule.starProjection_eq_self_iff]

Premises used: map_sub, vadd_eq_vadd_iff_sub_eq_vsub, AffineSubspace.coe_vadd, Submodule.coe_sub, vsub_sub_vsub_cancel_left, EuclideanGeometry.orthogonalProjection_apply, Submodule.coe_orthogonalProjection_apply, Submodule.starProjection_eq_self_iff
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p x : P
hx : x ∈ s
⊢ (↑(Classical.arbitrary ↥s) : P) -ᵥ x ∈ s.direction

Tactic:
s.vsub_mem_direction (SetLike.coe_mem _) hx

Premises used: SetLike.coe_mem, Set.Mem, AffineSubspace.vsub_mem_direction
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p x : P
hx : x ∈ s
⊢ (↑(Classical.arbitrary ↥s) : P) -ᵥ x ∈ s.direction

Tactic:
exact s.vsub_mem_direction (SetLike.coe_mem _) hx

Premises used: SetLike.coe_mem, AffineSubspace.vsub_mem_direction
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
p₁ p₂ : P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : s₁.direction.HasOrthogonalProjection
h : s₁ = s₂
hp : p₁ = p₂
subst :
  Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p₁) : P)
    (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p₁) : P)
⊢ Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p₁) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p₂) : P)

Tactic:
subst h hp
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ : AffineSubspace 𝕜 P
p₁ : P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : s₁.direction.HasOrthogonalProjection
⊢ Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p₁) : P)
    (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p₁) : P)

Tactic:
rfl
-- Module: Mathlib.Geometry.Euclidean.Projection
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
⊢ AffineMap.linear (↑(orthogonalProjection s) : P →ᵃ[𝕜] ↥s) = (↑s.direction.orthogonalProjection : V →ₗ[𝕜] ↥s.direction)

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl