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
n : ℕ
s : Simplex ℝ P n
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ x,
        ((if x ∈ {i₁, i₂} then ((↑2)⁻¹ + (↑2)⁻¹) • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
          else 0) -
          if x = i₁ ∨ x = i₂ then 1 • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) else 0) +
      (-(1 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯)) -
        -(1 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯))) =
    0

Tactic:
sub_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
n : ℕ
s : Simplex ℝ P n
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ x,
        ((if x ∈ {i₁, i₂} then ((↑2)⁻¹ + (↑2)⁻¹) • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
          else 0) -
          if x = i₁ ∨ x = i₂ then 1 • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) else 0) +
      0 =
    0
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
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
⊢ Cospherical ps ↔ ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius

Tactic:
constructor
  · rintro ⟨c, hcr⟩
    rw [exists_dist_eq_iff_exists_dist_orthogonalProjection_eq h c] at hcr
    exact ⟨orthogonalProjection s c, orthogonalProjection_mem _, hcr⟩
  · exact fun ⟨c, _, hd⟩ => ⟨c, hd⟩

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 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
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
by_cases H3 : angle y z = 0

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

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
⊢ 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₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
⊢ π / 3 ≤ ∠ p₁ p₂ p₃

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

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

Goal state before:
pp: case neg.inl.inl
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₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne✝ : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
hne : ∠ p₁ p₂ p₃ < ∠ p₂ p₃ p₁
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

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

Goal state before:
pp: case neg.inl.inr
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₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne✝ : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
hne : ∠ p₂ p₃ p₁ < ∠ p₁ p₂ p₃
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

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

Goal state before:
pp: case neg.inr.inl.inl
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₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne✝ : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ < ∠ p₃ p₁ p₂
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

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

Goal state before:
pp: case neg.inr.inl.inr
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₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne✝ : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₁ p₂ p₃
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

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

Goal state before:
pp: case neg.inr.inr.inl
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₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne✝ : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₂ p₃ p₁ < ∠ p₃ p₁ p₂
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

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

Goal state before:
pp: case neg.inr.inr.inr
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₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
h : ¬p₂ = p₁
hne✝ : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₂ p₃ p₁
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Goal state after:
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₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃
h : ¬p₂ = p₁
⊢ ∠ p₁ p₂ p₃ ≤ π / 3

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

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

Goal state before:
pp: case neg.inl.inl
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₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne✝ : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
hne : ∠ p₁ p₂ p₃ < ∠ p₂ p₃ p₁
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

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

Goal state before:
pp: case neg.inl.inr
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₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne✝ : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁
hne : ∠ p₂ p₃ p₁ < ∠ p₁ p₂ p₃
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

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

Goal state before:
pp: case neg.inr.inl.inl
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₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne✝ : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ < ∠ p₃ p₁ p₂
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

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

Goal state before:
pp: case neg.inr.inl.inr
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₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne✝ : ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₁ p₂ p₃
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

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

Goal state before:
pp: case neg.inr.inr.inl
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₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne✝ : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₂ p₃ p₁ < ∠ p₃ p₁ p₂
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ h]

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

Goal state before:
pp: case neg.inr.inr.inr
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₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
hne✝ : ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
hne : ∠ p₃ p₁ p₂ < ∠ p₂ p₃ p₁
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
linarith [angle_add_angle_add_angle_eq_pi p₃ 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 z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
⊢ angle x z ≠ π →
    angle x z = angle x y + angle y z → Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
by
  intros H H0
  by_cases H1 : angle x z = 0
  · grind [angle_nonneg, Real.sin_zero, zero_smul]
  have Hxz : Real.sin (angle x z) ≠ 0 := by
    grind [sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi]
  by_cases H2 : angle x y = 0
  · grind [Real.sin_zero, zero_smul, eq_of_angle_eq_zero]
  by_cases H3 : angle y z = 0
  · grind [Real.sin_zero, zero_smul, smul_right_inj, eq_of_angle_eq_zero]
  by_cases H4 : angle x y = π
  · grind [angle_le_pi, angle_nonneg]
  by_cases H5 : angle y z = π
  · grind [angle_le_pi, angle_nonneg]
  have H6 : ⟪x, z⟫ = ⟪x, z⟫ := rfl
  nth_rw 2 [angle_le_angle_add_angle_aux hx hy, angle_le_angle_add_angle_aux hz hy] at H6
  simp only [inner_add_left, inner_add_right, real_inner_smul_left, real_inner_smul_right,
             real_inner_comm y (normalize _), real_inner_self_eq_norm_sq, hy, angle_comm z y,
             inner_normalize_ortho] at H6
  simp only [one_pow, mul_one, mul_zero, add_zero, zero_add] at H6
  rw [inner_eq_cos_angle_of_norm_eq_one hx hz, H0, Real.cos_add] at H6
  ring_nf at H6
  have Hw : Real.sin (angle x y) * Real.sin (angle y z) ≠ 0 := by
    grind [sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi]
  have H8 : ⟪normalize (ortho y x), normalize (ortho y z)⟫ = -1 := by
    grind
  have H9 : ortho y x ≠ 0 := by
    grind [ortho_ne_zero_of_not_collinear, angle_comm]
  have H10 : ortho y z ≠ 0 := by
    grind [ortho_ne_zero_of_not_collinear]
  have H11 : ‖normalize (ortho y x)‖ = 1 := norm_normalize_eq_one_iff.mpr H9
  have H12 : ‖normalize (ortho y z)‖ = 1 := norm_normalize_eq_one_iff.mpr H10
  rw [inner_eq_neg_one_iff_of_norm_eq_one H11 H12] at H8
  nth_rw 2 [angle_le_angle_add_angle_aux hx hy]
  nth_rw 3 [angle_le_angle_add_angle_aux hz hy]
  rw [H8]; match_scalars <;> grind [Real.sin_add, angle_comm]

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

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

Tactic:
grind [isUnit_iff_ne_zero]

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

Goal state before:
pp: n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ ∑ i, mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ i = 0

Tactic:
mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub h

Goal state after:
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ ∑ i, (mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ) i = 0
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ {i₁, i₂}ᶜ.Nonempty

Tactic:
simp [← card_pos, card_compl, h]

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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ (univ.weightedVSub s.pointsWithCircumcenter)
      (mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ) =
    (univ.weightedVSub s.pointsWithCircumcenter) (mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂)

Tactic:
mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub h

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

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

Tactic:
sub_self,

Goal state after:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p a b : P
hp : p ∈ line[ℝ, a, b]
ha : a ∈ s
hb : b ∈ s
hp_on : p ∈ s
hq : dist a s.center = dist b s.center
⊢ |0| = 0
Module: Mathlib.Geometry.Euclidean.MongePoint

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
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
h : t.orthocenter ∈ Set.range p
⊢ ∃ i₁ i₂ i₃ j₂ j₃,
    i₁ ≠ i₂ ∧
      i₁ ≠ i₃ ∧
        i₂ ≠ i₃ ∧
          (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
            p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃

Tactic:
rcases h with ⟨i₁, h₁⟩

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
t : Triangle ℝ P
ho : t.orthocenter ∉ Set.range t.points
p : Fin 3 → P
hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)
hpi : Function.Injective p
i₁ : Fin 3
h₁ : p i₁ = t.orthocenter
⊢ ∃ i₁ i₂ i₃ j₂ j₃,
    i₁ ≠ i₂ ∧
      i₁ ≠ i₃ ∧
        i₂ ≠ i₃ ∧
          (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧
            p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃
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
x : M
⊢ I.IsInteriorPoint x ↔ ¬I.IsBoundaryPoint x

Tactic:
by
  refine ⟨?_,
    by simpa only [or_iff_not_imp_right] using isInteriorPoint_or_isBoundaryPoint x (I := I)⟩
  by_contra! h
  rw [← mem_empty_iff_false (extChartAt I x x),
    ← disjoint_iff_inter_eq_empty.mp disjoint_interior_frontier, mem_inter_iff]
  exact h

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
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
EM : Type u_10
inst✝¹³ : NormedAddCommGroup EM
inst✝¹² : NormedSpace 𝕜 EM
HM : Type u_11
inst✝¹¹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace HM M
inst✝⁸ : TopologicalSpace B
inst✝⁷ : ChartedSpace HB B
inst✝⁶ : FiberBundle F E
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module 𝕜 (E x)
e e' : Trivialization F TotalSpace.proj
inst✝³ : MemTrivializationAtlas e
inst✝² : MemTrivializationAtlas e'
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : ContMDiffVectorBundle 1 F E IB
s : Set M
f : M → B
g : M → F
x : M
hf : MDiffAt[s] f x
hg : MDiffAt[s] g x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
⊢ (fun y ↦ e.coordChange e' (f y) (g y)) =ᶠ[𝓝[s] x] fun x ↦ ↑(Trivialization.coordChangeL 𝕜 e e' (f x)) (g x)

Tactic:
have : e.baseSet ∩ e'.baseSet ∈ 𝓝 (f x) :=
     (e.open_baseSet.inter e'.open_baseSet).mem_nhds ⟨he, he'⟩
    filter_upwards [hf.continuousWithinAt this] with y hy
    exact (Trivialization.coordChangeL_apply' e e' hy (g y)).symm

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ mulInvariantVectorField (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1) g =
    mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) g

Tactic:
mulInvariantVectorField_eq_mpullback,

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
v w : GroupLieAlgebra I G
g : G
⊢ mpullback I I (fun x ↦ g⁻¹ * x) (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w)) g =
    mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) g
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G✝ : Type u_4
inst✝⁸ : TopologicalSpace G✝
inst✝⁷ : ChartedSpace H G✝
inst✝⁶ : Group G✝
inst✝⁵ : LieGroup I (minSmoothness 𝕜 3) G✝
inst✝⁴ : CompleteSpace E
G : Type u_5
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : AddGroup G
inst✝ : LieAddGroup I (minSmoothness 𝕜 3) G
c : 𝕜
v w : AddGroupLieAlgebra I G
⊢ mlieBracket I (addInvariantVectorField v) (c • addInvariantVectorField w) 0 =
    c • mlieBracket I (addInvariantVectorField v) (addInvariantVectorField w) 0

Tactic:
rw [mlieBracket_const_smul_right]

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G✝ : Type u_4
inst✝⁸ : TopologicalSpace G✝
inst✝⁷ : ChartedSpace H G✝
inst✝⁶ : Group G✝
inst✝⁵ : LieGroup I (minSmoothness 𝕜 3) G✝
inst✝⁴ : CompleteSpace E
G : Type u_5
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : AddGroup G
inst✝ : LieAddGroup I (minSmoothness 𝕜 3) G
c : 𝕜
v w : AddGroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, addInvariantVectorField w x⟩) 0
Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
c : 𝕜
v w : GroupLieAlgebra I G
⊢ mlieBracket I (mulInvariantVectorField v) (c • mulInvariantVectorField w) 1 =
    c • mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1

Tactic:
rw [mlieBracket_const_smul_right]

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : ChartedSpace H G
inst✝² : Group G
inst✝¹ : LieGroup I (minSmoothness 𝕜 3) G
inst✝ : CompleteSpace E
c : 𝕜
v w : GroupLieAlgebra I G
⊢ (MDiffAt fun x ↦ ⟨x, mulInvariantVectorField w x⟩) 1
Module: Mathlib.Geometry.Manifold.LocalSourceTargetProperty

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_4
H : Type u_6
G : Type u_8
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_10
N : Type u_12
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop
hf : ContinuousAt f x
hP : IsLocalSourceTargetProperty P
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : domChart ∈ IsManifold.maximalAtlas I n M
hcodChart : codChart ∈ IsManifold.maximalAtlas J n N
hfP : P f domChart codChart
s : Set M
hs : s ⊆ f ⁻¹' codChart.source
hsopen : IsOpen[inst✝³] s
hxs : x ∈ s
⊢ LiftSourceTargetPropertyAt I J n f x P

Tactic:
exact ⟨domChart.restr s, codChart, by grind, hfx,
    restr_mem_maximalAtlas (contDiffGroupoid n I) hdomChart hsopen, hcodChart, by grind,
    hP.mono_source hsopen hfP⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: case neg
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ¬↑z < y
⊢ z ∈ (if ↑z < y then IccLeftChart x y else IccRightChart x y).source

Tactic:
simp only [h', if_false]

Goal state after:
case neg
x✝ y✝ : ℝ
hxy : Fact (x✝ < y✝)
x y : ℝ
h : Fact (x < y)
z : ↑(Icc x y)
h' : ¬↑z < y
⊢ z ∈ (IccRightChart x y).source
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: case inr.inr.hb
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : ↑p ∈ Ioo x y
⊢ p ∉ {⊥, ⊤}

Tactic:
· rintro (rfl | rfl) <;> simp at hp

Goal state after: