mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P},
    AffineIndependent ℝ p →
      ∀ (val : Fintype ι),
        Fintype.card ι = m + 1 →
          ∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x // x ≠ i }
⊢ (Finset.univ \ {i}).card = m + 1

Tactic:
Finset.card_sdiff,

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 : ℕ
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P},
    AffineIndependent ℝ p →
      ∀ (val : Fintype ι),
        Fintype.card ι = m + 1 →
          ∃! cs, cs.center ∈ affineSpan ℝ (Set.range p) ∧ Set.range p ⊆ Metric.sphere cs.center cs.radius
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x // x ≠ i }
⊢ Finset.univ.card - ({i} ∩ Finset.univ).card = m + 1
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case intro.succ.succ
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 i ∉ affineSpan ℝ (Set.range fun i2 ↦ p ↑i2)

Tactic:
convert! ha.notMem_affineSpan_sdiff i Set.univ

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)
⊢ (Set.range fun i2 ↦ p ↑i2) = p '' (Set.univ \ {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
n : ℕ
s : Simplex ℝ P (n + 1)
i : Fin (n + 2)
⊢ s.circumcenter ≠ s.points i

Tactic:
by
  rw [← dist_ne_zero, dist_circumcenter_eq_circumradius']
  exact s.circumradius_pos.ne'

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
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).circumcenter = f s.circumcenter

Tactic:
by
  rw [eq_comm]
  refine (s.map f.toAffineMap f.injective).eq_circumcenter_of_dist_eq (r := s.circumradius) ?_
    fun i ↦ by simp
  rw [map_points, Set.range_comp, ← AffineSubspace.map_span]
  exact AffineSubspace.mem_map_of_mem _ s.circumcenter_mem_affineSpan

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 : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ p b a = π
⊢ ∠ b a p + ∠ p a c = ∠ b a c

Tactic:
have ec := angle_add_angle_add_angle_eq_pi p hc.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 : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
pb : ¬p = b
pc : ¬p = c
ea : ∠ b a c + ∠ a c b + ∠ c b a = π
eb : ∠ b a p + ∠ a p b + ∠ p b a = π
ec : ∠ a c p + ∠ c p a + ∠ p a c = π
⊢ ∠ b a p + ∠ p a c = ∠ b a c
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
hr : ∃ r, ∀ (i : Fin (n + 1)), dist (s.points i) p = r
⊢ ↑(s.orthogonalProjectionSpan p) = s.circumcenter

Tactic:
change ∃ r : ℝ, ∀ i, (fun x => dist x p = r) (s.points i) at hr

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
hr : ∃ r, ∀ (i : Fin (n + 1)), (fun x ↦ dist x p = r) (s.points i)
⊢ ↑(s.orthogonalProjectionSpan p) = s.circumcenter
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₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
⊢ Cospherical {p₁, p₂, p₃, p₄}

Tactic:
have hn' : ¬Collinear ℝ ({p₁, p₃, p₄} : Set P) := by
    rwa [← collinear_iff_of_two_zsmul_oangle_eq h]

Goal state after:
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₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
hn' : ¬Collinear ℝ {p₁, p₃, p₄}
⊢ Cospherical {p₁, p₂, p₃, p₄}
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))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : ∑ i, w i = 1
hp : (Finset.affineCombination ℝ Finset.univ s.points) w ∈ affineSpan ℝ (Set.range s.points)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) = (if i ∈ signs then -1 else 1) * r
i : Fin (n + 1)
h' : w i = (if i ∈ signs then -1 else 1) * r / s.height i
⊢ (r * if i ∈ signs then -1 else 1) / s.height i = r * ((if i ∈ signs then -1 else 1) * (s.height i)⁻¹)

Tactic:
div_eq_mul_inv,

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
signs : Finset (Fin (n + 1))
r : ℝ
w : Fin (n + 1) → ℝ
h1 : ∑ i, w i = 1
hp : (Finset.affineCombination ℝ Finset.univ s.points) w ∈ affineSpan ℝ (Set.range s.points)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) w) = (if i ∈ signs then -1 else 1) * r
i : Fin (n + 1)
h' : w i = (if i ∈ signs then -1 else 1) * r / s.height i
⊢ (r * if i ∈ signs then -1 else 1) * (s.height i)⁻¹ = r * ((if i ∈ signs then -1 else 1) * (s.height 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
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)
⊢ ((affineCombination ℝ univ s.pointsWithCircumcenter) (centroidWeightsWithCircumcenter {i₁, i₂}) -ᵥ s.circumcenter) +ᵥ
      (affineCombination ℝ univ s.pointsWithCircumcenter) (centroidWeightsWithCircumcenter {i₁, i₂}) =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)

Tactic:
circumcenter_eq_affineCombination_of_pointsWithCircumcenter,

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)
⊢ ((affineCombination ℝ univ s.pointsWithCircumcenter) (centroidWeightsWithCircumcenter {i₁, i₂}) -ᵥ
        (affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter n)) +ᵥ
      (affineCombination ℝ univ s.pointsWithCircumcenter) (centroidWeightsWithCircumcenter {i₁, i₂}) =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₂ p₃ p₁ ≤ ∠ p₁ p₂ p₃
h₃₁₂ : ∠ p₃ p₁ p₂ ≤ ∠ p₁ p₂ p₃
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
⊢ π / 3 < ∠ p₁ p₂ p₃

Tactic:
· rcases hne with hne | hne | hne <;>
      rcases hne.lt_or_gt with hne | hne <;>
      linarith [angle_add_angle_add_angle_eq_pi p₃ h]

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
p₁ p₂ p₃ : P
h₂₃₁ : ∠ p₁ p₂ p₃ ≤ ∠ p₂ p₃ p₁
h₃₁₂ : ∠ p₁ p₂ p₃ ≤ ∠ p₃ p₁ p₂
hne : ∠ p₁ p₂ p₃ ≠ ∠ p₂ p₃ p₁ ∨ ∠ p₁ p₂ p₃ ≠ ∠ p₃ p₁ p₂ ∨ ∠ p₂ p₃ p₁ ≠ ∠ p₃ p₁ p₂
h : ¬p₂ = p₁
⊢ ∠ p₁ p₂ p₃ < π / 3

Tactic:
· rcases hne with hne | hne | hne <;>
      rcases hne.lt_or_gt with hne | hne <;>
      linarith [angle_add_angle_add_angle_eq_pi p₃ h]

Goal state after:
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))
i : Fin (n + 1)
⊢ s.touchpoint signs i ∈ affineSpan ℝ (s.points '' {i}ᶜ)

Tactic:
convert! s.touchpoint_mem_affineSpan _ _

Goal state after:
case e'_4
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))
i : Fin (n + 1)
⊢ s.points '' {i}ᶜ = Set.range (s.faceOpposite i).points
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)
⊢ (↑(n + 2 + 1) / ↑(n + 2 - 1)) •
        ((affineCombination ℝ univ s.pointsWithCircumcenter) (centroidWeightsWithCircumcenter univ) -ᵥ
          s.circumcenter) +ᵥ
      s.circumcenter =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (mongePointWeightsWithCircumcenter n)

Tactic:
circumcenter_eq_affineCombination_of_pointsWithCircumcenter,

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)
⊢ (↑(n + 2 + 1) / ↑(n + 2 - 1)) •
        ((affineCombination ℝ univ s.pointsWithCircumcenter) (centroidWeightsWithCircumcenter univ) -ᵥ
          (affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter (n + 2))) +ᵥ
      (affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter (n + 2)) =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (mongePointWeightsWithCircumcenter n)
Module: Mathlib.Geometry.Euclidean.MongePoint

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 : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ -((if True ∨ i₁ = i₂ then (↑(n + 1))⁻¹ else 0) * ((if True then 1 else 0) - if i₁ = i₂ then 1 else 0) *
                  (dist (s.points i₁) (s.points i₁) * dist (s.points i₁) (s.points i₁)) +
                (if True ∨ i₁ = i₂ then (↑(n + 1))⁻¹ else 0) * ((if i₂ = i₁ then 1 else 0) - if True then 1 else 0) *
                  (dist (s.points i₁) (s.points i₂) * dist (s.points i₁) (s.points i₂)) +
              (if True ∨ i₁ = i₂ then (↑(n + 1))⁻¹ else 0) * (0 - 0) *
                (dist (s.points i₁) s.circumcenter * dist (s.points i₁) s.circumcenter) +
            ((if i₂ = i₁ ∨ True then (↑(n + 1))⁻¹ else 0) * ((if True then 1 else 0) - if i₁ = i₂ then 1 else 0) *
                  (dist (s.points i₂) (s.points i₁) * dist (s.points i₂) (s.points i₁)) +
                (if i₂ = i₁ ∨ True then (↑(n + 1))⁻¹ else 0) * ((if i₂ = i₁ then 1 else 0) - if True then 1 else 0) *
                  (dist (s.points i₂) (s.points i₂) * dist (s.points i₂) (s.points i₂)) +
              (if i₂ = i₁ ∨ True then (↑(n + 1))⁻¹ else 0) * (0 - 0) *
                (dist (s.points i₂) s.circumcenter * dist (s.points i₂) s.circumcenter)) +
          (-2 / ↑(n + 1) * ((if True then 1 else 0) - if i₁ = i₂ then 1 else 0) *
                (dist s.circumcenter (s.points i₁) * dist s.circumcenter (s.points i₁)) +
              -2 / ↑(n + 1) * ((if i₂ = i₁ then 1 else 0) - if True then 1 else 0) *
                (dist s.circumcenter (s.points i₂) * dist s.circumcenter (s.points i₂)) +
            -2 / ↑(n + 1) * (0 - 0) * (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
      2 =
    0

Tactic:
simp [h, Ne.symm h, dist_comm (s.points i₁)]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.Ptolemy

Goal state before:
pp: case h
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
⊢ ∠ d p a = ∠ c p b

pp: case hab
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
⊢ dist d p = dist a p / dist b p * dist c p

pp: case hcb
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
⊢ dist a p = dist a p / dist b p * dist b p

Tactic:
· rwa [angle_comm, angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi]; rwa [angle_comm]

Goal state after:
case hab
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
⊢ dist d p = dist a p / dist b p * dist c p

case hcb
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d p : P
h : Cospherical {a, b, c, d}
hapc : ∠ a p c = π
hbpd : ∠ b p d = π
h' : Cospherical {a, c, b, d}
hmul : dist a p * dist c p = dist b p * dist d p
hbp : dist b p ≠ 0
h₁ : dist c d = dist c p / dist b p * dist a b
⊢ dist a p = dist a p / dist b p * dist b p
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₁ i₂ : Fin (n + 3)
r : ℝ
hv : r • (s.points i₁ -ᵥ s.points i₂) ∈ ℝ ∙ (s.points i₁ -ᵥ s.points i₂)
⊢ ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, r • (s.points i₁ -ᵥ s.points i₂)⟫ = 0

Tactic:
rw [inner_smul_right, s.inner_mongePoint_vsub_face_centroid_vsub, mul_zero]

Goal state after:
Module: Mathlib.Geometry.Group.Growth.LinearLowerBound

Goal state before:
pp: case inr.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
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)
hXn : ∀ (d : ℕ), X ^ (n + d) = X ^ n
⊢ ↑X ^ n = ↑(closure (↑X ^ n))

Tactic:
exact mod_cast this (one_mem_pow hX₁) (hX.pow hn) one_ne_zero
      (by simp [hXn, ← pow_mul, mul_two]) (by simp)

Goal state after:
Module: Mathlib.Geometry.Manifold.DerivationBundle

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : f x = y
v : PointDerivation I x
g g' : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ ContMDiffMap.comp g f • v (ContMDiffMap.comp g' f) + ContMDiffMap.comp g' f • v (ContMDiffMap.comp g f) =
    g • v (ContMDiffMap.comp g' f) + g' • v (ContMDiffMap.comp g f)

Tactic:
PointedContMDiffMap.smul_def,

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : f x = y
v : PointDerivation I x
g g' : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ (ContMDiffMap.comp g f) x * v (ContMDiffMap.comp g' f) + ContMDiffMap.comp g' f • v (ContMDiffMap.comp g f) =
    g • v (ContMDiffMap.comp g' f) + g' • v (ContMDiffMap.comp g f)
Module: Mathlib.Geometry.Manifold.DerivationBundle

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : f x = y
v : PointDerivation I x
g g' : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ g (f x) * v (ContMDiffMap.comp g' f) + ContMDiffMap.comp g' f • v (ContMDiffMap.comp g f) =
    g • v (ContMDiffMap.comp g' f) + g' • v (ContMDiffMap.comp g f)

Tactic:
PointedContMDiffMap.smul_def,

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
n : ℕ∞ω
X : Derivation 𝕜 C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
f✝ : C^∞⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : C^∞⟮I, M; I', M'⟯
x : M
y : M'
h : f x = y
v : PointDerivation I x
g g' : C^∞⟮I', M'; 𝕜⟯⟨y⟩
⊢ g (f x) * v (ContMDiffMap.comp g' f) + (ContMDiffMap.comp g' f) x * v (ContMDiffMap.comp g f) =
    g • v (ContMDiffMap.comp g' f) + g' • v (ContMDiffMap.comp g f)
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)
h : ∀ (y : E), F ((fderiv ℝ f x) y) = 0
y : H
hy : y ∈ interior s
z : E
⊢ 0 ≠ F (f x - y)

Tactic:
F.map_sub

Goal state after:
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)
h : ∀ (y : E), F ((fderiv ℝ f x) y) = 0
y : H
hy : y ∈ interior s
z : E
⊢ 0 ≠ F (f x) - F y
Module: Mathlib.Geometry.Euclidean.MongePoint

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 : Set P
t : Triangle ℝ P
hto : t.orthocenter ∉ Set.range t.points
hts : s = insert t.orthocenter (Set.range t.points)
t₂ : Triangle ℝ P
ht₂ : Set.range t₂.points ⊆ insert t.orthocenter (Set.range t.points)
ht₂s : Set.range t₂.points ⊆ s
c : P
hc : c ∈ affineSpan ℝ (Set.range t₂.points)
h : ∀ (i : Fin 3), dist (t₂.points i) c = Simplex.circumradius t
hs : Set.range t.points ⊆ s
⊢ Simplex.circumradius t₂ = Simplex.circumradius t

Tactic:
exact (t₂.eq_circumradius_of_dist_eq hc h).symm

Goal state after: