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

Goal state before:
pp: case refine_2.inl
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
p : P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
h' : p ∈ s₁
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
hp'₁ : p ∈ s₁
hp'₂ : p ∈ s₂
h : ∠ p p p = ∠ p p ↑((orthogonalProjection s₂) p)
⊢ p ∈ s₂

Tactic:
exact hp'₂

Goal state after:
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
v : V
p q : P
r : ℝ
⊢ ((signedDist (r • v)) p) q = ↑(SignType.sign r) * ((signedDist v) p) q

Tactic:
simp only [signedDist_apply_apply]
  rw [normalize_smul, real_inner_smul_left]

Goal state after:
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
v w : V
p q : P
⊢ ((signedDist v) p) (w +ᵥ q) = ((signedDist v) (-w +ᵥ p)) q

Tactic:
rw [signedDist_vadd_left_swap, neg_neg]

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

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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
hc : Collinear ℝ {p', ↑((orthogonalProjection s₁) p), ↑((orthogonalProjection s₂) p)}
h₁ : ↑((orthogonalProjection s₁) p) ∈ line[ℝ, p', ↑((orthogonalProjection s₂) p)]
h₁' : ↑((orthogonalProjection s₁) p) ∈ s₁ ⊓ s₂
⊢ ↑((orthogonalProjection (s₁ ⊓ s₂)) ↑((orthogonalProjection s₁) p)) = ↑((orthogonalProjection s₁) p)

Tactic:
orthogonalProjection_eq_self_iff

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
hc : Collinear ℝ {p', ↑((orthogonalProjection s₁) p), ↑((orthogonalProjection s₂) p)}
h₁ : ↑((orthogonalProjection s₁) p) ∈ line[ℝ, p', ↑((orthogonalProjection s₂) p)]
h₁' : ↑((orthogonalProjection s₁) p) ∈ s₁ ⊓ s₂
⊢ ↑((orthogonalProjection s₁) p) ∈ s₁ ⊓ s₂
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
hc : Collinear ℝ {p', ↑((orthogonalProjection s₁) p), ↑((orthogonalProjection s₂) p)}
h₁ : ↑((orthogonalProjection s₁) p) ∈ line[ℝ, p', ↑((orthogonalProjection s₂) p)]
h₁' : ↑((orthogonalProjection s₁) p) ∈ s₁ ⊓ s₂
h₁'' : ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection (s₁ ⊓ s₂)) p)
h₂ : ↑((orthogonalProjection s₂) p) ∈ line[ℝ, p', ↑((orthogonalProjection s₁) p)]
h₂' : ↑((orthogonalProjection s₂) p) ∈ s₁ ⊓ s₂
⊢ ↑((orthogonalProjection (s₁ ⊓ s₂)) ↑((orthogonalProjection s₂) p)) = ↑((orthogonalProjection s₂) p)

Tactic:
orthogonalProjection_eq_self_iff

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
hc : Collinear ℝ {p', ↑((orthogonalProjection s₁) p), ↑((orthogonalProjection s₂) p)}
h₁ : ↑((orthogonalProjection s₁) p) ∈ line[ℝ, p', ↑((orthogonalProjection s₂) p)]
h₁' : ↑((orthogonalProjection s₁) p) ∈ s₁ ⊓ s₂
h₁'' : ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection (s₁ ⊓ s₂)) p)
h₂ : ↑((orthogonalProjection s₂) p) ∈ line[ℝ, p', ↑((orthogonalProjection s₁) p)]
h₂' : ↑((orthogonalProjection s₂) p) ∈ s₁ ⊓ s₂
⊢ ↑((orthogonalProjection s₂) p) ∈ s₁ ⊓ s₂
Module: Mathlib.Geometry.Euclidean.Basic

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 : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
i : Fin 2
⊢ b i ≠ 0

Tactic:
fin_cases i

Goal state after:
case refine_1.«0»
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✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
⊢ b ((fun i ↦ i) ⟨0, ⋯⟩) ≠ 0

case refine_1.«1»
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✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
⊢ b ((fun i ↦ i) ⟨1, ⋯⟩) ≠ 0
Module: Mathlib.Geometry.Euclidean.Basic

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 : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
i j : Fin 2
hij : i ≠ j
⊢ ⟪b i, b j⟫ = 0

Tactic:
fin_cases i

Goal state after:
case refine_2.«0»
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✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
j : Fin 2
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ ⟪b ((fun i ↦ i) ⟨0, ⋯⟩), b j⟫ = 0

case refine_2.«1»
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✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
j : Fin 2
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ ⟪b ((fun i ↦ i) ⟨1, ⋯⟩), b j⟫ = 0
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
h : s.IsDiameter p₁ p₂
hr : s.radius ≠ 0
⊢ Sbtw ℝ p₁ s.center p₂

Tactic:
by
  rw [← h.midpoint_eq_center]
  exact sbtw_midpoint_of_ne _ (h.left_ne_right_iff_radius_ne_zero.2 hr)

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

Goal state before:
pp: case inl
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₂ p₃ : P
h₂ : p ≠ p₂
h : 2 • ∡ p₂ p p = 2 • ∡ p p p₃
h' : ↑((orthogonalProjection line[ℝ, p, p₂]) p) = p
⊢ ↑((orthogonalProjection line[ℝ, p, p₃]) p) = p

Tactic:
orthogonalProjection_eq_self_iff

Goal state after:
case inl
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₂ p₃ : P
h₂ : p ≠ p₂
h : 2 • ∡ p₂ p p = 2 • ∡ p p p₃
h' : ↑((orthogonalProjection line[ℝ, p, p₂]) p) = p
⊢ p ∈ line[ℝ, p, p₃]
Module: Mathlib.Geometry.Euclidean.Basic

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 : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
i : Fin 2
⊢ b i ∈ ↑s.direction

Tactic:
fin_cases i

Goal state after:
case refine_1.«0»
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✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
⊢ b ((fun i ↦ i) ⟨0, ⋯⟩) ∈ ↑s.direction

case refine_1.«1»
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✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
⊢ b ((fun i ↦ i) ⟨1, ⋯⟩) ∈ ↑s.direction
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

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
h : p = q ∨ q = s.center
⊢ s.orthRadius p ≤ s.orthRadius q

Tactic:
rcases h with rfl | rfl <;> 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 q : P
⊢ s.orthRadius p ∥ s.orthRadius q ↔ ∃ r, r ≠ 0 ∧ q -ᵥ s.center = r • (p -ᵥ s.center)

Tactic:
simp_rw [orthRadius, parallel_iff_direction_eq_and_eq_bot_iff_eq_bot, direction_mk',
    Submodule.orthogonalComplement_eq_orthogonalComplement,
    Submodule.span_singleton_eq_span_singleton, ← coe_eq_bot_iff,
    ← Set.not_nonempty_iff_eq_empty, mk'_nonempty, and_true, ← Units.exists_iff_ne_zero, eq_comm,
    Units.smul_def]

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

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h : dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
ho : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
⊢ 2 • ∡ p₂ p₁ p = 2 • ∡ p p₁ p₃

Tactic:
suffices p = p₁ by simp [this]
    have hs := orthogonalProjection_sup_of_orthogonalProjection_eq ho
    have hinf : line[ℝ, p₁, p₂] ⊓ line[ℝ, p₁, p₃] = affineSpan ℝ {p₁} := by
      convert! (ha.inf_affineSpan_eq_affineSpan_inter {0, 1} {0, 2})
      · simp [Set.image_insert_eq]
      · simp [Set.image_insert_eq]
      · suffices {p₁} = ![p₁, p₂, p₃] '' {0} by grind
        simp
    have hsup : line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃] = ⊤ := by
      rw [← AffineSubspace.span_union]
      convert! ha.affineSpan_eq_top_iff_card_eq_finrank_add_one.2 ?_
      · simp
        grind
      · simpa using Fact.out
    have hp : orthogonalProjection (line[ℝ, p₁, p₂]) p = p₁ := by
      suffices (orthogonalProjection (line[ℝ, p₁, p₂]) p : P) ∈ affineSpan ℝ {p₁} by
        simpa using this
      have hi : (orthogonalProjection (line[ℝ, p₁, p₂]) p : P) ∈
          line[ℝ, p₁, p₂] ⊓ line[ℝ, p₁, p₃] :=
        ⟨orthogonalProjection_mem _, ho ▸ orthogonalProjection_mem _⟩
      rwa [hinf] at hi
    rw [← orthogonalProjection_sup_of_orthogonalProjection_eq ho] at hp
    rw [← hp, eq_comm, orthogonalProjection_eq_self_iff, hsup]
    exact AffineSubspace.mem_top ℝ V p

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

Goal state before:
pp: case inr.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 : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr0 : r ≠ 0
hr' : dist q s.center = |r| * dist p s.center
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)

Tactic:
mem_sphere.1 hp,

Goal state after:
case inr.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 : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr0 : r ≠ 0
hr' : dist q s.center = |r| * s.radius
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
i j : Fin (Nat.succ 0).succ.succ
hij : ![i₁, i₂, i₃] i = ![i₁, i₂, i₃] j
⊢ i = j

Tactic:
fin_cases i

Goal state after:
case «0»
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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
j : Fin (Nat.succ 0).succ.succ
hij : ![i₁, i₂, i₃] ((fun i ↦ i) ⟨0, ⋯⟩) = ![i₁, i₂, i₃] j
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = j

case «1»
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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
j : Fin (Nat.succ 0).succ.succ
hij : ![i₁, i₂, i₃] ((fun i ↦ i) ⟨1, ⋯⟩) = ![i₁, i₂, i₃] j
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = j

case «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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
j : Fin (Nat.succ 0).succ.succ
hij : ![i₁, i₂, i₃] ((fun i ↦ i) ⟨2, ⋯⟩) = ![i₁, i₂, i₃] j
⊢ (fun i ↦ i) ⟨2, ⋯⟩ = j
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
i : Fin (Nat.succ 0).succ.succ
⊢ ![t.points i₁, t.points i₂, t.points i₃] i = (t.points ∘ ⇑{ toFun := ![i₁, i₂, i₃], inj' := ⋯ }) i

Tactic:
fin_cases i

Goal state after:
case «0»
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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
⊢ ![t.points i₁, t.points i₂, t.points i₃] ((fun i ↦ i) ⟨0, ⋯⟩) =
    (t.points ∘ ⇑{ toFun := ![i₁, i₂, i₃], inj' := ⋯ }) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
⊢ ![t.points i₁, t.points i₂, t.points i₃] ((fun i ↦ i) ⟨1, ⋯⟩) =
    (t.points ∘ ⇑{ toFun := ![i₁, i₂, i₃], inj' := ⋯ }) ((fun i ↦ i) ⟨1, ⋯⟩)

case «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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
⊢ ![t.points i₁, t.points i₂, t.points i₃] ((fun i ↦ i) ⟨2, ⋯⟩) =
    (t.points ∘ ⇑{ toFun := ![i₁, i₂, i₃], inj' := ⋯ }) ((fun i ↦ i) ⟨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
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

Tactic:
rw [zero_smul, eq_comm, vsub_eq_zero_iff_eq] at hc

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 : p = s.center
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃) + ↑π
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}

Tactic:
have hs := t.excenter_eq_incenter_or_excenter_singleton_of_ne signs h₁₂ h₁₃ h₂₃
  rcases hs with hs | hs | hs | hs
  · rw [hs, t.oangle_incenter_eq h₁₂ h₁₃ h₂₃] at h
    simp [Real.Angle.pi_ne_zero] at h
  · rw [hs, t.oangle_excenter_singleton_eq h₁₂ h₁₃ h₂₃] at h
    simp [Real.Angle.pi_ne_zero] at h
  · exact .inl hs
  · exact .inr hs

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‖
hy : y ≠ 0
hx : x ≠ 0
hz : z ≠ 0
⊢ ↑π - 2 • o.oangle (x - z) x - (↑π - 2 • o.oangle (x - y) x) = 2 • (o.oangle (x - y) x - o.oangle (x - z) x)

Tactic:
by abel

Goal state after:
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case refine_2.refine_2
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 j : Fin (n + 1)
hj : j ∈ {k | k ≠ i}
⊢ -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) < 1

Tactic:
rw [neg_lt]

Goal state after:
case refine_2.refine_2
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 j : Fin (n + 1)
hj : j ∈ {k | k ≠ i}
⊢ -1 < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ ∡ p₁ s.center p₂ = ↑π - 2 • ∡ p₂ p₁ s.center

Tactic:
by
  rw [oangle_eq_pi_sub_two_zsmul_oangle_center_left hp₁ hp₂ h,
    oangle_eq_oangle_of_dist_eq (dist_center_eq_dist_center_of_mem_sphere' hp₂ hp₁)]

Goal state after: