mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤

Tactic:
have hσ' := orderOf_eq_card_of_forall_mem_zpowers hσ

Goal state after:
K : Type u
inst✝⁵ : Field K
L : Type u_1
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
ζ : K
hζ : IsPrimitiveRoot ζ (finrank K L)
σ : Gal(L/K)
hσ : Function.Surjective fun x ↦ σ ^ x
hσ' : orderOf σ = Nat.card Gal(L/K)
⊢ ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ c.minpoly.aroots L = (c.minpoly.aroots L).toFinset.val

Tactic:
Multiset.toFinset_val,

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ c.minpoly.aroots L = (c.minpoly.aroots L).dedup
Module: Mathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
p : ℕ
inst✝ : ExpChar k p
x : k
⊢ (root k) x ^ p = (algebraMap k (AdjoinPthRoots k)) x

Tactic:
← ringExpChar.eq k p

Goal state after:
k : Type u_1
inst✝¹ : Field k
p : ℕ
inst✝ : ExpChar k p
x : k
⊢ (root k) x ^ ringExpChar k = (algebraMap k (AdjoinPthRoots k)) x
Module: Mathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
p : ℕ
inst✝ : ExpChar k p
x : AdjoinPthRoots k
⊢ (algebraMap k (AdjoinPthRoots k)) ((root k).symm x) = x ^ p

Tactic:
← ringExpChar.eq k p

Goal state after:
k : Type u_1
inst✝¹ : Field k
p : ℕ
inst✝ : ExpChar k p
x : AdjoinPthRoots k
⊢ (algebraMap k (AdjoinPthRoots k)) ((root k).symm x) = x ^ ringExpChar k
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q : ℕ
inst✝ : ExpChar F q
x : E
⊢ x ∈ perfectClosure F E ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
by
  rw [mem_perfectClosure_iff, ringExpChar.eq F q]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) f.num - (algebraMap K[X] K⟮X⟯) f.num = 0

Tactic:
exact sub_self _

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B : Subfield E
⊢ (A ⊓ B).relrank A = B.relrank A

Tactic:
by
  rw [inf_comm, inf_relrank_right]

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
⊢ (A ⊓ B).relrank A = B.relrank A

Tactic:
by
  rw [inf_comm, inf_relrank_right]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) *
      Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E) / c E) *
      (Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) * Polynomial.C (c E) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
mul_comm _ (Polynomial.C (c E))

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) *
      Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E) / c E) *
      (Polynomial.C (c E) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A : IntermediateField F E
⊢ ⊥.relrank A = Module.rank F ↥A

Tactic:
by
  rw [← rank_bot_mul_relrank (show ⊥ ≤ A from bot_le), IntermediateField.rank_bot, one_mul]

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace 𝕜 V
inst✝⁶ : MetricSpace P
inst✝⁵ : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst✝⁴ : Nonempty ↥s₁
inst✝³ : Nonempty ↥s₂
inst✝² : s₁.direction.HasOrthogonalProjection
inst✝¹ : s₂.direction.HasOrthogonalProjection
p : P
h : ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)
inst✝ : (s₁ ⊔ s₂).direction.HasOrthogonalProjection
⊢ ↑((orthogonalProjection (s₁ ⊔ s₂)) p) = ↑((orthogonalProjection s₁) p)

Tactic:
by
  rw [coe_orthogonalProjection_eq_iff_mem]
  refine ⟨SetLike.le_def.1 le_sup_left (orthogonalProjection_mem _), ?_⟩
  rw [direction_sup_eq_sup_direction (orthogonalProjection_mem p) (h ▸ orthogonalProjection_mem p),
    ← Submodule.inf_orthogonal]
  exact ⟨vsub_orthogonalProjection_mem_direction_orthogonal _ _,
    h ▸ vsub_orthogonalProjection_mem_direction_orthogonal _ _⟩

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ (reflection s) p = (↑((orthogonalProjection s) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s) p)

Tactic:
by
  rw [reflection_apply, orthogonalProjection_apply', Submodule.coe_orthogonalProjectionOnto_apply]
  set x : P := ↑(Classical.arbitrary s)
  set v : V := s.direction.starProjection (p -ᵥ x)
  rw [Submodule.reflection_apply, two_smul, sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_assoc,
    add_comm v, add_vadd, vadd_vsub_assoc]

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

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.altitudeFoot i ∈ affineSpan ℝ (s.points '' {i}ᶜ)

Tactic:
by
  rw [← range_faceOpposite_points]
  exact orthogonalProjection_mem _

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

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
h : ℝ ∙ y = ℝ ∙ z
⊢ 2 • o.oangle x y = 2 • o.oangle x z

Tactic:
rw [Submodule.span_singleton_eq_span_singleton] at h
  rcases h with ⟨r, rfl⟩
  exact (o.two_zsmul_oangle_smul_right_of_ne_zero _ _ (Units.ne_zero _)).symm

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

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
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
⊢ p₃ -ᵥ p₁ = (1 - r) • (p₃ -ᵥ p₁) + r • (p₃ -ᵥ p₁)

Tactic:
←
    add_smul,

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
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
⊢ p₃ -ᵥ p₁ = (1 - r + r) • (p₃ -ᵥ p₁)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
hx : ¬‖x‖ = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / ‖x‖ / ‖x + y‖) = Real.arccos (‖x‖ / ‖x + y‖)

Tactic:
mul_self_div_self

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
hx : ¬‖x‖ = 0
⊢ Real.arccos (‖x‖ / ‖x + y‖) = Real.arccos (‖x‖ / ‖x + y‖)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
w x y z : V
h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z
hs : (o.oangle w x).sign = (o.oangle y z).sign
h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0
⊢ o.oangle w x = o.oangle y z

Tactic:
have hs' : (o.oangle w x).sign = 0 ∧ (o.oangle y z).sign = 0 := by
      rcases h0 with ((rfl | rfl) | rfl | rfl)
      · simpa using hs.symm
      · simpa using hs.symm
      · simpa using hs
      · simpa using hs
    rcases hs' with ⟨hswx, hsyz⟩
    have h' : InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y z = π / 2 := by
      rcases h0 with ((rfl | rfl) | rfl | rfl)
      · simpa using h.symm
      · simpa using h.symm
      · simpa using h
      · simpa using h
    rcases h' with ⟨hwx, hyz⟩
    have hpi : π / 2 ≠ π := by
      intro hpi
      rw [div_eq_iff, eq_comm, ← sub_eq_zero, mul_two, add_sub_cancel_right] at hpi
      · exact Real.pi_pos.ne.symm hpi
      · exact two_ne_zero
    have h0wx : w = 0 ∨ x = 0 := by
      have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hswx
      simpa [hwx, Real.pi_pos.ne.symm, hpi] using h0'
    have h0yz : y = 0 ∨ z = 0 := by
      have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hsyz
      simpa [hyz, Real.pi_pos.ne.symm, hpi] using h0'
    rcases h0wx with (h0wx | h0wx) <;> rcases h0yz with (h0yz | h0yz) <;> simp [h0wx, h0yz]

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

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
⊢ ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₂ -ᵥ p₃‖ * ‖p₂ -ᵥ p₃‖ ↔
    InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π / 2

Tactic:
← norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two,

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
⊢ ‖p₁ -ᵥ p₃‖ * ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₂ -ᵥ p₃‖ * ‖p₂ -ᵥ p₃‖ ↔
    ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ * ‖p₁ -ᵥ p₂ - (p₃ -ᵥ p₂)‖ = ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ * ‖p₃ -ᵥ p₂‖
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

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
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).cos * dist p₁ p₃ = dist p₁ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe, dist_comm p₁ p₃,
    cos_angle_mul_dist_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ p₁ ∈ perpBisector p₁ p₂ ↔ p₁ = p₂

Tactic:
rw [perpBisector_comm, right_mem_perpBisector, eq_comm]

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✝² : 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:
rintro p (rfl | rfl | _)
    · rw [dist_comm, dist_midpoint_left (𝕜 := ℝ)]
    · rw [dist_comm, dist_midpoint_right (𝕜 := ℝ)]

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

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
hp : s.IsTangentAt p as
hq : s.IsTangentAt q as
hqp : ⟪p -ᵥ q, p -ᵥ s.center⟫ = 0
hpq : ⟪p -ᵥ q, q -ᵥ s.center⟫ = 0
⊢ p = q

Tactic:
← hpq,

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
hp : s.IsTangentAt p as
hq : s.IsTangentAt q as
hqp : ⟪p -ᵥ q, p -ᵥ s.center⟫ = ⟪p -ᵥ q, q -ᵥ s.center⟫
hpq : ⟪p -ᵥ q, q -ᵥ s.center⟫ = 0
⊢ p = q
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

Goal state before:
pp: case neg
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ : P
ha : AffineIndependent ℝ ![p₁, p₂, p₃]
h : dist p ↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = dist p ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
ho : ¬↑((orthogonalProjection line[ℝ, p₁, p₂]) p) = ↑((orthogonalProjection line[ℝ, p₁, p₃]) p)
⊢ 2 • ∡ p₂ p₁ p = 2 • ∡ p p₁ p₃

Tactic:
have hp := oangle_eq_of_dist_orthogonalProjection_eq
      (left_mem_affineSpan_pair _ _ _) (left_mem_affineSpan_pair _ _ _) ho h
    have h₂₁ : p₂ ≠ p₁ := ha.injective.ne (by decide : (1 : Fin 3) ≠ 0)
    have h₃₁ : p₃ ≠ p₁ := ha.injective.ne (by decide : (2 : Fin 3) ≠ 0)
    have hp₁ : orthogonalProjection line[ℝ, p₁, p₂] p ≠ p₁ := by
      intro hp
      rw [hp, eq_comm, dist_orthogonalProjection_eq_dist_iff_eq_of_mem
        (left_mem_affineSpan_pair ℝ _ p₃)] at h
      grind
    have hp₂ : orthogonalProjection line[ℝ, p₁, p₃] p ≠ p₁ := by
      intro hp
      rw [hp, dist_orthogonalProjection_eq_dist_iff_eq_of_mem
          (left_mem_affineSpan_pair ℝ _ p₂)] at h
      grind
    rw [← (collinear_insert_of_mem_affineSpan_pair
             (orthogonalProjection_mem p)).two_zsmul_oangle_eq_left hp₁ h₂₁,
        ← (collinear_insert_of_mem_affineSpan_pair
             (orthogonalProjection_mem p)).two_zsmul_oangle_eq_right hp₂ h₃₁, hp]

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

Goal state before:
pp: case inl.inl.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
h : dist s.center s.center < s.radius
hs : Subsingleton V
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius s.center) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬s.center = s.center ∨ Subsingleton V

pp: case inl.inl.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
h : dist s.center s.center < s.radius
hs : Nontrivial V
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius s.center) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬s.center = s.center ∨ Subsingleton V

Tactic:
· have hs' := (AddTorsor.subsingleton_iff V P).1 hs
        simp [hs, Metric.sphere_eq_empty_of_subsingleton (dist_nonneg.trans_lt h).ne']

Goal state after:
case inl.inl.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
h : dist s.center s.center < s.radius
hs : Nontrivial V
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius s.center) = ∅ ↔
    Module.finrank ℝ V = 1 ∧ ¬s.center = s.center ∨ Subsingleton V
Module: Mathlib.Geometry.Euclidean.Angle.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
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₃
⊢ ∡ (touchpoint t {i₁} i₃) (t.points i₁) (excenter t {i₁}) = ∡ (excenter t {i₁}) (t.points i₁) (touchpoint t {i₁} i₂)

Tactic:
have hd := (t.excenterExists_singleton i₁).dist_excenter_eq_dist_excenter i₃ i₂

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)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hd : dist (excenter t {i₁}) (touchpoint t {i₁} i₃) = dist (excenter t {i₁}) (touchpoint t {i₁} i₂)
⊢ ∡ (touchpoint t {i₁} i₃) (t.points i₁) (excenter t {i₁}) = ∡ (excenter t {i₁}) (t.points i₁) (touchpoint t {i₁} 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
this :
  ∀ (i : Fin (n + 1)),
    i ≠ 0 → ∑ j, ⟪s.points i -ᵥ s.points 0, (s.height j)⁻¹ ^ 2 • (s.points j -ᵥ s.altitudeFoot j)⟫ = 0
⊢ ∑ i, (s.height i)⁻¹ ^ 2 • (s.points i -ᵥ s.altitudeFoot i) = 0

Tactic:
rw [← Submodule.mem_bot ℝ,
      ← Submodule.inf_orthogonal_eq_bot (vectorSpan ℝ (Set.range s.points))]
    refine ⟨Submodule.sum_smul_mem _ _ fun i hi ↦
              vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan
                (mem_affineSpan _ (Set.mem_range_self _))
                (altitudeFoot_mem_affineSpan  _ _),
            ?_⟩
    rw [vectorSpan_range_eq_span_range_vsub_right_ne _ _ 0, Submodule.span_range_eq_iSup,
      ← Submodule.iInf_orthogonal, Submodule.coe_iInf, Set.mem_iInter]
    intro i
    rcases i with ⟨i, hi⟩
    simpa only [SetLike.mem_coe, Submodule.mem_orthogonal_singleton_iff_inner_right, inner_sum]
      using this i hi

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))
h : s.ExcenterExists signs
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : s.excenter signs ∈ affineSpan ℝ (s.points '' ↑fs)
hc : #fs < #Finset.univ
i : Fin (n + 1)
hi : i ∉ fs
⊢ ∃ i, i ∉ fs

Tactic:
exact ⟨i, hi⟩

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h✝ : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
this : -1 < n
h : angle x y + n • (2 * π) ≤ angle x (x + y) + angle y (x + y)
hn : 1 ≤ n
⊢ False

Tactic:
grw [← hn, one_smul, ← angle_nonneg x y, zero_add, two_mul] at h

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h✝ : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
this : -1 < n
h : π + π ≤ angle x (x + y) + angle y (x + y)
hn : 1 ≤ n
⊢ 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
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).circumradius = s.circumradius

Tactic:
circumradius,

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 : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).circumsphere.radius = s.circumsphere.radius
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
h : p₂ ≠ p₁
⊢ InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) + InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃) +
      InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) =
    π

Tactic:
← angle_neg_neg (p₁ -ᵥ p₃),

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
h : p₂ ≠ p₁
⊢ InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) + InnerProductGeometry.angle (-(p₁ -ᵥ p₃)) (-(p₂ -ᵥ p₃)) +
      InnerProductGeometry.angle (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))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ dist (s.excenter signs) ↑((s.faceOpposite i).orthogonalProjectionSpan (s.excenter signs)) = s.exradius signs

Tactic:
← abs_signedInfDist_eq_dist_of_mem_affineSpan_range i h.excenter_mem_affineSpan_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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ |(s.signedInfDist i) (s.excenter signs)| = s.exradius signs
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
⊢ ∀ i2 ∈ univ, i2 ≠ circumcenterIndex → circumcenterWeightsWithCircumcenter n i2 = 0

Tactic:
rintro ⟨i⟩ _ hn <;> tauto

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

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✝ : NeZero 1
s : Simplex ℝ P 1
signs : Finset (Fin (1 + 1))
h : s.ExcenterExists signs
i j : Fin (1 + 1)
hij : s.points i.rev = s.points j.rev
hne : ¬i = j
⊢ i = j.rev

Tactic:
clear hij

Goal state after:
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✝ : NeZero 1
s : Simplex ℝ P 1
signs : Finset (Fin (1 + 1))
h : s.ExcenterExists signs
i j : Fin (1 + 1)
hne : ¬i = j
⊢ i = j.rev
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
inst✝ : NeZero 1
s : Simplex ℝ P 1
signs : Finset (Fin (1 + 1))
h : s.ExcenterExists signs
i j : Fin (1 + 1)
hij : s.points i.rev = s.points j.rev
hne : ¬i = j
⊢ j = i.rev

Tactic:
clear hij

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✝ : NeZero 1
s : Simplex ℝ P 1
signs : Finset (Fin (1 + 1))
h : s.ExcenterExists signs
i j : Fin (1 + 1)
hne : ¬i = j
⊢ j = i.rev
Module: Mathlib.Geometry.Euclidean.Incenter

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : n = 1
⊢ False

Tactic:
subst hn1
    rw [s.touchpoint_eq_point_rev signs i, s.touchpoint_eq_point_rev signs j] at hij
    apply s.independent.injective.ne hne
    convert! hij.symm <;> clear hij <;> decide +revert

Goal state after: