mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p ↦ (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}
hc : IsConnected sp
p' : P
hp' : s.SSameSide p₃ p'
⊢ p₂ ≠ p'

Tactic:
rintro rfl

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p ↦ (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}
hc : IsConnected sp
hp' : s.SSameSide p₃ p₂
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₃ p₄
⊢ p₁ ≠ p₃

Tactic:
rintro rfl

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₁ p₄
⊢ False
Module: Mathlib.Geometry.Euclidean.SignedDist

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p x : P
h : ∃ r, ∃ p0 ∈ s, x = r • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ p0
⊢ |(s.signedInfDist p) x| = dist x ↑((orthogonalProjection s) x)

Tactic:
rcases h with ⟨r, p₀, hp₀, rfl⟩

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
r : ℝ
p₀ : P
hp₀ : p₀ ∈ s
⊢ |(s.signedInfDist p) (r • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ p₀)| =
    dist (r • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ p₀)
      ↑((orthogonalProjection s) (r • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ p₀))
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
⊢ p₃ ≠ p₂

Tactic:
rintro rfl

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₃ p₄ : P
h₁₂ : p₁ ≠ p₃
ha : ∡ p₁ p₃ p₃ = ∡ p₃ p₃ p₄
hs : line[ℝ, p₁, p₃].SSameSide p₃ p₄
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₂
⊢ p₄ ≠ p₂

Tactic:
rintro rfl

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₃ p₄ : P
h₁₂ : p₁ ≠ p₄
ha : ∡ p₁ p₄ p₃ = ∡ p₃ p₄ p₄
hs : line[ℝ, p₁, p₄].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₄
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : line[ℝ, p₁, p₂].SOppSide p₃ p₄
⊢ p₃ ≠ p₂

Tactic:
rintro rfl

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₃ p₄ : P
h₁₂ : p₁ ≠ p₃
ha : ∡ p₁ p₃ p₃ = ∡ p₃ p₃ p₄
hs : line[ℝ, p₁, p₃].SOppSide p₃ p₄
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : line[ℝ, p₁, p₂].SOppSide p₃ p₄
h₃₂ : p₃ ≠ p₂
⊢ p₄ ≠ p₂

Tactic:
rintro rfl

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₃ p₄ : P
h₁₂ : p₁ ≠ p₄
ha : ∡ p₁ p₄ p₃ = ∡ p₃ p₄ p₄
hs : line[ℝ, p₁, p₄].SOppSide p₃ p₄
h₃₂ : p₃ ≠ p₄
⊢ False
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
⊢ Sphere.ofDiameter p₁ p₂ = s → s.IsDiameter p₁ p₂

Tactic:
rintro rfl

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ (Sphere.ofDiameter p₁ p₂).IsDiameter p₁ p₂
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + ↑π
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
⊢ p₃ ≠ p₂

Tactic:
rintro rfl

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₃ p₄ : P
h₁₂ : p₁ ≠ p₃
ha : ∡ p₁ p₃ p₃ = ∡ p₃ p₃ p₄ + ↑π
hs : line[ℝ, p₁, p₃].SSameSide p₃ p₄
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + ↑π
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₂
⊢ p₄ ≠ p₂

Tactic:
rintro rfl

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₃ p₄ : P
h₁₂ : p₁ ≠ p₄
ha : ∡ p₁ p₄ p₃ = ∡ p₃ p₄ p₄ + ↑π
hs : line[ℝ, p₁, p₄].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₄
⊢ False
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Cospherical s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
hc : ∃ v, ∀ p_1 ∈ Set.range p, ∃ r, p_1 = r • v +ᵥ p 0
⊢ False

Tactic:
rcases hc with ⟨v, hv⟩

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Cospherical s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv : ∀ p_1 ∈ Set.range p, ∃ r, p_1 = r • v +ᵥ p 0
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + ↑π
hs : line[ℝ, p₁, p₂].SOppSide p₃ p₄
⊢ p₃ ≠ p₂

Tactic:
rintro rfl

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₃ p₄ : P
h₁₂ : p₁ ≠ p₃
ha : ∡ p₁ p₃ p₃ = ∡ p₃ p₃ p₄ + ↑π
hs : line[ℝ, p₁, p₃].SOppSide p₃ p₄
⊢ False
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Cospherical s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv : ∀ (i : Fin 3), ∃ r, p i = r • v +ᵥ p 0
h : v = 0
⊢ False

Tactic:
have he : p 1 = p 0 := by simpa [h] using hv 1

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Cospherical s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv : ∀ (i : Fin 3), ∃ r, p i = r • v +ᵥ p 0
h : v = 0
he : p 1 = p 0
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + ↑π
hs : line[ℝ, p₁, p₂].SOppSide p₃ p₄
h₃₂ : p₃ ≠ p₂
⊢ p₄ ≠ p₂

Tactic:
rintro rfl

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₃ p₄ : P
h₁₂ : p₁ ≠ p₄
ha : ∡ p₁ p₄ p₃ = ∡ p₃ p₄ p₄ + ↑π
hs : line[ℝ, p₁, p₄].SOppSide p₃ p₄
h₃₂ : p₃ ≠ p₄
⊢ False
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p q : P
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
⊢ q = p → q ∈ s ∧ q ∈ as

Tactic:
rintro rfl

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
q : P
as : AffineSubspace ℝ P
h : s.IsTangentAt q as
⊢ q ∈ s ∧ q ∈ as
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case neg.refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ dist p₂ s.center ≤ dist p₁ s.center

Tactic:
hp₁

Goal state after:
case neg.refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ dist p₂ s.center ≤ s.radius
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case neg.refine_2.inl.refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center < s.radius
⊢ p₁ ≠ s.center

Tactic:
rintro rfl

Goal state after:
case neg.refine_2.inl.refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₂ : P
hp₂ : dist p₂ s.center ≤ s.radius
hp₂' : dist p₂ s.center < s.radius
hp₁ : dist s.center s.center = s.radius
h : ¬s.center = p₂
⊢ False
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: case mpr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hp : dist p s.center = s.radius
p' : P
⊢ p' = p → p' ∈ s ∧ p' ∈ s.orthRadius p

Tactic:
rintro rfl

Goal state after:
case mpr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p' : P
hp : dist p' s.center = s.radius
⊢ p' ∈ s ∧ p' ∈ s.orthRadius p'
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case neg.refine_2.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖p₁ -ᵥ s.center‖
⊢ p₁ ≠ s.center

Tactic:
rintro rfl

Goal state after:
case neg.refine_2.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₂ : P
hp₂ : dist p₂ s.center ≤ s.radius
hp₁ : dist s.center s.center = s.radius
h : ¬s.center = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = ‖s.center -ᵥ s.center‖
⊢ False
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center ≤ s.radius
⊢ 0 ≤ ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

Tactic:
rcases inner_pos_or_eq_of_dist_le_radius hp₁ hp₂ with (h | rfl)
  · exact h.le
  · simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hp : s.radius < dist p s.center
p' : P
⊢ 0 ≤ s.radius ∧ p' -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖p' -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2 ↔ p' ∈ ∅

Tactic:
simp only [Set.mem_empty_iff_false, iff_false, not_and]

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hp : s.radius < dist p s.center
p' : P
⊢ 0 ≤ s.radius → p' -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ → ¬‖p' -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
⊢ 0 ≤ s.radius ∧ p' -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖p' -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2 ↔ p' ∈ ∅

Tactic:
simp only [Set.mem_empty_iff_false, iff_false, not_and]

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
⊢ 0 ≤ s.radius → p' -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ → ¬‖p' -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
this : FiniteDimensional ℝ V
ha : ℝ ∙ (p -ᵥ s.center) = ⊤
hpo : p' = p
⊢ ¬0 = s.radius ^ 2 - dist p s.center ^ 2

Tactic:
rw [eq_comm, sub_eq_zero, eq_comm, sq_eq_sq₀ dist_nonneg hr]

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
this : FiniteDimensional ℝ V
ha : ℝ ∙ (p -ᵥ s.center) = ⊤
hpo : p' = p
⊢ ¬dist p s.center = s.radius
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
⊢ s₁.IsExtTangentAt s₂ s₁.center → s₁.radius = 0 ∧ s₁.center ∈ s₂

pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
⊢ s₁.radius = 0 ∧ s₁.center ∈ s₂ → s₁.IsExtTangentAt s₂ s₁.center

Tactic:
· rintro ⟨h₁, h₂, -⟩
    rw [center_mem_iff] at h₁
    exact ⟨h₁, h₂⟩

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
⊢ s₁.radius = 0 ∧ s₁.center ∈ s₂ → s₁.IsExtTangentAt s₂ s₁.center
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
⊢ s₁.IsIntTangentAt s₂ s₁.center → s₁.radius = 0 ∧ s₁.center ∈ s₂

pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
⊢ s₁.radius = 0 ∧ s₁.center ∈ s₂ → s₁.IsIntTangentAt s₂ s₁.center

Tactic:
· rintro ⟨h₁, h₂, -⟩
    rw [center_mem_iff] at h₁
    exact ⟨h₁, h₂⟩

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
⊢ s₁.radius = 0 ∧ s₁.center ∈ s₂ → s₁.IsIntTangentAt s₂ s₁.center
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : ℝ ∙ (p -ᵥ s.center) ≠ ⊤
hn : ¬Subsingleton V
v : V
hv0 : v ≠ 0
hv : ∀ (w : V), ∃ c, c • v = w
c : ℝ
hc : c • v = p -ᵥ s.center
⊢ c ≠ 0

Tactic:
rintro rfl

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
h : dist p s.center < s.radius
hp : p ≠ s.center
hb : ℝ ∙ (p -ᵥ s.center) ≠ ⊤
hn : ¬Subsingleton V
v : V
hv0 : v ≠ 0
hv : ∀ (w : V), ∃ c, c • v = w
hc : 0 • v = p -ᵥ s.center
⊢ False
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case h.left.right
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
p₁ : P
⊢ p₁ ∈ insert p ps → p₁ ∈ Metric.sphere { center := cc₂, radius := cr₂ }.center { center := cc₂, radius := cr₂ }.radius

Tactic:
hp₁

Goal state after:
case h.left.right
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
p₁ : P
hp₁ : p₁ ∈ insert p ps
⊢ p₁ ∈ Metric.sphere { center := cc₂, radius := cr₂ }.center { center := cc₂, radius := cr₂ }.radius
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hpc : p ≠ s.center
⊢ (Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)).ncard ≤ 2

Tactic:
by
  rcases lt_trichotomy (dist p s.center) s.radius with h | h | h
  · exact (ncard_inter_orthRadius_eq_two_of_dist_lt_radius h hpc).le
  · simp [inter_orthRadius_eq_singleton_of_dist_eq_radius h]
  · simp [inter_orthRadius_eq_empty_of_radius_lt_dist h]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hxyne : x ≠ y
hxzne : x ≠ z
hxy : ‖x‖ = ‖y‖
hxz : ‖x‖ = ‖z‖
⊢ y ≠ 0

Tactic:
rintro rfl

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x z : V
hxzne : x ≠ z
hxz : ‖x‖ = ‖z‖
hxyne : x ≠ 0
hxy : ‖x‖ = ‖0‖
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: case mpr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hr : s.radius ≠ 0
⊢ p₁ = p₂ → ∠ p₁ s.center p₂ = 0

Tactic:
rintro rfl

Goal state after:
case mpr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ : P
hp₁ : p₁ ∈ s
hr : s.radius ≠ 0
hp₂ : p₁ ∈ s
⊢ ∠ p₁ s.center p₁ = 0
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
n : ℕ
inst✝¹ : NeZero n
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i : Fin (n + 1)
⊢ {k | k ≠ i}.Nonempty

Tactic:
rw [Finset.filter_ne', ← Finset.card_ne_zero]
    simp only [Finset.mem_univ, Finset.card_erase_of_mem, Finset.card_univ, Fintype.card_fin,
      add_tsub_cancel_right]
    exact NeZero.ne _

Goal state after: