mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Basic

Goal state before:
pp: case refine_1.«0»
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 : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
⊢ b ((fun i ↦ i) ⟨0, ⋯⟩) ∈ ↑s.direction

pp: case refine_1.«1»
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 : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
⊢ b ((fun i ↦ i) ⟨1, ⋯⟩) ∈ ↑s.direction

Tactic:
· exact vsub_mem_direction hc₂s hc₁s

Goal state after:
case refine_1.«1»
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 : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
⊢ b ((fun i ↦ i) ⟨1, ⋯⟩) ∈ ↑s.direction
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: case mp
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
h : Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)
h' : ∀ (q' : P), q' ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) ↔ q' = q
hr : 0 ≤ s.radius
⊢ q = p ∧ dist p s.center = s.radius

Tactic:
simp_rw [mem_inter_orthRadius_iff_vsub_mem_and_norm_sq hr] at h'

Goal state after:
case mp
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
h : Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)
hr : 0 ≤ s.radius
h' : ∀ (q' : P), q' -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖q' -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2 ↔ q' = q
⊢ q = p ∧ dist p s.center = s.radius
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
pp: case inl
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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃) + ↑π
hs : excenter t signs = incenter t
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}

Tactic:
rw [hs, t.oangle_incenter_eq h₁₂ h₁₃ h₂₃] at h

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h : ∡ (incenter t) (t.points i₁) (t.points i₃) = ∡ (incenter t) (t.points i₁) (t.points i₃) + ↑π
hs : excenter t signs = incenter t
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

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 z : V
hxzne : x ≠ z
hxz : ‖x‖ = ‖z‖
hxyne : x ≠ 0
hxy : ‖x‖ = ‖0‖
⊢ False

Tactic:
norm_zero,

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x z : V
hxzne : x ≠ z
hxz : ‖x‖ = ‖z‖
hxyne : x ≠ 0
hxy : ‖x‖ = 0
⊢ False
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p q : P
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
hq_mem : q ∈ as
h1 : InnerProductGeometry.angle (q -ᵥ p) (p -ᵥ s.center) = π / 2
⊢ InnerProductGeometry.angle (q -ᵥ p) (-(p -ᵥ s.center)) = π / 2

Tactic:
angle_neg_right,

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
as : AffineSubspace ℝ P
h : s.IsTangentAt p as
hq_mem : q ∈ as
h1 : InnerProductGeometry.angle (q -ᵥ p) (p -ᵥ s.center) = π / 2
⊢ π - InnerProductGeometry.angle (q -ᵥ p) (p -ᵥ s.center) = π / 2
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
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (s.reindex e).inradius = s.inradius

Tactic:
simp_rw [inradius, exsphere_reindex]
  simp

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

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖0‖ - ‖y‖ = ⟪0, y⟫ * (‖0‖⁻¹ - ‖y‖⁻¹)
hx0 : x = 0
⊢ ‖x‖ = ‖y‖

Tactic:
norm_zero,

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : 0 - ‖y‖ = ⟪0, y⟫ * (0⁻¹ - ‖y‖⁻¹)
hx0 : x = 0
⊢ ‖x‖ = ‖y‖
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖y‖ = 0
hx0 : x = 0
⊢ ‖0‖ = ‖y‖

Tactic:
norm_zero,

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖y‖ = 0
hx0 : x = 0
⊢ 0 = ‖y‖
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖0‖ = ⟪x, 0⟫ * (‖x‖⁻¹ - ‖0‖⁻¹)
hx0 : ¬x = 0
hy0 : y = 0
⊢ ‖x‖ = ‖y‖

Tactic:
norm_zero,

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - 0 = ⟪x, 0⟫ * (‖x‖⁻¹ - 0⁻¹)
hx0 : ¬x = 0
hy0 : y = 0
⊢ ‖x‖ = ‖y‖
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ = 0
hx0 : ¬x = 0
hy0 : y = 0
⊢ ‖x‖ = ‖0‖

Tactic:
norm_zero,

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ = 0
hx0 : ¬x = 0
hy0 : y = 0
⊢ ‖x‖ = 0
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

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)
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁ : t₁.points i₁ = t₂.points i₁
h₃ : t₁.points i₃ = t₂.points i₃
h₂ : 2 • ∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃) = 2 • ∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)
⊢ Simplex.circumsphere t₁ = Simplex.circumsphere t₂

Tactic:
rw [t₁.circumsphere_eq_of_dist_of_oangle h₁₂ h₁₃ h₂₃,
    t₂.circumsphere_eq_of_dist_of_oangle h₁₂ h₁₃ h₂₃,
    Real.Angle.tan_eq_of_two_zsmul_eq h₂, Real.Angle.abs_sin_eq_of_two_zsmul_eq h₂, h₁, h₃]

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (-(p₁ -ᵥ p₂)))

Tactic:
angle_neg_right,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
    Real.sin (π - InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂))
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case e'_2
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₂ p₃ p₁
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ dist p₁ p₂ = ‖p₂ -ᵥ p₁‖

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
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₂ p₃ p₁
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ dist p₁ p₃ = ‖p₃ -ᵥ p₁‖

pp: V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₂ p₃ p₁
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ 2 • o.oangle (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) = 2 • o.oangle (p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) (p₂ -ᵥ p₁)

Tactic:
· rw [dist_eq_norm_vsub']

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
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₂ p₃ p₁
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ dist p₁ p₃ = ‖p₃ -ᵥ p₁‖

V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₂ p₃ p₁
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ 2 • o.oangle (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) = 2 • o.oangle (p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) (p₂ -ᵥ p₁)
Module: Mathlib.Geometry.Euclidean.Triangle

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
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₂ p₃ p₁
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ dist p₁ p₃ = ‖p₃ -ᵥ p₁‖

pp: V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₂ p₃ p₁
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ 2 • o.oangle (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) = 2 • o.oangle (p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) (p₂ -ᵥ p₁)

Tactic:
· rw [dist_eq_norm_vsub']

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✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h : 2 • ∡ p₁ p₂ p₃ = 2 • ∡ p₂ p₃ p₁
h0 : ∡ p₃ p₁ p₂ ≠ 0
hpi : ∡ p₃ p₁ p₂ ≠ ↑π
⊢ 2 • o.oangle (p₃ -ᵥ p₁) (p₃ -ᵥ p₁ - (p₂ -ᵥ p₁)) = 2 • o.oangle (p₂ -ᵥ p₁ - (p₃ -ᵥ p₁)) (p₂ -ᵥ p₁)
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ ∀ (x : Fin (n + 1)), ¬(x ∈ univ ∧ (pointIndexEmbedding n) x = circumcenterIndex)

Tactic:
rintro x ⟨_, h⟩

Goal state after:
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h✝ : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
x : Fin (n + 1)
left✝ : x ∈ univ
h : (pointIndexEmbedding n) x = circumcenterIndex
⊢ False
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case h
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
c : P
hc✝ : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
hsx : affineSpan ℝ (Set.range sx.points) = s
hc : c ∈ affineSpan ℝ (Set.range sx.points)
⊢ sx.circumradius = r

Tactic:
exact
    (sx.eq_circumradius_of_dist_eq hc fun i =>
        hcr (sx.points i) (hsxps (Set.mem_range_self i))).symm

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

Tactic:
grind [angle_le_pi, angle_nonneg]

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‖ = 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
H4 : ¬angle x y = π
H5 : angle y z = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
grind [angle_le_pi, angle_nonneg]

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

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : r ∈ Set.Icc 0 1
t : ℝ
ht : t ∈ Set.Icc 0 1
⊢ (s.signedInfDist j) ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) t) ≠ 0

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : r ∈ Set.Icc 0 1
t : ℝ
ht : t ∈ Set.Icc 0 1
⊢ Continuous ⇑(AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i))

Tactic:
· intro h0
      rw [← abs_eq_zero, abs_signedInfDist_eq_dist_of_mem_affineSpan_range] at h0
      · rw [orthogonalProjectionSpan, dist_orthogonalProjection_eq_zero_iff] at h0
        by_cases ht1 : t = 1
        · subst ht1
          rw [AffineMap.lineMap_apply_one] at h0
          exact h.touchpoint_notMem_affineSpan_of_ne hne h0
        · refine (h.isTangentAt_touchpoint j).isTangent.notMem_of_dist_lt ?_ h0
          simp only [exsphere_center, dist_lineMap_left, Real.norm_eq_abs, h.dist_excenter,
            exsphere_radius, h.exradius_pos, mul_lt_iff_lt_one_left]
          rw [abs_lt]
          rcases ht with ⟨ht0, ht1'⟩
          exact ⟨by linarith, ht1'.lt_of_ne ht1⟩
      · exact AffineMap.lineMap_mem _ h.excenter_mem_affineSpan_range
          (s.touchpoint_mem_affineSpan_simplex _ _)

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : r ∈ Set.Icc 0 1
t : ℝ
ht : t ∈ Set.Icc 0 1
⊢ Continuous ⇑(AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i))
Module: Mathlib.Geometry.Euclidean.Inversion.Calculus

Goal state before:
pp: case refine_2.refine_1
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x ↦ c + x) x ≠ c
this :
  HasFDerivAt (inversion c R)
    ((R ^ 2 * ((fun y ↦ y⁻¹) ∘ fun x ↦ ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
      (R ^ 2 •
            -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
              2 • (innerSL ℝ) (_root_.id (c + x) - c) ∘SL ContinuousLinearMap.id ℝ F).smulRight
        (_root_.id (c + x) - c))
    (c + x)
⊢ EqOn
    ⇑↑((R ^ 2 * ((fun y ↦ y⁻¹) ∘ fun x ↦ ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
          (R ^ 2 •
                -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
                  2 • (innerSL ℝ) (_root_.id (c + x) - c) ∘SL ContinuousLinearMap.id ℝ F).smulRight
            (_root_.id (c + x) - c))
    ⇑↑((R / dist ((fun x ↦ c + x) x) c) ^ 2 • ↑↑(ℝ ∙ ((fun x ↦ c + x) x - c))ᗮ.reflection) {x}

pp: case refine_2.refine_2
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x ↦ c + x) x ≠ c
this :
  HasFDerivAt (inversion c R)
    ((R ^ 2 * ((fun y ↦ y⁻¹) ∘ fun x ↦ ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
      (R ^ 2 •
            -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
              2 • (innerSL ℝ) (_root_.id (c + x) - c) ∘SL ContinuousLinearMap.id ℝ F).smulRight
        (_root_.id (c + x) - c))
    (c + x)
y : F
hy : y ∈ ↑(ℝ ∙ x)ᗮ
⊢ ((R ^ 2 * ((fun y ↦ y⁻¹) ∘ fun x ↦ ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
        (R ^ 2 •
              -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
                2 • (innerSL ℝ) (_root_.id (c + x) - c) ∘SL ContinuousLinearMap.id ℝ F).smulRight
          (_root_.id (c + x) - c))
      y =
    ((R / dist ((fun x ↦ c + x) x) c) ^ 2 • ↑↑(ℝ ∙ ((fun x ↦ c + x) x - c))ᗮ.reflection) y

Tactic:
· have : ((‖x‖ ^ 2) ^ 2)⁻¹ * (‖x‖ ^ 2) = (‖x‖ ^ 2)⁻¹ := by
      rw [← div_eq_inv_mul, sq (‖x‖ ^ 2), div_self_mul_self']
    simp [Submodule.reflection_orthogonalComplement_singleton_eq_neg,
      two_mul, this, div_eq_mul_inv, mul_add, add_smul, mul_pow]

Goal state after:
case refine_2.refine_2
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x ↦ c + x) x ≠ c
this :
  HasFDerivAt (inversion c R)
    ((R ^ 2 * ((fun y ↦ y⁻¹) ∘ fun x ↦ ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
      (R ^ 2 •
            -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
              2 • (innerSL ℝ) (_root_.id (c + x) - c) ∘SL ContinuousLinearMap.id ℝ F).smulRight
        (_root_.id (c + x) - c))
    (c + x)
y : F
hy : y ∈ ↑(ℝ ∙ x)ᗮ
⊢ ((R ^ 2 * ((fun y ↦ y⁻¹) ∘ fun x ↦ ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
        (R ^ 2 •
              -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
                2 • (innerSL ℝ) (_root_.id (c + x) - c) ∘SL ContinuousLinearMap.id ℝ F).smulRight
          (_root_.id (c + x) - c))
      y =
    ((R / dist ((fun x ↦ c + x) x) c) ^ 2 • ↑↑(ℝ ∙ ((fun x ↦ c + x) x - c))ᗮ.reflection) y
Module: Mathlib.Geometry.Euclidean.NinePointCircle

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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : ↑(n - 1) = ↑n - 1
⊢ ⅟2 • (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      ⅟2 •
        (((↑n)⁻¹ • (s.points i -ᵥ ((↑(n + 1) / ↑(n - 1)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)) +ᵥ
            (↑(n + 1) / ↑(n - 1)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) -ᵥ
          s.circumcenter) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)

Tactic:
vadd_vadd,

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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : ↑(n - 1) = ↑n - 1
⊢ ⅟2 • (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      ⅟2 •
        ((((↑n)⁻¹ • (s.points i -ᵥ ((↑(n + 1) / ↑(n - 1)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)) +
              (↑(n + 1) / ↑(n - 1)) • (s.centroid -ᵥ s.circumcenter)) +ᵥ
            s.circumcenter) -ᵥ
          s.circumcenter) =
    ((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter)
Module: Mathlib.Geometry.Euclidean.Similarity

Goal state before:
pp: 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₁ : ∠ a b c = ∠ a' b' c'
h₂ : ∠ b c a = ∠ b' c' a'
⊢ ![a, b, c] ∼ ![a', b', c']

Tactic:
by
  have hne_pi_div_two : ∠ a b c ≠ Real.pi / 2 ∨ ∠ b c a ≠ Real.pi / 2 := by
    by_contra! hq
    have := angle_lt_pi_div_two_of_angle_eq_pi_div_two hq.1 (ne₂₃_of_not_collinear h_not_col).symm
    grind
  have not_all_eq : a' ≠ b' ∨ b' ≠ c' ∨ a' ≠ c' := by grind [angle_self_left]
  have h_not_col' : ¬ Collinear ℝ {a', b', c'} := by
    grind only [collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, angle_self_right,
      angle_self_left, Set.insert_comm, Set.pair_comm]
  have h_pos1 : 0 < dist a b := by simp [dist_pos, ne₁₂_of_not_collinear h_not_col]
  have h_pos1' : 0 < dist a' b' := by simp [dist_pos, ne₁₂_of_not_collinear h_not_col']
  have h_pos2 : 0 < dist b c := by simp [dist_pos, ne₂₃_of_not_collinear h_not_col]
  have h_pos2' : 0 < dist b' c' := by simp [dist_pos, ne₂₃_of_not_collinear h_not_col']
  have h₃ : ∠ c a b = ∠ c' a' b' := by
    have hsum := angle_add_angle_add_angle_eq_pi c (ne₁₂_of_not_collinear h_not_col)
    have hsum' := angle_add_angle_add_angle_eq_pi c' (ne₁₂_of_not_collinear h_not_col')
    grind [angle_comm]
  have h_sin_ne1 : Real.sin (∠ b c a) ≠ 0 := by
    grind only [sin_ne_zero_of_not_collinear, Set.pair_comm, Set.insert_comm]
  have h_sin_ne2 : Real.sin (∠ c a b) ≠ 0 := by
    grind only [sin_ne_zero_of_not_collinear, Set.pair_comm, Set.insert_comm]
  have h_sin1 := law_sin c a b
  have h_sin1' := law_sin c' a' b'
  rw [← eq_div_iff_mul_eq (by positivity)] at h_sin1 h_sin1'
  rw [← h₃, ← h₂] at h_sin1'
  rw [h_sin1', mul_div_assoc, mul_div_assoc, mul_right_inj' h_sin_ne1,
    div_eq_div_iff (by positivity) (by positivity), mul_comm] at h_sin1
  have h_sin2 := law_sin a b c
  have h_sin2' := law_sin a' b' c'
  rw [← eq_div_iff_mul_eq (by positivity)] at h_sin2 h_sin2'
  rw [← h₁, ← h₃] at h_sin2'
  rw [h_sin2', mul_div_assoc, mul_div_assoc, mul_right_inj' h_sin_ne2,
    div_eq_div_iff (by positivity) (by positivity), mul_comm] at h_sin2
  apply Similar.reverse_of_three
  apply Similar.comm_left
  exact similar_of_side_side (by positivity) (by positivity) h_sin2 h_sin1.symm

Goal state after: