mathlib-initiative/mathlib-tactics huggingface dataset:
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
p p' : P
s₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h' : p ∉ s₁ ∧ p ∉ s₂
⊢ dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p) ↔
    Real.arcsin (dist p ↑((orthogonalProjection s₁) p) / dist p p') =
      Real.arcsin (dist p ↑((orthogonalProjection s₂) p) / dist p p')

Tactic:
· refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
    · rw [h]
    · have hp : p ≠ p' := by
        rintro rfl
        exact h'.1 hp'₁
      have hpd : 0 < dist p p' := dist_pos.2 hp
      rw [Real.arcsin_inj (le_trans (by norm_num : (-1 : ℝ) ≤ 0) (by positivity))
        ((div_le_one hpd).2 ?_)
        (le_trans (by norm_num : (-1 : ℝ) ≤ 0) (by positivity)) ((div_le_one hpd).2 ?_)] at h
      · rwa [div_left_inj' hpd.ne'] at h
      · rw [dist_orthogonalProjection_eq_infDist]
        exact Metric.infDist_le_dist_of_mem (SetLike.mem_coe.1 hp'₁)
      · rw [dist_orthogonalProjection_eq_infDist]
        exact Metric.infDist_le_dist_of_mem (SetLike.mem_coe.1 hp'₂)

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

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 q : P
⊢ |((signedDist v) p) q| = dist p q ↔ ∃ a, a • v = q -ᵥ p

Tactic:
signedDist_apply_apply,

Goal state after:
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
⊢ |⟪NormedSpace.normalize v, q -ᵥ p⟫| = dist p q ↔ ∃ a, a • v = q -ᵥ p
Module: Mathlib.Geometry.Euclidean.SignedDist

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 q : P
⊢ ((signedDist v) p) q = dist p q ↔ ∃ a, a • v = q -ᵥ p

Tactic:
signedDist_apply_apply,

Goal state after:
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
⊢ ⟪NormedSpace.normalize v, q -ᵥ p⟫ = dist p q ↔ ∃ a, a • v = q -ᵥ p
Module: Mathlib.Geometry.Euclidean.SignedDist

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 q : P
c₁ c₂ : ℝ
⊢ c₂ * ((signedDist v) p) q + c₁ * -((signedDist v) p) q = c₂ * ((signedDist v) p) q - c₁ * ((signedDist v) p) q

Tactic:
mul_neg,

Goal state after:
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
c₁ c₂ : ℝ
⊢ c₂ * ((signedDist v) p) q + -(c₁ * ((signedDist v) p) q) = c₂ * ((signedDist v) p) q - c₁ * ((signedDist v) p) q
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ dist (midpoint ℝ p₁ p₂) p₂ = ‖2‖⁻¹ * dist p₁ p₂

Tactic:
dist_midpoint_right (𝕜 := ℝ)

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ ‖2‖⁻¹ * dist p₁ p₂ = ‖2‖⁻¹ * dist p₁ p₂
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
p₁ p₂ : P
⊢ ∀ p ∈ {p₁, p₂}, dist p (midpoint ℝ p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂

Tactic:
by
    rintro p (rfl | rfl | _)
    · rw [dist_comm, dist_midpoint_left (𝕜 := ℝ)]
    · rw [dist_comm, dist_midpoint_right (𝕜 := ℝ)]

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

Goal state before:
pp: case refine_2.«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₁]
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ ⟪b ((fun i ↦ i) ⟨1, ⋯⟩), b ((fun i ↦ i) ⟨0, ⋯⟩)⟫ = 0

Tactic:
· rw [real_inner_comm]
        exact ho

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✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
ht₁' : t < 1
u : V := p₁ -ᵥ o
v : V := p₂ -ᵥ o
hu : ‖u‖ = s.radius
hv : ‖v‖ = s.radius
h : u = v
⊢ (AffineMap.lineMap p₂ p₂) t = p₂

Tactic:
AffineMap.lineMap_same,

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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
ht₁' : t < 1
u : V := p₁ -ᵥ o
v : V := p₂ -ᵥ o
hu : ‖u‖ = s.radius
hv : ‖v‖ = s.radius
h : u = v
⊢ (AffineMap.const ℝ ℝ p₂) t = p₂
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
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)
hs : ↑((orthogonalProjection (line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃])) p) = ↑((orthogonalProjection line[ℝ, p₁, p₂]) p)
hinf : line[ℝ, p₁, p₂] ⊓ line[ℝ, p₁, p₃] = affineSpan ℝ {p₁}
hsup : line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃] = ⊤
hp : ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = p₁
⊢ p = p₁

Tactic:
← orthogonalProjection_sup_of_orthogonalProjection_eq ho

Goal state after:
case pos
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
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)
hs : ↑((orthogonalProjection (line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃])) p) = ↑((orthogonalProjection line[ℝ, p₁, p₂]) p)
hinf : line[ℝ, p₁, p₂] ⊓ line[ℝ, p₁, p₃] = affineSpan ℝ {p₁}
hsup : line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃] = ⊤
hp : ↑((orthogonalProjection (line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃])) p) = p₁
⊢ p = p₁
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case neg.refine_2.inl.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₁ p₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center < dist p₁ s.center
⊢ ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖

Tactic:
@dist_eq_norm_vsub V,

Goal state after:
case neg.refine_2.inl.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₁ p₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ < dist p₁ s.center
⊢ ‖p₂ -ᵥ s.center‖ < ‖p₁ -ᵥ s.center‖
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
h : dist q s.center ^ 2 - dist p s.center ^ 2 = dist q p ^ 2
⊢ q ∈ s ↔ 0 ≤ s.radius ∧ dist q s.center ^ 2 - dist p s.center ^ 2 = s.radius ^ 2 - dist p s.center ^ 2

Tactic:
rcases le_or_gt 0 s.radius with h0 | h0

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

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

Goal state before:
pp: case neg.refine_2.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₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : dist p₂ s.center = dist p₁ s.center
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖

Tactic:
@dist_eq_norm_vsub V,

Goal state after:
case neg.refine_2.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₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
hp₂' : ‖p₂ -ᵥ s.center‖ = dist p₁ s.center
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
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.height 0 ^ 2 + (s.height i)⁻¹ ^ 2 * s.height i ^ 2

Tactic:
mul_neg,

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.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
h : ⟪q -ᵥ p, -(p -ᵥ s.center)⟫_ℝ = 0
hp : p ∈ s
hp_mem : p ∈ line[ℝ, p, q]
⊢ ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0

Tactic:
inner_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
h : -⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
hp : p ∈ s
hp_mem : p ∈ line[ℝ, p, q]
⊢ ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
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
⊢ s.exsphere Finset.univ = s.insphere

Tactic:
← Finset.compl_empty,

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
⊢ s.exsphere ∅ᶜ = s.insphere
Module: Mathlib.Geometry.Euclidean.Incenter

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
w : Fin (n + 1) → ℝ
hw : ∑ j, w j = 1
⊢ (Finset.affineCombination ℝ Finset.univ s.points) w = s.excenter signs → w = s.excenterWeights signs

Tactic:
simp_rw [excenter, exsphere]
    exact fun he ↦ (affineIndependent_iff_eq_of_fintype_affineCombination_eq ℝ s.points).1
      s.independent _ _ hw h.sum_excenterWeights_eq_one he

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
ι : Type u_3
hne : Nonempty ι
inst✝ : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val✝ : Fintype ι
m : ℕ
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x // x ≠ i }
hc : Fintype.card ι2 = m + 1
this : Nonempty ι2
ha2 : AffineIndependent ℝ fun i2 ↦ p ↑i2
hm :
  ∃! cs,
    cs.center ∈ affineSpan ℝ (Set.range fun i2 ↦ p ↑i2) ∧ (Set.range fun i2 ↦ p ↑i2) ⊆ Metric.sphere cs.center cs.radius
hr : Set.range p = insert (p i) (Set.range fun i2 ↦ p ↑i2)
⊢ (Set.range fun i2 ↦ p ↑i2) = p '' (Set.univ \ {i})

Tactic:
rw [← Set.image_eq_range]

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ι : Type u_3
hne : Nonempty ι
inst✝ : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val✝ : Fintype ι
m : ℕ
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x // x ≠ i }
hc : Fintype.card ι2 = m + 1
this : Nonempty ι2
ha2 : AffineIndependent ℝ fun i2 ↦ p ↑i2
hm :
  ∃! cs,
    cs.center ∈ affineSpan ℝ (Set.range fun i2 ↦ p ↑i2) ∧ (Set.range fun i2 ↦ p ↑i2) ⊆ Metric.sphere cs.center cs.radius
hr : Set.range p = insert (p i) (Set.range fun i2 ↦ p ↑i2)
⊢ p '' {x | x ≠ i} = p '' (Set.univ \ {i})
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
H : |⟪x, NormedSpace.normalize (ortho y x)⟫| = Real.sin (angle x y)
H0 : 0 ≤ ⟪x, NormedSpace.normalize (ortho y x)⟫
⊢ ⟪x, NormedSpace.normalize (ortho y x)⟫ = Real.sin (angle x y)

Tactic:
simp_all [abs_of_nonneg H0]

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

Goal state before:
pp: case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
h : ¬Collinear ℝ {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
h3 : Real.sin (π - ∠ a b c) ≤ Real.sin (∠ a c b)
h5 : π - ∠ a b c < π / 2
h6 : π - ∠ a b c ≤ ∠ a c b
⊢ False

Tactic:
have h7 := angle_add_angle_add_angle_eq_pi c (ne₁₂_of_not_collinear h).symm

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
a b c : P
h : ¬Collinear ℝ {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
h3 : Real.sin (π - ∠ a b c) ≤ Real.sin (∠ a c b)
h5 : π - ∠ a b c < π / 2
h6 : π - ∠ a b c ≤ ∠ a c b
h7 : ∠ a b c + ∠ b c a + ∠ c a b = π
⊢ False
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ (reflection (affineSpan ℝ (s.points '' {i₁, i₂}))) s.circumcenter =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)

Tactic:
have hc : #{i₁, i₂} = 2 := by simp [h]
  -- Making the next line a separate definition helps the elaborator:
  set W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
  have h_faces :
    (orthogonalProjection W s.circumcenter : P) =
      ↑((s.face hc).orthogonalProjectionSpan s.circumcenter) := by
    apply eq_orthogonalProjection_of_eq_subspace
    simp [W]
  rw [reflection_apply', h_faces, s.orthogonalProjection_circumcenter hc,
    circumcenter_eq_centroid, s.face_centroid_eq_centroid hc,
    centroid_eq_affineCombination_of_pointsWithCircumcenter,
    circumcenter_eq_affineCombination_of_pointsWithCircumcenter, ← @vsub_eq_zero_iff_eq V,
    affineCombination_vsub, weightedVSub_vadd_affineCombination, affineCombination_vsub,
    weightedVSub_apply, sum_pointsWithCircumcenter]
  simp_rw [Pi.sub_apply, Pi.add_apply, Pi.sub_apply, sub_smul, add_smul, sub_smul,
    centroidWeightsWithCircumcenter, circumcenterWeightsWithCircumcenter,
    reflectionCircumcenterWeightsWithCircumcenter, ite_smul, zero_smul, sub_zero,
    apply_ite₂ (· + ·), add_zero, ← add_smul, hc, zero_sub, neg_smul, sub_self, add_zero]
  convert! sum_const_zero
  norm_num

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

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
a b c : P
h : ¬Collinear ℝ {a, b, c}
h1 : dist a b < dist a c
w : ∠ a b c ≤ ∠ a c b
h2 : ∠ a b c = ∠ a c b
⊢ False

Tactic:
have h4 : dist a b = dist a c := by
        apply dist_eq_of_angle_eq_angle_of_angle_ne_pi h2
        rw [show ({a, b, c} : Set P) = {b, a, c} by exact Set.insert_comm a b {c}] at h
        linarith [angle_lt_pi_of_not_collinear h]
      linarith

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

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
H5 : ¬angle y z = π
H6 :
  ⟪x, z⟫ =
    Real.cos (angle y z) * Real.cos (angle x y) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
inner_eq_cos_angle_of_norm_eq_one hx hz,

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
H5 : ¬angle y z = π
H6 :
  Real.cos (angle x z) =
    Real.cos (angle y z) * Real.cos (angle x y) +
      Real.sin (angle y z) *
        (Real.sin (angle x y) * ⟪NormedSpace.normalize (ortho y x), NormedSpace.normalize (ortho y z)⟫)
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
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
inst✝ : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : Pi.single j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : SignType.sign (s.excenterWeights signs k) = 0
⊢ False

Tactic:
sign_eq_zero_iff,

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
inst✝ : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : Pi.single j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : s.excenterWeights signs k = 0
⊢ False
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✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
⊢ (∃ r, r ≠ 0 ∧ ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)) ↔
    ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)

Tactic:
refine ⟨?_, ?_⟩ <;> rintro ⟨r, hr, h⟩

Goal state after:
case refine_1
ι : 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 : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)
⊢ ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)

case refine_2
ι : 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₂)
⊢ ∃ r, r ≠ 0 ∧ ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ =
    mongePointWeightsWithCircumcenter n - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ

Tactic:
by
  ext i
  obtain i | i := i
  · rw [Pi.sub_apply, mongePointWeightsWithCircumcenter, centroidWeightsWithCircumcenter,
      mongePointVSubFaceCentroidWeightsWithCircumcenter]
    have hu : #{i₁, i₂}ᶜ = n + 1 := by
      simp [card_compl, Fintype.card_fin, h]
    rw [hu]
    by_cases hi : i = i₁ ∨ i = i₂ <;> simp [compl_eq_univ_sdiff, hi]
  · simp [mongePointWeightsWithCircumcenter, centroidWeightsWithCircumcenter,
      mongePointVSubFaceCentroidWeightsWithCircumcenter]

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Goal state before:
pp: E : Type u_5
H : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, F a < F (f x)
⊢ MapsTo (⇑F) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)) (closure (Iio (F (f x))))

Tactic:
exact .closure hF F.continuous

Goal state after: