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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
⊢ Irreducible (f.minpolyX ↥K⟮f⟯)

Tactic:
have : UniqueFactorizationMonoid K[f] :=
    (f.transcendental_of_ne_C hf).uniqueFactorizationMonoid_adjoin
  rw [← f.minpolyX_map K[f] K⟮f⟯,
    ← IsPrimitive.irreducible_iff_irreducible_map_fraction_map]
  · exact f.irreducible_minpolyX' hf
  · apply (f.irreducible_minpolyX' hf).isPrimitive
    intro H
    have := natDegree_map_le (f := algebraMap K[f] K⟮f⟯) (p := f.minpolyX K[f])
    rw [f.minpolyX_map K[f] K⟮f⟯, H, nonpos_iff_eq_zero, f.natDegree_minpolyX,
      Nat.max_eq_zero_iff, ← f.eq_C_iff] at this
    exact hf this

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 ≠ ⊥
⊢ (algebraMap K[X] K⟮X⟯) (Φ' E).content ≠ 0

Tactic:
· rw [ne_eq, FaithfulSMul.algebraMap_eq_zero_iff, content_eq_zero_iff]
    exact Φ'_ne_zero h

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
⊢ (inftyValuation F) (1 / RatFunc.X) = exp (-1)

Tactic:
rw [one_div, ← zpow_neg_one, inftyValuation.X_zpow]

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F₁ F₂ : PointedCone R M
h₁ : F₂.IsFaceOf F₁
h₂ : F₁.IsFaceOf C
⊢ F₂.IsFaceOf C

Tactic:
refine ⟨h₁.1.trans h₂.1, fun hx hy ha hxy ↦ h₁.2 (h₂.2 hx hy ha (h₁.le hxy)) ?_ ha hxy⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F₁ F₂ : PointedCone R M
h₁ : F₂.IsFaceOf F₁
h₂ : F₁.IsFaceOf C
x✝ y✝ : M
a✝ : R
hx : x✝ ∈ C
hy : y✝ ∈ C
ha : 0 < a✝
hxy : a✝ • x✝ + y✝ ∈ F₂
⊢ y✝ ∈ F₁
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case mem_of_smul_add_mem
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
x y : M
a : R
hx : x ∈ C₁
⊢ y ∈ C₁ → 0 < a → ∀ (x_1 : N), (a • x + y, x_1) ∈ F → ∃ x_2, (x, x_2) ∈ F

Tactic:
hy

Goal state after:
case mem_of_smul_add_mem
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : DivisionRing R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
C₁ : PointedCone R M
C₂ : PointedCone R N
F : PointedCone R (M × N)
hF : F.IsFaceOf (prod C₁ C₂)
x y : M
a : R
hx : x ∈ C₁
hy : y ∈ C₁
⊢ 0 < a → ∀ (x_1 : N), (a • x + y, x_1) ∈ F → ∃ x_2, (x, x_2) ∈ F
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 : ↥s
⊢ ↑p ∈ s

Tactic:
exact p.2

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

Goal state before:
pp: case «0»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos])
      ((o.basisRightAngleRotation x hx) ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
Matrix.toLin_self

Goal state after:
case «0»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ∑ j, !![θ.cos, -θ.sin; θ.sin, θ.cos] j ((fun i ↦ i) ⟨0, ⋯⟩) • (o.basisRightAngleRotation x hx) j
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: case «1»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ((Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx)) !![θ.cos, -θ.sin; θ.sin, θ.cos])
      ((o.basisRightAngleRotation x hx) ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
Matrix.toLin_self

Goal state after:
case «1»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
x : V
hx : x ≠ 0
⊢ ↑(o.rotation θ).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ∑ j, !![θ.cos, -θ.sin; θ.sin, θ.cos] j ((fun i ↦ i) ⟨1, ⋯⟩) • (o.basisRightAngleRotation x hx) j
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₂ : P
⊢ dist p₁ ((reflection s) p₂) = dist ((reflection s) p₁) p₂

Tactic:
by
  conv_lhs => rw [← reflection_reflection s p₁]
  exact (reflection s).dist_map _ _

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
hp₁ : p₁ ∈ s
p₂ : P
⊢ dist p₁ ((reflection s) p₂) = dist p₁ p₂

Tactic:
← reflection_eq_self_iff p₁

Goal state after:
𝕜 : 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
hp₁ : (reflection s) p₁ = p₁
p₂ : P
⊢ dist p₁ ((reflection s) p₂) = dist p₁ p₂
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: case mp
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (o.rotation (o.oangle x y)) x = y → ‖x‖ = ‖y‖

pp: case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ ‖x‖ = ‖y‖ → (o.rotation (o.oangle x y)) x = y

Tactic:
· intro h
    rw [← h, LinearIsometryEquiv.norm_map]

Goal state after:
case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ ‖x‖ = ‖y‖ → (o.rotation (o.oangle x y)) x = y
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₀ p₀ p = π / 2

Tactic:
unfold angle
  rw [vsub_self]
  exact angle_zero_left _

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₄ p₅ : P
hapc : ∠ p₁ p₅ p₃ = π
hbpd : ∠ p₂ p₅ p₄ = π
⊢ ∠ p₁ p₅ p₂ = ∠ p₃ p₅ p₄

Tactic:
by
  linarith [angle_add_angle_eq_pi_of_angle_eq_pi p₁ hbpd, angle_comm p₄ p₅ p₁,
    angle_add_angle_eq_pi_of_angle_eq_pi p₄ hapc, angle_comm p₄ p₅ p₃]

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 : V
h : (o.oangle x y).sign = 1
⊢ o.oangle x y = ↑(InnerProductGeometry.angle x y)

Tactic:
by_cases hx : x = 0; · simp [hx] at h
  by_cases hy : y = 0; · simp [hy] at h
  refine (o.oangle_eq_angle_or_eq_neg_angle hx hy).resolve_right ?_
  intro hxy
  rw [hxy, Real.Angle.sign_neg, neg_eq_iff_eq_neg, ← SignType.neg_iff, ← not_le] at h
  exact h (Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi (InnerProductGeometry.angle_nonneg _ _)
    (InnerProductGeometry.angle_le_pi _ _))

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).cos * ‖x + y‖ = ‖x‖

Tactic:
have hs : (o.oangle x (x + y)).sign = 1 := by
    rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
  rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    InnerProductGeometry.cos_angle_add_mul_norm_of_inner_eq_zero
      (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).cos * ‖x + y‖ = ‖x‖

Tactic:
by
  have hs : (o.oangle x (x + y)).sign = 1 := by
    rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]
  rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    InnerProductGeometry.cos_angle_add_mul_norm_of_inner_eq_zero
      (o.inner_eq_zero_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
a b p : P
hab : a ≠ b
hp : p ∈ perpBisector a b
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b) s)
⊢ ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a) + ⅟2 • (a -ᵥ b)⟫ = 0

Tactic:
← neg_vsub_eq_vsub_rev b a,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p : P
hab : a ≠ b
hp : p ∈ perpBisector a b
s : ℝ
h_wbtw : Wbtw ℝ a b ((AffineMap.lineMap a b) s)
⊢ ⟪p -ᵥ midpoint ℝ a b, s • (b -ᵥ a) + ⅟2 • -(b -ᵥ a)⟫ = 0
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p₁ p₂ p₃ p₄ : P
hp₁₃ : Sbtw ℝ p₁ p p₃
hp₂₄ : Sbtw ℝ p₂ p p₄
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign

Tactic:
by
  rw [← Sbtw.oangle_eq_right hp₂₄.symm, Sbtw.oangle_sign_eq _ hp₁₃, ← oangle_rotate_sign,
    Sbtw.oangle_sign_eq _ hp₂₄.symm, Sbtw.oangle_eq_left hp₁₃.symm]

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

Goal state before:
pp: P : Type u_2
inst✝ : MetricSpace P
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ s.radius = dist s.center p₂

Tactic:
mem_sphere'.1 hp₂

Goal state after:
P : Type u_2
inst✝ : MetricSpace P
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ s.radius = s.radius
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

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
s : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ Set.range ![p₁, p₂, p₃] ⊆ s

pp: case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ Function.Injective ![p₁, p₂, p₃]

Tactic:
· simp [h₁, h₂, h₃, Set.insert_subset_iff]

Goal state after:
case refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Cospherical s
p₁ p₂ p₃ : P
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
h₃ : p₃ ∈ s
h₁₂ : p₁ ≠ p₂
h₁₃ : p₁ ≠ p₃
h₂₃ : p₂ ≠ p₃
⊢ Function.Injective ![p₁, p₂, p₃]
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
⊢ s.orthRadius p ≤ s.orthRadius q ↔ p = q ∨ q = s.center

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · have h' := direction_le h
    simp only [direction_orthRadius] at h'
    have h'' := Submodule.orthogonal_le h'
    simp only [Submodule.orthogonal_orthogonal, Submodule.span_singleton_le_iff_mem,
      Submodule.mem_span_singleton] at h''
    rcases h'' with ⟨r, hr⟩
    have hp : p ∈ s.orthRadius q := h (s.self_mem_orthRadius p)
    rw [mem_orthRadius_iff_inner_left, ← vsub_sub_vsub_cancel_right p q s.center, ← hr,
      inner_sub_left, real_inner_smul_left, real_inner_smul_right, ← mul_assoc, ← sub_mul,
      mul_eq_zero] at hp
    rcases hp with hp | hp
    · nth_rw 1 [← one_mul r] at hp
      rw [← sub_mul, mul_eq_zero] at hp
      rcases hp with hp | rfl
      · rw [sub_eq_zero] at hp
        rw [← hp, one_smul, vsub_left_cancel_iff] at hr
        exact .inl hr
      · rw [zero_smul, eq_comm, vsub_eq_zero_iff_eq] at hr
        exact .inr hr
    · simp only [inner_self_eq_zero, vsub_eq_zero_iff_eq] at hp
      rw [hp, vsub_self, smul_zero, eq_comm, vsub_eq_zero_iff_eq] at hr
      exact .inr hr
  · rcases h with rfl | rfl <;> simp

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

Goal state before:
pp: case inr.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
hp : p ∈ s
q : P
hqs : q ∈ s
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
hpar : s.orthRadius q ∥ s.orthRadius p
hqas : q ∈ s.orthRadius q
hqo : s.orthRadius q ≤ s.orthRadius q
hr0 : r ≠ 0
⊢ s.orthRadius q = s.orthRadius p ∨ s.orthRadius q = s.orthRadius ((Equiv.pointReflection s.center) p)

Tactic:
have hr' : ‖q -ᵥ s.center‖ = ‖r • (p -ᵥ s.center)‖ := by
      rw [hr]
    simp_rw [norm_smul, Real.norm_eq_abs, ← dist_eq_norm_vsub, mem_sphere.1 hp,
      mem_sphere.1 hqs, right_eq_mul₀ hrad] at hr'
    rcases eq_or_eq_neg_of_abs_eq hr' with rfl | rfl
    · simp_all
    · right
      convert! rfl
      rw [← eq_vadd_iff_vsub_eq] at hr
      rw [hr]
      simp [Equiv.pointReflection_apply]

Goal state after:
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₃
p : P
h₁ : dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₂).orthogonalProjectionSpan p)
h₂ : dist p ↑((faceOpposite t i₁).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p)
⊢ Fintype.card (Fin (2 + 1)) = finrank ℝ V + 1

Tactic:
simp [hd2.out]

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

Goal state before:
pp: case h.left.right
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✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
p₁ : P
hp₁ : p₁ ∈ insert p ps
⊢ dist p₁ { center := cc₂, radius := cr₂ }.center * dist p₁ { center := cc₂, radius := cr₂ }.center =
    cr * cr + ycc₂ * ycc₂

Tactic:
rcases hp₁ with hp₁ | hp₁

Goal state after:
case h.left.right.inl
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✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
p₁ : P
hp₁ : p₁ = p
⊢ dist p₁ { center := cc₂, radius := cr₂ }.center * dist p₁ { center := cc₂, radius := cr₂ }.center =
    cr * cr + ycc₂ * ycc₂

case h.left.right.inr
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✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
p₁ : P
hp₁ : p₁ ∈ ps
⊢ dist p₁ { center := cc₂, radius := cr₂ }.center * dist p₁ { center := cc₂, radius := cr₂ }.center =
    cr * cr + ycc₂ * ycc₂
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 : ↥(s.orthRadius p).direction
hv : ∀ (w : ↥(s.orthRadius p).direction), ∃ c, c • v = w
hv0 : ↑v ≠ 0
⊢ (Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)).ncard = 2

Tactic:
inter_orthRadius_eq_of_dist_le_radius hp.le hpc (by simpa using v.property) hv0,

Goal state after:
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 : ↥(s.orthRadius p).direction
hv : ∀ (w : ↥(s.orthRadius p).direction), ∃ c, c • v = w
hv0 : ↑v ≠ 0
⊢ {(√(s.radius ^ 2 - dist p s.center ^ 2) / ‖↑v‖) • ↑v +ᵥ p,
        -(√(s.radius ^ 2 - dist p s.center ^ 2) / ‖↑v‖) • ↑v +ᵥ p}.ncard =
    2
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 : ↥(s.orthRadius p).direction
hv : ∀ (w : ↥(s.orthRadius p).direction), ∃ c, c • v = w
hv0 : ↑v ≠ 0
⊢ {(√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • ↑v +ᵥ p,
        -((√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • ↑v) +ᵥ p}.ncard =
    2

Tactic:
Set.ncard_pair

Goal state after:
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 : ↥(s.orthRadius p).direction
hv : ∀ (w : ↥(s.orthRadius p).direction), ∃ c, c • v = w
hv0 : ↑v ≠ 0
⊢ 2 = 2

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 : ↥(s.orthRadius p).direction
hv : ∀ (w : ↥(s.orthRadius p).direction), ∃ c, c • v = w
hv0 : ↑v ≠ 0
⊢ (√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • ↑v +ᵥ p ≠ -((√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • ↑v) +ᵥ p
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f' : E →L[ℝ] F
h : IsConformalMap f'
u v : E
⊢ angle (f' u) (f' v) = angle u v

Tactic:
obtain ⟨c, hc, li, rfl⟩ := h

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
u v : E
c : ℝ
hc : c ≠ 0
li : E →ₗᵢ[ℝ] F
⊢ angle ((c • li.toContinuousLinearMap) u) ((c • li.toContinuousLinearMap) v) = angle u v
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * √(1 + (∡ p₂ p₁ s.center).tan ^ 2) =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁ + (∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖

Tactic:
← mul_self_inj (by positivity) (by positivity),

Goal state after:
V : Type u_3
P : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * √(1 + (∡ p₂ p₁ s.center).tan ^ 2) *
      (‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ * √(1 + (∡ p₂ p₁ s.center).tan ^ 2)) =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁ + (∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖ *
      ‖midpoint ℝ p₁ p₂ -ᵥ p₁ + (∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