mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h✝ :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ u,
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
x : EuclideanSpace ℝ (Fin n)
x✝ : x ∈ Set.univ
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
h : d.isPlot (p ∘ ↑(OpenPartialHomeomorph.univBall x ε))
h' : d.isPlotOn ⋯ ((p ∘ ↑(OpenPartialHomeomorph.univBall x ε)) ∘ ↑(OpenPartialHomeomorph.univBall x ε).symm)
⊢ Set.EqOn ((p ∘ ↑(OpenPartialHomeomorph.univBall x ε)) ∘ ↑(OpenPartialHomeomorph.univBall x ε).symm) p
    (Metric.ball x ε)

Tactic:
Function.comp_assoc,

Goal state after:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h✝ :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ u,
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
x : EuclideanSpace ℝ (Fin n)
x✝ : x ∈ Set.univ
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
h : d.isPlot (p ∘ ↑(OpenPartialHomeomorph.univBall x ε))
h' : d.isPlotOn ⋯ ((p ∘ ↑(OpenPartialHomeomorph.univBall x ε)) ∘ ↑(OpenPartialHomeomorph.univBall x ε).symm)
⊢ Set.EqOn (p ∘ ↑(OpenPartialHomeomorph.univBall x ε) ∘ ↑(OpenPartialHomeomorph.univBall x ε).symm) p (Metric.ball x ε)
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : FiniteDimensional ℝ X
u : Set X
h : ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X), ContDiff ℝ ∞ p → IsOpen (p ⁻¹' u)
⊢ TopologicalSpace.IsOpen (⇑toEuclidean ⁻¹' ⇑toEuclidean.symm ⁻¹' u)

Tactic:
exact toEuclidean.continuous.isOpen_preimage _ (h _ toEuclidean.symm.contDiff)

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

Goal state before:
pp: case refine_3
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
hf : Function.Injective ⇑f.linear
⊢ (Submodule.map f.linear (vectorSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ vectorSpan ℝ (⇑f.toAffineMap '' Set.range s.points) =
    (Submodule.map f.linear (vectorSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ f.linear.range ⊓
      Submodule.map f.linear (vectorSpan ℝ (Set.range s.points))

Tactic:
inf_assoc,

Goal state after:
case refine_3
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
hf : Function.Injective ⇑f.linear
⊢ (Submodule.map f.linear (vectorSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ vectorSpan ℝ (⇑f.toAffineMap '' Set.range s.points) =
    (Submodule.map f.linear (vectorSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓
      (f.linear.range ⊓ Submodule.map f.linear (vectorSpan ℝ (Set.range s.points)))
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
this : Nontrivial V
⊢ LinearMap.det ↑(o.rotation θ).toLinearEquiv = 1

Tactic:
obtain ⟨x, hx⟩ : ∃ x, x ≠ (0 : V) := exists_ne (0 : V)

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ LinearMap.det ↑(o.rotation θ).toLinearEquiv = 1
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
hps : ps ⊆ ↑s
p : P
⊢ (∃ r, ∀ p₁ ∈ ps, dist p₁ p = r) ↔ ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑((orthogonalProjection s) p) = r

Tactic:
have h := dist_set_eq_iff_dist_orthogonalProjection_eq hps p

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
hps : ps ⊆ ↑s
p : P
h :
  (ps.Pairwise fun p₁ p₂ ↦ dist p₁ p = dist p₂ p) ↔
    ps.Pairwise fun p₁ p₂ ↦ dist p₁ ↑((orthogonalProjection s) p) = dist p₂ ↑((orthogonalProjection s) p)
⊢ (∃ r, ∀ p₁ ∈ ps, dist p₁ p = r) ↔ ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑((orthogonalProjection s) p) = r
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
⊢ ∃ θ, f = o.rotation θ

Tactic:
obtain ⟨x, hx⟩ : ∃ x, x ≠ (0 : V) := exists_ne (0 : V)

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ∃ θ, f = o.rotation θ
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ -⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ < s.height i * s.height j

Tactic:
refine lt_of_abs_lt ?_

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ |(-⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫)| < s.height i * s.height j
Module: Mathlib.Geometry.Euclidean.Altitude

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
n : ℕ
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
⊢ -(s.height i * s.height j) < ⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫

Tactic:
by
  obtain rfl | hij := eq_or_ne i j
  · rw [real_inner_self_eq_norm_sq]
    refine lt_of_lt_of_le (b := 0) ?_ ?_
    · rw [neg_lt_zero]
      positivity
    · positivity
  rw [neg_lt]
  refine lt_of_abs_lt ?_
  rw [abs_neg]
  exact abs_inner_vsub_altitudeFoot_lt_mul s hij

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π * 2 - π = 0
⊢ False

pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 = π
⊢ 2 ≠ 0

Tactic:
mul_two,

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π + π - π = 0
⊢ False

V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
hswx : (o.oangle w x).sign = 0
hsyz : (o.oangle y z).sign = 0
hwx : InnerProductGeometry.angle w x = π / 2
hyz : InnerProductGeometry.angle y z = π / 2
hpi : π / 2 = π
⊢ 2 ≠ 0
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x ≠ 0 ∨ -y = 0
⊢ Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖

Tactic:
rw [sub_eq_add_neg, tan_angle_add_mul_norm_of_inner_eq_zero h h0, norm_neg]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x + y) y).sin = ‖x‖ / ‖x + y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
  rw [add_comm]
  exact (-o).sin_oangle_add_right_of_oangle_eq_pi_div_two h

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case neg.refine_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
h : InnerProductGeometry.angle x y = π / 2
⊢ o.oangle x y = ↑(π / 2) ∨ o.oangle x y = ↑(-π / 2)

Tactic:
convert! o.oangle_eq_angle_or_eq_neg_angle hx hy using 2

Goal state after:
case e'_1
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
h : InnerProductGeometry.angle x y = π / 2
⊢ ↑(π / 2) = ↑(InnerProductGeometry.angle x y)

case e'_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
h : InnerProductGeometry.angle x y = π / 2
⊢ ↑(-π / 2) = -↑(InnerProductGeometry.angle x y)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

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
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂

Tactic:
by
  rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
    inner_neg_left, neg_vsub_eq_vsub_rev] at h
  rw [ne_comm, ← @vsub_ne_zero V, ← @vsub_eq_zero_iff_eq V, or_comm] at h0
  rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub' V p₃ p₂, ← vsub_add_vsub_cancel p₁ p₂ p₃,
    add_comm, tan_angle_add_mul_norm_of_inner_eq_zero h h0]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case neg.inr.inl
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 : Collinear ℝ {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₂ p₁' p₁
⊢ 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₁' p₂ p₃

Tactic:
rw [hw.oangle_eq_left hp₁'p₂]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection

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
p p' : P
s : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
h : p' ∈ s
⊢ ∠ p (↑((orthogonalProjection s) p)) p' = π / 2

Tactic:
by
  have : Nonempty s := ⟨p', h⟩
  rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
  exact Submodule.inner_left_of_mem_orthogonal (K := s.direction)
    (AffineSubspace.vsub_mem_direction h (orthogonalProjection_mem _))
    (vsub_orthogonalProjection_mem_direction_orthogonal _ _)

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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h' : p ∈ s₁
⊢ dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p) ↔
    ∠ p p' ↑((orthogonalProjection s₁) p) = ∠ p p' ↑((orthogonalProjection s₂) p)

Tactic:
exact dist_orthogonalProjection_eq_iff_angle_eq_aux₁ hp'₁ hp'₂ h'

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

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
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).tan = dist p₁ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.tan_coe,
    dist_div_tan_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (right_ne_of_oangle_eq_pi_div_two h))]

Goal state after:
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₂
⊢ Wbtw ℝ p₁ s.center p₂

Tactic:
by
  rw [← h.midpoint_eq_center]
  exact wbtw_midpoint _ _ _

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

Goal state before:
pp: case inl.inl.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
h : dist s.center s.center < s.radius
hs : Nontrivial V
⊢ (Metric.sphere s.center s.radius).Nonempty

Tactic:
obtain ⟨v, hv⟩ := exists_norm_eq V (dist_nonneg.trans_lt h).le

Goal state after:
case inl.inl.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
h : dist s.center s.center < s.radius
hs : Nontrivial V
v : V
hv : ‖v‖ = s.radius
⊢ (Metric.sphere s.center s.radius).Nonempty
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
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
hv0 : v ≠ 0
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) =
    {(√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • v +ᵥ p, -(√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • v +ᵥ p}

Tactic:
by
  convert!
    inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one hp hpc (v := ‖v‖⁻¹ • v)
      (Submodule.smul_mem _ _ hv) ?_ using 2
  · simp [div_eq_mul_inv, smul_smul]
  · simp [div_eq_mul_inv, smul_smul]
  · simp [norm_smul, norm_ne_zero_iff.2 hv0]

Goal state after:
Module: Mathlib.Geometry.Euclidean.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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ 0 < s.excenterWeights ∅ i

Tactic:
simp only [excenterWeights, excenterWeightsUnnorm_empty_apply, Pi.smul_apply, smul_eq_mul]
  positivity

Goal state after:
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
h₁ : ∡ (t.points i₂) (t.points i₁) p = ∡ p (t.points i₁) (t.points i₃) + ↑π
h₂ : ∡ (t.points i₃) (t.points i₂) p = ∡ p (t.points i₂) (t.points i₁) + ↑π
⊢ 2 • ∡ (t.points i₂) (t.points i₁) ?m.162 = 2 • ∡ ?m.162 (t.points i₁) (t.points i₃)

Tactic:
by rw [h₁]; simp

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

Goal state before:
pp: case e'_2.a
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
i : Fin (n + 1)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ∈ (Finset.univ.erase 0).erase i
⊢ (s.height j)⁻¹ ^ 2 * ⟪s.points i -ᵥ s.points 0, s.points j -ᵥ s.altitudeFoot j⟫ = 0

Tactic:
convert! mul_zero _

Goal state after:
case e'_2.e'_6
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
i : Fin (n + 1)
hi : i ≠ 0
j : Fin (n + 1)
hj : j ∈ (Finset.univ.erase 0).erase i
⊢ ⟪s.points i -ᵥ s.points 0, s.points j -ᵥ s.altitudeFoot j⟫ = 0
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case e'_2
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₂ p₃ p₁
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ dist p₁ p₂ = ‖p₂ -ᵥ p₁‖

Tactic:
rw [dist_eq_norm_vsub']

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

Goal state before:
pp: case e'_3
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₂ p₃ p₁
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ dist p₁ p₃ = ‖p₃ -ᵥ p₁‖

Tactic:
rw [dist_eq_norm_vsub']

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

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
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h : 2 • ∡ (t.points i₁) p (t.points i₃) = 2 • ∡ (t.points i₁) (t.points i₂) (t.points i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = t.points i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = t.points i₃
ha : AffineIndependent ℝ t'p
t' : Triangle ℝ P := { points := t'p, independent := ha }
h₁' : t'.points i₁ = t.points i₁
h₂' : t'.points i₂ = p
h₃' : t'.points i₃ = t.points i₃
⊢ p ∈ Simplex.circumsphere t

Tactic:
have h' : (2 : ℤ) • ∡ (t'.points i₁) (t'.points i₂) (t'.points i₃) =
      (2 : ℤ) • ∡ (t.points i₁) (t.points i₂) (t.points i₃) := by rwa [h₁', h₂', h₃']

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)
t : Triangle ℝ P
p : P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h : 2 • ∡ (t.points i₁) p (t.points i₃) = 2 • ∡ (t.points i₁) (t.points i₂) (t.points i₃)
t'p : Fin 3 → P := Function.update t.points i₂ p
h₁ : t'p i₁ = t.points i₁
h₂ : t'p i₂ = p
h₃ : t'p i₃ = t.points i₃
ha : AffineIndependent ℝ t'p
t' : Triangle ℝ P := { points := t'p, independent := ha }
h₁' : t'.points i₁ = t.points i₁
h₂' : t'.points i₂ = p
h₃' : t'.points i₃ = t.points i₃
h' : 2 • ∡ (t'.points i₁) (t'.points i₂) (t'.points i₃) = 2 • ∡ (t.points i₁) (t.points i₂) (t.points i₃)
⊢ p ∈ Simplex.circumsphere t
Module: Mathlib.Geometry.Euclidean.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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ (s.exsphere signs).IsTangentAt (s.touchpoint signs i) (affineSpan ℝ (Set.range (s.faceOpposite i).points))

Tactic:
rw [touchpoint, orthogonalProjectionSpan, excenter,
    ← EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt,
    ← orthogonalProjectionSpan, ← excenter, ← exradius, ← touchpoint, h.dist_excenter]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - ⟪x, y⟫ ^ 2 ≠ 0
⊢ x = ⟪y, x⟫ • y + ((1 - ⟪y, x⟫ ^ 2) / ‖x - ⟪y, x⟫ • y‖ ^ 2) • (x - ⟪y, x⟫ • y)

Tactic:
← real_inner_self_eq_norm_sq

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
H : 1 - ⟪x, y⟫ ^ 2 ≠ 0
⊢ x = ⟪y, x⟫ • y + ((1 - ⟪y, x⟫ ^ 2) / ⟪x - ⟪y, x⟫ • y, x - ⟪y, x⟫ • y⟫) • (x - ⟪y, x⟫ • y)
Module: Mathlib.Geometry.Euclidean.Circumcenter

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 : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
⊢ (∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius) → Cospherical ps

Tactic:
· exact fun ⟨c, _, hd⟩ => ⟨c, hd⟩

Goal state after: