mathlib-initiative/mathlib-tactics huggingface dataset:
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
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
L1 L2 : IntermediateField F E
h1 : IsPurelyInseparable F ↥L1
h2 : IsPurelyInseparable F ↥L2
⊢ IsPurelyInseparable F ↥(L1 ⊔ L2)

Tactic:
rw [← le_perfectClosure_iff] at h1 h2 ⊢

Goal state after:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
L1 L2 : IntermediateField F E
h1 : L1 ≤ perfectClosure F E
h2 : L2 ≤ perfectClosure F E
⊢ L1 ⊔ L2 ≤ perfectClosure F E
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 n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
⊢ Submodule.span F (Set.range fun x ↦ v x ^ q ^ n) =
    Subalgebra.toSubmodule (Algebra.adjoin F (Set.range fun x ↦ x ^ q ^ n))

Tactic:
Algebra.adjoin_eq_span

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
⊢ Submodule.span F (Set.range fun x ↦ v x ^ q ^ n) = Submodule.span F ↑(Submonoid.closure (Set.range fun x ↦ x ^ q ^ n))
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 : ℕ
hF : ExpChar F q
inst✝ : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
hai : IsIntegral F a
hapi : IsIntegral F ((iterateFrobenius E q n) a)
⊢ minpoly F ((iterateFrobenius E q n) a) = Polynomial.map (iterateFrobenius F q n) (minpoly F a)

Tactic:
symm

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q : ℕ
hF : ExpChar F q
inst✝ : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
hai : IsIntegral F a
hapi : IsIntegral F ((iterateFrobenius E q n) a)
⊢ Polynomial.map (iterateFrobenius F q n) (minpoly F a) = minpoly F ((iterateFrobenius E q n) a)
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ ↑(x.num * y.denom + x.denom * y.num).natDegree - ↑(x.denom * y.denom).natDegree ≤
    max (↑(x.num * y.denom).natDegree - ↑(y.denom * x.denom).natDegree) y.intDegree

Tactic:
mul_comm y.denom,

Goal state after:
case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ ↑(x.num * y.denom + x.denom * y.num).natDegree - ↑(x.denom * y.denom).natDegree ≤
    max (↑(x.num * y.denom).natDegree - ↑(x.denom * y.denom).natDegree) y.intDegree
Module: Mathlib.FieldTheory.Relrank

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

Tactic:
simp_rw [relrank]

Goal state after:
E : Type v
inst✝ : Field E
A B C : Subfield E
h : A ⊓ C = B ⊓ C
⊢ Module.rank ↥(A ⊓ C) ↥(extendScalars ⋯) = Module.rank ↥(B ⊓ C) ↥(extendScalars ⋯)
Module: Mathlib.FieldTheory.Relrank

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

Tactic:
by
  simp_rw [relrank]
  congr!

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 : (Bivariate.swap (Q₁ h) * Bivariate.swap (Φ E)).natDegree = (Bivariate.swap (θ E)).natDegree
⊢ (Bivariate.swap (Q₁ h)).natDegree = 0

Tactic:
natDegree_mul
    ((map_ne_zero_iff _ Bivariate.swap.injective).mpr (Q₁_ne_zero h))
    ((map_ne_zero_iff _ Bivariate.swap.injective).mpr (Φ_ne_zero h))

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : (Bivariate.swap (Q₁ h)).natDegree + (Bivariate.swap (Φ E)).natDegree = (Bivariate.swap (θ E)).natDegree
⊢ (Bivariate.swap (Q₁ h)).natDegree = 0
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: case mpr
𝕜 : 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
h : p ∈ s
hp : p ∈ {↑((orthogonalProjection s) p)}
⊢ ↑((orthogonalProjection s) p) = p

Tactic:
symm

Goal state after:
case mpr
𝕜 : 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
h : p ∈ s
hp : p ∈ {↑((orthogonalProjection s) p)}
⊢ p = ↑((orthogonalProjection s) p)
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
⊢ 1 ≠ 0

Tactic:
decide

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
⊢ -1 ≠ 0

Tactic:
decide

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
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : NormedAddCommGroup V₂
inst✝⁷ : InnerProductSpace 𝕜 V₂
inst✝⁶ : MetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : MetricSpace P₂
inst✝³ : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst✝² : Nonempty ↥s
inst✝¹ : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst✝ : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
⊢ f p -ᵥ f ↑((orthogonalProjection s) p) ∈ (Submodule.map f.linearIsometry.toLinearMap s.direction)ᗮ

Tactic:
← AffineIsometry.coe_toAffineMap,

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace 𝕜 V
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : NormedAddCommGroup V₂
inst✝⁷ : InnerProductSpace 𝕜 V₂
inst✝⁶ : MetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : MetricSpace P₂
inst✝³ : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst✝² : Nonempty ↥s
inst✝¹ : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst✝ : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
⊢ f.toAffineMap p -ᵥ f.toAffineMap ↑((orthogonalProjection s) p) ∈
    (Submodule.map f.linearIsometry.toLinearMap s.direction)ᗮ
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
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[ℝ] P₂
p₁ p₂ p₃ : P
⊢ ∠ (f p₁) (f p₂) (f p₃) = ∠ p₁ p₂ p₃

Tactic:
angle,

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[ℝ] P₂
p₁ p₂ p₃ : P
⊢ InnerProductGeometry.angle (f p₁ -ᵥ f p₂) (f p₃ -ᵥ f p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
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
r : ℝ
h : r ≠ 0
⊢ ∠ ((AffineMap.homothety p r) p₁) ((AffineMap.homothety p r) p₂) ((AffineMap.homothety p r) p₃) = ∠ p₁ p₂ p₃

Tactic:
angle,

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
r : ℝ
h : r ≠ 0
⊢ InnerProductGeometry.angle ((AffineMap.homothety p r) p₁ -ᵥ (AffineMap.homothety p r) p₂)
      ((AffineMap.homothety p r) p₃ -ᵥ (AffineMap.homothety p r) p₂) =
    InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle x y = θ ↔ (x ≠ 0 ∧ y ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • (o.rotation θ) x) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
o.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero hx hy

Goal state after:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
hx : ¬x = 0
hy : ¬y = 0
⊢ (∃ r, 0 < r ∧ y = r • (o.rotation θ) x) ↔
    (x ≠ 0 ∧ y ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • (o.rotation θ) x) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

Goal state before:
pp: case h
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
i : Fin 2
⊢ ↑f.toLinearEquiv ((o.basisRightAngleRotation x hx) i) =
    ↑(o.rotation (o.oangle x (f x))).toLinearEquiv ((o.basisRightAngleRotation x hx) i)

Tactic:
symm

Goal state after:
case h
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
i : Fin 2
⊢ ↑(o.rotation (o.oangle x (f x))).toLinearEquiv ((o.basisRightAngleRotation x hx) i) =
    ↑f.toLinearEquiv ((o.basisRightAngleRotation x hx) i)
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case a
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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
⊢ |⟪s.points i -ᵥ s.altitudeFoot i, s.points j -ᵥ s.altitudeFoot j⟫| ≠ s.height i * s.height j

Tactic:
simp_rw [height, dist_eq_norm_vsub]
    rw [← Real.norm_eq_abs, ne_eq, norm_inner_eq_norm_iff (by simp) (by simp)]
    rintro ⟨r, hr, h⟩
    suffices s.points j -ᵥ s.altitudeFoot j = 0 by
      simp at this
    rw [← Submodule.mem_bot ℝ,
      ← Submodule.inf_orthogonal_eq_bot (vectorSpan ℝ (Set.range s.points))]
    refine ⟨vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan
      (mem_affineSpan _ (Set.mem_range_self _)) ?_, ?_⟩
    · refine SetLike.le_def.1 (affineSpan_mono _ ?_) (Subtype.property _)
      simp
    · rw [SetLike.mem_coe]
      have hk : ∃ k, k ≠ i ∧ k ≠ j := Fin.exists_ne_and_ne_of_two_lt i j
        (by linarith only [Nat.AtLeastTwo.one_lt (n := n)])
      have hs : vectorSpan ℝ (Set.range s.points) =
          vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔
            vectorSpan ℝ (Set.range (s.faceOpposite j).points) := by
        rcases hk with ⟨k, hki, hkj⟩
        have hki' : s.points k ∈ Set.range (s.faceOpposite i).points := by
          rw [range_faceOpposite_points]
          exact Set.mem_image_of_mem _ hki
        have hkj' : s.points k ∈ Set.range (s.faceOpposite j).points := by
          rw [range_faceOpposite_points]
          exact Set.mem_image_of_mem _ hkj
        have hs :
            Set.range s.points =
              Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points := by
          simp only [range_faceOpposite_points, ← Set.image_union]
          simp_rw [← Set.image_univ, ← Set.compl_inter]
          rw [Set.inter_singleton_eq_empty.mpr ?_, Set.compl_empty]
          simpa using hij.symm
        convert! AffineSubspace.vectorSpan_union_of_mem_of_mem ℝ hki' hkj'
      rw [hs, ← Submodule.inf_orthogonal, Submodule.mem_inf]
      refine ⟨?_, ?_⟩
      · rw [h, ← direction_affineSpan]
        exact Submodule.smul_mem _ _ (vsub_orthogonalProjection_mem_direction_orthogonal _ _)
      · rw [← direction_affineSpan]
        exact vsub_orthogonalProjection_mem_direction_orthogonal _ _

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
h : Sbtw ℝ p₁ p₂ p₃
⊢ ∠ p₁ p₂ p₃ = π

Tactic:
angle,

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 : Sbtw ℝ p₁ p₂ p₃
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

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

Tactic:
angle,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ Real.arccos (⟪x, x + y⟫ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
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
h : (∡ p₁ p₂ p₃).sign = 1
⊢ 1 ≠ 0

Tactic:
decide

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₂ p₃ = π → Sbtw ℝ p₁ p₂ p₃

Tactic:
angle,

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
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π → Sbtw ℝ p₁ p₂ p₃
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
h : (∡ p₁ p₂ p₃).sign = -1
⊢ -1 ≠ 0

Tactic:
decide

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
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : p₂ ≠ p₁
⊢ ∠ p₂ p₁ p₃ = 0

Tactic:
angle,

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 : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : p₂ ≠ p₁
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₁) (p₃ -ᵥ p₁) = 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₂ p₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ ↑π ↔ AffineIndependent ℝ ![p₁, p₂, p₃]

Tactic:
rw [oangle, o.oangle_ne_zero_and_ne_pi_iff_linearIndependent,
    affineIndependent_iff_linearIndependent_vsub ℝ _ (1 : Fin 3), ←
    linearIndependent_equiv (finSuccAboveEquiv (1 : Fin 3))]
  convert! Iff.rfl
  ext i
  fin_cases i <;> rfl

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

Tactic:
inv_mul_cancel₀ hr0',

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

Goal state before:
pp: case mp
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ ∠ p₁ p₂ p₃ = 0 → p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁

Tactic:
angle,

Goal state after:
case mp
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
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = 0 → p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
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
h : dist p₁ p₂ = dist p₁ p₃
⊢ ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁

Tactic:
dist_eq_norm_vsub V

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
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ∡ p₁ p₂ p₃ = ∡ p₂ p₃ p₁
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
hn : p₂ ≠ p₃
h : dist p₁ p₂ = dist p₁ p₃
⊢ ∡ p₃ p₁ p₂ = ↑π - 2 • ∡ p₁ p₂ p₃

Tactic:
dist_eq_norm_vsub V

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
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ∡ p₃ p₁ p₂ = ↑π - 2 • ∡ p₁ p₂ p₃
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₃‖ ↔ ∠ p₁ p₂ p₃ = π / 2

Tactic:
angle,

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₃‖ ↔
    InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π / 2
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
h : ∠ p₁ p₂ p₃ = π / 2
⊢ ∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)

Tactic:
angle,

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 : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π / 2
⊢ ∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
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
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
⊢ ∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)

Tactic:
angle,

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₃, p₁ -ᵥ p₂⟫ = 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
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
h : dist p₁ p₂ = dist p₁ p₃
⊢ |(∡ p₁ p₂ p₃).toReal| < π / 2

Tactic:
dist_eq_norm_vsub V

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
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ |(∡ p₁ p₂ p₃).toReal| < π / 2
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
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)

Tactic:
angle,

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 : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
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
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)

Tactic:
angle,

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₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
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
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)

Tactic:
angle,

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 : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π / 2
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
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
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)

Tactic:
angle,

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₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₁ -ᵥ p₃) = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
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
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ 0 < ∠ p₂ p₃ p₁

Tactic:
angle,

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 : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ 0 < ∠ p₂ p₃ p₁