mathlib-initiative/mathlib-tactics huggingface dataset:
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
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
⊢ (orthogonalProjection s) (v +ᵥ p) = ⟨p, hp⟩

Tactic:
ext
  exact coe_orthogonalProjection_eq_iff_mem.mpr (by simp [*])

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

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ LinearMap.det ↑(o.rotation θ).toLinearEquiv = 1

Tactic:
rw [o.rotation_eq_matrix_toLin θ hx]

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ LinearMap.det
      ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx))
        !![θ.cos, -θ.sin; θ.sin, θ.cos]) =
    1
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

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
⊢ ⟪x, y⟫ = 0 ↔ x = 0 ∨ ∃ r, r • (o.rotation ↑(π / 2)) x = y

Tactic:
by
  by_cases! +distrib H : x = 0 ∨ y = 0
  · rcases H with (rfl | rfl) <;> simp
  simp only [← o.eq_zero_or_oangle_eq_iff_inner_eq_zero, H, ← neg_smul, false_or,
    o.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero H.1 H.2, ← o.neg_rotation_pi_div_two, smul_neg]
  constructor
  · grind
  · rintro ⟨r, rfl⟩
    rcases lt_trichotomy 0 r with (hr0 | rfl | hr0)
    · grind
    · simp_all
    · right
      use -r
      simp_all

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
r : ℝ
⊢ (o.oangle x (r • x - y)).sign = -(o.oangle x y).sign

Tactic:
rw [← oangle_sign_neg_right, sub_eq_add_neg, oangle_sign_smul_add_right]

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

Goal state before:
pp: case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ r₃ r₄ : ℝ
hr₁ : r₁ = 0
⊢ SignType.sign r₂ * (SignType.sign r₃ * -(o.oangle x y).sign) = -SignType.sign (r₂ * r₃) * (o.oangle x y).sign

Tactic:
sign_mul,

Goal state after:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ r₃ r₄ : ℝ
hr₁ : r₁ = 0
⊢ SignType.sign r₂ * (SignType.sign r₃ * -(o.oangle x y).sign) =
    -(SignType.sign r₂ * SignType.sign r₃) * (o.oangle x y).sign
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
a b c p : P
h_sbtw : Sbtw ℝ a b c
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c) t = b
ht0 : 0 < t
ht1 : t < 1
hb : b -ᵥ a = t • (c -ᵥ a)
hpc : ⟪p -ᵥ a, c -ᵥ a⟫ = 0
⊢ dist p b < dist p c

Tactic:
have h_sq_ineq : dist p b ^ 2 < dist p c ^ 2 := by
    rw [← hb_eq, dist_sq_lineMap_of_inner_eq_zero t hpc, dist_sq_of_inner_eq_zero hpc]
    have hv_pos : 0 < dist a c ^ 2 := sq_pos_of_pos (dist_pos.mpr h_sbtw.left_ne_right)
    have ht_sq_lt : t ^ 2 < 1 := sq_lt_one_iff₀ ht0.le |>.mpr ht1
    nlinarith [sq_nonneg (dist p a), sq_nonneg (dist a c)]

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c p : P
h_sbtw : Sbtw ℝ a b c
h_inner : ⟪p -ᵥ a, b -ᵥ a⟫ = 0
t : ℝ
hb_eq : (AffineMap.lineMap a c) t = b
ht0 : 0 < t
ht1 : t < 1
hb : b -ᵥ a = t • (c -ᵥ a)
hpc : ⟪p -ᵥ a, c -ᵥ a⟫ = 0
h_sq_ineq : dist p b ^ 2 < dist p c ^ 2
⊢ dist p b < dist p c
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 x : P
⊢ x ∈ s.orthRadius p ↔ ⟪p -ᵥ s.center, x -ᵥ p⟫ = 0

Tactic:
rw [mem_orthRadius_iff_inner_left, inner_eq_zero_symm]

Goal state after:
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
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = s.direction
hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₁ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
hp' : p₂ -ᵥ p₁ ≠ 0
hp₂ : dist (1 • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = r₁
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂

Tactic:
rw [← hp₁c₁, dist_smul_vadd_eq_dist _ _ hp'] at hpc₁ 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
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = s.direction
hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₁ : t₂ = 0 ∨ t₂ = -2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ c₁⟫ / ⟪p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
hp' : p₂ -ᵥ p₁ ≠ 0
hp₂ : 1 = 0 ∨ 1 = -2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ c₁⟫ / ⟪p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: case refine_1
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
x✝ : q ∈ s ∧ q ∈ as
hs : q ∈ s
has : q ∈ as
hd : dist q s.center ^ 2 = s.radius ^ 2 + dist q p ^ 2
⊢ q = p

Tactic:
hs

Goal state after:
case refine_1
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
x✝ : q ∈ s ∧ q ∈ as
hs : q ∈ s
has : q ∈ as
hd : s.radius ^ 2 = s.radius ^ 2 + dist q p ^ 2
⊢ q = p
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

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
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)
hp : ∡ (↑((orthogonalProjection line[ℝ, p₁, p₂]) p)) p₁ p = ∡ p p₁ ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
⊢ 2 • ∡ p₂ p₁ p = 2 • ∡ p p₁ p₃

Tactic:
have h₂₁ : p₂ ≠ p₁ := ha.injective.ne (by decide : (1 : Fin 3) ≠ 0)

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
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)
hp : ∡ (↑((orthogonalProjection line[ℝ, p₁, p₂]) p)) p₁ p = ∡ p p₁ ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
h₂₁ : p₂ ≠ p₁
⊢ 2 • ∡ p₂ p₁ p = 2 • ∡ p p₁ p₃
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case e'_2.e'_6.refine_1
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
j : Fin (n + 1)
hj : j ≠ i ∧ j ≠ 0
⊢ ∃ x ∈ {j}ᶜ, s.points x = s.points i

pp: case e'_2.e'_6.refine_2
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
j : Fin (n + 1)
hj : j ≠ i ∧ j ≠ 0
⊢ ∃ x ∈ {j}ᶜ, s.points x = s.points 0

Tactic:
· exact ⟨i, hj.1.symm, rfl⟩

Goal state after:
case e'_2.e'_6.refine_2
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
j : Fin (n + 1)
hj : j ≠ i ∧ j ≠ 0
⊢ ∃ x ∈ {j}ᶜ, s.points x = s.points 0
Module: Mathlib.Geometry.Euclidean.Incenter

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
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
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
⊢ s.excenter signs -ᵥ s.touchpoint signs i ∈ (vectorSpan ℝ (Set.range s.points))ᗮ

Tactic:
hu,

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
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
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
⊢ s.excenter signs -ᵥ s.touchpoint signs i ∈
    (vectorSpan ℝ (Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points))ᗮ
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]
  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.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 y + angle y z

Tactic:
rcases lt_or_ge π (angle x y + angle y z) with H | H
  · linarith [angle_le_pi x z]
  suffices Real.cos (angle x y + angle y z) ≤ Real.cos (angle x z) by
    have H0 : 0 ≤ angle x y + angle y z :=
      add_nonneg (angle_nonneg x y) (angle_nonneg y z)
    rwa [Real.strictAntiOn_cos.le_iff_ge ⟨H0, H⟩ ⟨angle_nonneg x z, angle_le_pi x z⟩] at this
  have H1 : ⟪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 H1
  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 H1
  simp only [one_pow, mul_one, mul_zero, add_zero, zero_add] at H1
  rw [mul_comm (Real.cos (angle y z))] at H1
  rw [Real.cos_add, ← inner_eq_cos_angle_of_norm_eq_one hx hz, H1]
  have H2 : -1 ≤ ⟪normalize (ortho y x), normalize (ortho y z)⟫ := by
    by_cases H3 : ortho y x = 0
    · simp [*]
    by_cases H4 : ortho y z = 0
    · simp [*]
    exact neg_one_le_real_inner_of_norm_eq_one
      (norm_normalize_eq_one_iff.mpr H3) (norm_normalize_eq_one_iff.mpr H4)
  have := sin_angle_nonneg x y; have := sin_angle_nonneg y z
  grw [← H2]
  apply le_of_eq
  ring

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

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : x = 0
⊢ angle x z ≤ angle x y + angle y z

Tactic:
simpa [hx] using angle_nonneg y z

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

Goal state before:
pp: ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
P₄ : Type u_6
v₁ : ι → P₁
v₂ : ι → P₂
inst✝⁷ : PseudoEMetricSpace P₁
inst✝⁶ : PseudoEMetricSpace P₂
inst✝⁵ : PseudoEMetricSpace P₃
inst✝⁴ : PseudoEMetricSpace P₄
F₁ : Type u_7
F₂ : Type u_8
inst✝³ : FunLike F₁ P₁ P₃
inst✝² : DilationClass F₁ P₁ P₃
inst✝¹ : FunLike F₂ P₂ P₄
inst✝ : DilationClass F₂ P₂ P₄
f₁ : F₁
f₂ : F₂
h : v₁ ≅ v₂
hf : Dilation.ratio f₁ = Dilation.ratio f₂
i j : ι
⊢ edist ((⇑f₁ ∘ v₁) i) ((⇑f₁ ∘ v₁) j) = edist ((⇑f₂ ∘ v₂) i) ((⇑f₂ ∘ v₂) j)

Tactic:
by simp [hf, h i j]

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
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter
r₁ r₂ : ℝ
hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)
hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)
hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
h : s.points 0 ∈ span_s
hd₁ :
  r₁ *
      (r₁ *
        ⟪p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p),
          p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)⟫) =
    r₂ *
      (r₂ *
        ⟪p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p),
          p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)⟫)
hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) p₂

Tactic:
←
    mul_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
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter
r₁ r₂ : ℝ
hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)
hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)
hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
h : s.points 0 ∈ span_s
hd₁ :
  r₁ * r₁ *
      ⟪p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p),
        p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)⟫ =
    r₂ *
      (r₂ *
        ⟪p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p),
          p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)⟫)
hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) p₂
Module: Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane

Goal state before:
pp: case inr
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
x : P
hx : x ≠ c
⊢ x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c ↑(perpBisector c (inversion c R y))

Tactic:
rw [mem_preimage, mem_sphere, ← inversion_mem_perpBisector_inversion_iff hR]

Goal state after:
case inr
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
x : P
hx : x ≠ c
⊢ inversion c R (inversion c R x) ∈ perpBisector c (inversion c R y) ↔ x ∈ insert c ↑(perpBisector c (inversion c R y))

case inr.hx
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
x : P
hx : x ≠ c
⊢ inversion c R x ≠ c

case inr.hy
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
x : P
hx : x ≠ c
⊢ y ≠ c
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✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ (∃ x,
      ∃ (hx : 0 ≤ x),
        0 < NNReal.mk x hx ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = ↑(NNReal.mk x hx) * dist (v₂ i₁) (v₂ i₂)) ↔
    ∃ r, 0 < r ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)

Tactic:
← NNReal.coe_pos,

Goal state after:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ (∃ x,
      ∃ (h : 0 ≤ x),
        0 < ↑(NNReal.mk x ⋯) ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = ↑(NNReal.mk x ⋯) * dist (v₂ i₁) (v₂ i₂)) ↔
    ∃ r, 0 < r ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)
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✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ (∃ x,
      ∃ (hx : 0 ≤ x),
        0 < NNReal.mk x hx ∧ Pairwise fun i₁ i₂ ↦ dist (v₁ i₁) (v₁ i₂) = ↑(NNReal.mk x hx) * dist (v₂ i₁) (v₂ i₂)) ↔
    ∃ r, 0 < r ∧ Pairwise fun i₁ i₂ ↦ dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)

Tactic:
← NNReal.coe_pos,

Goal state after:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ (∃ x,
      ∃ (h : 0 ≤ x),
        0 < ↑(NNReal.mk x ⋯) ∧ Pairwise fun i₁ i₂ ↦ dist (v₁ i₁) (v₁ i₂) = ↑(NNReal.mk x ⋯) * dist (v₂ i₁) (v₂ i₂)) ↔
    ∃ r, 0 < r ∧ Pairwise fun i₁ i₂ ↦ dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)
Module: Mathlib.Geometry.Euclidean.Simplex

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
⊢ Simplex.AcuteAngled t ↔
    ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
      ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2

Tactic:
refine ⟨fun h ↦ ⟨h _ _ _ (by decide) (by decide) (by decide),
                   h _ _ _ (by decide) (by decide) (by decide),
                   h _ _ _ (by decide) (by decide) (by decide)⟩,
          fun ⟨h012, h120, h201⟩ ↦ ?_⟩
  have h210 := angle_comm (t.points 0) _ _ ▸ h012
  have h021 := angle_comm (t.points 1) _ _ ▸ h120
  have h102 := angle_comm (t.points 2) _ _ ▸ h201
  intro i₁ i₂ i₃ h₁₂ h₁₃ h₂₃
  fin_cases i₁ <;> fin_cases i₂ <;> fin_cases i₃ <;> simp [*] at *

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₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (Submodule.span ℝ (⋃ i, {s.points i₁ -ᵥ s.points ↑i}))ᗮ
hu : ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x ↦ s.points i₁ -ᵥ x) '' s.points '' (Set.univ \ {i₁})
⊢ p -ᵥ s.mongePoint = 0

Tactic:
hu,

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 + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈ (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
hi : p -ᵥ s.mongePoint ∈ (Submodule.span ℝ ((fun x ↦ s.points i₁ -ᵥ x) '' s.points '' (Set.univ \ {i₁})))ᗮ
hu : ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x ↦ s.points i₁ -ᵥ x) '' s.points '' (Set.univ \ {i₁})
⊢ p -ᵥ s.mongePoint = 0
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
hu : Set.univ = {j₁, j₂, j₃}
⊢ t₂.points '' Set.univ ⊆ ↑(affineSpan ℝ (Set.range t₁.points))

Tactic:
hu,

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3
hi₁₂ : i₁ ≠ i₂
hi₁₃ : i₁ ≠ i₃
hi₂₃ : i₂ ≠ i₃
hj₁₂ : j₁ ≠ j₂
hj₁₃ : j₁ ≠ j₃
hj₂₃ : j₂ ≠ j₃
h₁ : t₂.points j₁ = t₁.orthocenter
h₂ : t₂.points j₂ = t₁.points i₂
h₃ : t₂.points j₃ = t₁.points i₃
hu : Set.univ = {j₁, j₂, j₃}
⊢ t₂.points '' {j₁, j₂, j₃} ⊆ ↑(affineSpan ℝ (Set.range t₁.points))