awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n : ℕ
inst_4 : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (w i)
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P :=
  (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w) :
      (a : ℝ) → P)
    r
hp' :
  p' -ᵥ sx.points i =
    r • ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i)
j : Fin (n + 1)
hj : ¬j = i
⊢ 0 <
    HAdd.hAdd (β := ℝ) (r * HSub.hSub (β := ℝ) (w j) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 j : ℝ))
      (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 j : ℝ)

Tactic:
simp [hj, hrpos, (hw01 j).1]

Premises used: And.left
-- 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
n : ℕ
inst_4 : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ i : Fin (n + 1), w i) 1
hw01 : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) (w i)
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P :=
  (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w) :
      (a : ℝ) → P)
    r
hp' :
  p' -ᵥ sx.points i =
    r • ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P) w -ᵥ sx.points i)
⊢ Eq (α := ℝ)
    (∑ i_1 : Fin (n + 1),
      HAdd.hAdd (β := Fin (n + 1) → ℝ) (r • (w - Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1))
        (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) i_1)
    1

Tactic:
simp [Finset.sum_add_distrib, ← Finset.mul_sum, hw]

Premises used: Finset.mul_sum, Finset.sum_add_distrib
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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.IsTangentAt p (s.orthRadius p) ↔ p ∈ s

Tactic:
⟨fun h ↦ h.mem_sphere, fun h ↦ ⟨h, self_mem_orthRadius _ _, le_rfl⟩⟩

Premises used: le_rfl, EuclideanGeometry.Sphere.IsTangentAt.mem_sphere, EuclideanGeometry.Sphere.IsTangentAt.mk, Iff.intro, EuclideanGeometry.Sphere.self_mem_orthRadius
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
x : P
hx : x ∈ as
⊢ ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0

Tactic:
mem_orthRadius_iff_inner_left.1 (h.le_orthRadius hx)

Premises used: EuclideanGeometry.Sphere.IsTangentAt.le_orthRadius, Iff.mp, EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_left
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
x : P
hx : x ∈ as
⊢ ⟪p -ᵥ s.center, x -ᵥ p⟫ = 0

Tactic:
mem_orthRadius_iff_inner_right.1 (h.le_orthRadius hx)

Premises used: EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_right, EuclideanGeometry.Sphere.IsTangentAt.le_orthRadius, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 q : P
as : AffineSubspace ℝ P
hp : s.IsTangentAt p as
hq : s.IsTangentAt q as
⊢ ⟪q -ᵥ p, p -ᵥ s.center⟫ = 0

Tactic:
have hqp := hp.inner_left_eq_zero_of_mem hq.mem_space
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 q : P
as : AffineSubspace ℝ P
hp : s.IsTangentAt p as
hq : s.IsTangentAt q as
hqp : ⟪q -ᵥ p, p -ᵥ s.center⟫ = 0
⊢ ⟪p -ᵥ q, q -ᵥ s.center⟫ = 0

Tactic:
have hpq := hq.inner_left_eq_zero_of_mem hp.mem_space
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 q : P
as : AffineSubspace ℝ P
hp : s.IsTangentAt p as
hq : s.IsTangentAt q as
hqp : ⟪q -ᵥ p, p -ᵥ s.center⟫ = 0
hpq : ⟪p -ᵥ q, q -ᵥ s.center⟫ = 0
⊢ ⟪p -ᵥ q, p -ᵥ q⟫ = 0

Tactic:
rw [← neg_vsub_eq_vsub_rev, inner_neg_left, neg_eq_zero, ← hpq, ← sub_eq_zero,
    ← inner_sub_right, vsub_sub_vsub_cancel_right] at hqp

Premises used: sub_eq_zero, neg_eq_zero, vsub_sub_vsub_cancel_right, inner_sub_right, neg_vsub_eq_vsub_rev, inner_neg_left
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 q : P
as : AffineSubspace ℝ P
hp : s.IsTangentAt p as
hq : s.IsTangentAt q as
hqp : ⟪q -ᵥ p, p -ᵥ s.center⟫ = 0
hpq : ⟪p -ᵥ q, q -ᵥ s.center⟫ = 0
hqp₁ : ⟪p -ᵥ q, p -ᵥ q⟫ = 0
⊢ ⟪p -ᵥ q, q -ᵥ s.center⟫ = 0

Tactic:
rw [← neg_vsub_eq_vsub_rev, inner_neg_left, neg_eq_zero, ← hpq, ← sub_eq_zero,
    ← inner_sub_right, vsub_sub_vsub_cancel_right] at hqp

Premises used: sub_eq_zero, neg_eq_zero, vsub_sub_vsub_cancel_right, inner_sub_right, neg_vsub_eq_vsub_rev, inner_neg_left
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 q : P
as : AffineSubspace ℝ P
hp : s.IsTangentAt p as
hq : s.IsTangentAt q as
hqp : ⟪p -ᵥ q, p -ᵥ q⟫ = 0
hpq : ⟪p -ᵥ q, q -ᵥ s.center⟫ = 0
⊢ p = q

Tactic:
simpa using hqp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
⊢ s.IsTangentAt s.center as ↔ s.radius = 0 ∧ s.center ∈ as

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
refine_1 : s.IsTangentAt s.center as → s.radius = 0 ∧ s.center ∈ as
refine_2 : s.radius = 0 ∧ s.center ∈ as → s.IsTangentAt s.center as
⊢ s.IsTangentAt s.center as ↔ s.radius = 0 ∧ s.center ∈ as

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
hr : s.center ∈ s
hm : s.center ∈ as
⊢ s.radius = 0

Tactic:
rw [center_mem_iff] at hr

Premises used: EuclideanGeometry.Sphere.center_mem_iff
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
hr : s.center ∈ s
hm : s.center ∈ as
hr₁ : s.radius = 0
⊢ s.center ∈ as

Tactic:
rw [center_mem_iff] at hr

Premises used: EuclideanGeometry.Sphere.center_mem_iff
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
hr : s.radius = 0
hm : s.center ∈ as
⊢ s.radius = 0 ∧ s.center ∈ as

Tactic:
⟨hr, hm⟩

Premises used: And.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
hr : s.radius = 0
hm : s.center ∈ as
⊢ s.radius = 0 ∧ s.center ∈ as

Tactic:
exact ⟨hr, hm⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
hr : s.radius = 0
hm : s.center ∈ as
⊢ s.IsTangentAt s.center as

Tactic:
⟨?_, hm, ?_⟩

Premises used: EuclideanGeometry.Sphere.IsTangentAt.mk
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
hr : s.radius = 0
hm : s.center ∈ as
refine_2 : s.center ∈ s
refine_2₁ : as ≤ s.orthRadius s.center
⊢ s.IsTangentAt s.center as

Tactic:
refine ⟨?_, hm, ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
hr : s.radius = 0
hm : s.center ∈ as
refine_2 : s.radius = 0
refine_2₁ refine_2₂ : Eq (α := ℝ) 0 0
⊢ s.center ∈ s

Tactic:
rw [center_mem_iff, hr]

Premises used: EuclideanGeometry.Sphere.center_mem_iff
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
hr : s.radius = 0
hm : s.center ∈ as
⊢ as ≤ s.orthRadius s.center

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 q : P
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
hq : q ∈ as
rw : HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2
⊢ HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p) 2

Tactic:
rw [← h.mem_sphere]

Premises used: EuclideanGeometry.Sphere.IsTangentAt.mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 q : P
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
hq : q ∈ as
⊢ HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2

Tactic:
s.dist_sq_eq_of_mem_orthRadius (SetLike.le_def.1 h.le_orthRadius hq)

Premises used: SetLike.le_def, EuclideanGeometry.Sphere.dist_sq_eq_of_mem_orthRadius, EuclideanGeometry.Sphere.IsTangentAt.le_orthRadius, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 q : P
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
hq : q ∈ as
⊢ HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2

Tactic:
exact s.dist_sq_eq_of_mem_orthRadius (SetLike.le_def.1 h.le_orthRadius hq)

Premises used: SetLike.le_def, EuclideanGeometry.Sphere.dist_sq_eq_of_mem_orthRadius, EuclideanGeometry.Sphere.IsTangentAt.le_orthRadius, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 q : P
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
⊢ q ∈ s ∧ q ∈ as ↔ q = p

Tactic:
⟨fun ⟨hs, has⟩ ↦ ?_, ?_⟩

Premises used: Iff.intro, Eq, _private.0.EuclideanGeometry.Sphere.IsTangentAt.mem_and_mem_iff_eq.match_1
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 q : P
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
refine_1 : q ∈ s ∧ q ∈ as → ∀ (hs : q ∈ s) (has : q ∈ as), q = p
refine_2 : q = p → q ∈ s ∧ q ∈ as
⊢ q ∈ s ∧ q ∈ as ↔ q = p

Tactic:
refine ⟨fun ⟨hs, has⟩ ↦ ?_, ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 q : P
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
h_1 : q ∈ s ∧ q ∈ as
hs : q ∈ s
has : q ∈ as
⊢ HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p) 2

Tactic:
have hd := h.dist_sq_eq_of_mem has
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 q : P
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
h_1 : q ∈ s ∧ q ∈ as
hs : q ∈ s
has : q ∈ as
hd : HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p) 2
⊢ HPow.hPow (β := ℕ) s.radius 2 = HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p) 2

Tactic:
rw [hs] at hd
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 q : P
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
h_1 : q ∈ s ∧ q ∈ as
hs : q ∈ s
has : q ∈ as
hd : HPow.hPow (β := ℕ) s.radius 2 = HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p) 2
⊢ q = p

