mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∡ p₂ p₃ p₁ = ↑(Real.arcsin (dist p₁ p₂ / dist p₁ p₃))

Tactic:
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
  rw [oangle_eq_angle_of_sign_eq_one hs,
    angle_eq_arcsin_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (left_ne_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
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₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).cos = dist p₁ p₂ / dist p₁ p₃

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe,
    cos_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h),
    dist_comm p₁ p₃]

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

Goal state before:
pp: case neg.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
hr : ∃ r, 0 ≤ r ∧ r • y = x - y
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
rcases hr with ⟨r, hr0, hr⟩

Goal state after:
case neg.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hy : y ≠ 0
r : ℝ
hr0 : 0 ≤ r
hr : r • y = x - y
⊢ |(o.oangle (y - x) y).toReal| < π / 2
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
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
h : ∡ (↑((orthogonalProjection s₁) p)) p' p = ∡ p p' ↑((orthogonalProjection s₂) p)
⊢ dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)

Tactic:
dist_orthogonalProjection_eq_iff_angle_eq hp'₁ hp'₂,

Goal state after:
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
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
h : ∡ (↑((orthogonalProjection s₁) p)) p' p = ∡ p p' ↑((orthogonalProjection s₂) p)
⊢ ∠ p p' ↑((orthogonalProjection s₁) p) = ∠ p p' ↑((orthogonalProjection s₂) p)
Module: Mathlib.Geometry.Euclidean.Basic

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₁ p₂ : P
hv : v ≠ 0
r : ℝ
⊢ dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫

Tactic:
conv_lhs =>
    rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_smul_vadd_sq, mul_assoc,
      ← sub_eq_zero, add_sub_assoc, dist_eq_norm_vsub V p₁ p₂, ← real_inner_self_eq_norm_mul_norm,
      sub_self]
  have hvi : ⟪v, v⟫ ≠ 0 := by simpa using hv
  have hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫) := by
    rw [discrim]
    ring
  rw [quadratic_eq_zero_iff hvi hd, neg_add_cancel, zero_div, neg_mul_eq_neg_mul, ←
    mul_sub_right_distrib, sub_eq_add_neg, ← mul_two, mul_assoc, mul_div_assoc, mul_div_mul_left,
    mul_div_assoc]
  simp

Goal state after:
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
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
hc : ¬Collinear ℝ {p', ↑((orthogonalProjection s₁) p), ↑((orthogonalProjection s₂) p)}
⊢ ∡ (↑((orthogonalProjection s₁) p)) p' p = ∡ p p' ↑((orthogonalProjection s₂) p)

Tactic:
dist_orthogonalProjection_eq_iff_angle_eq hp'₁ hp'₂,

Goal state after:
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
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : ∠ p p' ↑((orthogonalProjection s₁) p) = ∠ p p' ↑((orthogonalProjection s₂) p)
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
hc : ¬Collinear ℝ {p', ↑((orthogonalProjection s₁) p), ↑((orthogonalProjection s₂) p)}
⊢ ∡ (↑((orthogonalProjection s₁) p)) p' p = ∡ p p' ↑((orthogonalProjection s₂) p)
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
c : E
r : ℝ
hc : ∀ p ∈ ps, dist p c = r
⊢ Cospherical (f '' ps)

Tactic:
refine ⟨f c, r, ?_⟩

Goal state after:
E : Type u_3
F : Type u_4
inst✝¹ : MetricSpace E
inst✝ : MetricSpace F
f : E → F
hf : Isometry f
ps : Set E
c : E
r : ℝ
hc : ∀ p ∈ ps, dist p c = r
⊢ ∀ p ∈ f '' ps, dist p (f c) = r
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₃ : P
h₁₂ : s.IsDiameter p₁ p₂
h₁₃ : s.IsDiameter p₁ p₃
⊢ p₂ = p₃

Tactic:
← h₁₂.pointReflection_center_left,

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₃ : P
h₁₂ : s.IsDiameter p₁ p₂
h₁₃ : s.IsDiameter p₁ p₃
⊢ (Equiv.pointReflection s.center) p₁ = p₃
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
as : AffineSubspace ℝ P
h : s.IsTangent as
p : P
hp : dist p s.center < s.radius
⊢ p ∉ as

Tactic:
contrapose! hp
  exact h.radius_le_dist_center hp

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
⊢ q ∈ s ∧ dist q s.center ^ 2 = dist p s.center ^ 2 + dist q p ^ 2 ↔
    0 ≤ s.radius ∧
      dist q p ^ 2 = s.radius ^ 2 - dist p s.center ^ 2 ∧ dist q s.center ^ 2 = dist p s.center ^ 2 + dist q p ^ 2

Tactic:
← and_assoc,

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 q : P
⊢ q ∈ s ∧ dist q s.center ^ 2 = dist p s.center ^ 2 + dist q p ^ 2 ↔
    (0 ≤ s.radius ∧ dist q p ^ 2 = s.radius ^ 2 - dist p s.center ^ 2) ∧
      dist q s.center ^ 2 = dist p s.center ^ 2 + dist q p ^ 2
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

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₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ s.center ∈ line[ℝ, p₁, p₂] ↔ s.IsDiameter p₁ p₂

Tactic:
rcases eq_or_ne p₁ p₂ with rfl | hp₁p₂

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
s : Sphere P
p₁ : P
hp₁ hp₂ : p₁ ∈ s
⊢ s.center ∈ line[ℝ, p₁, p₁] ↔ s.IsDiameter p₁ p₁

case 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₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
⊢ s.center ∈ line[ℝ, p₁, p₂] ↔ s.IsDiameter p₁ p₂
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
hr' : |r| = 1
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)

Tactic:
rcases eq_or_eq_neg_of_abs_eq hr' with rfl | rfl

Goal state after:
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
s : Sphere P
p : P
hp : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr : q -ᵥ s.center = 1 • (p -ᵥ s.center)
hr0 : 1 ≠ 0
hr' : |1| = 1
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)

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
s : Sphere P
p : P
hp : p ∈ s
q : P
hqs : q ∈ s
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr : q -ᵥ s.center = -1 • (p -ᵥ s.center)
hr0 : -1 ≠ 0
hr' : |(-1)| = 1
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

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

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

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

Goal state before:
pp: case e'_3
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)
hi : i ≠ 0
⊢ 0 =
    (s.height 0)⁻¹ ^ 2 * -⟪s.points 0 -ᵥ s.points i, s.points 0 -ᵥ s.altitudeFoot 0⟫ +
      (s.height i)⁻¹ ^ 2 * s.height i ^ 2

Tactic:
inner_vsub_vsub_altitudeFoot_eq_height_sq _ hi.symm,

Goal state after:
case e'_3
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)
hi : i ≠ 0
⊢ 0 = (s.height 0)⁻¹ ^ 2 * -s.height 0 ^ 2 + (s.height i)⁻¹ ^ 2 * s.height i ^ 2
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
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₂
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)⁻¹
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)
⊢ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ

Tactic:
mul_eq_mul_left_iff

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₂
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)⁻¹
hi :
  ∀ (i : Fin (n + 1)),
    -SignType.sign (s.excenterWeightsUnnorm signs₁ i) = SignType.sign (s.excenterWeightsUnnorm signs₂ i) ∨
      SignType.sign (∑ i, s.excenterWeightsUnnorm signs₂ i)⁻¹ = 0
⊢ signs₁ = signs₂ ∨ signs₁ = signs₂ᶜ
Module: Mathlib.Geometry.Euclidean.Triangle

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
h : 2 • o.oangle x (x - y) = 2 • o.oangle (y - x) y
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ ↑π
⊢ ‖x‖ = ‖y‖

Tactic:
have hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign := by simp

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : 2 • o.oangle x (x - y) = 2 • o.oangle (y - x) y
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ ↑π
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
⊢ ‖x‖ = ‖y‖
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 : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0
H2 : (1 - ⟪y, x⟫ * ⟪x, y⟫) ^ 2 + ‖x - ⟪y, x⟫ • y‖ ^ 2 * ⟪x, y⟫ ^ 2 = ‖x - ⟪y, x⟫ • y‖ ^ 2
⊢ (1 - ⟪y, x⟫ * ⟪x, y⟫) ^ 2 + ‖x - ⟪y, x⟫ • y‖ ^ 2 * ⟪x, y⟫ ^ 2 = ‖x - ⟪y, x⟫ • y‖ ^ 2

Tactic:
exact H2

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

Tactic:
by
  rw [← inner_ortho_right_eq_sin_angle hx hy, ← inner_eq_cos_angle_of_norm_eq_one hx hy,
    ortho_eq_sub_inner _ hy]
  by_cases hxy : x - ⟪x, y⟫ • y = 0
  · simp [hxy, real_inner_comm, ← sub_eq_zero]
  rw [NormedSpace.normalize, real_inner_smul_right, inner_sub_right, real_inner_smul_right,
    real_inner_self_eq_norm_sq, hx, real_inner_comm y, ← sq, mul_smul, ← smul_assoc]
  simp only [one_pow, smul_eq_mul]
  have H : 1 - ⟪x, y⟫ ^ 2 ≠ 0 := by
    rw [sub_ne_zero, ne_comm, sq_ne_one_iff]
    constructor <;> contrapose hxy
    · rw [inner_eq_one_iff_of_norm_eq_one hx hy] at hxy
      simp [hy, hxy]
    · rw [inner_eq_neg_one_iff_of_norm_eq_one hx hy] at hxy
      simp [hy, hxy]
  rw [← smul_assoc, smul_eq_mul]
  field_simp
  rw [← real_inner_self_eq_norm_sq]
  have H0 : ⟪x - ⟪x, y⟫ • y, x - ⟪x, y⟫ • y⟫ = 1 - ⟪x, y⟫ ^ 2 := by
    rw [inner_sub_left, inner_sub_right, inner_sub_right, inner_self_eq_one_of_norm_eq_one hx,
      real_inner_smul_right, ← sq, real_inner_smul_left, real_inner_smul_left,
      real_inner_smul_right, inner_self_eq_one_of_norm_eq_one hy, real_inner_comm y x]
    ring
  rw [real_inner_comm x, H0]
  simp [H]

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
⊢ sx₁.circumradius = sx₂.circumradius

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
⊢ sx₁.circumradius = sx₂.circumradius

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r
⊢ sx₁.circumcenter = sx₂.circumcenter

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r
⊢ sx₁.circumcenter = sx₂.circumcenter

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : Sphere P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r
⊢ sx₁.circumsphere = sx₂.circumsphere

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : Sphere P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r
⊢ sx₁.circumsphere = sx₂.circumsphere

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]

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
a b c d p : P
h : Cospherical {a, b, c, d}
hapb : p ∈ line[ℝ, a, b]
hcpd : p ∈ line[ℝ, c, d]
q : P
r : ℝ
h' : ∀ p ∈ {a, b, c, d}, dist p q = r
ha : dist a q = r
hb : dist b q = r
hc : dist c q = dist d q
hd : dist d q = r
⊢ dist a p * dist b p = dist c p * dist d p

Tactic:
rw [← hb] at ha

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 c d p : P
h : Cospherical {a, b, c, d}
hapb : p ∈ line[ℝ, a, b]
hcpd : p ∈ line[ℝ, c, d]
q : P
r : ℝ
h' : ∀ p ∈ {a, b, c, d}, dist p q = r
ha : dist a q = dist b q
hb : dist b q = r
hc : dist c q = dist d q
hd : dist d q = r
⊢ dist a p * dist b p = dist c p * dist d p
Module: Mathlib.Geometry.Euclidean.Similarity

Goal state before:
pp: case h
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
h_not_col : ¬Collinear ℝ {a, b, c}
h_not_col' : ¬Collinear ℝ {a', b', c'}
h : ∠ a b c = ∠ a' b' c'
dist_a'b' : dist a' b' ≠ 0
dist_b'c' : dist b' c' ≠ 0
k : ℝ := ⋯
hd : k = dist b c / dist b' c'
hk : k = dist a b / dist a' b'
k_pos : 0 < k
h_ab : dist a b = k * dist a' b'
h_bc : dist b c = k * dist b' c'
hcos : dist c a = k * dist c' a'
hcos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
dist_ac_pos : 0 < dist a c
k_dist_a'c' : 0 ≤ k * dist a' c'
⊢ 0 < k ∧ Pairwise fun i₁ i₂ ↦ dist (![a, b, c] i₁) (![a, b, c] i₂) = k * dist (![a', b', c'] i₁) (![a', b', c'] i₂)

Tactic:
refine ⟨k_pos, ?_⟩

Goal state after:
case h
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
h_not_col : ¬Collinear ℝ {a, b, c}
h_not_col' : ¬Collinear ℝ {a', b', c'}
h : ∠ a b c = ∠ a' b' c'
dist_a'b' : dist a' b' ≠ 0
dist_b'c' : dist b' c' ≠ 0
k : ℝ := dist a b / dist a' b'
hd : k = dist b c / dist b' c'
hk : k = dist a b / dist a' b'
k_pos : 0 < k
h_ab : dist a b = k * dist a' b'
h_bc : dist b c = k * dist b' c'
hcos : dist c a = k * dist c' a'
hcos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
dist_ac_pos : 0 < dist a c
k_dist_a'c' : 0 ≤ k * dist a' c'
⊢ Pairwise fun i₁ i₂ ↦ dist (![a, b, c] i₁) (![a, b, c] i₂) = k * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
Module: Mathlib.Geometry.Group.Growth.LinearLowerBound

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hXclosure : (↑(closure ↑X)).Infinite
⊢ StrictMono fun n ↦ X ^ n

Tactic:
obtain rfl | hX := eq_singleton_or_nontrivial hX₁

Goal state after:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
hX₁ : 1 ∈ {1}
hXclosure : (↑(closure ↑{1})).Infinite
⊢ StrictMono fun n ↦ {1} ^ n

case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hXclosure : (↑(closure ↑X)).Infinite
hX : X.Nontrivial
⊢ StrictMono fun n ↦ X ^ n