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

Goal state before:
pp: case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (⇑(frobenius K p))^[n + z] x = (⇑(frobenius K p))^[m + z] y
⊢ mk K p (n + z + m, (⇑(frobenius K p))^[n + z] x) = mk K p (n, y)

Tactic:
R.sound K p (m + z) n y _ rfl,

Goal state after:
case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
m : ℕ
x : K
n : ℕ
y : K
z : ℕ
H : (⇑(frobenius K p))^[n + z] x = (⇑(frobenius K p))^[m + z] y
⊢ mk K p (n + z + m, (⇑(frobenius K p))^[n + z] x) = mk K p (m + z + n, (⇑(frobenius K p))^[m + z] y)
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
⊢ Function.Bijective fun x ↦ ↑(g ↑x)

Tactic:
Fintype.bijective_iff_surjective_and_card

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this : Fintype (G ⧸ H)
⊢ (Function.Surjective fun x ↦ ↑(g ↑x)) ∧ Fintype.card ↥s = Fintype.card (G ⧸ H)
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case adjoin_rootSet'
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
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ Algebra.adjoin K ((X ^ finrank K L - C a).rootSet L) = ⊤

Tactic:
rw [eq_top_iff, ← IntermediateField.top_toSubalgebra, ← hα,
      IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.of_finite K α)]
    apply Algebra.adjoin_mono
    rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero finrank_pos a),
      aeval_def, eval₂_sub, eval₂_X_pow, eval₂_C, ha, sub_self]

Goal state after:
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
h : ∀ i ∈ s, (H i).FiniteIndex → s.card < (H i).index
x✝ : s = ∅ ∨ s.Nonempty
⊢ ∑ i ∈ s, (↑(H i).index)⁻¹ < 1

Tactic:
cases s.eq_empty_or_nonempty with

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
A : Subalgebra R S
x y : ↥⊥
a b : ↥A
⊢ (toSubmodule A).lTensorOne ((x * y) ⊗ₜ[R] (a * b)) =
    (toSubmodule A).lTensorOne (x ⊗ₜ[R] a) * (toSubmodule A).lTensorOne (y ⊗ₜ[R] b)

Tactic:
obtain ⟨x', hx⟩ := Algebra.mem_bot.1 x.2

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
A : Subalgebra R S
x y : ↥⊥
a b : ↥A
x' : R
hx : (algebraMap R S) x' = ↑x
⊢ (toSubmodule A).lTensorOne ((x * y) ⊗ₜ[R] (a * b)) =
    (toSubmodule A).lTensorOne (x ⊗ₜ[R] a) * (toSubmodule A).lTensorOne (y ⊗ₜ[R] b)
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
A : Subalgebra R S
a b : ↥A
x y : ↥⊥
⊢ (toSubmodule A).rTensorOne ((a * b) ⊗ₜ[R] (x * y)) =
    (toSubmodule A).rTensorOne (a ⊗ₜ[R] x) * (toSubmodule A).rTensorOne (b ⊗ₜ[R] y)

Tactic:
obtain ⟨x', hx⟩ := Algebra.mem_bot.1 x.2

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
A : Subalgebra R S
a b : ↥A
x y : ↥⊥
x' : R
hx : (algebraMap R S) x' = ↑x
⊢ (toSubmodule A).rTensorOne ((a * b) ⊗ₜ[R] (x * y)) =
    (toSubmodule A).rTensorOne (a ⊗ₜ[R] x) * (toSubmodule A).rTensorOne (b ⊗ₜ[R] y)
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: case prime
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
n : ℕ
h : a ^ ringExpChar K ^ n ∈ (algebraMap K L).range
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
⊢ elemExponent K a ≤ n

Tactic:
· obtain ⟨y, hy⟩ := RingHom.mem_range.mp <| h
    let f := X ^ ringExpChar K ^ n - C y
    have hf₁ : f.aeval a = 0 := by rwa [map_sub, aeval_C, aeval_X_pow, sub_eq_zero, eq_comm]
    have hf₂ : f.Monic := monic_X_pow_sub_C y <| Nat.pos_iff_ne_zero.mp <| expChar_pow_pos K _ _
    have hf₃ : f.natDegree = ringExpChar K ^ n := by
      rw [natDegree_sub_C, natDegree_pow, natDegree_X, mul_one]
    exact (Nat.pow_le_pow_iff_right <| Nat.Prime.one_lt hp).mp <|
      ringExpChar.eq K p ▸ hf₃ ▸ minpoly_natDegree_eq K a ▸
      natDegree_le_natDegree (minpoly.min K a hf₂ hf₁)

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝³ : Free R ↥A
inst✝² : Flat R ↥B
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ Module.rank ↥B ↥(toSubmodule (Algebra.adjoin ↥B ↑A)) = Cardinal.mk (Free.ChooseBasisIndex R ↥A)

Tactic:
A.adjoin_eq_span_basis B (Module.Free.chooseBasis R A)

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝³ : Free R ↥A
inst✝² : Flat R ↥B
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ Module.rank ↥B ↥(Submodule.span (↥B) (Set.range fun i ↦ ↑((Free.chooseBasis R ↥A) i))) =
    Cardinal.mk (Free.ChooseBasisIndex R ↥A)
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

Goal state before:
pp: case pos
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
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsPurelyInseparable F E
ι : Type u_1
v : ι → K
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
q : ℕ
h✝ : ExpChar F q
this✝ : ExpChar K q
l : ι →₀ E
hl : (Finsupp.linearCombination E v) l = 0
i✝ : ι
f : ι → ℕ
hf : ∀ (i : ι), l i ^ q ^ f i ∈ (algebraMap F E).range
n : ℕ := l.support.sup f
this : q ^ n ≠ 0
i : ι
hs : i ∈ l.support
⊢ l i ^ q ^ n ∈ (algebraMap F E).range

Tactic:
convert! pow_mem (hf i) (q ^ (n - f i)) using 1
      rw [← pow_mul, ← pow_add, Nat.add_sub_of_le (Finset.le_sup hs)]

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

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
inst✝ : FiniteDimensional F E
h₁ : A.LinearDisjoint B.toSubalgebra
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ (Algebra.trace (↥A) E) ((algebraMap (↥B) E) x) = (algebraMap F ↥A) ((Algebra.trace F ↥B) x)

Tactic:
refine h₁.trace_algebraMap ?_ x

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
A B : IntermediateField F E
inst✝ : FiniteDimensional F E
h₁ : A.LinearDisjoint B.toSubalgebra
h₂ : A ⊔ B = ⊤
x : ↥B
⊢ A.toSubalgebra ⊔ B.toSubalgebra = ⊤
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝⁹ : Field K
f : K⟮X⟯
A : Type u_2
inst✝⁸ : CommRing A
inst✝⁷ : Algebra K A
inst✝⁶ : Algebra (↥K[f]) A
B : Type u_3
inst✝⁵ : CommRing B
inst✝⁴ : Algebra K B
inst✝³ : Algebra (↥K[f]) B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower K A B
inst✝ : IsScalarTower (↥K[f]) A B
⊢ Polynomial.map (algebraMap A B) (f.minpolyX A) = f.minpolyX B

Tactic:
simp [minpolyX, Polynomial.map_map, ← IsScalarTower.algebraMap_eq,
    ← IsScalarTower.algebraMap_apply]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
s : K[X]
hs : s ≠ 0
⊢ x.num * s * x.denom = x.num * (s * x.denom)

Tactic:
mul_assoc

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
s : K[X]
hs : s ≠ 0
⊢ x.num * (s * x.denom) = x.num * (s * x.denom)
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
c : K
hf₁ : C c ∈ E
hf₂ : C c ∉ ⊥
⊢ False

Tactic:
exact hf₂ ⟨c, rfl⟩

Goal state after:
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B : Subfield E
⊢ (extendScalars ⋯).toSubfield = ⊥.toSubfield ↔ B ≤ A

Tactic:
extendScalars_toSubfield,

Goal state after:
E : Type v
inst✝ : Field E
A B : Subfield E
⊢ B = ⊥.toSubfield ↔ B ≤ A
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (Φ' E).content)⁻¹ * Polynomial.C ((algebraMap K[X] K⟮X⟯) (b E)) *
      Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

Tactic:
mul_assoc

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (Φ' E).content)⁻¹ *
      (Polynomial.C ((algebraMap K[X] K⟮X⟯) (b E)) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: case inl
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H✝ : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
eq :
  (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))
H : (aeval α) (generator E).num ≠ 0
⊢ Polynomial.C ((aeval α) (g E)) ≠ Polynomial.C 0

Tactic:
rw [map_zero, ← mul_ne_zero_iff_left <| Polynomial.map_ne_zero <|
        num_ne_zero (generator_ne_zero h)]

Goal state after:
case inl
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := AlgebraicClosure K
H✝ : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
eq :
  (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))
H : (aeval α) (generator E).num ≠ 0
⊢ Polynomial.map ?m.538 (generator E).num * Polynomial.C ((aeval α) (g E)) ≠ 0

K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
F : Type u_1 := ⋯
H✝ : ¬(Polynomial.map (algebraMap K F) (Q₂ h)).degree ≤ 0
α : F
hα : (aeval α) (Q₂ h) = 0
eq :
  (Polynomial.mapRingHom (algebraMap K F)) (g E) * Polynomial.C ((aeval α) (f E)) =
    (Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E))
H : (aeval α) (generator E).num ≠ 0
⊢ K →+* F
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E = ⊥
⊢ E = K⟮generator E⟯

Tactic:
rwa [generator_eq_zero h, adjoin_zero]

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 q : P
⊢ (orthogonalProjection s) p = (orthogonalProjection s) q ↔ p -ᵥ q ∈ s.directionᗮ

Tactic:
rw [orthogonalProjection_eq_iff_mem, ← s.directionᗮ.add_mem_iff_left (x := p -ᵥ q)
    (vsub_orthogonalProjection_mem_direction_orthogonal s q)]
  simp

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

Goal state before:
pp: case mpr.refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
p : P
hne : p ≠ s.points i
h : p -ᵥ s.points i ∈ (s.altitude i).direction
⊢ finrank ℝ ↥(ℝ ∙ (p -ᵥ s.points i)) = finrank ℝ ↥(s.altitude i).direction

Tactic:
rw [finrank_direction_altitude, finrank_span_set_eq_card]
      · simp
      · exact .singleton <| by simpa using hne

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

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 : V
hx : x ≠ 0
θ : Real.Angle
⊢ o.oangle ((o.rotation θ) x) x = -θ

Tactic:
by simp [hx]

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

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 : V
hx : x ≠ 0
θ : Real.Angle
⊢ o.oangle x ((o.rotation θ) x) = θ

Tactic:
by simp [hx]

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 : V
hx : x ≠ 0
⊢ o.oangle x (-x) = ↑π

Tactic:
by
  simp [oangle_neg_right, hx]

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 : ∠ p₁ p₂ p₃ = π
⊢ ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖

Tactic:
← vsub_sub_vsub_cancel_right

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₁ -ᵥ ?p₃ - (p₃ -ᵥ ?p₃)‖ = ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖

case p₃
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
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
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ ‖p₁ -ᵥ p₃‖ = ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ ↔ ∠ p₁ p₂ p₃ = π

Tactic:
← vsub_sub_vsub_cancel_right

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
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ ‖p₁ -ᵥ ?p₃ - (p₃ -ᵥ ?p₃)‖ = ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ ↔ ∠ p₁ p₂ p₃ = π

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

Tactic:
← vsub_sub_vsub_cancel_right

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₃ = 0
⊢ ‖p₁ -ᵥ ?p₃ - (p₃ -ᵥ ?p₃)‖ = |‖p₁ -ᵥ p₂‖ - ‖p₃ -ᵥ p₂‖|

case p₃
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₃ = 0
⊢ 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
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ ‖p₁ -ᵥ p₃‖ = |‖p₁ -ᵥ p₂‖ - ‖p₃ -ᵥ p₂‖| ↔ ∠ p₁ p₂ p₃ = 0

Tactic:
← vsub_sub_vsub_cancel_right

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
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ ‖p₁ -ᵥ ?p₃ - (p₃ -ᵥ ?p₃)‖ = |‖p₁ -ᵥ p₂‖ - ‖p₃ -ᵥ p₂‖| ↔ ∠ p₁ p₂ p₃ = 0

case p₃
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
hp₁p₂ : p₁ ≠ p₂
hp₃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
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = π / 2

Tactic:
rw [norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero]
  exact inner_eq_zero_iff_angle_eq_pi_div_two x y

Goal state after:
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₃ = ↑π) ↔ ¬Collinear ℝ {p₁, p₂, p₃}

Tactic:
not_or,

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₁ p₂ p₃ = 0 ∧ ¬∡ p₁ p₂ p₃ = ↑π ↔ ¬Collinear ℝ {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
h : sin (∠ p₁ p₂ p₃) = 0
⊢ Collinear ℝ {p₁, p₂, p₃}

Tactic:
revert 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
p₁ p₂ p₃ : P
⊢ sin (∠ p₁ p₂ p₃) = 0 → Collinear ℝ {p₁, p₂, p₃}
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hn : p₂ ≠ p₃
h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖
⊢ ↑π - 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ↑π - 2 • o.oangle (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃)

Tactic:
rw [← o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]; simp

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)
⊢ ‖x‖ / (o.oangle (x + y) y).sin = ‖x + y‖

Tactic:
by
  rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
  rw [add_comm]
  exact (-o).norm_div_sin_oangle_add_right_of_oangle_eq_pi_div_two h

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

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
    inner_neg_left, neg_vsub_eq_vsub_rev] at h
  rw [← @vsub_ne_zero V, @ne_comm _ p₃, ← @vsub_ne_zero V _ _ _ p₂, or_comm] at h0
  rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
    add_comm, sin_angle_add_of_inner_eq_zero h h0]

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)
hs : (o.oangle y (y - x)).sign = 1
⊢ o.oangle y (y - x) = ↑(Real.arcsin (‖x‖ / ‖y - x‖))

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs,
    InnerProductGeometry.angle_sub_eq_arcsin_of_inner_eq_zero
      (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inl (o.right_ne_zero_of_oangle_eq_pi_div_two h))]

Goal state after:
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)
x y : V
r₁ r₂ r₃ r₄ : ℝ
hr₁ : r₁ = 0
⊢ -(SignType.sign r₂ * (SignType.sign r₃ * (o.oangle x y).sign)) =
    -(SignType.sign r₂ * SignType.sign r₃ * (o.oangle x y).sign)

Tactic:
mul_assoc

Goal state after:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ r₃ r₄ : ℝ
hr₁ : r₁ = 0
⊢ -(SignType.sign r₂ * (SignType.sign r₃ * (o.oangle x y).sign)) =
    -(SignType.sign r₂ * (SignType.sign r₃ * (o.oangle x y).sign))
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)
x y : V
h : ‖x‖ = ‖y‖
hn : x = y
⊢ |(o.oangle (y - x) y).toReal| < π / 2

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
h : ‖x‖ = ‖y‖
hn : ¬x = y
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
· simp [hn, Real.pi_pos]

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
h : ‖x‖ = ‖y‖
hn : ¬x = y
⊢ |(o.oangle (y - x) y).toReal| < π / 2
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₁).sin = dist p₁ p₂ / dist p₁ p₃

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
    sin_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)
      (Or.inl (left_ne_of_oangle_eq_pi_div_two h))]

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

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 : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : ⟪v, v⟫ ≠ 0
hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫)
⊢ ⟪v, v⟫ * (r * r) + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + 0 = 0 ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫

Tactic:
quadratic_eq_zero_iff hvi hd,

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 : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : ⟪v, v⟫ ≠ 0
hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫)
⊢ r = (-(2 * ⟪v, p₁ -ᵥ p₂⟫) + 2 * ⟪v, p₁ -ᵥ p₂⟫) / (2 * ⟪v, v⟫) ∨
      r = (-(2 * ⟪v, p₁ -ᵥ p₂⟫) - 2 * ⟪v, p₁ -ᵥ p₂⟫) / (2 * ⟪v, v⟫) ↔
    r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