awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : HPow.hPow (β := ℕ) (dist p t) 2 = s.power p
⊢ ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0

Tactic:
have h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0 := by
      simp only [Sphere.power, ← mem_sphere.mp ht, dist_eq_norm_vsub V, sq,
                 ← vsub_add_vsub_cancel p t s.center] at h_dist_eq
      exact (norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero _ _).mp (by linarith)
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : HPow.hPow (β := ℕ) (dist p t) 2 = s.power p
h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
⊢ s.IsTangentAt t (affineSpan ℝ {p, t})

Tactic:
⟨ht, right_mem_affineSpan_pair ℝ p t, fun x hx ↦ ?_⟩

Premises used: Real, right_mem_affineSpan_pair, EuclideanGeometry.Sphere.IsTangentAt.mk
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : HPow.hPow (β := ℕ) (dist p t) 2 = s.power p
h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
refine :
  ∀ (x : P) (hx : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, t}) x),
    Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius t) x
⊢ s.IsTangentAt t (affineSpan ℝ {p, t})

Tactic:
refine ⟨ht, right_mem_affineSpan_pair ℝ p t, fun x hx ↦ ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : HPow.hPow (β := ℕ) (dist p t) 2 = s.power p
h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
x : P
hx : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, t}) x
rw : ⟪x -ᵥ t, t -ᵥ s.center⟫ = 0
⊢ Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius t) x

Tactic:
rw [mem_orthRadius_iff_inner_left]

Premises used: EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_left
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : HPow.hPow (β := ℕ) (dist p t) 2 = s.power p
h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
x : P
hx : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, t}) x
obtain : ∀ (r : ℝ) (hr : r • (p -ᵥ t) = x -ᵥ t), ⟪x -ᵥ t, t -ᵥ s.center⟫ = 0
⊢ ⟪x -ᵥ t, t -ᵥ s.center⟫ = 0

Tactic:
obtain ⟨r, hr⟩ := (vadd_right_mem_affineSpan_pair (k := ℝ)).mp (vsub_vadd x t ▸ hx)

Premises used: vadd_right_mem_affineSpan_pair, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Power
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t p : P
s : Sphere P
ht : t ∈ s
h_dist_eq : HPow.hPow (β := ℕ) (dist p t) 2 = s.power p
h_orth : ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
x : P
hx : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, t}) x
r : ℝ
hr : r • (p -ᵥ t) = x -ᵥ t
rw : ⟪r • (p -ᵥ t), t -ᵥ s.center⟫ = 0
rw₁ : HMul.hMul (α := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) ⟪p -ᵥ t, t -ᵥ s.center⟫ = 0
rw₂ : HMul.hMul (α := ℝ) (β := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) (0 : ℝ) = 0
rw₃ rw₄ : Eq (α := ℝ) 0 0
⊢ ⟪x -ᵥ t, t -ᵥ s.center⟫ = 0

Tactic:
rw [← hr, inner_smul_left, h_orth, mul_zero]

Premises used: MulZeroClass.mul_zero, inner_smul_left
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
rwa rwa₁ rwa₂ rwa₃ : Cospherical (P := P) {a, b, c, d}
⊢ Cospherical (P := P) {a, c, b, d}

Tactic:
rwa [Set.insert_comm c b {d}]

Premises used: Set.insert_comm, Singleton.singleton
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
⊢ Cospherical (P := P) {a, c, b, d}

Tactic:
have h' : Cospherical ({a, c, b, d} : Set P) := by rwa [Set.insert_comm c b {d}]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
⊢ dist a p * dist c p = dist b p * dist d p

Tactic:
have hmul := mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi h' hapc hbpd
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
⊢ dist b p ≠ 0

Tactic:
have hbp := left_dist_ne_zero_of_angle_eq_pi hbpd
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : ∠ c p d = ∠ b p a
hab : dist c p = dist c p / dist b p * dist b p
hcb : dist d p = dist c p / dist b p * dist a p
⊢ dist c d = dist c p / dist b p * dist a b

Tactic:
rw [dist_mul_of_eq_angle_of_dist_mul b p a c p d, dist_comm a b]

Premises used: dist_comm, EuclideanGeometry.dist_mul_of_eq_angle_of_dist_mul
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : ∠ c p d = ∠ d p c
h₂ h₃ : ∠ d p c = ∠ d p c
⊢ ∠ c p d = ∠ b p a

Tactic:
rw [angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi hbpd hapc, angle_comm]

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
⊢ dist c p = dist c p / dist b p * dist b p

Tactic:
simp [field, mul_comm, hmul]

Premises used: mul_comm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
⊢ dist d p = dist c p / dist b p * dist a p

Tactic:
simp [field, mul_comm, hmul]

Premises used: mul_comm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
⊢ dist c d = dist c p / dist b p * dist a b

Tactic:
have h₁ : dist c d = dist c p / dist b p * dist a b := by
    rw [dist_mul_of_eq_angle_of_dist_mul b p a c p d, dist_comm a b]
    · rw [angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi hbpd hapc, angle_comm]
    all_goals simp [field, mul_comm, hmul]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ : ∠ d p a = ∠ c p b
hab : dist d p = dist a p / dist b p * dist c p
hcb : dist a p = dist a p / dist b p * dist b p
⊢ dist d a = dist a p / dist b p * dist b c

Tactic:
rw [dist_mul_of_eq_angle_of_dist_mul c p b d p a, dist_comm c b]

Premises used: dist_comm, EuclideanGeometry.dist_mul_of_eq_angle_of_dist_mul
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ : ∠ d p b = π
⊢ ∠ d p a = ∠ c p b

Tactic:
rwa [angle_comm, angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi]

Premises used: EuclideanGeometry.angle_comm, EuclideanGeometry.angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ h₃ h₄ h₅ : ∠ b p d = π
⊢ ∠ d p b = π

Tactic:
rwa [angle_comm]

Premises used: EuclideanGeometry.angle_comm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
⊢ dist d p = dist a p / dist b p * dist c p

Tactic:
simp [field, mul_comm, hmul]

Premises used: mul_comm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
⊢ dist a p = dist a p / dist b p * dist b p

Tactic:
simp [field, mul_comm, hmul]

Premises used: mul_comm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
⊢ dist d a = dist a p / dist b p * dist b c

Tactic:
have h₂ : dist d a = dist a p / dist b p * dist b c := by
    rw [dist_mul_of_eq_angle_of_dist_mul c p b d p a, dist_comm c b]
    · rwa [angle_comm, angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi]; rwa [angle_comm]
    all_goals simp [field, mul_comm, hmul]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ : dist d a = dist a p / dist b p * dist b c
⊢ dist d p = dist a p * dist c p / dist b p

Tactic:
simp [field, hmul]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ : dist d a = dist a p / dist b p * dist b c
⊢ dist d p = dist a p * dist c p / dist b p

Tactic:
have h₃ : dist d p = dist a p * dist c p / dist b p := by simp [field, hmul]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ : dist d a = dist a p / dist b p * dist b c
h₃ : dist d p = dist a p * dist c p / dist b p
x y : ℝ
rw : y * (x * x) = x * x * y
rw₁ rw₂ : x * x * y = x * x * y
⊢ x * (y * x) = x * x * y

Tactic:
rw [mul_left_comm, mul_comm]

Premises used: mul_left_comm, mul_comm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ : dist d a = dist a p / dist b p * dist b c
h₃ : dist d p = dist a p * dist c p / dist b p
⊢ ∀ (x y : ℝ), x * (y * x) = x * x * y

