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

Goal state before:
pp: case 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)
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₃) + ↑π
hs : excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}

pp: case inr.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)
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₃) + ↑π
hs : excenter t signs = excenter t {i₂}
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}

pp: case inr.inr.inr
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₃) + ↑π
hs : excenter t signs = excenter t {i₃}
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}

Tactic:
· rw [hs, t.oangle_excenter_singleton_eq h₁₂ h₁₃ h₂₃] at h
    simp [Real.Angle.pi_ne_zero] at h

Goal state after:
case inr.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)
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₃) + ↑π
hs : excenter t signs = excenter t {i₂}
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}

case inr.inr.inr
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₃) + ↑π
hs : excenter t signs = excenter t {i₃}
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
⊢ ∠ p₁ p₂ p₃ = π / 2 ↔ p₂ ∈ s

Tactic:
rw [mem_sphere', EuclideanGeometry.angle,
    ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]
  let o := s.center
  have h_center : o = midpoint ℝ p₁ p₃ := hd.midpoint_eq_center.symm
  rw [← vsub_add_vsub_cancel p₁ o p₂, ← vsub_add_vsub_cancel p₃ o p₂,
    inner_add_left, inner_add_right, inner_add_right]
  have h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o) := by
    rw [h_center, left_vsub_midpoint, right_vsub_midpoint, ← smul_neg, neg_vsub_eq_vsub_rev]
  rw [h_opp, inner_neg_left, inner_neg_left, real_inner_comm (p₃ -ᵥ o) (o -ᵥ p₂)]
  ring_nf
  rw [neg_add_eq_zero, real_inner_self_eq_norm_sq, ← dist_eq_norm_vsub,
    real_inner_self_eq_norm_sq, ← dist_eq_norm_vsub, sq_eq_sq₀ dist_nonneg dist_nonneg,
    mem_sphere.mp hd.right_mem]
  exact eq_comm

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

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = ⟪x, y⟫ * (‖x‖⁻¹ - ‖y‖⁻¹)
hx0 : ¬x = 0
hy0 : y = 0
⊢ ‖x‖ = ‖y‖

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = ⟪x, y⟫ * (‖x‖⁻¹ - ‖y‖⁻¹)
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ‖x‖ = ‖y‖

Tactic:
· rw [hy0, norm_zero, inner_zero_right, zero_mul, sub_zero] at h
        rw [hy0, norm_zero, h]

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = ⟪x, y⟫ * (‖x‖⁻¹ - ‖y‖⁻¹)
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ‖x‖ = ‖y‖
Module: Mathlib.Geometry.Euclidean.Circumcenter

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)
⊢ (s.reindex e).circumsphere.center ∈ affineSpan ℝ (Set.range s.points)

Tactic:
← s.reindex_range_points e

Goal state after:
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)
⊢ (s.reindex e).circumsphere.center ∈ affineSpan ℝ (Set.range (s.reindex e).points)
Module: Mathlib.Geometry.Euclidean.Circumcenter

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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Set.range s.points ⊆ Metric.sphere (s.reindex e).circumsphere.center (s.reindex e).circumsphere.radius

Tactic:
← s.reindex_range_points e

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)
⊢ Set.range (s.reindex e).points ⊆ Metric.sphere (s.reindex e).circumsphere.center (s.reindex e).circumsphere.radius
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)
⊢ (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SOppSide (s.excenter {i}) (s.points i)

Tactic:
rw [(s.excenterExists_singleton i).sOppSide_excenter_point_iff, ← sign_eq_neg_one_iff,
    s.sign_excenterWeights_singleton_neg i]

Goal state after:
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
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ ∃ r, ∀ (i : Fin (m + 1)), dist ((s.face h).points i) s.circumcenter = r

Tactic:
by
    use s.circumradius
    simp [face_points]

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

Goal state before:
pp: α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
⊢ ∑ i, f i = ∑ i, f (pointIndex i) + f circumcenterIndex

Tactic:
have h : univ = insert circumcenterIndex (univ.map (pointIndexEmbedding n)) := by
    ext x
    refine ⟨fun h => ?_, fun _ => mem_univ _⟩
    obtain i | - := x
    · exact mem_insert_of_mem (mem_map_of_mem _ (mem_univ i))
    · exact mem_insert_self _ _

Goal state after:
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ ∑ i, f i = ∑ i, f (pointIndex i) + f circumcenterIndex
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 : Fin (n + 1)
⊢ s.points i = (affineCombination ℝ univ s.pointsWithCircumcenter) (pointWeightsWithCircumcenter i)

Tactic:
← pointsWithCircumcenter_point

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 : Fin (n + 1)
⊢ s.pointsWithCircumcenter (pointIndex i) =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (pointWeightsWithCircumcenter i)
Module: Mathlib.Geometry.Euclidean.Triangle

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
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : ¬a = b
⊢ dist a' c' = r * dist a c

Tactic:
have h1 : 0 ≤ r * dist a b := by rw [← hab]; exact dist_nonneg
    have h2 : 0 ≤ r := nonneg_of_mul_nonneg_left h1 (dist_pos.mpr hab₁)
    exact (sq_eq_sq₀ dist_nonneg (mul_nonneg h2 dist_nonneg)).mp h'

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
H : |⟪x, NormedSpace.normalize (ortho y x)⟫| = |Real.sin (angle x y)|
⊢ ⟪x, NormedSpace.normalize (ortho y x)⟫ = Real.sin (angle x y)

Tactic:
abs_of_nonneg (sin_angle_nonneg x y)

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
H : |⟪x, NormedSpace.normalize (ortho y x)⟫| = Real.sin (angle x y)
⊢ ⟪x, NormedSpace.normalize (ortho y x)⟫ = Real.sin (angle x y)
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 • (((↑n)⁻¹ • (s.centroid -ᵥ s.points i) +ᵥ s.centroid) -ᵥ s.circumcenter) +
      ⅟2 • ((↑n)⁻¹ • (s.points i -ᵥ s.circumcenter) + (↑(n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)

Tactic:
← smul_add,

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

Tactic:
← smul_add,

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 •
      ((↑n)⁻¹ • (s.centroid -ᵥ s.points i + (s.points i -ᵥ s.circumcenter)) +
        (s.centroid -ᵥ s.circumcenter + (↑(n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter))) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)
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
s : Triangle ℝ P
i : Fin 3
⊢ Simplex.altitudeFoot s i ∈ Simplex.ninePointCircle s

Tactic:
convert! s.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle 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 : Triangle ℝ P
i : Fin 3
⊢ Simplex.altitudeFoot s i = ↑((Simplex.faceOpposite s i).orthogonalProjectionSpan (Simplex.eulerPoint s i))
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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ {p₁, p, p₃}
⊢ Cospherical {p₁, p₂, p₃, p₄}

Tactic:
suffices h_equiv : Cospherical ({p₁, p₂, p₄, p₃} : Set P) by grind [Set.pair_comm p₄ p₃]
  have h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂ := by
    grind [angle_comm, angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi hp₃p₄]
  rw [angle_eq_pi_iff_sbtw] at hp₁p₂ hp₃p₄
  have hcol_p₁pp₂ := hp₁p₂.wbtw.collinear
  have hcol_p₃pp₄ := hp₃p₄.wbtw.collinear
  have h_notcol_p₁p₂p₃ : ¬ Collinear ℝ ({p₁, p₂, p₃} : Set P) := by
    have : AffineIndependent ℝ ![p₁, p, p₃] := affineIndependent_iff_not_collinear_set.mpr hn
    rw [← affineIndependent_iff_not_collinear_set]
    grind [hp₁p₂.left_ne_right, affineIndependent_of_affineIndependent_collinear_ne,
      AffineIndependent.comm_left, AffineIndependent.comm_right]
  apply cospherical_of_two_zsmul_oangle_eq_of_not_collinear ?_ h_notcol_p₁p₂p₃
  suffices ∡ p₁ p₂ p₃ = ∡ p₁ p₄ p₃ by grind
  suffices ∠ p₁ p₂ p₃ = ∠ p₁ p₄ p₃ by
    grind [oangle_eq_of_angle_eq_of_sign_eq, Sbtw.oangle_sign_eq_of_sbtw]
  rw [angle_comm, ← angle_eq_angle_of_angle_eq_pi p₃ hp₁p₂.angle₃₂₁_eq_pi,
    ← angle_eq_angle_of_angle_eq_pi p₁ hp₃p₄.angle₃₂₁_eq_pi]
  suffices h_sim : Similar ![p₁, p, p₄] ![p₃, p, p₂] by
    grind [angle_comm, h_sim.angle_eq_all.right.left]
  have h_notcol_p₁pp₄ : ¬ Collinear ℝ ({p₁, p, p₄} : Set P) := by
    intro hcol
    suffices hcol : Collinear ℝ ({p₁, p, p₃} : Set P) by grind
    suffices hcol : Collinear ℝ ({p₁, p₃, p, p₄} : Set P) by grind [Collinear.subset _ hcol]
    have hne_pp₄ := hp₃p₄.ne_right
    grind [collinear_insert_insert_of_mem_affineSpan_pair, Collinear.mem_affineSpan_of_mem_of_ne]
  have h_notcol_p₃pp₂ : ¬ Collinear ℝ ({p₃, p, p₂} : Set P) := by
    intro hcol
    suffices hcol : Collinear ℝ ({p₁, p, p₃} : Set P) by grind
    suffices hcol : Collinear ℝ ({p₃, p₁, p, p₂} : Set P) by grind [Collinear.subset _ hcol]
    have hne_pp₂ := hp₁p₂.ne_right
    grind [collinear_insert_insert_of_mem_affineSpan_pair, Collinear.mem_affineSpan_of_mem_of_ne]
  apply similar_of_side_angle_side h_notcol_p₁pp₄ h_notcol_p₃pp₂ h_angle_eq ?_
  grind [dist_comm]

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
hp' : p' -ᵥ sx.points i = r • ((Finset.affineCombination ℝ Finset.univ sx.points) w -ᵥ sx.points i)
⊢ (Finset.affineCombination ℝ Finset.univ sx.points) (r • (w - Pi.single i 1) + Pi.single i 1) ∈ (sx.face ⋯).interior

Tactic:
rw [Affine.Simplex.affineCombination_mem_interior_face_iff_pos]

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
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
hp' : p' -ᵥ sx.points i = r • ((Finset.affineCombination ℝ Finset.univ sx.points) w -ᵥ sx.points i)
⊢ (∀ i_1 ∈ {i}ᶜ, 0 < (r • (w - Pi.single i 1) + Pi.single i 1) i_1) ∧
    ∀ i_1 ∉ {i}ᶜ, (r • (w - Pi.single i 1) + Pi.single i 1) i_1 = 0

case hw
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
hp' : p' -ᵥ sx.points i = r • ((Finset.affineCombination ℝ Finset.univ sx.points) w -ᵥ sx.points i)
⊢ ∑ i_1, (r • (w - Pi.single i 1) + Pi.single i 1) i_1 = 1
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
F' : Type u_4
inst✝¹⁰ : NormedAddCommGroup F'
inst✝⁹ : NormedSpace 𝕜 F'
H₁ : Type u_5
inst✝⁸ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁷ : TopologicalSpace H₂
H₃ : Type u_7
inst✝⁶ : TopologicalSpace H₃
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
K : 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
P : Type u_10
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace H₃ P
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
⊢ M ≃ₘ^n⟮I, J⟯ N

Tactic:
choose g hgInverse using (Function.bijective_iff_has_inverse).mp hf'

Goal state after:
𝕜 : 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
F' : Type u_4
inst✝¹⁰ : NormedAddCommGroup F'
inst✝⁹ : NormedSpace 𝕜 F'
H₁ : Type u_5
inst✝⁸ : TopologicalSpace H₁
H₂ : Type u_6
inst✝⁷ : TopologicalSpace H₂
H₃ : Type u_7
inst✝⁶ : TopologicalSpace H₃
I : ModelWithCorners 𝕜 E H₁
J : ModelWithCorners 𝕜 F H₂
K : 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
P : Type u_10
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace H₃ P
n : WithTop ℕ∞
f : M → N
s : Set M
x : M
hf : IsLocalDiffeomorph I J n f
hf' : Function.Bijective f
g : N → M
hgInverse : Function.LeftInverse g f ∧ Function.RightInverse g f
⊢ M ≃ₘ^n⟮I, J⟯ N
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
t₂ : Triangle ℝ P
ht₂ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)
ht₂s : Set.range t₂.points ⊆ s
c : P
hc : c ∈ affineSpan ℝ (Set.range t.points)
h : ∀ p₁ ∈ Set.range t₂.points, dist p₁ c = Simplex.circumradius t
⊢ Simplex.circumradius t₂ = Simplex.circumradius t

Tactic:
rw [Set.forall_mem_range] at h

Goal state after:
case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
t₂ : Triangle ℝ P
ht₂ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)
ht₂s : Set.range t₂.points ⊆ s
c : P
hc : c ∈ affineSpan ℝ (Set.range t.points)
h : ∀ (i : Fin 3), dist (t₂.points i) c = Simplex.circumradius t
⊢ Simplex.circumradius t₂ = Simplex.circumradius t
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
    rw [IsInteriorPoint, ← aux, mem_prod]
    obtain h := Set.mem_prod.mp hp
    rw [ModelWithCorners.interior] at h
    exact h

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_1.h
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization F TotalSpace.proj := ⋯
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
⊢ ∀ x ∈ e.baseSet, (fun b ↦ (↑e ⟨b, (-s) b⟩).2) x = (-fun b ↦ (↑e ⟨b, s b⟩).2) x

Tactic:
exact fun x hx ↦ (e.linear 𝕜 hx).map_neg ..

Goal state after: