mathlib-initiative/mathlib-tactics huggingface dataset:
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 : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
cc₃ : P
cr₃ : ℝ
hcc₃ : cc₃ ∈ affineSpan ℝ (insert p ↑s)
hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃
t₃ : ℝ
hcc₃' : cc ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
hcr₃' : ∀ p₁ ∈ ps, dist p₁ ↑⟨cc, hcc₃'⟩ = cr
⊢ cr₃ = √(cr * cr + t₃ * y * (t₃ * y))

Tactic:
obtain ⟨p0, hp0⟩ := hnps

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 : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
cc₃ : P
cr₃ : ℝ
hcc₃ : cc₃ ∈ affineSpan ℝ (insert p ↑s)
hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃
t₃ : ℝ
hcc₃' : cc ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
hcr₃' : ∀ p₁ ∈ ps, dist p₁ ↑⟨cc, hcc₃'⟩ = cr
p0 : P
hp0 : p0 ∈ ps
⊢ cr₃ = √(cr * cr + t₃ * y * (t₃ * y))
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)
⊢ SignType.sign (s.excenterWeights {i} i) = -1

Tactic:
simp_rw [excenterWeights, Pi.smul_apply, smul_eq_mul, sign_mul]

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)
⊢ SignType.sign (∑ i_1, s.excenterWeightsUnnorm {i} i_1)⁻¹ * SignType.sign (s.excenterWeightsUnnorm {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 j : Fin (n + 1)
h : i ≠ j
⊢ SignType.sign (s.excenterWeights {i} j) = 1

Tactic:
simp_rw [excenterWeights, Pi.smul_apply, smul_eq_mul, sign_mul]

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 j : Fin (n + 1)
h : i ≠ j
⊢ SignType.sign (∑ i_1, s.excenterWeightsUnnorm {i} i_1)⁻¹ * SignType.sign (s.excenterWeightsUnnorm {i} j) = 1
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:
hxy

Goal state after:
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
⊢ ‖y‖ = ‖y‖
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case refine_1.inl
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₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : s.excenterWeights signs₁ = s.excenterWeights signs₂
hi :
  ∀ (i : Fin (n + 1)),
    SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₁ i) =
      SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₂ i)
hn₁ : ∑ i, s.excenterWeightsUnnorm signs₁ i ≠ 0
hn₂ : ∑ i, s.excenterWeightsUnnorm signs₂ i ≠ 0
hs : SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ = SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹
⊢ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ

pp: case refine_1.inr
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₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : s.excenterWeights signs₁ = s.excenterWeights signs₂
hi :
  ∀ (i : Fin (n + 1)),
    SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₁ i) =
      SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₂ i)
hn₁ : ∑ i, s.excenterWeightsUnnorm signs₁ i ≠ 0
hn₂ : ∑ i, s.excenterWeightsUnnorm signs₂ i ≠ 0
hs : SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ = -SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹
⊢ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ

Tactic:
· simp only [hs, mul_eq_mul_left_iff, sign_eq_zero_iff, inv_eq_zero, hn₂, or_false] at hi
      simp only [excenterWeightsUnnorm, sign_mul, inv_pos, height_pos, sign_pos, mul_one] at hi
      left
      ext i
      replace hi := hi i
      split_ifs at hi <;> simp_all

Goal state after:
case refine_1.inr
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₁ signs₂ : Finset (Fin (n + 1))
h₁ : s.ExcenterExists signs₁
h₂ : s.ExcenterExists signs₂
h : s.excenterWeights signs₁ = s.excenterWeights signs₂
hi :
  ∀ (i : Fin (n + 1)),
    SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₁ i) =
      SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹ * SignType.sign (s.excenterWeightsUnnorm signs₂ i)
hn₁ : ∑ i, s.excenterWeightsUnnorm signs₁ i ≠ 0
hn₂ : ∑ i, s.excenterWeightsUnnorm signs₂ i ≠ 0
hs : SignType.sign (∑ i, s.excenterWeightsUnnorm signs₁ i)⁻¹ = -SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹
⊢ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: case h
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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0

Tactic:
· simpa using h.symm

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

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

Tactic:
have h := angle_eq_angle_add_add_angle_add (x - y) hy

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
h : angle (x - y) y = angle (x - y) (x - y + y) + angle y (x - y + y)
⊢ angle x y + angle x (x - y) + angle y (y - x) = π
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)
⊢ (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SOppSide (s.points i) (s.excenter signs) ↔
    s.excenterWeights signs i < 0

Tactic:
by
  rw [excenter_eq_affineCombination,
    s.sOppSide_affineSpan_faceOpposite_point_left_iff h.sum_excenterWeights_eq_one]

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 c p x : P
hx : Sbtw ℝ a x c
⊢ ∠ a p x + ∠ x p c = ∠ a p c

Tactic:
rcases eq_or_ne p a with rfl | hpa

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
c p x : P
hx : Sbtw ℝ p x c
⊢ ∠ p p x + ∠ x p c = ∠ p p c

case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a c p x : P
hx : Sbtw ℝ a x c
hpa : p ≠ a
⊢ ∠ a p x + ∠ x p c = ∠ a p c
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: n : ℕ
⊢ ∑ i, circumcenterWeightsWithCircumcenter n i = 1

Tactic:
by
  classical
  convert! sum_ite_eq' univ circumcenterIndex (Function.const _ (1 : ℝ)) with j
  · cases j <;> simp [circumcenterWeightsWithCircumcenter]
  · simp

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 = y
h₂ : ¬x = -y
⊢ ¬x = ⟪y, x⟫ • y

Tactic:
intro H2

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H2 : x = ⟪y, x⟫ • y
⊢ False
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 j : Fin (n + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
this : s.excenter signs -ᵥ s.touchpoint signs i ∈ (vectorSpan ℝ (Set.range s.points))ᗮ
h' : s.excenter signs -ᵥ s.touchpoint signs i ∈ vectorSpan ℝ (Set.range s.points)
h0 : s.exradius signs = 0
⊢ False

Tactic:
exact h.exradius_pos.ne' h0

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

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
hz : z = 0
⊢ angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)

Tactic:
have hx : x ≠ 0 := by simp_all

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
hz : z = 0
hx : x ≠ 0
⊢ angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
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
t : Triangle ℝ P
i : Fin 3
⊢ Simplex.ExcenterExists t {i}

Tactic:
exact t.excenterExists_singleton _

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

Goal state before:
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
t : Triangle ℝ P
i : Fin 3
⊢ Simplex.ExcenterExists t {i}

Tactic:
exact t.excenterExists_singleton _

Goal state after:
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
this :
  HasFDerivAt (inversion c R)
    ((R ^ 2 * ((fun y ↦ y⁻¹) ∘ fun x ↦ ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
      (R ^ 2 •
            -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
              2 • (innerSL ℝ) (_root_.id (c + x) - c) ∘SL ContinuousLinearMap.id ℝ F).smulRight
        (_root_.id (c + x) - c))
    (c + x)
⊢ ‖x‖ ^ 2 / (‖x‖ ^ 2 * ‖x‖ ^ 2) = (‖x‖ ^ 2)⁻¹

Tactic:
div_self_mul_self'

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x ↦ c + x) x ≠ c
this :
  HasFDerivAt (inversion c R)
    ((R ^ 2 * ((fun y ↦ y⁻¹) ∘ fun x ↦ ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
      (R ^ 2 •
            -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
              2 • (innerSL ℝ) (_root_.id (c + x) - c) ∘SL ContinuousLinearMap.id ℝ F).smulRight
        (_root_.id (c + x) - c))
    (c + x)
⊢ (‖x‖ ^ 2)⁻¹ = (‖x‖ ^ 2)⁻¹
Module: Mathlib.Geometry.Euclidean.Simplex

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₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
⊢ 0 ≤ π / 3

Tactic:
linarith [Real.pi_nonneg]

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

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₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
⊢ π / 3 ≤ π

Tactic:
linarith [Real.pi_nonneg]

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

Tactic:
have hp' : (p' -ᵥ (sx.points i)) =
      r • (Finset.univ.affineCombination ℝ sx.points w -ᵥ (sx.points i)) := by simp [p']

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)
⊢ (affineSpan ℝ (Set.range (sx.faceOpposite i).points)).SOppSide (sx.points i)
    (s.secondInter (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points) w -ᵥ sx.points i))
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
t t₀ : Triangle ℝ P
ht : Set.range t.points ⊆ insert t₀.orthocenter (Set.range t₀.points)
ht₀o : t₀.orthocenter ∉ Set.range t₀.points
ht₀s : s = insert t₀.orthocenter (Set.range t₀.points)
i₁ i₂ i₃ j₂ j₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ : t.points i₁ = t₀.orthocenter
hj₂₃ : j₂ ≠ j₃
h₂ : t₀.points j₂ = t.points i₂
h₃ : t₀.points j₃ = t.points i₃
j₁ : Fin 3
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₁₂₃ : ∀ (j : Fin 3), j = j₁ ∨ j = j₂ ∨ j = j₃
h : t₀.points j₁ = t.orthocenter
⊢ s = insert t.orthocenter (Set.range t.points)

Tactic:
by
      have hui : (Set.univ : Set (Fin 3)) = {i₁, i₂, i₃} := by ext x; simpa using h₁₂₃ x
      have huj : (Set.univ : Set (Fin 3)) = {j₁, j₂, j₃} := by ext x; simpa using hj₁₂₃ x
      rw [← h, ht₀s, ← Set.image_univ, huj, ← Set.image_univ, hui]
      simp_rw [Set.image_insert_eq, Set.image_singleton, h₁, ← h₂, ← h₃]
      rw [Set.insert_comm]

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✝
E'✝ : Type u_5
inst✝¹⁵ : NormedAddCommGroup E'✝
inst✝¹⁴ : NormedSpace 𝕜✝ E'✝
H'✝ : Type u_6
inst✝¹³ : TopologicalSpace H'✝
I'✝ : ModelWithCorners 𝕜✝ E'✝ H'✝
N✝ : Type u_7
inst✝¹² : TopologicalSpace N✝
inst✝¹¹ : ChartedSpace H'✝ N✝
𝕜 : 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'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h✝ : IsRCLikeNormedField 𝕜
x✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝ : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' : Surjective ⇑(if True then fderiv 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x) else 0)
hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x)
⊢ Surjective ⇑(fderiv ℝ (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x))

Tactic:
hf''.fderiv_restrictScalars (𝕜 := ℝ),

Goal state after:
𝕜✝ : 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'✝
I'✝ : ModelWithCorners 𝕜✝ E'✝ H'✝
N✝ : Type u_7
inst✝¹² : TopologicalSpace N✝
inst✝¹¹ : ChartedSpace H'✝ N✝
𝕜 : 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'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
f : M → N
x : M
hf : MDiffAt f x
hx : I.IsInteriorPoint x
h✝ : IsRCLikeNormedField 𝕜
x✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝ : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
hf' : Surjective ⇑(if True then fderiv 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x) else 0)
hf'' : DifferentiableAt 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x)
⊢ Surjective ⇑(ContinuousLinearMap.restrictScalars ℝ (fderiv 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x) x)))
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
U : Set M
a b : M
hpc : IsPreconnected U
hc✝ : IsCompact U
ho : IsOpen[inst✝²] U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDiff[U] f
hb₀ : f b = 0
c : M
hcU : c ∈ U
hc : IsMaxOn (fun x ↦ ‖f x‖) U c
this : ∀ x ∈ U, ‖f x‖ = ‖f c‖
⊢ ‖f a‖ = 0

Tactic:
this a ha,

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
U : Set M
a b : M
hpc : IsPreconnected U
hc✝ : IsCompact U
ho : IsOpen[inst✝²] U
ha : a ∈ U
hb : b ∈ U
f : M → F
hd : MDiff[U] f
hb₀ : f b = 0
c : M
hcU : c ∈ U
hc : IsMaxOn (fun x ↦ ‖f x‖) U c
this : ∀ x ∈ U, ‖f x‖ = ‖f c‖
⊢ ‖f c‖ = 0
Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

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
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g h : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝕜⟯⟨g * h⟩
⊢ ((𝒅 (𝑳 I (g * h)) 1) ((evalAt 1) X)) f = ((𝒅 (𝑳 I g) h) ((evalAt h) X)) f

Tactic:
L_mul,

Goal state after:
𝕜 : 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
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g h : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝕜⟯⟨g * h⟩
⊢ ((𝒅 ((𝑳 I g).comp (𝑳 I h)) 1) ((evalAt 1) X)) f = ((𝒅 (𝑳 I g) h) ((evalAt h) X)) f
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
x : TotalSpace F E
this : MDiffAt id x
⊢ MDiffAt TotalSpace.proj x

Tactic:
rw [mdifferentiableAt_totalSpace] at this

Goal state after:
𝕜 : 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
x : TotalSpace F E
this : (MDiffAt fun x ↦ (id x).proj) x ∧ (MDiffAt fun x_1 ↦ (↑(trivializationAt F E (id x).proj) (id x_1)).2) x
⊢ MDiffAt TotalSpace.proj x