Tactic:
simpa using hd
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
q : P
as : AffineSubspace ℝ P
h : s.IsTangentAt q as
⊢ q ∈ s ∧ q ∈ as

Tactic:
⟨h.mem_sphere, h.mem_space⟩

Premises used: EuclideanGeometry.Sphere.IsTangentAt.mem_space, EuclideanGeometry.Sphere.IsTangentAt.mem_sphere, And.intro
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
q : P
as : AffineSubspace ℝ P
h : s.IsTangentAt q as
⊢ q ∈ s ∧ q ∈ as

Tactic:
exact ⟨h.mem_sphere, h.mem_space⟩
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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 q : P
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
hs : q ∈ s
has : q ∈ as
⊢ q = p

Tactic:
h.mem_and_mem_iff_eq.1 ⟨hs, has⟩

Premises used: EuclideanGeometry.Sphere.IsTangentAt.mem_and_mem_iff_eq, And.intro, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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₂ q : P
as₁ as₂ : AffineSubspace ℝ P
h₁ : s.IsTangentAt p₁ as₁
h₂ : s.IsTangentAt p₂ as₂
hq_mem₁ : q ∈ as₁
hq_mem₂ : q ∈ as₂
⊢ HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p₁) 2

Tactic:
have h1 := dist_sq_eq_of_mem h₁ hq_mem₁
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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₂ q : P
as₁ as₂ : AffineSubspace ℝ P
h₁ : s.IsTangentAt p₁ as₁
h₂ : s.IsTangentAt p₂ as₂
hq_mem₁ : q ∈ as₁
hq_mem₂ : q ∈ as₂
h1 : HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p₁) 2
⊢ HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p₂) 2

Tactic:
have h2 := dist_sq_eq_of_mem h₂ hq_mem₂
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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₂ q : P
as₁ as₂ : AffineSubspace ℝ P
h₁ : s.IsTangentAt p₁ as₁
h₂ : s.IsTangentAt p₂ as₂
hq_mem₁ : q ∈ as₁
hq_mem₂ : q ∈ as₂
h1 : HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p₁) 2
h2 : HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p₂) 2
rwa :
  ∀
    (h2 :
      HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p₁) 2 =
        HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p₂) 2),
    dist q p₁ = dist q p₂
rwa₁ : ∀ (h2 : HPow.hPow (β := ℕ) (dist q p₁) 2 = HPow.hPow (β := ℕ) (dist q p₂) 2), dist q p₁ = dist q p₂
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h2 : dist q p₁ = dist q p₂), dist q p₁ = dist q p₂
⊢ dist q p₁ = dist q p₂

Tactic:
rwa [h1, add_left_cancel_iff, sq_eq_sq₀ dist_nonneg dist_nonneg] at h2

Premises used: dist_nonneg, add_left_cancel_iff, sq_eq_sq₀
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p q : P
h : s.IsTangentAt p as
hq : q ∈ as
hqp : q ≠ p
this : HPow.hPow (β := ℕ) s.radius 2 < HPow.hPow (β := ℕ) (dist q s.center) 2
⊢ s.radius < dist q s.center

Tactic:
simpa [sq_lt_sq, abs_of_nonneg (s.radius_nonneg_of_mem h.mem_sphere)] using this

Premises used: sq_lt_sq, EuclideanGeometry.Sphere.radius_nonneg_of_mem, EuclideanGeometry.Sphere.IsTangentAt.mem_sphere, abs_of_nonneg
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p q : P
h : s.IsTangentAt p as
hq : q ∈ as
hqp : q ≠ p
suffices : HPow.hPow (β := ℕ) s.radius 2 < HPow.hPow (β := ℕ) (dist q s.center) 2
⊢ s.radius < dist q s.center

Tactic:
suffices s.radius ^ 2 < dist q s.center ^ 2 by
    simpa [sq_lt_sq, abs_of_nonneg (s.radius_nonneg_of_mem h.mem_sphere)] using this
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p q : P
h : s.IsTangentAt p as
hq : q ∈ as
hqp : q ≠ p
rw : HPow.hPow (β := ℕ) s.radius 2 < HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p) 2
⊢ HPow.hPow (β := ℕ) s.radius 2 < HPow.hPow (β := ℕ) (dist q s.center) 2

Tactic:
rw [h.dist_sq_eq_of_mem hq]

Premises used: EuclideanGeometry.Sphere.IsTangentAt.dist_sq_eq_of_mem
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p q : P
h : s.IsTangentAt p as
hq : q ∈ as
hqp : q ≠ p
⊢ HPow.hPow (β := ℕ) s.radius 2 < HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p) 2

Tactic:
simp [hqp]
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
ht : s.IsTangentAt p as
hr : s.radius ≠ 0
hfr : Module.finrank.{0, u_1} ℝ ↥as.direction + 1 = Module.finrank ℝ V
⊢ FiniteDimensional ℝ V

Tactic:
have : FiniteDimensional ℝ V := Module.finite_of_finrank_eq_succ hfr.symm
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
ht : s.IsTangentAt p as
hr : s.radius ≠ 0
hfr : Module.finrank.{0, u_1} ℝ ↥as.direction + 1 = Module.finrank ℝ V
this : FiniteDimensional ℝ V
⊢ p ≠ s.center

Tactic:
have hp : p ≠ s.center := fun h ↦ (h ▸ s.center_mem_iff).not.2 hr ht.mem_sphere
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
ht : s.IsTangentAt p as
hr : s.radius ≠ 0
hfr : Module.finrank.{0, u_1} ℝ ↥as.direction + 1 = Module.finrank ℝ V
this : FiniteDimensional ℝ V
hp : p ≠ s.center
⊢ Module.finrank.{0, u_1} ℝ ↥as.direction = Module.finrank.{0, u_1} ℝ ↥(direction (s.orthRadius p))

Tactic:
rw [← finrank_orthRadius hp, Nat.add_right_cancel_iff] at hfr

Premises used: Nat.add_right_cancel_iff, EuclideanGeometry.Sphere.finrank_orthRadius
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
ht : s.IsTangentAt p as
hr : s.radius ≠ 0
hfr : Module.finrank.{0, u_1} ℝ ↥as.direction + 1 = Module.finrank ℝ V
this : FiniteDimensional ℝ V
hp : p ≠ s.center
hfr₁ : Module.finrank.{0, u_1} ℝ ↥as.direction = Module.finrank.{0, u_1} ℝ ↥(direction (s.orthRadius p))
⊢ FiniteDimensional ℝ V

Tactic:
rw [← finrank_orthRadius hp, Nat.add_right_cancel_iff] at hfr

Premises used: Nat.add_right_cancel_iff, EuclideanGeometry.Sphere.finrank_orthRadius
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
ht : s.IsTangentAt p as
hr : s.radius ≠ 0
hfr : Module.finrank.{0, u_1} ℝ ↥as.direction + 1 = Module.finrank ℝ V
this : FiniteDimensional ℝ V
hp : p ≠ s.center
hfr₁ : Module.finrank.{0, u_1} ℝ ↥as.direction = Module.finrank.{0, u_1} ℝ ↥(direction (s.orthRadius p))
this₁ : FiniteDimensional ℝ V
⊢ p ≠ s.center

Tactic:
rw [← finrank_orthRadius hp, Nat.add_right_cancel_iff] at hfr

Premises used: Nat.add_right_cancel_iff, EuclideanGeometry.Sphere.finrank_orthRadius
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
ht : s.IsTangentAt p as
hr : s.radius ≠ 0
hfr : Module.finrank.{0, u_1} ℝ ↥as.direction = Module.finrank.{0, u_1} ℝ ↥(direction (s.orthRadius p))
this : FiniteDimensional ℝ V
hp : p ≠ s.center
⊢ as = s.orthRadius p

Tactic:
eq_of_direction_eq_of_nonempty_of_le
    (Submodule.eq_of_le_of_finrank_eq (direction_le ht.le_orthRadius) hfr) ⟨p, ht.mem_space⟩
    ht.le_orthRadius

Premises used: AffineSubspace.direction_le, EuclideanGeometry.Sphere.IsTangentAt.mem_space, EuclideanGeometry.Sphere.IsTangentAt.le_orthRadius, Submodule.eq_of_le_of_finrank_eq, Exists.intro, AffineSubspace.eq_of_direction_eq_of_nonempty_of_le
-- Module: Mathlib.Geometry.Euclidean.Sphere.Tangent
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
as : AffineSubspace ℝ P
p : P
ht : s.IsTangentAt p as
hr : s.radius ≠ 0
hfr : Module.finrank.{0, u_1} ℝ ↥as.direction = Module.finrank.{0, u_1} ℝ ↥(direction (s.orthRadius p))
this : FiniteDimensional ℝ V
hp : p ≠ s.center
⊢ as = s.orthRadius p

Tactic:
exact eq_of_direction_eq_of_nonempty_of_le
    (Submodule.eq_of_le_of_finrank_eq (direction_le ht.le_orthRadius) hfr) ⟨p, ht.mem_space⟩
    ht.le_orthRadius

Premises used: AffineSubspace.direction_le, EuclideanGeometry.Sphere.IsTangentAt.mem_space, EuclideanGeometry.Sphere.IsTangentAt.le_orthRadius, Submodule.eq_of_le_of_finrank_eq, Exists.intro, AffineSubspace.eq_of_direction_eq_of_nonempty_of_le