Tactic:
have h₄ : ∀ x y : ℝ, x * (y * x) = x * x * y := fun x y => by rw [mul_left_comm, mul_comm]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
P : Type u_2
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d p : P
h : Cospherical (P := P) {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical (P := P) {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
h₂ : dist d a = dist a p / dist b p * dist b c
h₃ : dist d p = dist a p * dist c p / dist b p
h₄ : ∀ (x y : ℝ), x * (y * x) = x * x * y
⊢ dist a b * dist c d + dist b c * dist d a = dist a c * dist b d

Tactic:
simp [field, h₁, h₂, dist_eq_add_dist_of_angle_eq_pi hbpd, h₃, dist_comm a b, h₄, ← sq,
    dist_sq_mul_dist_add_dist_sq_mul_dist b, hapc]

Premises used: EuclideanGeometry.dist_eq_add_dist_of_angle_eq_pi, dist_comm, sq, EuclideanGeometry.dist_sq_mul_dist_add_dist_sq_mul_dist
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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₂
s : Sphere P
p : P
v : V
f : P →ᵃⁱ[ℝ] P₂
⊢ Eq.{u_4 + 1} (α := P₂)
    (secondInter.{u_3, u_4} (V := V₂) { center := (f : (a : P) → P₂) s.center, radius := s.radius }
        ((f : (a : P) → P₂) p) ((f.linearIsometry : (a : V) → V₂) v : V₂) :
      P₂)
    ((f : (a : P) → P₂) (s.secondInter p v) : P₂)

Tactic:
simp [secondInter, ← AffineIsometry.map_vsub]

Premises used: AffineIsometry.map_vsub, EuclideanGeometry.Sphere.secondInter
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
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
as : AffineSubspace ℝ P
inst_4 : Nonempty.{u_2 + 1} ↥as
s : Sphere ↥as
p : ↥as
v : ↥as.direction
⊢ (↑(s.secondInter p v) : P) = secondInter { center := (↑s.center : P), radius := s.radius } (↑p : P) (↑v : V)

Tactic:
rfl

Premises used: EuclideanGeometry.Sphere.secondInter, rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
rw : dist ((-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) s.center = dist p s.center
⊢ dist (s.secondInter p v) s.center = dist p s.center

Tactic:
rw [Sphere.secondInter]

Premises used: EuclideanGeometry.Sphere.secondInter
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
pos : ∀ (hv : v = 0), dist ((-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) s.center = dist p s.center
neg : ∀ (hv : ¬v = 0), dist ((-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) s.center = dist p s.center
⊢ dist ((-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) s.center = dist p s.center

Tactic:
by_cases hv : v = 0
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hv : v = 0
⊢ dist ((-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) s.center = dist p s.center

Tactic:
simp [hv]
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hv : ¬v = 0
neg : -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = 0 ∨ -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫
⊢ dist ((-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) s.center = dist p s.center

Tactic:
rw [dist_smul_vadd_eq_dist _ _ hv]

Premises used: EuclideanGeometry.dist_smul_vadd_eq_dist
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hv : ¬v = 0
⊢ -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = 0 ∨ -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫

Tactic:
Or.inr rfl

Premises used: Or.inr, rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hv : ¬v = 0
⊢ -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = 0 ∨ -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫

Tactic:
exact Or.inr rfl

Premises used: Or.inr, rfl
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
⊢ s.secondInter p 0 = p

Tactic:
simp [Sphere.secondInter]

Premises used: EuclideanGeometry.Sphere.secondInter
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
⊢ s.secondInter p v = p ↔ ⟪v, p -ᵥ s.center⟫ = 0

Tactic:
⟨fun hp => ?_, fun hp => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
refine_1 : ∀ (hp : s.secondInter p v = p), ⟪v, p -ᵥ s.center⟫ = 0
refine_2 : ∀ (hp : ⟪v, p -ᵥ s.center⟫ = 0), s.secondInter p v = p
⊢ s.secondInter p v = p ↔ ⟪v, p -ᵥ s.center⟫ = 0

Tactic:
refine ⟨fun hp => ?_, fun hp => ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
pos : ∀ (hv : v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg : ∀ (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0

Tactic:
by_cases hv : v = 0
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
hv : v = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0

Tactic:
simp [hv]
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : Eq (α := ℝ) (-2) 0 ∨ ⟪v, p -ᵥ s.center⟫ = 0
hv : ¬v = 0
⊢ Ne (α := ℝ) (-2) 0

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : Sphere P
p : P
v : V
hp : s.secondInter p v = p
hv : ¬v = 0
neg : ∀ (hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p = p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₁ : ∀ (hp : p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₂ : ∀ (hp : p -ᵥ p = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₃ : ∀ (hp : 0 = (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₄ : ∀ (hp : (-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₅ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = 0 ∨ v = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₆ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫ = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₇ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ = 0 ∨ ⟪v, v⟫ = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₈ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ = 0 ∨ v = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₉ : ∀ (hp : -2 * ⟪v, p -ᵥ s.center⟫ = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₁₀ : ∀ (hp : Eq (α := ℝ) (-2) 0 ∨ ⟪v, p -ᵥ s.center⟫ = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
neg₁₁ neg₁₂ neg₁₃ neg₁₄ : ∀ (hp : ⟪v, p -ᵥ s.center⟫ = 0) (hv : ¬v = 0), ⟪v, p -ᵥ s.center⟫ = 0
⊢ ⟪v, p -ᵥ s.center⟫ = 0

Tactic:
rwa [Sphere.secondInter, eq_comm, eq_vadd_iff_vsub_eq, vsub_self, eq_comm, smul_eq_zero,
      or_iff_left hv, div_eq_zero_iff, inner_self_eq_zero, or_iff_left hv, mul_eq_zero,
      or_iff_right (by simp : (-2 : ℝ) ≠ 0)] at hp

Premises used: eq_comm, mul_eq_zero, inner_self_eq_zero, EuclideanGeometry.Sphere.secondInter, or_iff_right, or_iff_left, div_eq_zero_iff, vsub_self, eq_vadd_iff_vsub_eq, smul_eq_zero