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

Goal state before:
pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
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))ᗮ
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf : ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ), ∃ c, c • ⟨v, hv⟩ = w
hvc : ∀ w ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ, ∃ c, c • v = w
hvp : 0 ≤ s.radius ^ 2 - dist p s.center ^ 2
p' : P
h : p' ∈ {√(s.radius ^ 2 - dist p s.center ^ 2) • v +ᵥ p, -(√(s.radius ^ 2 - dist p s.center ^ 2) • v) +ᵥ p}
⊢ p' ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)

Tactic:
rw [← neg_smul] at h
    rcases h with rfl | rfl <;>
      rw [vadd_mem_inter_orthRadius_iff_norm_sq hr (Submodule.smul_mem _ _ hv)] <;>
      simp [norm_smul, hv1, hvp]

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

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 : ℕ
inst✝¹ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
inst✝ : Decidable (s.ExcenterExists signs)
h : ¬∑ i, s.excenterWeightsUnnorm signs i ≠ 0
⊢ ∑ i, ((∑ i, s.excenterWeightsUnnorm signs i)⁻¹ • s.excenterWeightsUnnorm signs) i =
    if ∑ i, s.excenterWeightsUnnorm signs i ≠ 0 then 1 else 0

Tactic:
· simp only [ne_eq, not_not] at h
    simp [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
inst✝ : n.AtLeastTwo
i : Fin (n + 1)
⊢ (s.height i)⁻¹ < ∑ j with j ≠ i, (s.height j)⁻¹

Tactic:
inv_height_eq_sum_mul_inv_dist

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)
⊢ ∑ j with j ≠ i,
      -(⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫ / (s.height i * s.height j)) * (s.height j)⁻¹ <
    ∑ j with j ≠ i, (s.height j)⁻¹
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 ≠ π
h : ⟪x, x - y⟫ / (‖x‖ * ‖x - y‖) = ⟪y, y - x⟫ / (‖y‖ * ‖y - x‖)
hxy : x = y
⊢ ‖x‖ = ‖y‖

Tactic:
rw [hxy]

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
ι : Type u_3
hne : Nonempty ι
inst✝ : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val✝ : Fintype ι
m : ℕ
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P},
    AffineIndependent ℝ p →
      ∀ (val : Fintype ι),
        Fintype.card ι = m + 1 →
          ∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x // x ≠ i }
⊢ Fintype.card ι2 = m + 1

Tactic:
Fintype.card_of_subtype {x | x ≠ 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
ι : Type u_3
hne : Nonempty ι
inst✝ : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val✝ : Fintype ι
m : ℕ
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P},
    AffineIndependent ℝ p →
      ∀ (val : Fintype ι),
        Fintype.card ι = m + 1 →
          ∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x // x ≠ i }
⊢ {x | x ≠ i}.card = m + 1

case H
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ι : Type u_3
hne : Nonempty ι
inst✝ : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val✝ : Fintype ι
m : ℕ
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P},
    AffineIndependent ℝ p →
      ∀ (val : Fintype ι),
        Fintype.card ι = m + 1 →
          ∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x // x ≠ i }
⊢ ∀ (x : ι), x ∈ {x | x ≠ i} ↔ x ≠ i
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 = π
H5 : ¬angle y z = π
H6 :
  Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle x y) * Real.sin (angle y z) *
        ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
Hw : Real.sin (angle x y) * Real.sin (angle y z) ≠ 0
H8 : ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫ = -1
H9 : ortho y x ≠ 0
H10 : ortho y z ≠ 0
H11 : ‖NormedSpace.normalize (ortho y x)‖ = 1
H12 : ‖NormedSpace.normalize (ortho y z)‖ = 1
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
inner_eq_neg_one_iff_of_norm_eq_one H11 H12

Goal state after:
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 = π
H6 :
  Real.cos (angle x y) * Real.cos (angle y z) - Real.sin (angle x y) * Real.sin (angle y z) =
    Real.cos (angle x y) * Real.cos (angle y z) +
      Real.sin (angle x y) * Real.sin (angle y z) *
        ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫
Hw : Real.sin (angle x y) * Real.sin (angle y z) ≠ 0
H8 : NormedSpace.normalize (ortho y x) = -NormedSpace.normalize (ortho y z)
H9 : ortho y x ≠ 0
H10 : ortho y z ≠ 0
H11 : ‖NormedSpace.normalize (ortho y x)‖ = 1
H12 : ‖NormedSpace.normalize (ortho y z)‖ = 1
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
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
p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₂ p₃ ≤ ∠ p₂ p₃ p₂
h₃₁₂ : ∠ p₂ p₂ p₃ ≤ ∠ p₃ p₂ p₂
hne : ∠ p₂ p₂ p₃ ≠ ∠ p₂ p₃ p₂ ∨ ∠ p₂ p₂ p₃ ≠ ∠ p₃ p₂ p₂ ∨ ∠ p₂ p₃ p₂ ≠ ∠ p₃ p₂ p₂
h₂₃ : ¬p₂ = p₃
⊢ ∠ p₂ p₂ p₃ < π / 3

Tactic:
simp_all [angle_self_of_ne]
      linarith [Real.pi_pos]

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

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
y : V
hy left✝ : y ≠ 0
r : ℝ≥0
hr : 0 < ↑r
hxz₁ : ¬angle 0 (↑r • y) = π
hxz₂ : ¬angle 0 (↑r • y) = 0
h_sin_xz : Real.sin (angle 0 (↑r • y)) ≠ 0
⊢ y ∈ Submodule.span ℝ≥0 {0, ↑r • y}

Tactic:
rw [← NNReal.smul_def, Submodule.span_insert_zero, Submodule.span_singleton_smul_eq]

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
y : V
hy left✝ : y ≠ 0
r : ℝ≥0
hr : 0 < ↑r
hxz₁ : ¬angle 0 (↑r • y) = π
hxz₂ : ¬angle 0 (↑r • y) = 0
h_sin_xz : Real.sin (angle 0 (↑r • y)) ≠ 0
⊢ y ∈ ℝ≥0 ∙ y

case pos.hr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
y : V
hy left✝ : y ≠ 0
r : ℝ≥0
hr : 0 < ↑r
hxz₁ : ¬angle 0 (↑r • y) = π
hxz₂ : ¬angle 0 (↑r • y) = 0
h_sin_xz : Real.sin (angle 0 (↑r • y)) ≠ 0
⊢ IsUnit r
Module: Mathlib.Geometry.Euclidean.Inversion.Calculus

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x ↦ c + x) x ≠ c
A : HasFDerivAt (fun x ↦ _root_.id x - c) (ContinuousLinearMap.id ℝ F) (c + x)
⊢ ‖_root_.id (c + x) - c‖ ^ 2 ≠ 0

Tactic:
simpa using hx

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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ line[ℝ, t.points i₂, t.points i₃].SOppSide (t.points i₁) (Simplex.excenter t {i₁})

Tactic:
convert! t.sOppSide_point_excenter_singleton i₁
  simp
  grind

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
t : Triangle ℝ P
inst✝ : Fact (Module.finrank ℝ V = 2)
signs : Finset (Fin 3)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ line[ℝ, t.points i₂, t.points i₃] = (Simplex.exsphere t signs).orthRadius (Simplex.touchpoint t signs i₁)

Tactic:
convert! (t.excenterExists signs).affineSpan_faceOpposite_eq_orthRadius i₁
  have hc : {i₁}ᶜ = ({i₂, i₃} : Set (Fin 3)) := by grind
  simp [Simplex.range_faceOpposite_points, hc, Set.image_insert_eq]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
r : ℝ≥0
hr : r ≠ 0
h : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)
x✝¹ x✝ : ι
⊢ edist (v₂ x✝¹) (v₂ x✝) = edist (v₁ x✝¹) (v₁ x✝) / ↑r

Tactic:
ENNReal.eq_div_iff _ ENNReal.coe_ne_top,

Goal state after:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
r : ℝ≥0
hr : r ≠ 0
h : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)
x✝¹ x✝ : ι
⊢ ↑r * edist (v₂ x✝¹) (v₂ x✝) = edist (v₁ x✝¹) (v₁ x✝)

ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
r : ℝ≥0
hr : r ≠ 0
h : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)
x✝¹ x✝ : ι
⊢ ↑r ≠ 0
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
hl : ![b, a, c] = ![a, b, c] ∘ ⇑(Equiv.swap 0 1)
hr : ![b', a', c'] = ![a', b', c'] ∘ ⇑(Equiv.swap 0 1)
⊢ ![b, a, c] ∼ ![b', a', c']

Tactic:
grind [index_equiv]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
hl : ![a, c, b] = ![a, b, c] ∘ ⇑(Equiv.swap 1 2)
hr : ![a', c', b'] = ![a', b', c'] ∘ ⇑(Equiv.swap 1 2)
⊢ ![a, c, b] ∼ ![a', c', b']

Tactic:
grind [index_equiv]

Goal state after:
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.circumcenter) + (s.centroid -ᵥ s.circumcenter) +
        ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)

Tactic:
have : (n : ℝ)⁻¹ • (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
      (((n + 1) / n : ℝ)) • (s.centroid -ᵥ s.circumcenter) := by
    rw [add_comm (n : ℝ) 1, add_div, div_self (by simpa using hn.out), add_smul, one_smul, one_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
this :
  (↑n)⁻¹ • (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)
⊢ ⅟2 •
      ((↑n)⁻¹ • (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) +
        ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)
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₂ : Sbtw ℝ p₁ p p₂
hp₃p₄ : Sbtw ℝ p₃ p p₄
hn : ¬Collinear ℝ {p₁, p, p₃}
h_angle_eq : ∠ p₁ p p₄ = ∠ p₃ p p₂
hcol_p₁pp₂ : Collinear ℝ {p₁, p, p₂}
hcol_p₃pp₄ : Collinear ℝ {p₃, p, p₄}
this : AffineIndependent ℝ ![p₁, p, p₃]
⊢ AffineIndependent ℝ ![p₁, p₂, p₃]

Tactic:
grind [hp₁p₂.left_ne_right, affineIndependent_of_affineIndependent_collinear_ne,
      AffineIndependent.comm_left, AffineIndependent.comm_right]

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)
⊢ (affineSpan ℝ (Set.range (sx.faceOpposite i).points)).SOppSide (sx.points i)
    (s.secondInter (sx.points i) (p' -ᵥ sx.points i))

Tactic:
refine s.sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite hi hsx ?_

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)
⊢ p' ∈ (sx.faceOpposite i).interior
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₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ affineSpan ℝ (Set.range t₂.points) = affineSpan ℝ (Set.range t₁.points)

Tactic:
refine ext_of_direction_eq ?_
      ⟨t₁.points i₃, mem_affineSpan ℝ ⟨j₃, h₃⟩, mem_affineSpan ℝ (Set.mem_range_self _)⟩

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
⊢ (affineSpan ℝ (Set.range t₂.points)).direction = (affineSpan ℝ (Set.range t₁.points)).direction
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
x : M
hf : IsLocalDiffeomorphAt I J n f x
x' : M
hx' : x' ∈ hf.localInverse.target
⊢ ↑hf.localInverse.toPartialEquiv (↑(Exists.choose hf).toPartialEquiv x') = x'

Tactic:
exact hf.choose.left_inv hx'

Goal state after:
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
s : Set P
ho : OrthocentricSystem s
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
⊢ AffineIndependent ℝ p

Tactic:
by
  rcases ho with ⟨t, hto, hst⟩
  rw [hst] at hps
  rcases exists_dist_eq_circumradius_of_subset_insert_orthocenter hto hps hpi with ⟨c, _, hc⟩
  exact Cospherical.affineIndependent ⟨c, t.circumradius, hc⟩ Set.Subset.rfl hpi

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

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝³ : I.Boundaryless
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
f : M → F
U : Set M
c : M
hd : MDiff[U] f
hc : IsPreconnected U
ho : IsOpen[inst✝²] U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
hVo : IsOpen[inst✝²] V
hVne : (U ∩ V).Nonempty
W : Set M := U ∩ {z | ‖f z‖ = ‖f c‖}ᶜ
hWo : IsOpen[inst✝²] W
⊢ U ⊆ V

Tactic:
have hdVW : Disjoint V W := disjoint_compl_right.mono inf_le_right inf_le_right

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℂ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝³ : I.Boundaryless
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
f : M → F
U : Set M
c : M
hd : MDiff[U] f
hc : IsPreconnected U
ho : IsOpen[inst✝²] U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set M := {z | z ∈ U ∧ ‖f z‖ = ‖f c‖}
hVo : IsOpen[inst✝²] V
hVne : (U ∩ V).Nonempty
W : Set M := U ∩ {z | ‖f z‖ = ‖f c‖}ᶜ
hWo : IsOpen[inst✝²] W
hdVW : Disjoint V W
⊢ U ⊆ V
Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent

Goal state before:
pp: case e_f.e_f.hc
𝕜 : 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
inst✝⁶ : IsManifold I 1 M
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)
x₀ x : N
hx : f x ∈ (chartAt H (f x₀)).source
hy : g x ∈ (chartAt H' (g x₀)).source
⊢ f x ∈ (extChartAt I (f x₀)).source

Tactic:
simpa using hx

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁵ : NontriviallyNormedField 𝕜
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace 𝕜 F
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝¹⁰ : NormedAddCommGroup EB
inst✝⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁷ : TopologicalSpace B
inst✝⁶ : ChartedSpace HB B
inst✝⁵ : FiberBundle F E
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle 1 F E IB
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
s : (b : B) → E b
b₀ : B
hex₀ : b₀ ∈ e.baseSet
⊢ MDiffAt (T% s) b₀ ↔ (MDiffAt fun x ↦ (↑e ⟨x, s x⟩).2) b₀

Tactic:
simpa [← mdifferentiableWithinAt_univ] using e.mdifferentiableWithinAt_section_iff IB s hex₀

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiff[u]
t' : Set N := t ∩ g ⁻¹' (extChartAt I (g x₀)).source
ht't : t' ⊆ t
⊢ ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv[u] (f x) (g x)) x₀) t' x₀

Tactic:
have hx₀gx₀ : (x₀, g x₀) ∈ t ×ˢ u := by simp [hx₀, hu hx₀]

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiff[u]
t' : Set N := t ∩ g ⁻¹' (extChartAt I (g x₀)).source
ht't : t' ⊆ t
hx₀gx₀ : (x₀, g x₀) ∈ t ×ˢ u
⊢ ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv[u] (f x) (g x)) x₀) t' x₀
Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace

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
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
s : Set M
x : M
hg : MDiffAt[s] g x
hf : MDiffAt[s] f x
⊢ MapsTo (fun x ↦ (g x, f x)) s univ

Tactic:
simp_rw [mapsTo_univ]

Goal state after: