mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: case mp
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
hp's : p' ∈ s
hp'i : p' ∈ s.orthRadius p
h' : s.radius ^ 2 = dist p s.center ^ 2 + dist p' p ^ 2
⊢ p' = p

Tactic:
hp

Goal state after:
case mp
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
hp's : p' ∈ s
hp'i : p' ∈ s.orthRadius p
h' : s.radius ^ 2 = s.radius ^ 2 + dist p' p ^ 2
⊢ p' = p
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case neg.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₂
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖

Tactic:
· rcases hp₂.lt_or_eq with (hp₂' | hp₂')
    · refine ((real_inner_le_norm _ _).trans_lt (mul_lt_mul_of_pos_right ?_ ?_)).ne
      · rwa [← hp₁, @dist_eq_norm_vsub V, @dist_eq_norm_vsub V] at hp₂'
      · rw [norm_pos_iff, vsub_ne_zero]
        rintro rfl
        rw [← hp₁] at hp₂'
        refine (dist_nonneg.not_gt : ¬dist p₂ s.center < 0) ?_
        simpa using hp₂'
    · rw [← hp₁, @dist_eq_norm_vsub V, @dist_eq_norm_vsub V] at hp₂'
      nth_rw 1 [← hp₂']
      rw [Ne, inner_eq_norm_mul_iff_real, hp₂', ← sub_eq_zero, ← smul_sub,
        vsub_sub_vsub_cancel_right, ← Ne, smul_ne_zero_iff, vsub_ne_zero,
        and_iff_left (Ne.symm h), norm_ne_zero_iff, vsub_ne_zero]
      rintro rfl
      refine h (Eq.symm ?_)
      simpa using hp₂'

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

Goal state before:
pp: case neg
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)
hp : ∡ (↑((orthogonalProjection line[ℝ, p₁, p₂]) p)) p₁ p = ∡ p p₁ ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
hp₁ : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) ≠ p₁
hp₂ : ↑((orthogonalProjection line[ℝ, p₁, p₃]) p) ≠ p₁
⊢ 2 • ∡ (↑((orthogonalProjection line[ℝ, p₁, p₂]) p)) p₁ p = 2 • ∡ p p₁ ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)

Tactic:
hp

Goal state after:
case neg
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)
hp : ∡ (↑((orthogonalProjection line[ℝ, p₁, p₂]) p)) p₁ p = ∡ p p₁ ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
h₂₁ : p₂ ≠ p₁
h₃₁ : p₃ ≠ p₁
hp₁ : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) ≠ p₁
hp₂ : ↑((orthogonalProjection line[ℝ, p₁, p₃]) p) ≠ p₁
⊢ 2 • ∡ p p₁ ↑((orthogonalProjection line[ℝ, p₁, p₃]) p) = 2 • ∡ p p₁ ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

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✝ : Nontrivial V
s : Sphere P
⊢ (∃ p, p ∈ s) ↔ 0 ≤ s.radius

Tactic:
← nonempty_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✝ : Nontrivial V
s : Sphere P
⊢ (∃ p, p ∈ s) ↔ (Metric.sphere s.center s.radius).Nonempty
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.151 = 2 • ∡ ?m.151 (t.points i₁) (t.points i₃)

Tactic:
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
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 • ∡ p (t.points i₁) (t.points i₃) = 2 • ∡ p (t.points i₁) (t.points i₃)
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.158 = 2 • ∡ ?m.158 (t.points i₁) (t.points i₃)

Tactic:
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
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 • ∡ p (t.points i₁) (t.points i₃) = 2 • ∡ p (t.points i₁) (t.points i₃)
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:
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
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 • (∡ p (t.points i₁) (t.points i₃) + ↑π) = 2 • ∡ p (t.points i₁) (t.points i₃)
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
this :
  ∀ (i : Fin (n + 1)),
    i ≠ 0 → ∑ j, ⟪s.points i -ᵥ s.points 0, (s.height j)⁻¹ ^ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫ = 0
i : { x // x ≠ 0 }
⊢ ∑ i, (s.height i)⁻¹ ^ 2 • (s.points i -ᵥ s.altitudeFoot i) ∈ ↑(ℝ ∙ (s.points ↑i -ᵥ s.points 0))ᗮ

Tactic:
rcases i with ⟨i, hi⟩

Goal state after:
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
this :
  ∀ (i : Fin (n + 1)),
    i ≠ 0 → ∑ j, ⟪s.points i -ᵥ s.points 0, (s.height j)⁻¹ ^ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫ = 0
i : Fin (n + 1)
hi : i ≠ 0
⊢ ∑ i, (s.height i)⁻¹ ^ 2 • (s.points i -ᵥ s.altitudeFoot i) ∈ ↑(ℝ ∙ (s.points ↑⟨i, hi⟩ -ᵥ s.points 0))ᗮ
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
inst✝ : n.AtLeastTwo
i : Fin (n + 1)
⊢ (s.height i)⁻¹ < ∑ j with j ≠ i, (s.height j)⁻¹

Tactic:
rw [inv_height_eq_sum_mul_inv_dist]
  refine Finset.sum_lt_sum_of_nonempty ?_ ?_
  · 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 _
  · rintro j hj
    refine mul_lt_of_lt_one_left ?_ ?_
    · simp [height_pos]
    · rw [neg_lt]
      exact neg_one_lt_inner_vsub_altitudeFoot_div _ _ _

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
V₂ : Type u_3
P₂ : Type u_4
inst✝⁴ : NormedAddCommGroup V₂
inst✝³ : InnerProductSpace ℝ V₂
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₂ P₂
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).exradius = s.exradius

Tactic:
by
  ext
  simp [exradius, exsphere]

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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ (s.restrict S hS).exradius = s.exradius

Tactic:
by
  ext
  simp [exradius, exsphere]

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)
hp : 1 ≤ s.excenterWeights ∅ i
j : Fin (n + 1)
hj : j ≠ i
⊢ 1 < s.excenterWeights ∅ i + s.excenterWeights ∅ j + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i

Tactic:
hp

Goal state after:
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)
hp : 1 ≤ s.excenterWeights ∅ i
j : Fin (n + 1)
hj : j ≠ i
⊢ s.excenterWeights ∅ i < s.excenterWeights ∅ i + s.excenterWeights ∅ j + ∑ i ∈ {j, i}ᶜ, s.excenterWeights ∅ i
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x (x - y) = angle y (y - x)
hpi : angle x y ≠ π
⊢ ‖x‖ = ‖y‖

Tactic:
replace h := Real.arccos_injOn (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x (x - y)))
    (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one y (y - x))) h
  by_cases hxy : x = y
  · rw [hxy]
  · rw [← norm_neg (y - x), neg_sub, mul_comm, mul_comm ‖y‖, div_eq_mul_inv, div_eq_mul_inv,
      mul_inv_rev, mul_inv_rev, ← mul_assoc, ← mul_assoc] at h
    replace h :=
      mul_right_cancel₀ (inv_ne_zero fun hz => hxy (eq_of_sub_eq_zero (norm_eq_zero.1 hz))) h
    rw [inner_sub_right, inner_sub_right, real_inner_comm x y, real_inner_self_eq_norm_mul_norm,
      real_inner_self_eq_norm_mul_norm, mul_sub_right_distrib, mul_sub_right_distrib,
      mul_self_mul_inv, mul_self_mul_inv, sub_eq_sub_iff_sub_eq_sub, ← mul_sub_left_distrib] at h
    by_cases hx0 : x = 0
    · rw [hx0, norm_zero, inner_zero_left, zero_mul, zero_sub, neg_eq_zero] at h
      rw [hx0, norm_zero, h]
    · by_cases hy0 : y = 0
      · rw [hy0, norm_zero, inner_zero_right, zero_mul, sub_zero] at h
        rw [hy0, norm_zero, h]
      · rw [inv_sub_inv (fun hz => hx0 (norm_eq_zero.1 hz)) fun hz => hy0 (norm_eq_zero.1 hz), ←
          neg_sub, ← mul_div_assoc, mul_comm, mul_div_assoc, ← mul_neg_one] at h
        symm
        by_contra hyx
        replace h := (mul_left_cancel₀ (sub_ne_zero_of_ne hyx) h).symm
        rw [real_inner_div_norm_mul_norm_eq_neg_one_iff, ← angle_eq_pi_iff] at h
        exact hpi h

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

Goal state before:
pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h✝ : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
h : angle x y + (fun x ↦ x • (2 * π)) n = angle x (x + y) + angle y (x + y)
⊢ angle x y = angle x (x + y) + angle y (x + y)

Tactic:
simp only at h

Goal state after:
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h✝ : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
h : angle x y + n • (2 * π) = angle x (x + y) + angle y (x + y)
⊢ angle x y = angle x (x + y) + angle y (x + y)
Module: Mathlib.Geometry.Euclidean.Circumcenter

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 : Simplex ℝ P 1
i : Fin 2
hi : i ∈ Set.univ
j : Fin 2
hj : j ∈ Set.univ
hij : i ≠ j
⊢ ‖s.points i -ᵥ (2⁻¹ • (s.points 1 -ᵥ s.points 0) +ᵥ s.points 0)‖ =
    dist (s.points j) (2⁻¹ • (s.points 1 -ᵥ s.points 0) +ᵥ s.points 0)

Tactic:
dist_eq_norm_vsub V (s.points j),

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 : Simplex ℝ P 1
i : Fin 2
hi : i ∈ Set.univ
j : Fin 2
hj : j ∈ Set.univ
hij : i ≠ j
⊢ ‖s.points i -ᵥ (2⁻¹ • (s.points 1 -ᵥ s.points 0) +ᵥ s.points 0)‖ =
    ‖s.points j -ᵥ (2⁻¹ • (s.points 1 -ᵥ s.points 0) +ᵥ s.points 0)‖
Module: Mathlib.Geometry.Euclidean.Circumcenter

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₂ : 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₂
⊢ f s.circumcenter ∈ affineSpan ℝ (Set.range (⇑f.toAffineMap ∘ s.points))

Tactic:
Set.range_comp,

Goal state after:
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₂
⊢ f s.circumcenter ∈ affineSpan ℝ (⇑f.toAffineMap '' Set.range s.points)
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:
by
  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.Triangle

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
a b c p : P
h : ∠ b p c = π
⊢ dist a b * dist a b * dist c p + dist a c * dist a c * dist b p = dist b c * (dist a p ^ 2 + dist b p * dist c p)

Tactic:
law_cos a p b,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c p : P
h : ∠ b p c = π
⊢ (dist a p * dist a p + dist b p * dist b p - 2 * dist a p * dist b p * Real.cos (∠ a p b)) * dist c p +
      dist a c * dist a c * dist b p =
    dist b c * (dist a p ^ 2 + dist b p * dist c p)
Module: Mathlib.Geometry.Euclidean.Circumcenter

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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ (reflection (affineSpan ℝ (s.points '' {i₁, i₂}))) s.circumcenter =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)

Tactic:
rw [reflection_apply', h_faces, s.orthogonalProjection_circumcenter hc,
    circumcenter_eq_centroid, s.face_centroid_eq_centroid hc,
    centroid_eq_affineCombination_of_pointsWithCircumcenter,
    circumcenter_eq_affineCombination_of_pointsWithCircumcenter, ← @vsub_eq_zero_iff_eq V,
    affineCombination_vsub, weightedVSub_vadd_affineCombination, affineCombination_vsub,
    weightedVSub_apply, sum_pointsWithCircumcenter]

Goal state after:
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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ i,
        (centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n +
                centroidWeightsWithCircumcenter {i₁, i₂} -
              reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
            (pointIndex i) •
          (s.pointsWithCircumcenter (pointIndex i) -ᵥ Classical.choice ⋯) +
      (centroidWeightsWithCircumcenter {i₁, i₂} - circumcenterWeightsWithCircumcenter n +
              centroidWeightsWithCircumcenter {i₁, i₂} -
            reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
          circumcenterIndex •
        (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) =
    0
Module: Mathlib.Geometry.Euclidean.Triangle

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
a b c : P
h : ¬Collinear ℝ {a, b, c}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
⊢ False

Tactic:
rcases w.eq_or_lt with h2 | h3

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
a b c : P
h : ¬Collinear ℝ {a, b, c}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
h2 : ∠ a b c = ∠ a c b
⊢ False

case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
h : ¬Collinear ℝ {a, b, c}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
h3 : ∠ a b c < ∠ a c b
⊢ False
Module: Mathlib.Geometry.Euclidean.MongePoint

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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : i₁ = i₂
⊢ ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, s.points i₁ -ᵥ s.points i₂⟫ = 0

pp: case neg
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 + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
⊢ ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, s.points i₁ -ᵥ s.points i₂⟫ = 0

Tactic:
· simp [h]

Goal state after:
case neg
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 + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
⊢ ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, s.points i₁ -ᵥ s.points i₂⟫ = 0
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

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
⊢ Collinear ℝ {p, p', s.secondInter p (p' -ᵥ p)}

Tactic:
rw [Set.pair_comm, Set.insert_comm]
  exact
    (collinear_insert_iff_of_mem_affineSpan (s.secondInter_vsub_mem_affineSpan _ _)).2
      (collinear_pair ℝ _ _)

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

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
s : Sphere P
p p' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
h : p' = p
⊢ Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))

pp: case neg
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
h : ¬p' = p
⊢ Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))

Tactic:
· simp [h]

Goal state after:
case neg
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
h : ¬p' = p
⊢ Wbtw ℝ p p' (s.secondInter p (p' -ᵥ p))
Module: Mathlib.Geometry.Euclidean.MongePoint

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
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist (circumcenter t) ((reflection (affineSpan ℝ (t.points '' {i₁, i₂}))) t.orthocenter) = circumradius t

Tactic:
exact dist_circumcenter_reflection_orthocenter _ h

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.SmoothFunctions

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
H : Type u_4
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace H N
E'' : Type u_7
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_8
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
N' : Type u_9
inst✝³ : TopologicalSpace N'
inst✝² : ChartedSpace H'' N'
n : ℕ∞ω
V : Type u_10
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
f : C^n⟮I, N; 𝓘(𝕜, V), V⟯
x : N
⊢ (1 • f) x = f x

Tactic:
exact one_smul 𝕜 (f x)

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ (ModelWithCorners.interior M)ᶜ = ModelWithCorners.boundary M

Tactic:
by
  apply compl_unique ?_ I.interior_union_boundary_eq_univ
  exact disjoint_iff_inter_eq_empty.mp I.disjoint_interior_boundary

Goal state after: