awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
rw : p₁ -ᵥ midpoint ℝ p₁ p₃ = -(p₃ -ᵥ midpoint ℝ p₁ p₃)
rw₁ :
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₃) =
    -(p₃ -ᵥ midpoint ℝ p₁ p₃)
rw₂ :
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₃) =
    -HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₃ -ᵥ p₁)
rw₃ :
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₃) =
    HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (-(p₃ -ᵥ p₁))
⊢ p₁ -ᵥ o = -(p₃ -ᵥ o)
have rw₄ : HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₃) =
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (p₁ -ᵥ p₃)
Tactic: rw [h_center, left_vsub_midpoint, right_vsub_midpoint, ← smul_neg, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
⊢ ⟪p₁ -ᵥ o, p₃ -ᵥ o⟫_ℝ + ⟪p₁ -ᵥ o, o -ᵥ p₂⟫_ℝ + (⟪o -ᵥ p₂, p₃ -ᵥ o⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ) = 0 ↔
    dist s.center p₂ = s.radius
have h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o)
Tactic: have h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o) := by
    rw [h_center, left_vsub_midpoint, right_vsub_midpoint, ← smul_neg, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o)
⊢ ⟪p₁ -ᵥ o, p₃ -ᵥ o⟫_ℝ + ⟪p₁ -ᵥ o, o -ᵥ p₂⟫_ℝ + (⟪o -ᵥ p₂, p₃ -ᵥ o⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ) = 0 ↔
    dist s.center p₂ = s.radius
have rw : -⟪p₃ -ᵥ o, p₃ -ᵥ o⟫_ℝ + -⟪p₃ -ᵥ o, o -ᵥ p₂⟫_ℝ + (⟪p₃ -ᵥ o, o -ᵥ p₂⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ) = 0 ↔
  dist s.center p₂ = s.radius
Tactic: rw [h_opp, inner_neg_left, inner_neg_left, real_inner_comm (p₃ -ᵥ o) (o -ᵥ p₂)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o)
⊢ -⟪p₃ -ᵥ o, p₃ -ᵥ o⟫_ℝ + -⟪p₃ -ᵥ o, o -ᵥ p₂⟫_ℝ + (⟪p₃ -ᵥ o, o -ᵥ p₂⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ) = 0 ↔
    dist s.center p₂ = s.radius
have ring_nf : -⟪p₃ -ᵥ o, p₃ -ᵥ o⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ = 0 ↔ dist s.center p₂ = s.radius
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o)
⊢ -⟪p₃ -ᵥ o, p₃ -ᵥ o⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ = 0 ↔ dist s.center p₂ = s.radius
have rw : s.radius = dist o p₂ ↔ dist s.center p₂ = s.radius
Tactic: rw [neg_add_eq_zero, real_inner_self_eq_norm_sq, ← dist_eq_norm_vsub,
    real_inner_self_eq_norm_sq, ← dist_eq_norm_vsub, sq_eq_sq₀ dist_nonneg dist_nonneg,
    mem_sphere.mp hd.right_mem]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
⊢ s.IsDiameter p₁ p₃
have this : FiniteDimensional ℝ V
Tactic: haveI : FiniteDimensional ℝ V := .of_finrank_eq_succ (Fact.out : finrank ℝ V = 2)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
h : p₁ = p₃
⊢ False
have hangle₁ : 0 = π / 2
Tactic: rw [h, angle_self_of_ne hne₂₃.symm] at hangle
Cleared hypotheses: hangle, this, h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : 0 = π / 2
this : FiniteDimensional ℝ V
h : p₁ = p₃
⊢ False
have linarith : 2 / 2 = 1
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : 0 = π / 2
this : FiniteDimensional ℝ V
h : p₁ = p₃
linarith : 2 / 2 = 1
⊢ False
have linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : 0 = π / 2
this : FiniteDimensional ℝ V
h : p₁ = p₃
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
⊢ False
have linarith₂ : GT.gt (α := ℝ) 2 0
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : 0 = π / 2
this : FiniteDimensional ℝ V
h : p₁ = p₃
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
⊢ False
have linarith₃ : -(HMul.hMul (α := ℝ) 2 0 - 1 * π) + (0 - π) = 0
Tactic: linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
⊢ s.IsDiameter p₁ p₃
have hne₁₃ : p₁ ≠ p₃
Tactic: have hne₁₃ : p₁ ≠ p₃ := fun h ↦ by
    rw [h, angle_self_of_ne hne₂₃.symm] at hangle; linarith [Real.pi_pos]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
hne₁₃ : p₁ ≠ p₃
⊢ s.IsDiameter p₁ p₃
have hd : IsDiameter (Sphere.ofDiameter p₁ p₃) p₁ p₃
Tactic: have hd := Sphere.isDiameter_ofDiameter p₁ p₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
hne₁₃ : p₁ ≠ p₃
hd : IsDiameter (Sphere.ofDiameter p₁ p₃) p₁ p₃
⊢ s = Sphere.ofDiameter p₁ p₃
have by_contra : ∀ (hne : ¬s = Sphere.ofDiameter p₁ p₃), False
Tactic: by_contra hne
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
hne₁₃ : p₁ ≠ p₃
hd : IsDiameter (Sphere.ofDiameter p₁ p₃) p₁ p₃
hne : ¬s = Sphere.ofDiameter p₁ p₃
⊢ False
have this₁ : p₂ = p₁ ∨ p₂ = p₃
Tactic: have := eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two
      (Fact.out : finrank ℝ V = 2) hne hne₁₃ hp₁ hp₃ hp₂
      hd.left_mem hd.right_mem (angle_eq_pi_div_two_iff_mem_sphere_ofDiameter.mp hangle)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
p₁ p₂ p₃ : P
s : Sphere P
inst_4 : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
hne₁₃ : p₁ ≠ p₃
hd : IsDiameter (Sphere.ofDiameter p₁ p₃) p₁ p₃
⊢ s.IsDiameter p₁ p₃
have h_eq : s = Sphere.ofDiameter p₁ p₃
Tactic: have h_eq : s = Sphere.ofDiameter p₁ p₃ := by
    by_contra hne
    have := eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two
      (Fact.out : finrank ℝ V = 2) hne hne₁₃ hp₁ hp₃ hp₂
      hd.left_mem hd.right_mem (angle_eq_pi_div_two_iff_mem_sphere_ofDiameter.mp hangle)
    exact this.elim hne₁₂.symm hne₂₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
hq_mem : q ∈ as
⊢ ∠ q p s.center = π / 2
have h1 : ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
Tactic: have h1 := IsTangentAt.inner_left_eq_zero_of_mem h hq_mem
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
hq_mem : q ∈ as
h1 : ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
⊢ ∠ q p s.center = π / 2
have h1₁ : InnerProductGeometry.angle (q -ᵥ p) (p -ᵥ s.center) = π / 2
Tactic: rw [inner_eq_zero_iff_angle_eq_pi_div_two] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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_mem : q ∈ as
h1 : InnerProductGeometry.angle (q -ᵥ p) (p -ᵥ s.center) = π / 2
⊢ ∠ q p s.center = π / 2
have rw : π - π / 2 = π / 2
Tactic: rw [angle, ← neg_vsub_eq_vsub_rev _ s.center, angle_neg_right, h1]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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_mem : q ∈ as
h1 : InnerProductGeometry.angle (q -ᵥ p) (p -ᵥ s.center) = π / 2
⊢ π - π / 2 = π / 2
have linarith : π - π / 2 < π / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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_mem : q ∈ as
h1 : InnerProductGeometry.angle (q -ᵥ p) (p -ᵥ s.center) = π / 2
linarith : π - π / 2 < π / 2 → 2 / 2 = 1
⊢ π - π / 2 = π / 2
have linarith₁ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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_mem : q ∈ as
h1 : InnerProductGeometry.angle (q -ᵥ p) (p -ᵥ s.center) = π / 2
linarith : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₁ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₃ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π - π / 2 = π / 2
have linarith₄ : π - π / 2 < π / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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_mem : q ∈ as
h1 : InnerProductGeometry.angle (q -ᵥ p) (p -ᵥ s.center) = π / 2
linarith : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₁ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₃ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : π - π / 2 < π / 2 → GT.gt (α := ℝ) 2 0
linarith₅ : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₆ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : π - π / 2 < π / 2 → GT.gt (α := ℝ) 2 0
⊢ π - π / 2 = π / 2
have linarith₈ : π - π / 2 < π / 2 → 2 * π - 1 * π - 1 * π = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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_mem : q ∈ as
h1 : InnerProductGeometry.angle (q -ᵥ p) (p -ᵥ s.center) = π / 2
linarith : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₁ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₃ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : π - π / 2 < π / 2 → GT.gt (α := ℝ) 2 0
linarith₅ : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₆ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : π - π / 2 < π / 2 → GT.gt (α := ℝ) 2 0
linarith₈ : π - π / 2 < π / 2 → 2 * π - 1 * π - 1 * π = 0
⊢ π - π / 2 = π / 2
have linarith₉ : π / 2 < π - π / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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_mem : q ∈ as
h1 : InnerProductGeometry.angle (q -ᵥ p) (p -ᵥ s.center) = π / 2
linarith : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₁ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₃ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : π - π / 2 < π / 2 → GT.gt (α := ℝ) 2 0
linarith₅ : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₆ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : π - π / 2 < π / 2 → GT.gt (α := ℝ) 2 0
linarith₈ : π - π / 2 < π / 2 → 2 * π - 1 * π - 1 * π = 0
linarith₉ : π / 2 < π - π / 2 → 2 / 2 = 1
⊢ π - π / 2 = π / 2
have linarith₁₀ : π / 2 < π - π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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_mem : q ∈ as
h1 : InnerProductGeometry.angle (q -ᵥ p) (p -ᵥ s.center) = π / 2
linarith : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₁ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₃ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : π - π / 2 < π / 2 → GT.gt (α := ℝ) 2 0
linarith₅ : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₆ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : π - π / 2 < π / 2 → GT.gt (α := ℝ) 2 0
linarith₈ : π - π / 2 < π / 2 → 2 * π - 1 * π - 1 * π = 0
linarith₉ : π / 2 < π - π / 2 → 2 / 2 = 1
linarith₁₀ : π / 2 < π - π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : π / 2 < π - π / 2 → 2 / 2 = 1
linarith₁₂ : π / 2 < π - π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ π - π / 2 = π / 2
have linarith₁₃ : π / 2 < π - π / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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_mem : q ∈ as
h1 : InnerProductGeometry.angle (q -ᵥ p) (p -ᵥ s.center) = π / 2
linarith : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₁ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₃ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₄ : π - π / 2 < π / 2 → GT.gt (α := ℝ) 2 0
linarith₅ : π - π / 2 < π / 2 → 2 / 2 = 1
linarith₆ : π - π / 2 < π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : π - π / 2 < π / 2 → GT.gt (α := ℝ) 2 0
linarith₈ : π - π / 2 < π / 2 → 2 * π - 1 * π - 1 * π = 0
linarith₉ : π / 2 < π - π / 2 → 2 / 2 = 1
linarith₁₀ : π / 2 < π - π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : π / 2 < π - π / 2 → 2 / 2 = 1
linarith₁₂ : π / 2 < π - π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₃ : π / 2 < π - π / 2 → GT.gt (α := ℝ) 2 0
linarith₁₄ : π / 2 < π - π / 2 → 2 / 2 = 1
linarith₁₅ : π / 2 < π - π / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₆ : π / 2 < π - π / 2 → GT.gt (α := ℝ) 2 0
⊢ π - π / 2 = π / 2
have linarith₁₇ : π / 2 < π - π / 2 → 1 * π - (2 * π - 1 * π) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
h : ∠ q p s.center = π / 2
hp : p ∈ s
⊢ s.IsTangentAt p (affineSpan ℝ {p, q})
have hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p
Tactic: have hp_mem := left_mem_affineSpan_pair ℝ p q
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
h : ∠ q p s.center = π / 2
hp : p ∈ s
hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p
⊢ s.IsTangentAt p (affineSpan ℝ {p, q})
have refine : LE.le (α := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) (s.orthRadius p)
Tactic: refine ⟨hp, hp_mem, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
h : ∠ q p s.center = π / 2
hp : p ∈ s
hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p
⊢ ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
have rwa : ∀ (h : InnerProductGeometry.angle (q -ᵥ p) (s.center -ᵥ p) = π / 2) (hp : p ∈ s)
  (hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p), ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
Tactic: rwa [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, ← neg_vsub_eq_vsub_rev p s.center,
      inner_neg_right, neg_eq_zero] at h
Cleared hypotheses: h, hp, hp_mem
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
h : ∠ q p s.center = π / 2
hp : p ∈ s
hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p
rwa :
  ∀ (h : InnerProductGeometry.angle (q -ᵥ p) (s.center -ᵥ p) = π / 2) (hp : p ∈ s)
    (hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p), ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
⊢ ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
have rwa₁ : ∀ (h : ⟪q -ᵥ p, s.center -ᵥ p⟫_ℝ = 0) (hp : p ∈ s)
  (hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p), ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
Tactic: rwa [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, ← neg_vsub_eq_vsub_rev p s.center,
      inner_neg_right, neg_eq_zero] at h
Cleared hypotheses: h, hp, hp_mem
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
h : ∠ q p s.center = π / 2
hp : p ∈ s
hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p
rwa :
  ∀ (h : InnerProductGeometry.angle (q -ᵥ p) (s.center -ᵥ p) = π / 2) (hp : p ∈ s)
    (hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p), ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
rwa₁ :
  ∀ (h : ⟪q -ᵥ p, s.center -ᵥ p⟫_ℝ = 0) (hp : p ∈ s)
    (hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p), ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
⊢ ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
have rwa₂ : ∀ (h : ⟪q -ᵥ p, -(p -ᵥ s.center)⟫_ℝ = 0) (hp : p ∈ s)
  (hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p), ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
Tactic: rwa [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, ← neg_vsub_eq_vsub_rev p s.center,
      inner_neg_right, neg_eq_zero] at h
Cleared hypotheses: h, hp, hp_mem
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Sphere (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
h : ∠ q p s.center = π / 2
hp : p ∈ s
hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p
rwa :
  ∀ (h : InnerProductGeometry.angle (q -ᵥ p) (s.center -ᵥ p) = π / 2) (hp : p ∈ s)
    (hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p), ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
rwa₁ :
  ∀ (h : ⟪q -ᵥ p, s.center -ᵥ p⟫_ℝ = 0) (hp : p ∈ s)
    (hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p), ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
rwa₂ :
  ∀ (h : ⟪q -ᵥ p, -(p -ᵥ s.center)⟫_ℝ = 0) (hp : p ∈ s)
    (hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p), ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
⊢ ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
have rwa₃ : ∀ (h : -⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0) (hp : p ∈ s)
  (hp_mem : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p, q}) p), ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
Tactic: rwa [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, ← neg_vsub_eq_vsub_rev p s.center,
      inner_neg_right, neg_eq_zero] at h
Cleared hypotheses: h, hp, hp_mem