mathlib-initiative/mathlib-tactics huggingface dataset:
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
signs : Finset (Fin (n + 1))
⊢ s.ExcenterExists signsᶜ ↔ s.ExcenterExists signs

Tactic:
simp [ExcenterExists]

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
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))ᗮ
hv0 : v ≠ 0
⊢ ‖‖v‖⁻¹ • v‖ = 1

Tactic:
· simp [norm_smul, norm_ne_zero_iff.2 hv0]

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

Goal state before:
pp: case e'_2.e'_6
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
⊢ s.points i -ᵥ s.points 0 ∈ vectorSpan ℝ (Set.range (s.faceOpposite j).points)

Tactic:
refine vsub_mem_vectorSpan _ ?_ ?_

Goal state after:
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
⊢ s.points i ∈ Set.range (s.faceOpposite j).points

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
⊢ s.points 0 ∈ Set.range (s.faceOpposite j).points
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
pp: case inl.inr
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₃) + ↑π
h₂ : ∡ (t.points i₃) (t.points i₂) (excenter t signs) = ∡ (excenter t signs) (t.points i₂) (t.points i₁) + ↑π
h₁' : excenter t signs = excenter t {i₂}
h₂' : excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₃}

Tactic:
rw [h₂'] at h₁'

Goal state after:
case inl.inr
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₃) + ↑π
h₂ : ∡ (t.points i₃) (t.points i₂) (excenter t signs) = ∡ (excenter t signs) (t.points i₂) (t.points i₁) + ↑π
h₁' : excenter t {i₁} = excenter t {i₂}
h₂' : excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₃}
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ (s.height i)⁻¹ -
      ∑ x with x ≠ i,
        -(⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ / (s.height i * s.height x) *
            (s.height x)⁻¹) =
    0

Tactic:
Finset.sum_neg_distrib,

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ (s.height i)⁻¹ -
      -∑ x with x ≠ i,
          ⟪s.points i -ᵥ s.altitudeFoot i, s.points x -ᵥ s.altitudeFoot x⟫ / (s.height i * s.height x) *
            (s.height x)⁻¹ =
    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
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
⊢ (s.reindex e).exsphere signs = s.exsphere (Finset.map e.symm.toEmbedding signs)

Tactic:
simp_rw [exsphere, excenterWeightsUnnorm_reindex, excenterWeights_reindex, Finset.sum_comp_equiv,
    reindex, ← Equiv.coe_toEmbedding, ← Finset.affineCombination_map]

Goal state after:
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)
signs : Finset (Fin (m + 1))
⊢ {
      center :=
        (Finset.affineCombination ℝ (Finset.map e.symm.toEmbedding Finset.univ) s.points)
          (s.excenterWeights (Finset.map e.symm.toEmbedding signs)),
      radius :=
        |((Finset.map e.symm.toEmbedding Finset.univ).sum
              (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs)))⁻¹| } =
    {
      center :=
        (Finset.affineCombination ℝ Finset.univ s.points) (s.excenterWeights (Finset.map e.symm.toEmbedding signs)),
      radius := |(∑ i, s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i)⁻¹| }
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
⊢ ∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius

Tactic:
cases nonempty_fintype ι
  induction hn : Fintype.card ι generalizing ι with
  | zero =>
    exfalso
    have h := Fintype.card_pos_iff.2 hne
    lia
  | succ m hm =>
    rcases m with - | m
    · rw [Fintype.card_eq_one_iff] at hn
      obtain ⟨i, hi⟩ := hn
      have : Unique ι := ⟨⟨i⟩, hi⟩
      use ⟨p i, 0⟩
      simp only [Set.range_unique, AffineSubspace.mem_affineSpan_singleton]
      constructor
      · simp_rw [hi default, Set.singleton_subset_iff]
        exact ⟨⟨⟩, by simp only [Metric.sphere_zero, Set.mem_singleton_iff]⟩
      · rintro ⟨cc, cr⟩
        rintro ⟨rfl, hdist⟩
        replace hdist : 0 = cr := by simpa using hdist
        rw [hi default, hdist]
    · have i := hne.some
      let ι2 := { x // x ≠ i }
      classical
      have hc : Fintype.card ι2 = m + 1 := by
        rw [Fintype.card_of_subtype {x | x ≠ i}]
        · rw [Finset.filter_not, Finset.filter_eq' _ i, if_pos (Finset.mem_univ _),
            Finset.card_sdiff, Finset.card_univ, hn]
          simp
        · simp
      have : Nonempty ι2 := Fintype.card_pos_iff.1 (hc.symm ▸ Nat.zero_lt_succ _)
      have ha2 : AffineIndependent ℝ fun i2 : ι2 => p i2 := ha.subtype _
      replace hm := hm ha2 _ hc
      have hr : Set.range p = insert (p i) (Set.range fun i2 : ι2 => p i2) := by
        change _ = insert _ (Set.range fun i2 : { x | x ≠ i } => p i2)
        rw [← Set.image_eq_range, ← Set.image_univ, ← Set.image_insert_eq]
        congr with j
        simp [Classical.em]
      rw [hr, ← affineSpan_insert_affineSpan]
      refine existsUnique_dist_eq_of_insert (Set.range_nonempty _) (subset_affineSpan ℝ _) ?_ hm
      convert! ha.notMem_affineSpan_sdiff i Set.univ
      change (Set.range fun i2 : { x | x ≠ i } => p i2) = _
      rw [← Set.image_eq_range]
      congr 1 with j
      simp

Goal state after:
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)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
⊢ Concyclic {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}

Tactic:
rcases cospherical_or_collinear_of_two_zsmul_oangle_eq h with (hc | hc)
  · exact Or.inl ⟨hc, coplanar_of_fact_finrank_eq_two _⟩
  · exact Or.inr hc

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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ x,
        (((if x ∈ {i₁, i₂} then (↑(#{i₁, i₂}))⁻¹ • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
              else 0) -
              0 +
            if x ∈ {i₁, i₂} then (↑(#{i₁, i₂}))⁻¹ • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
            else 0) -
          if x = i₁ ∨ x = i₂ then 1 • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) else 0) +
      (0 - 1 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) + 0 -
        -1 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯)) =
    0

Tactic:
sub_zero,

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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ x,
        (((if x ∈ {i₁, i₂} then (↑(#{i₁, i₂}))⁻¹ • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
            else 0) +
            if x ∈ {i₁, i₂} then (↑(#{i₁, i₂}))⁻¹ • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
            else 0) -
          if x = i₁ ∨ x = i₂ then 1 • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) else 0) +
      (0 - 1 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯) + 0 -
        -1 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯)) =
    0
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₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ x,
        ((if x ∈ {i₁, i₂} then ((↑2)⁻¹ + (↑2)⁻¹) • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
          else 0) -
          if x = i₁ ∨ x = i₂ then 1 • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) else 0) +
      0 =
    0

Tactic:
add_zero

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
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := affineSpan ℝ (s.points '' {i₁, i₂})
h_faces : ↑((orthogonalProjection W) s.circumcenter) = ↑((s.face hc).orthogonalProjectionSpan s.circumcenter)
⊢ ∑ x,
      ((if x ∈ {i₁, i₂} then ((↑2)⁻¹ + (↑2)⁻¹) • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯)
        else 0) -
        if x = i₁ ∨ x = i₂ then 1 • (s.pointsWithCircumcenter (pointIndex x) -ᵥ Classical.choice ⋯) else 0) =
    0
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.circumcenter = c

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

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
h0 :
  dist ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) t)
      ↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite j).points)))
          ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) t)) =
    0
⊢ False

Tactic:
dist_orthogonalProjection_eq_zero_iff

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
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
h0 :
  (AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) t ∈ affineSpan ℝ (Set.range (s.faceOpposite j).points)
⊢ False
Module: Mathlib.Geometry.Euclidean.NinePointCircle

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
⊢ s.centroid -ᵥ s.circumcenter ∈ (affineSpan ℝ (Set.range s.points)).direction

Tactic:
exact AffineSubspace.vsub_mem_direction s.centroid_mem_affineSpan s.circumcenter_mem_affineSpan

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

Goal state before:
pp: case radius
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
h : n = m
⊢ (s.reindex e).ninePointCircle.radius = s.ninePointCircle.radius

Tactic:
simp [ninePointCircle_radius, h]

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Triangle ℝ P
i : Fin 3
⊢ ↑((orthogonalProjection (affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points))) (s.points i)) =
    ↑((orthogonalProjection (affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points))) (Simplex.eulerPoint s i))

Tactic:
congr 1

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 : Triangle ℝ P
i : Fin 3
⊢ (orthogonalProjection (affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points))) (s.points i) =
    (orthogonalProjection (affineSpan ℝ (Set.range (Simplex.faceOpposite s i).points))) (Simplex.eulerPoint s i)
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: n : ℕ
⊢ ∑ i, mongePointWeightsWithCircumcenter n (pointIndex i) + mongePointWeightsWithCircumcenter n circumcenterIndex = 1

Tactic:
mongePointWeightsWithCircumcenter,

Goal state after:
n : ℕ
⊢ ∑ i, (↑(n + 1))⁻¹ + -2 / ↑(n + 1) = 1
Module: Mathlib.Geometry.Euclidean.MongePoint

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

Tactic:
mongePointWeightsWithCircumcenter,

Goal state after:
case pointIndex
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
i : Fin (n + 2 + 1)
⊢ mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ (pointIndex i) =
    (↑(n + 1))⁻¹ - centroidWeightsWithCircumcenter {i₁, i₂}ᶜ (pointIndex i)
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 p q : P
hp : p ∈ line[ℝ, a, b]
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h1' : m -ᵥ a - (m -ᵥ p) = p -ᵥ a
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
r : P
⊢ b -ᵥ r = m -ᵥ r + (m -ᵥ a)

Tactic:
by
    rw [midpoint_vsub_left, ← right_vsub_midpoint, add_comm, vsub_add_vsub_cancel]

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

Goal state before:
pp: case e_a.e_p.e_s
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₁ i₂ : Fin (n + 3)
⊢ {i₁, i₂}ᶜ = {i₂, i₁}ᶜ

Tactic:
congr 1

Goal state after:
case e_a.e_p.e_s
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₁ i₂ : Fin (n + 3)
⊢ {i₁, i₂} = {i₂, i₁}
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

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
hp : p ∈ s
v : V
p' : P
hp' : p' ∈ AffineSubspace.mk' p (ℝ ∙ v)
⊢ p' = p ∨ p' = s.secondInter p v ↔ p' ∈ s

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
  · rcases h with (h | h)
    · rwa [h]
    · rwa [h, Sphere.secondInter_mem]
  · rw [AffineSubspace.mem_mk', Submodule.mem_span_singleton] at hp'
    rcases hp' with ⟨r, hr⟩
    rw [eq_comm, ← eq_vadd_iff_vsub_eq] at hr
    subst hr
    by_cases hv : v = 0
    · simp [hv]
    rw [Sphere.secondInter]
    rw [mem_sphere] at h hp
    rw [← hp, dist_smul_vadd_eq_dist _ _ hv] at h
    rcases h with (h | h) <;> simp [h]

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)
⊢ ∀ (i : { i // i₁ ≠ i }), p -ᵥ s.mongePoint ∈ (ℝ ∙ (s.points i₁ -ᵥ s.points ↑i))ᗮ

Tactic:
exact fun i => (Submodule.mem_inf.1 (h' i i.property)).1

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}))ᗮ
⊢ ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x ↦ s.points i₁ -ᵥ x) '' s.points '' (Set.univ \ {i₁})

Tactic:
rw [Set.image_image]

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 ℝ (⋃ i, {s.points i₁ -ᵥ s.points ↑i}))ᗮ
⊢ ⋃ i, {s.points i₁ -ᵥ s.points ↑i} = (fun x ↦ s.points i₁ -ᵥ s.points x) '' (Set.univ \ {i₁})
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

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
s : Sphere P
p p' : P
hp : p ∈ s
hp' : dist p' s.center ≤ s.radius
h : ¬p' = p
he : 0 = ⟪p -ᵥ p', p -ᵥ s.center⟫
⊢ False

Tactic:
exact ((inner_pos_or_eq_of_dist_le_radius hp hp').resolve_right (Ne.symm h)).ne he

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 t p : P
s : Sphere P
ha : a ∈ s
hb : b ∈ s
hp : p ∈ line[ℝ, a, b]
h_tangent : s.IsTangentAt t line[ℝ, p, t]
hr : 0 ≤ s.radius
radius_le_dist : s.radius ≤ dist p s.center
⊢ dist p t ^ 2 = dist p a * dist p b

Tactic:
rw [mul_dist_eq_power_of_radius_le_dist_center hr hp ha hb radius_le_dist,
    Sphere.power, h_tangent.dist_sq_eq_of_mem (left_mem_affineSpan_pair ℝ p t)]

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 t p : P
s : Sphere P
ha : a ∈ s
hb : b ∈ s
hp : p ∈ line[ℝ, a, b]
h_tangent : s.IsTangentAt t line[ℝ, p, t]
hr : 0 ≤ s.radius
radius_le_dist : s.radius ≤ dist p s.center
⊢ dist p t ^ 2 = s.radius ^ 2 + dist p t ^ 2 - s.radius ^ 2
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
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist (circumcenter t) ((reflection (affineSpan ℝ (t.points '' {i₁, i₂}))) t.orthocenter) = circumradius t

Tactic:
EuclideanGeometry.dist_reflection,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ dist ((reflection (affineSpan ℝ (t.points '' {i₁, i₂}))) (circumcenter t)) t.orthocenter = circumradius t
Module: Mathlib.Geometry.Group.Growth.LinearLowerBound

Goal state before:
pp: case zero
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {X : Finset G} {n : ℕ},
    1 ∈ X → X.Nontrivial → n ≠ 0 → X ^ n = X ^ (n + 1) → n = 1 → ↑X = ↑(closure ↑X)
⊢ X ^ (n + 0) = X ^ n

Tactic:
add_zero

Goal state after:
case zero
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {X : Finset G} {n : ℕ},
    1 ∈ X → X.Nontrivial → n ≠ 0 → X ^ n = X ^ (n + 1) → n = 1 → ↑X = ↑(closure ↑X)
⊢ X ^ n = X ^ n
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
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ ↑X ^ (n - 1) = ↑X ^ (n - m + (m - 1))

Tactic:
congr 1

Goal state after:
case e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ n - 1 = n - m + (m - 1)