awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (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
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)
rw :
  (∀ (i_1 : Fin (n + 1)),
      Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ i_1 →
        0 <
          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) ∧
    ∀ i_1 ∉ {i}ᶜ,
      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 =
        0
⊢ Membership.mem (α := P) (sx.face ⋯).interior
    ((Finset.affineCombination ℝ Finset.univ sx.points : (a : Fin (n + 1) → ℝ) → P)
        (r • (w - Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) + Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) :
      P)
have hw₁ : 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: rw [Affine.Simplex.affineCombination_mem_interior_face_iff_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (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
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)
⊢ (∀ (i_1 : Fin (n + 1)),
      Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ i_1 →
        0 <
          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) ∧
    ∀ i_1 ∉ {i}ᶜ,
      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 =
        0
have simp : (∀ (i_1 : Fin (n + 1)),
    ¬i_1 = i →
      0 <
        HAdd.hAdd (β := ℝ) (r * HSub.hSub (β := ℝ) (w i_1) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 i_1 : ℝ))
          (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 i_1 : ℝ)) ∧
  r * (w i - 1) + 1 = 0
Tactic: simp only [Finset.mem_compl, Finset.mem_singleton, Pi.add_apply, Pi.smul_apply, Pi.sub_apply,
      smul_eq_mul, Decidable.not_not, forall_eq, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.SecondInter (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
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)
⊢ (∀ (i_1 : Fin (n + 1)),
      ¬i_1 = i →
        0 <
          HAdd.hAdd (β := ℝ) (r * HSub.hSub (β := ℝ) (w i_1) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 i_1 : ℝ))
            (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1 i_1 : ℝ)) ∧
    r * (w i - 1) + 1 = 0
have refine : ∀ (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: refine ⟨fun j hj ↦ ?_, by grind⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
p q : P
as : AffineSubspace ℝ P
hp : s.IsTangentAt p as
hq : s.IsTangentAt q as
⊢ p = q
have hqp : ⟪q -ᵥ p, p -ᵥ s.center⟫ = 0
Tactic: have hqp := hp.inner_left_eq_zero_of_mem hq.mem_space
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
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
have hpq : ⟪p -ᵥ q, q -ᵥ s.center⟫ = 0
Tactic: have hpq := hq.inner_left_eq_zero_of_mem hp.mem_space
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
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
have hqp₁ : ⟪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
Cleared hypotheses: hqp, hpq
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
as : AffineSubspace ℝ P
⊢ s.IsTangentAt s.center as ↔ s.radius = 0 ∧ s.center ∈ as
have refine_1 : s.IsTangentAt s.center as → s.radius = 0 ∧ s.center ∈ as
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
as : AffineSubspace ℝ P
refine_1 : s.IsTangentAt s.center as → s.radius = 0 ∧ s.center ∈ as
⊢ s.IsTangentAt s.center as ↔ s.radius = 0 ∧ s.center ∈ as
have refine_2 : s.radius = 0 ∧ s.center ∈ as → s.IsTangentAt s.center as
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
as : AffineSubspace ℝ P
hr : s.center ∈ s
hm : s.center ∈ as
⊢ s.radius = 0 ∧ s.center ∈ as
have hr₁ : s.radius = 0
Tactic: rw [center_mem_iff] at hr
Cleared hypotheses: hr, hm
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
as : AffineSubspace ℝ P
hr : s.radius = 0
hm : s.center ∈ as
⊢ s.IsTangentAt s.center as
have refine_2 : s.center ∈ s
Tactic: refine ⟨?_, hm, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
as : AffineSubspace ℝ P
hr : s.radius = 0
hm : s.center ∈ as
refine_2 : s.center ∈ s
⊢ s.IsTangentAt s.center as
have refine_2₁ : as ≤ s.orthRadius s.center
Tactic: refine ⟨?_, hm, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
as : AffineSubspace ℝ P
hr : s.radius = 0
hm : s.center ∈ as
refine_2 : s.radius = 0
⊢ s.center ∈ s
have refine_2₁ : Eq (α := ℝ) 0 0
Tactic: rw [center_mem_iff, hr]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
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 (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p) 2
have rw : HPow.hPow (β := ℕ) (dist q s.center) 2 = HPow.hPow (β := ℕ) (dist p s.center) 2 + HPow.hPow (β := ℕ) (dist q p) 2
Tactic: rw [← h.mem_sphere]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
p q : P
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
⊢ q ∈ s ∧ q ∈ as ↔ q = p
have refine_1 : q ∈ s ∧ q ∈ as → ∀ (hs : q ∈ s) (has : q ∈ as), q = p
Tactic: refine ⟨fun ⟨hs, has⟩ ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
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
⊢ q ∈ s ∧ q ∈ as ↔ q = p
have refine_2 : q = p → q ∈ s ∧ q ∈ as
Tactic: refine ⟨fun ⟨hs, has⟩ ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
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
⊢ q = p
have hd : 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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
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
⊢ q = p
have hd₁ : HPow.hPow (β := ℕ) s.radius 2 = HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p) 2
Tactic: rw [hs] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
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₂
⊢ dist q p₁ = dist q p₂
have h1 : 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₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
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
⊢ dist q p₁ = dist q p₂
have h2 : 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₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
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
⊢ dist q p₁ = dist q p₂
have 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₂
Tactic: rwa [h1, add_left_cancel_iff, sq_eq_sq₀ dist_nonneg dist_nonneg] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
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₂
⊢ dist q p₁ = dist q p₂
have rwa₁ : ∀ (h2 : HPow.hPow (β := ℕ) (dist q p₁) 2 = HPow.hPow (β := ℕ) (dist q p₂) 2), dist q p₁ = dist q p₂
Tactic: rwa [h1, add_left_cancel_iff, sq_eq_sq₀ dist_nonneg dist_nonneg] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
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₂
⊢ dist q p₁ = dist q p₂
have rwa₂ : ∀ (h2 : 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
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
as : AffineSubspace ℝ P
p q : P
h : s.IsTangentAt p as
hq : q ∈ as
hqp : q ≠ p
⊢ s.radius < dist q s.center
have suffices : HPow.hPow (β := ℕ) s.radius 2 < HPow.hPow (β := ℕ) (dist q s.center) 2
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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
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 (β := ℕ) (dist q s.center) 2
have rw : HPow.hPow (β := ℕ) s.radius 2 < HPow.hPow (β := ℕ) s.radius 2 + HPow.hPow (β := ℕ) (dist q p) 2
Tactic: rw [h.dist_sq_eq_of_mem hq]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
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
⊢ as = s.orthRadius p
have this : FiniteDimensional ℝ V
Tactic: have : FiniteDimensional ℝ V := Module.finite_of_finrank_eq_succ hfr.symm
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
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
⊢ as = s.orthRadius p
have hp : p ≠ s.center
Tactic: have hp : p ≠ s.center := fun h ↦ (h ▸ s.center_mem_iff).not.2 hr ht.mem_sphere
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
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
⊢ as = s.orthRadius p
have hfr₁ : 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
Cleared hypotheses: hfr, this, hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
p : P
⊢ s.IsTangent (s.orthRadius p) ↔ p ∈ s
have refine : s.IsTangent (s.orthRadius p) → p ∈ s
Tactic: refine ⟨?_, fun h ↦ (isTangentAt_orthRadius_iff_mem.2 h).isTangent⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
p q : P
hs : q ∈ s
hsp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
hle : LE.le (α := AffineSubspace ℝ P) (s.orthRadius p) (s.orthRadius q)
⊢ p ∈ s
have hle₁ : p = q ∨ q = s.center
Tactic: rw [orthRadius_le_orthRadius_iff] at hle
Cleared hypotheses: hle
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
p q : P
hs : q ∈ s
hsp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
hle : p = q ∨ q = s.center
⊢ p ∈ s
have inl : ∀ (hs : p ∈ s) (hsp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p), p ∈ s
Tactic: rcases hle with rfl | rfl
Cleared hypotheses: q, hs, hsp, hle
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
p q : P
hs : q ∈ s
hsp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) q
hle : p = q ∨ q = s.center
inl : ∀ (hs : p ∈ s) (hsp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) p), p ∈ s
⊢ p ∈ s
have inr : ∀ (hs : s.center ∈ s) (hsp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) s.center), p ∈ s
Tactic: rcases hle with rfl | rfl
Cleared hypotheses: q, hs, hsp, hle
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
p : P
hs : s.center ∈ s
hsp : Membership.mem (γ := AffineSubspace ℝ P) (s.orthRadius p) s.center
⊢ p ∈ s
have hsp₁ : p = s.center
Tactic: rw [center_mem_orthRadius_iff] at hsp
Cleared hypotheses: hsp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
p : P
hs : s.center ∈ s
hsp : p = s.center
⊢ p ∈ s
have inr : ∀ (hs : p ∈ s) (hsp : p = s.center), p ∈ s
Tactic: rwa [← hsp] at hs
Cleared hypotheses: hs, hsp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
as : AffineSubspace ℝ P
h : s.IsTangent as
p : P
hp : p ∈ as
⊢ s.radius ≤ dist p s.center
have obtain : ∀ (x : P) (h : s.IsTangentAt x as), s.radius ≤ dist p s.center
Tactic: obtain ⟨x, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
as : AffineSubspace ℝ P
p : P
hp : p ∈ as
x : P
h : s.IsTangentAt x as
⊢ s.radius ≤ dist p s.center
have refine : HPow.hPow (β := ℕ) s.radius 2 ≤ HPow.hPow (β := ℕ) (dist p s.center) 2
Tactic: refine le_of_sq_le_sq ?_ dist_nonneg
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
as : AffineSubspace ℝ P
p : P
hp : p ∈ as
x : P
h : s.IsTangentAt x as
⊢ HPow.hPow (β := ℕ) s.radius 2 ≤ HPow.hPow (β := ℕ) (dist p s.center) 2
have rw : 0 ≤ HPow.hPow (β := ℕ) (dist p x) 2
Tactic: rw [h.dist_sq_eq_of_mem hp, le_add_iff_nonneg_right]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
as : AffineSubspace ℝ P
h : s.IsTangent as
p : P
hp : dist p s.center < s.radius
⊢ p ∉ as
have contrapose! : ∀ (hp : p ∈ as), s.radius ≤ dist p s.center
Tactic: contrapose! hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
as : AffineSubspace ℝ P
h : s.IsTangent as
⊢ Metric.infDist s.center (↑as : Set P) = s.radius
have obtain : ∀ (p : P) (h : s.IsTangentAt p as), Metric.infDist s.center (↑as : Set P) = s.radius
Tactic: obtain ⟨p, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Sphere.Tangent (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
s : Sphere P
as : AffineSubspace ℝ P
p : P
h : s.IsTangentAt p as
⊢ Metric.infDist s.center (↑as : Set P) = s.radius
have refine_1 : Metric.infDist s.center (↑as : Set P) ≤ s.radius
Tactic: refine le_antisymm ?_ ?_