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

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
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂

Tactic:
rw [eq_comm, ← @vsub_ne_zero V, ← @vsub_eq_zero_iff_eq V, or_comm] at h0

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₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hr : ∃ r, r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p
⊢ dist p₁ p = dist p₂ p

Tactic:
rcases hr with ⟨r, rfl⟩
    simp_rw [@dist_eq_norm_vsub V, vsub_vadd_eq_vsub_sub, left_vsub_midpoint, right_vsub_midpoint,
      invOf_eq_inv, ← neg_vsub_eq_vsub_rev p₂ p₁, ← mul_self_inj (norm_nonneg _) (norm_nonneg _), ←
      real_inner_self_eq_norm_mul_norm, inner_sub_sub_self]
    simp [-neg_vsub_eq_vsub_rev]

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 r : P
⊢ ⟪NormedSpace.normalize v, q -ᵥ p⟫ + ⟪NormedSpace.normalize v, r -ᵥ q⟫ = ⟪NormedSpace.normalize v, r -ᵥ p⟫

Tactic:
rw [add_comm, ← inner_add_right, vsub_add_vsub_cancel]

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

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
c p₁ p₂ : P
⊢ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪midpoint ℝ p₁ p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = dist p₁ p₂ ^ 2 / 2

Tactic:
midpoint_vsub_left,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪⅟2 • (p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = dist p₁ p₂ ^ 2 / 2
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

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₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
⊢ ((∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal) / 2 = (∡ p₁ p₂ p₄).toReal / 2

Tactic:
have hadd := oangle_add h₁₂ h₃₂ h₄₂

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
⊢ ((∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal) / 2 = (∡ p₁ p₂ p₄).toReal / 2
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₂ p : P
⊢ dist p (midpoint ℝ p p₂) = ‖2‖⁻¹ * dist p p₂

pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ dist p₂ (midpoint ℝ p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂

Tactic:
· rw [dist_comm, dist_midpoint_left (𝕜 := ℝ)]

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ dist p₂ (midpoint ℝ p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
⊢ Nonempty ↥(s.orthRadius p)

Tactic:
rw [orthRadius]

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
p : P
⊢ Nonempty ↥(mk' p (ℝ ∙ (p -ᵥ s.center))ᗮ)
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h : dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
ho : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
hs : ↑((orthogonalProjection (line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃])) p) = ↑((orthogonalProjection line[ℝ, p₁, p₂]) p)
hinf : line[ℝ, p₁, p₂] ⊓ line[ℝ, p₁, p₃] = affineSpan ℝ {p₁}
⊢ affineSpan ℝ ({p₁, p₂} ∪ {p₁, p₃}) = ⊤

Tactic:
convert! ha.affineSpan_eq_top_iff_card_eq_finrank_add_one.2 ?_

Goal state after:
case e'_8
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h : dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
ho : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
hs : ↑((orthogonalProjection (line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃])) p) = ↑((orthogonalProjection line[ℝ, p₁, p₂]) p)
hinf : line[ℝ, p₁, p₂] ⊓ line[ℝ, p₁, p₃] = affineSpan ℝ {p₁}
⊢ {p₁, p₂} ∪ {p₁, p₃} = Set.range ![p₁, p₂, p₃]

V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h : dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
ho : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
hs : ↑((orthogonalProjection (line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃])) p) = ↑((orthogonalProjection line[ℝ, p₁, p₂]) p)
hinf : line[ℝ, p₁, p₂] ⊓ line[ℝ, p₁, p₃] = affineSpan ℝ {p₁}
⊢ Fintype.card (Fin (Nat.succ 0).succ.succ) = finrank ℝ V + 1
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 : Sphere P
p q : P
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
hq : q ∈ as
⊢ dist q s.center ^ 2 = s.radius ^ 2 + dist q p ^ 2

Tactic:
rw [← h.mem_sphere]
  exact s.dist_sq_eq_of_mem_orthRadius (SetLike.le_def.1 h.le_orthRadius hq)

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p q : P
⊢ (s.orthRadius p).direction ≤ (s.orthRadius q).direction ↔ ∃ r, q -ᵥ s.center = r • (p -ᵥ s.center)

Tactic:
by
  simp [Submodule.orthogonal_le_orthogonal_iff, Submodule.mem_span_singleton, eq_comm]

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

Goal state before:
pp: case inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hp : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr0 : r ≠ 0
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)

Tactic:
have hr' : ‖q -ᵥ s.center‖ = ‖r • (p -ᵥ s.center)‖ := by
      rw [hr]

Goal state after:
case inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hp : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr0 : r ≠ 0
hr' : ‖q -ᵥ s.center‖ = ‖r • (p -ᵥ s.center)‖
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

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
inst✝ : Nontrivial V
s₁ s₂ : Sphere P
⊢ dist s₁.center s₂.center = s₂.radius - s₁.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius → s₁.IsIntTangent s₂

Tactic:
rintro ⟨h, h₁, h₂⟩
    by_cases h0 : s₁.center = s₂.center
    · rw [h0, dist_self, eq_comm, sub_eq_zero, eq_comm] at h
      have hs : s₁ = s₂ := by
        ext <;> assumption
      simp [hs, h₂]
    · rw [dist_comm] at h
      have ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius := by
        refine abs_of_nonneg ?_
        rw [← h]
        exact dist_nonneg
      have hr0 : s₂.radius - s₁.radius ≠ 0 := by
        intro hr0
        rw [hr0, dist_eq_zero] at h
        exact h0 h.symm
      refine ⟨AffineMap.lineMap s₂.center s₁.center (s₂.radius / (s₂.radius - s₁.radius)),
              ?_, ?_, ?_⟩
      · simp only [mem_sphere, dist_lineMap_right, Real.norm_eq_abs, h, one_sub_div hr0, abs_div,
          sub_sub_cancel_left, abs_neg, abs_of_nonneg h₁, ha]
        field
      · simp only [mem_sphere, dist_lineMap_left, norm_div, Real.norm_eq_abs, h, ha,
          abs_of_nonneg h₂]
        field
      · rw [wbtw_iff_left_eq_or_right_mem_image_Ici]
        simp only [Ne.symm h0, Set.mem_image, Set.mem_Ici, AffineMap.lineMap_eq_lineMap_iff,
          false_or, exists_eq_right]
        rw [one_le_div]
        · linarith
        · rw [← h]
          simp [Ne.symm h0]

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

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
n : ℕ
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 [← Finset.mul_sum, h]

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

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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(s.orthRadius p).direction
hv : ∀ (w : ↥(s.orthRadius p).direction), ∃ c, c • v = w
hv0 : ↑v ≠ 0
⊢ {(√(s.radius ^ 2 - dist p s.center ^ 2) / ‖↑v‖) • ↑v +ᵥ p,
        -(√(s.radius ^ 2 - dist p s.center ^ 2) / ‖↑v‖) • ↑v +ᵥ p}.ncard =
    2

Tactic:
Submodule.norm_coe,

Goal state after:
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 : ↥(s.orthRadius p).direction
hv : ∀ (w : ↥(s.orthRadius p).direction), ∃ c, c • v = w
hv0 : ↑v ≠ 0
⊢ {(√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • ↑v +ᵥ p,
        -(√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • ↑v +ᵥ p}.ncard =
    2
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
hxy : x ≠ -y
⊢ Real.sin (angle x y) = Real.sin (angle x (x + y) + angle y (y + x))

Tactic:
· rw [Real.sin_add, cos_angle, cos_angle, sin_angle_add hx (by grind),
      sin_angle_add hy (by grind), sin_angle hx hy, add_comm y x]
    have : x + y ≠ 0 := by grind
    simp only [field] -- non-recursive `field_simp`
    simp only [← real_inner_self_eq_norm_sq, inner_add_right, inner_add_left, real_inner_comm]
    ring_nf

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
p₁ p₂ p₃ : P
⊢ Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) * dist p₃ p₂ =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁)) * dist p₃ p₁

Tactic:
dist_eq_norm_vsub V p₃ 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
p₁ p₂ p₃ : P
⊢ Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) * ‖p₃ -ᵥ p₂‖ =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁)) * dist p₃ p₁
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
⊢ x = Real.cos (angle x y) • y + Real.sin (angle x y) • NormedSpace.normalize (ortho y x)

Tactic:
rw [← inner_ortho_right_eq_sin_angle hx hy, ← inner_eq_cos_angle_of_norm_eq_one hx hy,
    ortho_eq_sub_inner _ hy]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ x = ⟪x, y⟫ • y + ⟪x, NormedSpace.normalize (x - ⟪y, x⟫ • y)⟫ • NormedSpace.normalize (x - ⟪y, x⟫ • y)
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
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
⊢ False

Tactic:
subst hn1

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
inst✝ : NeZero 1
s : Simplex ℝ P 1
signs : Finset (Fin (1 + 1))
h : s.ExcenterExists signs
i j : Fin (1 + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
kx ky kz : ℝ≥0
hy : ky ≠ 0
hlincomb : ky • y = kx • x + kz • z
⊢ ky • y ∈ Submodule.span ℝ≥0 {x, z}

Tactic:
rw [Submodule.mem_span_pair]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
kx ky kz : ℝ≥0
hy : ky ≠ 0
hlincomb : ky • y = kx • x + kz • z
⊢ ∃ a b, a • x + b • z = ky • y
Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane

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
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R ⁻¹' sphere y (dist y c) = insert c ↑(perpBisector c (inversion c R y))

Tactic:
preimage_inversion_sphere_dist_center hR hy

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ insert c ↑(perpBisector c (inversion c R y)) = insert c ↑(perpBisector c (inversion c R y))
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, r ≠ 0 ∧ ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)) ↔
    ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)

Tactic:
refine ⟨?_, ?_⟩ <;> rintro ⟨r, hr, h⟩ <;> refine ⟨r, hr, fun i₁ i₂ ↦ ?_⟩

Goal state after:
case refine_1
ι : 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₂)
i₁ i₂ : ι
⊢ i₁ ≠ i₂ → (fun i₁ i₂ ↦ edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)) i₁ i₂

case refine_2
ι : 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 : Pairwise fun i₁ i₂ ↦ edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)
i₁ i₂ : ι
⊢ edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ 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
a b p q : P
hp : p ∈ line[ℝ, a, b]
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
r : P
⊢ b -ᵥ r = m -ᵥ r + (m -ᵥ a)

Tactic:
midpoint_vsub_left,

Goal state after:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : p ∈ line[ℝ, a, b]
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
r : P
⊢ b -ᵥ r = m -ᵥ r + ⅟2 • (b -ᵥ a)
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
p : P
hp : p ∈ sx.interior
⊢ (affineSpan ℝ (Set.range (sx.faceOpposite i).points)).SOppSide (sx.points i)
    (s.secondInter (sx.points i) (p -ᵥ sx.points i))

Tactic:
obtain ⟨w, hw, hw01, rfl⟩ := hp
  let r : ℝ := (1 - w i)⁻¹
  have hrpos : 0 < r := by simp [inv_pos, sub_pos, r, (hw01 i).2]
  let p' : P := AffineMap.lineMap (sx.points i) (Finset.univ.affineCombination ℝ sx.points w) r
  have hp' : (p' -ᵥ (sx.points i)) =
      r • (Finset.univ.affineCombination ℝ sx.points w -ᵥ (sx.points i)) := by simp [p']
  suffices (affineSpan ℝ (Set.range (sx.faceOpposite i).points)).SOppSide (sx.points i)
      (s.secondInter (sx.points i) (p' -ᵥ (sx.points i))) by
    rwa [hp', s.secondInter_smul _ _ hrpos.ne'] at this
  refine s.sOppSide_faceOpposite_secondInter_of_mem_interior_faceOpposite hi hsx ?_
  simp_rw [p', ← Finset.univ.affineCombination_piSingle ℝ (sx.points)
    (Finset.mem_univ i), AffineMap.lineMap_apply, Finset.affineCombination_vsub,
    ← LinearMap.map_smul, Finset.weightedVSub_vadd_affineCombination,
    Affine.Simplex.faceOpposite]
  rw [Affine.Simplex.affineCombination_mem_interior_face_iff_pos]
  · simp only [Finset.mem_compl, Finset.mem_singleton, Pi.add_apply, Pi.smul_apply, Pi.sub_apply,
      smul_eq_mul, Decidable.not_not, forall_eq, Pi.single_eq_same]
    refine ⟨fun j hj ↦ ?_, by grind⟩
    simp [hj, hrpos, (hw01 j).1]
  · simp [Finset.sum_add_distrib, ← Finset.mul_sum, hw]

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
c : M
hd : ∀ᶠ (z : M) in 𝓝 c, MDiffAt f z
hc : IsLocalMax (norm ∘ f) c
e : PartialEquiv M E := extChartAt I c
hI : range ↑I = univ
H₁ : 𝓝[range ↑I] ↑e c = 𝓝 (↑e c)
H₂ : map (↑e.symm) (𝓝 (↑e c)) = 𝓝 c
this : e.target ∈ 𝓝 (↑e c)
y : E
hyt : y ∈ e.target
hy₂ : MDiffAt f (↑e.symm y)
⊢ ↑e.symm y ∈ (extChartAt I c).source

Tactic:
exact (extChartAt I c).map_target hyt

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
hf' : Surjective ⇑(mfderiv% f x)
hx : I.IsInteriorPoint x
h✝ : IsRCLikeNormedField 𝕜
x✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x✝ : NormedSpace ℝ E' := NormedSpace.restrictScalars ℝ 𝕜 E'
⊢ I'.IsInteriorPoint (f x)

Tactic:
simp only [mfderiv, hf] at hf'

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 fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (range ↑I) (↑(extChartAt I x) x) else 0)
⊢ I'.IsInteriorPoint (f x)