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

Goal state before:
pp: case refine_2
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)
this : (minpoly K σ.toLinearMap).IsRoot ζ
v : L
hv : End.HasEigenvector σ.toLinearMap ζ v
hv' : ∀ (n : ℕ), (σ ^ n) v = ζ ^ n • v
⊢ K⟮v⟯ = ⊤

Tactic:
· -- Since `σ` does not fix `K⟮α⟯`, `K⟮α⟯` is `L`.
    apply IsGalois.intermediateFieldEquivSubgroup.injective
    rw [map_top, eq_top_iff]
    intro σ' hσ'
    obtain ⟨n, rfl : σ ^ n = σ'⟩ := mem_powers_iff_mem_zpowers.mpr (hσ σ')
    have := hσ' ⟨v, IntermediateField.mem_adjoin_simple_self K v⟩
    simp only [AlgEquiv.smul_def, hv'] at this
    conv_rhs at this => rw [← one_smul K v]
    obtain ⟨k, rfl⟩ := hζ.dvd_of_pow_eq_one n (smul_left_injective K hv.2 this)
    rw [pow_mul, ← IsGalois.card_aut_eq_finrank, pow_card_eq_one', one_pow]
    exact one_mem _

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : ι → ↥A
i : (ι →₀ ↥B) →ₗ[R] S := Submodule.mulLeftMap (toSubmodule B) a
j : (ι →₀ ↥B) →ₗ[R] S :=
  ↑(MulOpposite.opLinearEquiv R).symm ∘ₗ
    ↑R (Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)) ∘ₗ
      ↑(Finsupp.mapRange.linearEquiv B.linearEquivOp)
a✝ : ι
x✝ : ↥B
⊢ (Submodule.mulLeftMap (toSubmodule B) a) (Finsupp.single a✝ x✝) = B.linearEquivOp x✝ • ↑(a a✝)

Tactic:
exact Submodule.mulLeftMap_apply_single _ _ _

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 : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint L
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra L K
inst✝³ : IsScalarTower F L K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsScalarTower L E K
⊢ (IntermediateField.map (IsScalarTower.toAlgHom F E K) A).LinearDisjoint L

Tactic:
rw [linearDisjoint_iff] at H ⊢
  have := H.map (IsScalarTower.toAlgHom F E K) (RingHom.injective _)
  rw [← AlgHom.range_comp] at this
  convert! this
  ext; exact IsScalarTower.algebraMap_apply L E K _

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 : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : IsField (↥A ⊗[F] L)
⊢ A.LinearDisjoint L

Tactic:
apply Subalgebra.LinearDisjoint.of_isField
  -- need these otherwise the `exact` will stuck at typeclass
  have : SMulCommClass F A A := SMulCommClass.of_commMonoid F A A
  have : SMulCommClass F A.toSubalgebra A.toSubalgebra := ‹SMulCommClass F A A›
  let : Mul (A ⊗[F] L) := Algebra.TensorProduct.instMul
  let : Mul (A.toSubalgebra ⊗[F] (IsScalarTower.toAlgHom F L E).range) :=
    Algebra.TensorProduct.instMul
  exact Algebra.TensorProduct.congr (AlgEquiv.refl : A ≃ₐ[F] A)
    (AlgEquiv.ofInjective (IsScalarTower.toAlgHom F L E) (RingHom.injective _))
      |>.symm.toMulEquiv.isField H

Goal state after:
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
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
E' : IntermediateField F E := adjoin F (Set.range v)
this : Algebra.IsSeparable F ↥E'
⊢ LinearIndependent F fun x ↦ v x ^ q ^ n

Tactic:
let v' (i : ι) : E' := ⟨v i, subset_adjoin F _ ⟨i, rfl⟩⟩

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
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
E' : IntermediateField F E := adjoin F (Set.range v)
this : Algebra.IsSeparable F ↥E'
v' : ι → ↥E' := fun i ↦ ⟨v i, ⋯⟩
⊢ LinearIndependent F fun x ↦ v x ^ q ^ n
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:
enter [1, 2]
    rw [← Polynomial.smul_eq_C_mul, algebraMap_smul, ← Φ'_map, eq_C_content_mul_primPart (Φ' E)]

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
| Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (Φ' E).content * (Φ' E).primPart)
Module: Mathlib.FieldTheory.RatFunc.Valuation

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : x = 0
⊢ (if 0 = 0 then 0 else exp (intDegree 0)) =
    (if 0 = 0 then 0 else exp (intDegree 0)) * if y = 0 then 0 else exp y.intDegree

Tactic:
if_pos (Eq.refl _),

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : x = 0
⊢ 0 = 0 * if y = 0 then 0 else exp y.intDegree
Module: Mathlib.FieldTheory.RatFunc.Valuation

Goal state before:
pp: case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : y = 0
⊢ (if 0 = 0 then 0 else exp (intDegree 0)) =
    (if x = 0 then 0 else exp x.intDegree) * if 0 = 0 then 0 else exp (intDegree 0)

Tactic:
if_pos (Eq.refl _),

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : y = 0
⊢ 0 = (if x = 0 then 0 else exp x.intDegree) * 0
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
x : EuclideanSpace ℝ (Fin n)
x✝ : x ∈ Set.univ
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
x' : EuclideanSpace ℝ (Fin n)
h :
  x' ∈ (OpenPartialHomeomorph.univBall x ε).source →
    ↑(OpenPartialHomeomorph.univBall x ε) x' ∈ (OpenPartialHomeomorph.univBall x ε).target
⊢ ↑(OpenPartialHomeomorph.univBall x ε) x' ∈ u

Tactic:
rw [OpenPartialHomeomorph.univBall_target x hε] at h

Goal state after:
X : Type u_1
d : CorePlotsOn X
n : ℕ
p : EuclideanSpace ℝ (Fin n) → X
x : EuclideanSpace ℝ (Fin n)
x✝ : x ∈ Set.univ
u : Set (EuclideanSpace ℝ (Fin n))
hu : IsOpen u
hxu : x ∈ u
hu' :
  ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
    (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ ∞ f → p ∘ f ∈ {p | d.isPlot p}
ε : ℝ
hε : ε > 0
hε' : Metric.ball x ε ⊆ u
x' : EuclideanSpace ℝ (Fin n)
h : x' ∈ (OpenPartialHomeomorph.univBall x ε).source → ↑(OpenPartialHomeomorph.univBall x ε) x' ∈ Metric.ball x ε
⊢ ↑(OpenPartialHomeomorph.univBall x ε) x' ∈ u
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case refine_3
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ ((s.map f.toAffineMap ⋯).altitude i).direction = (AffineSubspace.map f.toAffineMap (s.altitude i)).direction

Tactic:
have hf : Function.Injective f.linear := f.linearIsometry.injective

Goal state after:
case refine_3
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
hf : Function.Injective ⇑f.linear
⊢ ((s.map f.toAffineMap ⋯).altitude i).direction = (AffineSubspace.map f.toAffineMap (s.altitude i)).direction
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
⊢ (reflection s).symm = reflection s

Tactic:
by
  ext
  rw [← (reflection s).injective.eq_iff]
  simp

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

Tactic:
rw [altitudeFoot, orthogonalProjectionSpan]

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
i : Fin (n + 1)
⊢ ↑((orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points))) (s.points i)) -ᵥ s.points i ∈
    (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ
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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ o.oangle x y = θ → ∃ r, 0 < r ∧ y = r • (o.rotation θ) x

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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ (∃ r, 0 < r ∧ y = r • (o.rotation θ) x) → o.oangle x y = θ

Tactic:
· intro h
    rw [o.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero hx hy] at h
    exact ⟨‖y‖ / ‖x‖, div_pos (norm_pos_iff.2 hy) (norm_pos_iff.2 hx), h⟩

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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ (∃ r, 0 < r ∧ y = r • (o.rotation θ) x) → o.oangle 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
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
left✝ : p₂ -ᵥ p₃ ≠ 0
r : ℝ
hr : r < 0
hpr : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)

Tactic:
replace hpr : (-r + 1) • (p₃ -ᵥ p₂) = p₄ -ᵥ p₂ := by
    rw [add_smul, ← neg_vsub_eq_vsub_rev p₂ p₃, smul_neg, neg_smul, ← hpr]
    simp

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
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
left✝ : p₂ -ᵥ p₃ ≠ 0
r : ℝ
hr : r < 0
hpr : (-r + 1) • (p₃ -ᵥ p₂) = p₄ -ᵥ p₂
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
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
r : ℝ
⊢ ⟪r • x, (o.rotation ↑(π / 2)) x⟫ = 0

Tactic:
by
  rw [real_inner_comm, inner_rotation_pi_div_two_left_smul]

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

Goal state before:
pp: case neg.mpr.inr.inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
H : x ≠ 0 ∧ r • (o.rotation ↑(π / 2)) x ≠ 0
hr0 : r < 0
⊢ (∃ r_1, 0 < r_1 ∧ r • (o.rotation ↑(π / 2)) x = r_1 • (o.rotation ↑(π / 2)) x) ∨
    ∃ r_1, 0 < r_1 ∧ r • (o.rotation ↑(π / 2)) x = -r_1 • (o.rotation ↑(π / 2)) x

Tactic:
right
      use -r
      simp_all

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
hn : x ≠ y
h : ‖x‖ = ‖y‖
⊢ o.oangle y x = ↑π - 2 • o.oangle (y - x) y

Tactic:
rw [two_zsmul]
  nth_rw 1 [← o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]
  rw [eq_sub_iff_add_eq, ← oangle_neg_neg, ← add_assoc]
  have hy : y ≠ 0 := by
    rintro rfl
    rw [norm_zero, norm_eq_zero] at h
    exact hn h
  have hx : x ≠ 0 := norm_ne_zero_iff.1 (h.symm ▸ norm_ne_zero_iff.2 hy)
  convert! o.oangle_add_cyc3_neg_right (neg_ne_zero.2 hy) hx (sub_ne_zero_of_ne hn.symm) using 1
  simp

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_iff_not,

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: case mpr
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₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ → ∠ p₁ p₂ p₃ = 0

Tactic:
rintro (⟨hp₁p₂, h⟩ | ⟨hp₃p₂, h⟩)

Goal state after:
case mpr.inl
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₂
h : Wbtw ℝ p₂ p₁ p₃
⊢ ∠ p₁ p₂ p₃ = 0

case mpr.inr
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₂
h : Wbtw ℝ p₂ p₃ p₁
⊢ ∠ p₁ p₂ p₃ = 0
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₃ = 0 ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁

Tactic:
angle_eq_zero_iff_ne_and_wbtw

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₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ 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₁ p₂ p₃ = 0 ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁

Tactic:
rw [angle_eq_zero_iff_ne_and_wbtw]

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₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h0 : 0 ≤ InnerProductGeometry.angle x y
hpi : InnerProductGeometry.angle x y ≤ π
h : o.oangle x y = -↑(InnerProductGeometry.angle x y)
⊢ InnerProductGeometry.angle x y = |(o.oangle x y).toReal|

Tactic:
rw [h, eq_comm, Real.Angle.abs_toReal_neg_coe_eq_self_iff]

Goal state after:
case inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
h0 : 0 ≤ InnerProductGeometry.angle x y
hpi : InnerProductGeometry.angle x y ≤ π
h : o.oangle x y = -↑(InnerProductGeometry.angle x y)
⊢ 0 ≤ InnerProductGeometry.angle x y ∧ InnerProductGeometry.angle x y ≤ π
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: case refine_2.inr.inr.inl
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
⊢ Collinear ℝ {p₁, p₂, p₃}

Tactic:
angle_eq_zero_iff_ne_and_wbtw

Goal state after:
case refine_2.inr.inr.inl
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₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
⊢ Collinear ℝ {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
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)

Tactic:
rw [ne_comm, ← @vsub_ne_zero V] at h0

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₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
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 : (o.oangle x y).sign = 1
hx : ¬x = 0
hy : y = 0
⊢ o.oangle x y = ↑(InnerProductGeometry.angle x y)

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 : (o.oangle x y).sign = 1
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle x y = ↑(InnerProductGeometry.angle x y)

Tactic:
· simp [hy] at h

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

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 : (o.oangle x y).sign = -1
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle x y = -↑(InnerProductGeometry.angle x y)

Tactic:
· simp [hy] at h

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 : (o.oangle x y).sign = -1
hx : ¬x = 0
hy : ¬y = 0
⊢ o.oangle x y = -↑(InnerProductGeometry.angle x y)
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₂
⊢ ∠ p₂ p₃ p₁ < π / 2

Tactic:
rw [ne_comm, ← @vsub_ne_zero V] at h0

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₃ p₁ < π / 2
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hp₁p₂ : ¬p₁ = p₂
hp₃p₂ : ¬p₃ = p₂
⊢ ∠ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁

Tactic:
angle_eq_zero_iff_ne_and_wbtw

Goal state after:
case neg
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
hp₁p₂ : ¬p₁ = p₂
hp₃p₂ : ¬p₃ = p₂
⊢ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁ ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
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 c p : P
h_sbtw : Sbtw ℝ a b c
hp : p ∈ perpBisector a b
⊢ ⟪p -ᵥ midpoint ℝ a b, b -ᵥ midpoint ℝ a b⟫ = 0

Tactic:
by
    rw [right_vsub_midpoint, inner_smul_right,
        mem_perpBisector_iff_inner_eq_zero.mp hp, invOf_eq_inv, mul_zero]

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
h : Wbtw ℝ p₁ p₂ p₃
hne : p₂ ≠ p₃
⊢ (∡ p₂ p₄ p₃).sign = (∡ p₁ p₄ p₃).sign

Tactic:
simp_rw [oangle_rev p₃, Real.Angle.sign_neg, h.symm.oangle_sign_eq_of_ne_left _ hne.symm]

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
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ Wbtw ℝ p₁ s.center p₂

Tactic:
rw [← h.midpoint_eq_center]

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ Wbtw ℝ p₁ (midpoint ℝ p₁ p₂) p₂
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
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
hr : s.radius ≠ 0
⊢ Sbtw ℝ p₁ s.center p₂

Tactic:
rw [← h.midpoint_eq_center]

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
hr : s.radius ≠ 0
⊢ Sbtw ℝ p₁ (midpoint ℝ p₁ p₂) p₂