mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ (∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F E).range) ↔ (minpoly F x).natSepDegree = 1

Tactic:
minpoly.natSepDegree_eq_one_iff_pow_mem (ringExpChar F)

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ (∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F E).range) ↔ ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F E).range
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

Goal state before:
pp: F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i✝ : ι
f : ι → ℕ
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
lF : ι → F
hlF : ∀ (i : ι), (algebraMap F E) (lF i) = l i ^ q ^ n
i : ι
hs : i ∉ l.support
⊢ (algebraMap F E) (lF i) = 0

Tactic:
rw [hlF, Finsupp.notMem_support_iff.1 hs, zero_pow this]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
⊢ (aeval X) (f.minpolyX ↥K⟮f⟯) = 0

Tactic:
simp only [aeval_sub, aeval_map_algebraMap, aeval_X_left_eq_algebraMap, map_mul, aeval_C,
    IntermediateField.algebraMap_apply, coe_algebraMap]

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) f.num - f * (algebraMap K[X] K⟮X⟯) f.denom = 0
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: case h
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ↑((f.minpolyX ↥K⟮f⟯).coeff f.denom.natDegree) = 0
⊢ C (f.num.coeff f.denom.natDegree) = f * C f.denom.leadingCoeff

Tactic:
simpa [sub_eq_zero] using hf

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

Goal state before:
pp: F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst✝ : IsPurelyInseparable F E
hi : IsIntegral F x
⊢ Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x

Tactic:
have hi' : IsIntegral E x := IsIntegral.tower_top hi

Goal state after:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst✝ : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
⊢ Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

Goal state before:
pp: F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst✝ : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this✝¹ : Algebra.IsSeparable F ↥F⟮x⟯
this✝ : Algebra.IsSeparable E ↥E⟮x⟯
this : Algebra.IsAlgebraic F ↥F⟮x⟯
⊢ (minpoly F x).natDegree = (minpoly E x).natDegree

Tactic:
← adjoin.finrank hi,

Goal state after:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst✝ : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this✝¹ : Algebra.IsSeparable F ↥F⟮x⟯
this✝ : Algebra.IsSeparable E ↥E⟮x⟯
this : Algebra.IsAlgebraic F ↥F⟮x⟯
⊢ Module.finrank F ↥F⟮x⟯ = (minpoly E x).natDegree
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
hF : F.IsFaceOf C
x y : M
hx : x ∈ C
hy : y ∈ C
hxy : x + y ∈ F
⊢ y ∈ F

Tactic:
by
  rw [add_comm x y] at hxy; exact mem_of_add_mem_left hF hy hx hxy

Goal state after:
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h✝ :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ u,
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
x : EuclideanSpace ℝ (Fin n)
x✝ : x ∈ Set.univ
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
h : d.isPlot (p ∘ ↑(OpenPartialHomeomorph.univBall x ε))
⊢ ∃ v, ∃ (hv : IsOpen v), x ∈ v ∧ d.isPlotOn hv p

Tactic:
have h' := d.isPlotOn_reparam (Metric.isOpen_ball) (Set.mapsTo_univ _ _)
      (d.isPlotOn_univ.mpr h) (OpenPartialHomeomorph.contDiffOn_univBall_symm (c := x) (r := ε))

Goal state after:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
h✝ :
  ∀ (x : EuclideanSpace ℝ (Fin n)),
    ∃ u,
      IsOpen u ∧
        x ∈ u ∧
          ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
            (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
x : EuclideanSpace ℝ (Fin n)
x✝ : x ∈ Set.univ
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
h : d.isPlot (p ∘ ↑(OpenPartialHomeomorph.univBall x ε))
h' : d.isPlotOn ⋯ ((p ∘ ↑(OpenPartialHomeomorph.univBall x ε)) ∘ ↑(OpenPartialHomeomorph.univBall x ε).symm)
⊢ ∃ v, ∃ (hv : IsOpen v), x ∈ v ∧ d.isPlotOn hv p
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ ((o.rotationAux θ).toLinearMap ∘ₗ (θ.cos • LinearMap.id - θ.sin • ↑o.rightAngleRotation.toLinearEquiv)) x =
    LinearMap.id x

Tactic:
convert! congr_arg (fun t : ℝ => t • x) θ.cos_sq_add_sin_sq using 1

Goal state after:
case e'_2
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ ((o.rotationAux θ).toLinearMap ∘ₗ (θ.cos • LinearMap.id - θ.sin • ↑o.rightAngleRotation.toLinearEquiv)) x =
    (θ.cos ^ 2 + θ.sin ^ 2) • x

case e'_3
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ LinearMap.id x = 1 • x
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ ((θ.cos • LinearMap.id - θ.sin • ↑o.rightAngleRotation.toLinearEquiv) ∘ₗ (o.rotationAux θ).toLinearMap) x =
    LinearMap.id x

Tactic:
convert! congr_arg (fun t : ℝ => t • x) θ.cos_sq_add_sin_sq using 1

Goal state after:
case e'_2
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ ((θ.cos • LinearMap.id - θ.sin • ↑o.rightAngleRotation.toLinearEquiv) ∘ₗ (o.rotationAux θ).toLinearMap) x =
    (θ.cos ^ 2 + θ.sin ^ 2) • x

case e'_3
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
⊢ LinearMap.id x = 1 • x
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ dist p ↑((orthogonalProjection s) p) ≤ Metric.infDist p ↑s

Tactic:
Metric.infDist_eq_iInf

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ dist p ↑((orthogonalProjection s) p) ≤ ⨅ y, dist p ↑y
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle x y = ↑π ↔ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)

Tactic:
by
  rw [← o.oangle_eq_zero_iff_sameRay]
  constructor
  · intro h
    by_cases hx : x = 0; · simp [hx, Real.Angle.pi_ne_zero.symm] at h
    by_cases hy : y = 0; · simp [hy, Real.Angle.pi_ne_zero.symm] at h
    refine ⟨hx, hy, ?_⟩
    rw [o.oangle_neg_right hx hy, h, Real.Angle.coe_pi_add_coe_pi]
  · rintro ⟨hx, hy, h⟩
    rwa [o.oangle_neg_right hx hy, ← Real.Angle.sub_coe_pi_eq_add_coe_pi, sub_eq_zero] at h

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle x y = 0 ∨ o.oangle x y = ↑π ↔ ¬LinearIndependent ℝ ![x, y]

Tactic:
exact oangle_eq_zero_or_eq_pi_iff_not_linearIndependent o

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ = r • (p₁ -ᵥ p₂) +ᵥ p₂
⊢ 1 / (1 - r) * -r + 1 / (1 - r) = 1

Tactic:
field [(sub_pos.2 (hr.trans zero_lt_one)).ne.symm]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

Tactic:
by_cases hxy : ‖x + y‖ = 0

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
hxy : ‖x + y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
hxy : ¬‖x + y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ ‖y‖ / (o.oangle x (x + y)).tan = ‖x‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    InnerProductGeometry.norm_div_tan_angle_add_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inr (o.right_ne_zero_of_oangle_eq_pi_div_two h))]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ ↑(InnerProductGeometry.angle y (y - x)) = ↑(Real.arccos (‖y‖ / ‖y - x‖))

Tactic:
InnerProductGeometry.angle_sub_eq_arccos_of_inner_eq_zero
      (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ ↑(Real.arccos (‖y‖ / ‖y - x‖)) = ↑(Real.arccos (‖y‖ / ‖y - x‖))
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).cos = ‖y‖ / ‖y - x‖

Tactic:
by
  have hs : (o.oangle y (y - x)).sign = 1 := by
    rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]
  rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    InnerProductGeometry.cos_angle_sub_of_inner_eq_zero
      (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ ‖x‖ / (o.oangle y (y - x)).sin = ‖y - x‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    InnerProductGeometry.norm_div_sin_angle_sub_of_inner_eq_zero
      (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inr (o.left_ne_zero_of_oangle_eq_pi_div_two h))]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (o.oangle x (x + y)).sign = (o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_smul_add_right x y 1, one_smul]

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

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
v : V
p q : P
h : ¬v = 0
⊢ ‖NormedSpace.normalize v‖ * ‖q -ᵥ p‖ ≤ dist p q

Tactic:
simp [norm_normalize h, dist_eq_norm_vsub']

Goal state after:
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₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ {p₅, p₁, p₂}
s : Set (P × P × P) := (fun x ↦ (↑x.1, p₅, x.2 +ᵥ ↑x.1)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p ↦ ∡ p.1 p.2.1 p.2.2) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : q ∈ line[ℝ, p₁, p₂]
⊢ r • (p₂ -ᵥ p₁) +ᵥ q ∈ line[ℝ, p₁, p₂]

Tactic:
refine vadd_mem_of_mem_direction ?_ hq
        rw [direction_affineSpan]
        exact smul_vsub_rev_mem_vectorSpan_pair _ _ _

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

Tactic:
← vsub_sub_vsub_cancel_right _ _ 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
c p₁ p₂ : P
⊢ ⟪c -ᵥ p₁ - (midpoint ℝ p₁ p₂ -ᵥ p₁), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = dist p₁ p₂ ^ 2 / 2
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p ↦ (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign

Tactic:
have hc : IsConnected sp :=
    (isConnected_setOfPred_sSameSide hp₃p₄.2.1 hp₃p₄.nonempty).image _ (by fun_prop)

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun p ↦ (p₁, p, p₂)) '' {p | s.SSameSide p₃ p}
hc : IsConnected sp
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝¹ : MetricSpace E
inst✝ : MetricSpace F
f : E → F
hf : Isometry f
ps : Set E
hps : Cospherical ps
⊢ Cospherical (f '' ps)

Tactic:
by
  rcases hps with ⟨c, r, hc⟩
  refine ⟨f c, r, ?_⟩
  rintro _ ⟨p, hp, rfl⟩
  rw [hf.dist_eq, hc p hp]

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : Nontrivial V
s : Sphere P
⊢ (Metric.sphere s.center s.radius).Nonempty ↔ 0 ≤ s.radius

Tactic:
refine ⟨fun ⟨p, hp⟩ ↦ radius_nonneg_of_mem hp, fun h ↦ ?_⟩

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : Nontrivial V
s : Sphere P
h : 0 ≤ s.radius
⊢ (Metric.sphere s.center s.radius).Nonempty
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ dist p₁ p₂ = 2 * s.radius

Tactic:
rw [← mem_sphere.1 h.left_mem, ← h.midpoint_eq_center, dist_left_midpoint]

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ dist p₁ p₂ = 2 * (‖2‖⁻¹ * dist p₁ p₂)
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
h₂ : p₁ ≠ p₂
h₃ : p₁ ≠ p₃
h : 2 • ∡ p₂ p₁ p = 2 • ∡ p p₁ p₃
⊢ dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)

Tactic:
by
  by_cases h' : orthogonalProjection line[ℝ, p₁, p₂] p = p₁ ∨
      orthogonalProjection line[ℝ, p₁, p₃] p = p₁
  · exact dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq_aux₂ h₂ h₃ h h'
  · rw [not_or] at h'
    refine dist_orthogonalProjection_eq_of_two_zsmul_oangle_eq
      (left_mem_affineSpan_pair _ _ _) (left_mem_affineSpan_pair _ _ _) h'.1 h'.2 ?_
    rw [(collinear_insert_of_mem_affineSpan_pair
          (orthogonalProjection_mem p)).two_zsmul_oangle_eq_left h'.1 h₂.symm,
      (collinear_insert_of_mem_affineSpan_pair
        (orthogonalProjection_mem p)).two_zsmul_oangle_eq_right h'.2 h₃.symm, h]

Goal state after:
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
s : Sphere P
as : AffineSubspace ℝ P
p : P
h : s.IsTangentAt p as
⊢ s.radius ≤ Metric.infDist s.center ↑as

Tactic:
Metric.infDist_eq_iInf

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
as : AffineSubspace ℝ P
p : P
h : s.IsTangentAt p as
⊢ s.radius ≤ ⨅ y, dist s.center ↑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
i : Fin (n + 1)
⊢ (s.height i)⁻¹ +
      (∑ x,
          ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ / (s.height i * s.height x) *
            (s.height x)⁻¹ -
        dist (s.points i) (s.altitudeFoot i) * dist (s.points i) (s.altitudeFoot i) / (s.height i * s.height i) *
          (s.height i)⁻¹) =
    0

Tactic:
simp only [height, ne_eq, mul_eq_zero, dist_eq_zero, ne_altitudeFoot, or_self,
    not_false_eq_true, div_self, one_mul, add_sub_cancel]

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
i : Fin (n + 1)
⊢ ∑ x,
      ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ /
          (dist (s.points i) (s.altitudeFoot i) * dist (s.points x) (s.altitudeFoot x)) *
        (dist (s.points x) (s.altitudeFoot x))⁻¹ =
    0
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case e'_5.e'_3
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
⊢ p₁ -ᵥ p₃ = p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)

Tactic:
exact (vsub_sub_vsub_cancel_right p₁ p₃ p₂).symm

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

Goal state before:
pp: case e'_6.e'_3
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
⊢ p₁ -ᵥ p₃ = p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)

Tactic:
exact (vsub_sub_vsub_cancel_right p₁ p₃ p₂).symm

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
h :
  InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) =
    InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂))
hpi : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₃) ≠ π
⊢ ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖

Tactic:
exact norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi h hpi

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

Goal state before:
pp: case neg
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
h : Pairwise fun i₁ i₂ ↦ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
i₁ i₂ : ι
hi : ¬i₁ = i₂
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

Tactic:
· exact h hi

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

Goal state before:
pp: case neg
ι : 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₂ : ι
hi : ¬i₁ = i₂
⊢ edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)

Tactic:
· exact h hi

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
hn : ¬n = 0
⊢ ↑n ≠ 0

Tactic:
by simpa using hn

Goal state after: