mathlib-initiative/mathlib-tactics huggingface dataset:
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
p : P
⊢ (reflection s) ((reflection s) p) = p

Tactic:
simp [reflection, -AffineIsometryEquiv.map_vadd]

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

Goal state before:
pp: case neg
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
⊢ o.oangle ((o.rotation (o.oangle x y)) x) y = 0

Tactic:
· by_cases hy : y = 0
    · simp [hy]
    · simp [hx, hy]

Goal state after:
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
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
⊢ dist p₁ ((reflection s) p₂) = dist p₁ p₂

Tactic:
by
  rw [← reflection_eq_self_iff p₁] at hp₁
  convert! (reflection s).dist_map p₁ p₂
  rw [hp₁]

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

Goal state before:
pp: case hy
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ (o.kahler y) z ≠ 0

Tactic:
· exact o.kahler_ne_zero hy hz

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h0 : ¬x = 0
h : ⟪x, y⟫ = 0
⊢ Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) =
    Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ * (‖x‖ * ‖x‖) / (‖x‖ * ‖x‖)))

Tactic:
← mul_div

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h0 : ¬x = 0
h : ⟪x, y⟫ = 0
⊢ Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) =
    Real.arcsin (‖y‖ / √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ * (‖x‖ * ‖x‖ / (‖x‖ * ‖x‖))))
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.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖

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

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst✝¹ : Oriented ℝ V (Fin 2)
p p' : P
s : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ ↑((orthogonalProjection s) p)
⊢ ∡ p (↑((orthogonalProjection s) p)) p' = ↑(-(-π / 2)) ∨ ∡ p (↑((orthogonalProjection s) p)) p' = -↑(π / 2)

Tactic:
neg_div,

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
s : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ ↑((orthogonalProjection s) p)
⊢ ∡ p (↑((orthogonalProjection s) p)) p' = ↑(- -(π / 2)) ∨ ∡ p (↑((orthogonalProjection s) p)) p' = -↑(π / 2)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case neg.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hn : ¬x = y
hy : y ≠ 0
r : ℝ
h : r = 0
hr0 : 0 ≤ r
hr : y = x
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
exact False.elim (hn hr.symm)

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
⊢ |((signedDist v) p) q| ≤ dist p q

Tactic:
by
  rw [signedDist_apply_apply]
  by_cases h : v = 0
  · simp [h]
  · grw [abs_real_inner_le_norm]
    simp [norm_normalize h, dist_eq_norm_vsub']

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
p q : P
⊢ ((signedDist (p -ᵥ q)) p) q = -dist p q

Tactic:
by
  rw [← neg_eq_iff_eq_neg, ← signedDist_neg, neg_vsub_eq_vsub_rev]
  apply signedDist_vsub_self

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
c₁ c₂ : ℝ
⊢ c₂ * ((signedDist v) p) q + c₁ * ((signedDist v) q) p = (c₂ - c₁) * ((signedDist v) p) q

Tactic:
· rw [sub_mul, ← signedDist_anticomm v p, mul_neg, sub_eq_add_neg]

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✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : Fin 3 → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
hf0 : f 0 = 0
i j : Fin 3
h : f i = f j
⊢ i = j

Tactic:
have hi := hf i

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
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : Fin 3 → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
hf0 : f 0 = 0
i j : Fin 3
h : f i = f j
hi : p i = f i • v +ᵥ p 0
⊢ i = j
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
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius
⊢ ‖p₂ -ᵥ p₁ + (p₁ -ᵥ s.center)‖ ^ 2 = ‖p₂ -ᵥ p₁‖ ^ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + ‖p₁ -ᵥ s.center‖ ^ 2

Tactic:
norm_add_sq_real

Goal state after:
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 : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius
⊢ ‖p₂ -ᵥ p₁‖ ^ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + ‖p₁ -ᵥ s.center‖ ^ 2 =
    ‖p₂ -ᵥ p₁‖ ^ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + ‖p₁ -ᵥ s.center‖ ^ 2
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
s₁ s₂ : Sphere P
as : AffineSubspace ℝ P
⊢ as ∈ s₁.commonIntTangents s₂ ∪ s₁.commonExtTangents s₂ ↔ as ∈ s₁.commonTangents s₂

Tactic:
Set.mem_union,

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₁ s₂ : Sphere P
as : AffineSubspace ℝ P
⊢ as ∈ s₁.commonIntTangents s₂ ∨ as ∈ s₁.commonExtTangents s₂ ↔ as ∈ s₁.commonTangents s₂
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.excenterWeights signs i ≠ 0

Tactic:
rw [excenterWeights]
  refine mul_ne_zero ?_ (s.excenterWeightsUnnorm_ne_zero _ _)
  rw [ExcenterExists] at h
  simp [h]

Goal state after:
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₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ ∡ p₁ s.center p₃ = 2 • ∡ p₁ p₂ p₃

Tactic:
rw [mem_sphere, @dist_eq_norm_vsub V] at hp₁ hp₂ hp₃

Goal state after:
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₃ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ ∡ p₁ s.center p₃ = 2 • ∡ p₁ p₂ p₃
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)
h : 2 * (s.height i)⁻¹ < ∑ j ∈ {i}, (s.height j)⁻¹ + ∑ j ∈ {i}ᶜ, (s.height j)⁻¹
⊢ (s.height i)⁻¹ / ∑ i, (s.height i)⁻¹ < 2⁻¹

Tactic:
rwa [sum_add_sum_compl, ← lt_inv_mul_iff₀ zero_lt_two, ← div_lt_iff₀ (by positivity)] at h

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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ (s.signedInfDist i) (s.excenter signs) = (if i ∈ signs then -1 else 1) * (∑ j, s.excenterWeightsUnnorm signs j)⁻¹

Tactic:
by
  simp_rw [excenter_eq_affineCombination,
    signedInfDist_affineCombination _ _ h.sum_excenterWeights_eq_one, excenterWeights,
    Pi.smul_apply, ← dist_eq_norm_vsub, excenterWeightsUnnorm]
  rw [← altitudeFoot, ← height]
  simp [(s.height_pos i).ne']

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

Goal state before:
pp: case e'_2.a
n : ℕ
i : Fin (n + 1)
j : PointsWithCircumcenterIndex n
a✝ : j ∈ univ
⊢ pointWeightsWithCircumcenter i j = if j = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 j else 0

pp: case e'_3
n : ℕ
i : Fin (n + 1)
⊢ 1 = if pointIndex i ∈ univ then Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex i) else 0

Tactic:
· cases j <;> simp [pointWeightsWithCircumcenter]

Goal state after:
case e'_3
n : ℕ
i : Fin (n + 1)
⊢ 1 = if pointIndex i ∈ univ then Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex i) else 0
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 z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
by_cases H5 : angle y z = π

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
H5 : angle y z = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
H5 : ¬angle y z = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
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)
⊢ (∀ i_1 ∈ {i}ᶜ, 0 < s.touchpointWeights ∅ i i_1) ∧ ∀ i_1 ∉ {i}ᶜ, s.touchpointWeights ∅ i i_1 = 0

Tactic:
simp only [Finset.mem_compl, Finset.mem_singleton, Decidable.not_not, forall_eq,
    touchpointWeights_eq_zero, and_true]

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
inst✝ : n.AtLeastTwo
i : Fin (n + 1)
⊢ ∀ (i_1 : Fin (n + 1)), ¬i_1 = i → 0 < s.touchpointWeights ∅ i i_1
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)
⊢ (∀ i_1 ∈ {i}ᶜ, 0 < s.touchpointWeights {i} i i_1) ∧ ∀ i_1 ∉ {i}ᶜ, s.touchpointWeights {i} i i_1 = 0

Tactic:
simp only [Finset.mem_compl, Finset.mem_singleton, Decidable.not_not, forall_eq,
    touchpointWeights_eq_zero, and_true]

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
inst✝ : n.AtLeastTwo
i : Fin (n + 1)
⊢ ∀ (i_1 : Fin (n + 1)), ¬i_1 = i → 0 < s.touchpointWeights {i} i i_1
Module: Mathlib.Geometry.Euclidean.NinePointCircle

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 : Fin (n + 1)
⊢ s.points i -ᵥ s.mongePoint - (↑n)⁻¹ • (s.points i -ᵥ s.mongePoint) = ((↑n - 1) / ↑n) • (s.points i -ᵥ s.mongePoint)

Tactic:
by_cases hn : n = 0

Goal state after:
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
i : Fin (n + 1)
hn : n = 0
⊢ s.points i -ᵥ s.mongePoint - (↑n)⁻¹ • (s.points i -ᵥ s.mongePoint) = ((↑n - 1) / ↑n) • (s.points i -ᵥ s.mongePoint)

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
i : Fin (n + 1)
hn : ¬n = 0
⊢ s.points i -ᵥ s.mongePoint - (↑n)⁻¹ • (s.points i -ᵥ s.mongePoint) = ((↑n - 1) / ↑n) • (s.points i -ᵥ s.mongePoint)
Module: Mathlib.Geometry.Euclidean.NinePointCircle

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
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : ↑(n - 1) = ↑n - 1
⊢ ⅟2 • (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      ⅟2 •
        ((↑n)⁻¹ • (s.points i -ᵥ s.circumcenter) -
          (-(↑n - 1) / ↑n * (↑(n + 1) / ↑(n - 1))) • (s.centroid -ᵥ s.circumcenter)) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)

Tactic:
neg_div,

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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : ↑(n - 1) = ↑n - 1
⊢ ⅟2 • (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      ⅟2 •
        ((↑n)⁻¹ • (s.points i -ᵥ s.circumcenter) -
          (-((↑n - 1) / ↑n) * (↑(n + 1) / ↑(n - 1))) • (s.centroid -ᵥ s.circumcenter)) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)
Module: Mathlib.Geometry.Euclidean.Simplex

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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).AcuteAngled
i₁ i₂ i₃ : Fin (m + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∠ (s.points i₁) (s.points i₂) (s.points i₃) < π / 2

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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : s.AcuteAngled
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∠ ((s.reindex e).points i₁) ((s.reindex e).points i₂) ((s.reindex e).points i₃) < π / 2

Tactic:
· convert! h (i₁ := e i₁) (i₂ := e i₂) (i₃ := e i₃) ?_ ?_ ?_ using 1 <;> simp [*]

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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : s.AcuteAngled
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ ∠ ((s.reindex e).points i₁) ((s.reindex e).points i₂) ((s.reindex e).points i₃) < π / 2
Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy

Goal state before:
pp: V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
⊢ Cospherical {a, c, b, d}

Tactic:
rwa [Set.insert_comm c b {d}]

Goal state after:
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
n : ℕ
inst✝ : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Ioo 0 1
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P := (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points) w)) r
⊢ p' -ᵥ sx.points i = r • ((Finset.affineCombination ℝ Finset.univ sx.points) w -ᵥ sx.points i)

Tactic:
simp [p']

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

Goal state before:
pp: V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p a b : P
hp : p ∈ line[ℝ, a, b]
ha : a ∈ s
hb : b ∈ s
hp_on : p ∈ s
⊢ dist p a * dist p b = 0

Tactic:
have hq : dist a s.center = dist b s.center := by
    rw [mem_sphere.mp ha, mem_sphere.mp hb]
  rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq,
      mem_sphere.mp hb, mem_sphere.mp hp_on, sub_self, abs_zero]

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⟯
⊢ 0 • f = 0

Tactic:
ext x; exact zero_smul _ _

Goal state after:
Module: Mathlib.Geometry.Manifold.LocalDiffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H₁ : Type u_5
inst✝⁵ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁴ : TopologicalSpace H₂
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
M : Type u_8
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H₁ M
N : Type u_9
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H₂ N
n : WithTop ℕ∞
f : M → N
s : Set M
hf : IsLocalDiffeomorphOn I J n f s
⊢ IsLocalHomeomorphOn f s

Tactic:
apply IsLocalHomeomorphOn.mk
  intro x hx
  choose U hyp using hf ⟨x, hx⟩
  exact ⟨U.toOpenPartialHomeomorph, hyp⟩

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

Goal state before:
pp: case mpr
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux : interior (range ↑I) ×ˢ interior (range ↑J) = interior (range ↑(I.prod J))
hp : p ∈ ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N
⊢ p ∈ ModelWithCorners.interior (M × N)

Tactic:
change (I.prod J).IsInteriorPoint p

Goal state after:
case mpr
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux : interior (range ↑I) ×ˢ interior (range ↑J) = interior (range ↑(I.prod J))
hp : p ∈ ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N
⊢ (I.prod J).IsInteriorPoint p
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
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
hx : I.IsInteriorPoint x
⊢ I.IsInteriorPoint (Sum.inr x)

Tactic:
by
  rw [I.isInteriorPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inr]
  dsimp
  rw [Sum.inr_injective.extend_apply (chartAt H x)]
  simpa [I.isInteriorPoint_iff, extChartAt] using hx

Goal state after: