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

Goal state before:
pp: case splits'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := ⋯
⊢ (Polynomial.map (algebraMap K K[n√a]) (X ^ n - C a)).Splits

Tactic:
Polynomial.map_sub,

Goal state after:
case splits'
K : Type u
inst✝ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ (Polynomial.map (algebraMap K K[n√a]) (X ^ n) - Polynomial.map (algebraMap K K[n√a]) (C a)).Splits
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case hf
K : Type u
inst✝³ : Field K
n : ℕ
hζ✝ : (primitiveRoots n K).Nonempty
a : K
H✝ : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα✝ : α ^ n = (algebraMap K L) a
hζ : (primitiveRoots n K).Nonempty
H : Irreducible (X ^ n - C a)
hα : α ^ n = (algebraMap K L) a
this✝ : Fact (Irreducible (X ^ n - C a))
this : IsSplittingField K K[n√a] (X ^ n - C a) := isSplittingField_AdjoinRoot_X_pow_sub_C hζ H
⊢ (Polynomial.map (algebraMap K K[n√a]) (X ^ n - C a)).Splits

Tactic:
exact IsSplittingField.splits _ _

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case splits'
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⟮α⟯ = ⊤
⊢ (Polynomial.map (algebraMap K L) (X ^ finrank K L - C a)).Splits

Tactic:
Polynomial.map_sub,

Goal state after:
case splits'
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⟮α⟯ = ⊤
⊢ (Polynomial.map (algebraMap K L) (X ^ finrank K L) - Polynomial.map (algebraMap K L) (C a)).Splits
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: case refine_2
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
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
⊢ 1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹

Tactic:
hdensity

Goal state after:
case refine_2
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
inst✝ : DecidablePred FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι}, i ∈ s → (H i).FiniteIndex → D ≤ H i
t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement ↑(t i hi hfi) ↑(D.subgroupOf (H i)) ∧ ⋃ g ∈ t i hi hfi, ↑g • ↑D = ↑(H i)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {1})
f : κ → G := fun k ↦ g ↑k.fst * ↑↑k.snd
K : κ → Subgroup G := fun k ↦ if (H ↑k.fst).FiniteIndex then D else H ↑k.fst
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
hcovers' : ⋃ i ∈ {x | K x = D}, f i • ↑D = Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity : ∑ i ∈ s, (↑(H i).index)⁻¹ = ↑{x | K x = D}.card * (↑D.index)⁻¹
⊢ 1 ≤ ↑{x | K x = D}.card * (↑D.index)⁻¹
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 : IsField (↥A ⊗[R] ↥B)
⊢ A.LinearDisjoint B

Tactic:
nontriviality S
  rw [linearDisjoint_iff_injective]
  let : Field (A ⊗[R] B) := H.toField
  -- need this otherwise `RingHom.injective` does not work
  let : NonAssocRing (A ⊗[R] B) := Ring.toNonAssocRing
  exact RingHom.injective _

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this✝ : FiniteDimensional F ↥F⟮a⟯
this : FiniteDimensional F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
hab : a + b ∈ E
a' : ↥E := ⟨a, ha⟩
b' : ↥E := ⟨b, hb⟩
ab' : ↥E := ⟨a + b, hab⟩
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F (↥E) a' + normalizedTraceAux F (↥E) b'

Tactic:
normalizedTraceAux_intermediateField F K ab',

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this✝ : FiniteDimensional F ↥F⟮a⟯
this : FiniteDimensional F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
hab : a + b ∈ E
a' : ↥E := ⟨a, ha⟩
b' : ↥E := ⟨b, hb⟩
ab' : ↥E := ⟨a + b, hab⟩
⊢ normalizedTraceAux F (↥E) ab' = normalizedTraceAux F (↥E) a' + normalizedTraceAux F (↥E) b'
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: case refine_2
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
⊢ (toSubmodule A).lTensorOne (1 ⊗ₜ[R] 1) = 1

Tactic:
exact Submodule.lTensorOne_one_tmul _

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
⊢ minpoly K a = X ^ ringExpChar K ^ elemExponent K a - C (elemReduct K a)

Tactic:
exact Classical.choose_spec <| Nat.find_spec <| minpoly_eq_X_pow_sub_C K (ringExpChar K) a

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 ↥(Algebra.adjoin ↥B ↑A) = Module.rank R ↥A

Tactic:
rw [← rank_toSubmodule, Module.Free.rank_eq_card_chooseBasisIndex R A,
    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.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 ↥(Algebra.adjoin ↥B ↑A) = Module.rank R ↥A

Tactic:
rw [← rank_toSubmodule, Module.Free.rank_eq_card_chooseBasisIndex R A,
    A.adjoin_eq_span_basis B (Module.Free.chooseBasis R A)]
  change Module.rank B (Submodule.span B (Set.range (A.val ∘ Module.Free.chooseBasis R A))) = _
  have := H.linearIndependent_left_of_flat (Module.Free.chooseBasis R A).linearIndependent
  rw [rank_span this, Cardinal.mk_range_eq _ this.injective]

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
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B
⊢ Function.Injective ⇑((toSubmodule A).mulMap (toSubmodule B))

Tactic:
intro x y hxy

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
A B : Subalgebra R S
inst✝ : Algebra.IsIntegral R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite R ↥A'], A'.LinearDisjoint B
x y : ↥(toSubmodule A) ⊗[R] ↥(toSubmodule B)
hxy : ((toSubmodule A).mulMap (toSubmodule B)) x = ((toSubmodule A).mulMap (toSubmodule B)) y
⊢ x = y
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 (adjoin F Set.univ).toSubalgebra

Tactic:
adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable' F E _ q n,

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) =
    Subalgebra.toSubmodule (adjoin F ((fun x ↦ x ^ q ^ n) '' Set.univ)).toSubalgebra
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
⊢ ↑1 - ↑X.denom.natDegree = 1

Tactic:
denom_X,

Goal state after:
K : Type u
inst✝ : Field K
⊢ ↑1 - ↑(natDegree 1) = 1
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ (↥E)⟮ X⟯ = ⊤

Tactic:
rw [← restrictScalars_eq_top_iff (K := K), IntermediateField.restrictScalars_adjoin,
    _root_.eq_top_iff]
  exact le_trans (le_of_eq RatFunc.adjoin_X.symm) (adjoin.mono _ _ _ (by simp))

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ↑((f.minpolyX ↥K⟮f⟯).coeff f.denom.natDegree) = 0
⊢ ∃ c, f = C c

Tactic:
use f.num.coeff f.denom.natDegree / f.denom.leadingCoeff

Goal state after:
case h
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ↑((f.minpolyX ↥K⟮f⟯).coeff f.denom.natDegree) = 0
⊢ f = C (f.num.coeff f.denom.natDegree / f.denom.leadingCoeff)
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
⊢ Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (Module.rank E ↥(separableClosure E K)) =
    Cardinal.lift.{v, w} (Module.rank F ↥(restrictScalars F (separableClosure E K)))

Tactic:
exact lift_rank_mul_lift_rank F E (separableClosure E K)

Goal state after:
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

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
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsAlgebraic F E
h :
  Cardinal.lift.{w, v} (Module.rank (↥(separableClosure F E)) E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree (↥(separableClosure F E)) K)
⊢ Cardinal.lift.{w, v} (insepDegree F E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree F K)

Tactic:
rwa [← insepDegree_eq_of_isSeparable F (separableClosure F E) K] at h

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : DecidableEq F⟮X⟯
x✝ : F
hx : x✝ ≠ 0
⊢ (inftyValuation F) ((algebraMap F F⟮X⟯) x✝) = 1

Tactic:
by simp [inftyValuation.C _ hx]

Goal state after:
Module: Mathlib.Geometry.Convex.Hull

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
x : X
hs : IsConvexSet R s
hsx : IsConvexSet R (s \ {x})
hx : x ∈ (convexHull R) (s \ {x})
⊢ False

Tactic:
by
    rw [hsx.convexHull_eq_self] at hx
    exact hx.2 (mem_singleton _)

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 ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
      Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
        ((generator E).minpolyX ↥K⟮generator E⟯) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
Polynomial.map_sub,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
      (Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
          (Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).num) -
        Polynomial.map ((algebraMap (↥E) K⟮X⟯).comp (algebraMap ↥K⟮generator E⟯ ↥E))
          (Polynomial.C ((algebraMap ↥K[generator E] ↥K⟮generator E⟯) ⟨generator E, ⋯⟩) *
            Polynomial.map (algebraMap K ↥K⟮generator E⟯) (generator E).denom)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)
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⟯) (g E)) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).num -
      Polynomial.C ((algebraMap K[X] K⟮X⟯) (generator E).num) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (θ E)

Tactic:
Polynomial.map_sub,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C ((algebraMap K[X] K⟮X⟯) (g E)) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).num -
      Polynomial.C ((algebraMap K[X] K⟮X⟯) (generator E).num) *
        Polynomial.map (((algebraMap (↥E) K⟮X⟯).comp ↑(inclusion ⋯)).comp (algebraMap K ↥K⟮generator E⟯))
          (generator E).denom =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (g E) * Polynomial.map Polynomial.C (f E)) -
      Polynomial.map (algebraMap K[X] K⟮X⟯) (Polynomial.C (f E) * Polynomial.map Polynomial.C (g E))
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: 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))
isUnit₁ : IsUnit (Polynomial.C ((aeval α) (f E)))
isUnit₂ : IsUnit (Polynomial.C ((aeval α) (g E)))
isCoprime :
  IsCoprime ((Polynomial.mapRingHom (algebraMap K F)) (generator E).num)
    ((Polynomial.mapRingHom (algebraMap K F)) (generator E).denom)
⊢ Associated ((Polynomial.mapRingHom (algebraMap K F)) (g E))
    ((Polynomial.mapRingHom (algebraMap K F)) (f E) * Polynomial.C ((aeval α) (g E)))

Tactic:
exact ⟨isUnit₁.unit, by simpa⟩

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

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

Tactic:
by
  rw [orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem]
  exact SetLike.le_def.1 (Submodule.orthogonal_le (direction_le h))
    (orthogonalProjection_vsub_mem_direction_orthogonal _ _)

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

Goal state before:
pp: case neg.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hx : ¬x = 0
hr : r < 0
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

pp: case neg.inr.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hx : ¬x = 0
hr : r = 0
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

pp: case neg.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 : ℝ
hx : ¬x = 0
hr : 0 < r
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

Tactic:
· rw [← neg_smul]
      exact Or.inr ⟨hx, smul_ne_zero hr.ne hx,
        SameRay.sameRay_pos_smul_right x (Left.neg_pos_iff.2 hr)⟩

Goal state after:
case neg.inr.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hx : ¬x = 0
hr : r = 0
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

case neg.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 : ℝ
hx : ¬x = 0
hr : 0 < r
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))
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
h0 : x = 0 ∨ -y ≠ 0
⊢ 0 < angle x (x + -y)

Tactic:
exact angle_add_pos_of_inner_eq_zero h h0

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

Tactic:
exact angle_add_pos_of_inner_eq_zero h h0

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

Tactic:
rw [oangle_eq_pi_iff_oangle_rev_eq_pi, ← h.oangle₁₂₃_eq_pi]

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
⊢ (o.oangle (-x) y).sign = -(o.oangle x y).sign

Tactic:
by
  by_cases hx : x = 0; · simp [hx]
  by_cases hy : y = 0; · simp [hy]
  rw [o.oangle_neg_left hx hy, Real.Angle.sign_add_pi]

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
⊢ Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂

Tactic:
by
  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 [angle, dist_eq_norm_vsub' V p₃ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
    add_comm, cos_angle_add_mul_norm_of_inner_eq_zero 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 : V
h : x ≠ 0
r : ℝ
⊢ o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)

Tactic:
by
  rcases lt_trichotomy r 0 with (hr | rfl | hr)
  · have ha : o.oangle x (r • o.rotation (π / 2 : ℝ) x) = -(π / 2 : ℝ) := by
      rw [o.oangle_smul_right_of_neg _ _ hr, o.oangle_neg_right h, o.oangle_rotation_self_right h, ←
        sub_eq_zero, add_comm, sub_neg_eq_add, ← Real.Angle.coe_add, ← Real.Angle.coe_add,
        add_assoc, add_halves, ← two_mul, Real.Angle.coe_two_pi]
      simpa using h
    rw [← neg_inj, ← oangle_neg_orientation_eq_neg, neg_neg] at ha
    rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj, oangle_rev,
      (-o).oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two ha, norm_smul,
      LinearIsometryEquiv.norm_map, mul_div_assoc, div_self (norm_ne_zero_iff.2 h), mul_one,
      Real.norm_eq_abs, abs_of_neg hr, Real.arctan_neg, Real.Angle.coe_neg, neg_neg]
  · simp
  · have ha : o.oangle x (r • o.rotation (π / 2 : ℝ) x) = (π / 2 : ℝ) := by
      rw [o.oangle_smul_right_of_pos _ _ hr, o.oangle_rotation_self_right h]
    rw [o.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two ha, norm_smul,
      LinearIsometryEquiv.norm_map, mul_div_assoc, div_self (norm_ne_zero_iff.2 h), mul_one,
      Real.norm_eq_abs, abs_of_pos hr]

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

Goal state before:
pp: case neg.refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p q : P
h✝ : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
⊢ ∃ x, 0 ≤ x ∧ x • v = q -ᵥ p

Tactic:
use ‖v‖⁻¹ * ‖q -ᵥ p‖

Goal state after:
case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p q : P
h✝ : ¬v = 0
h : ‖q -ᵥ p‖ • v = ‖v‖ • (q -ᵥ p)
⊢ 0 ≤ ‖v‖⁻¹ * ‖q -ᵥ p‖ ∧ (‖v‖⁻¹ * ‖q -ᵥ p‖) • v = q -ᵥ p
Module: Mathlib.Geometry.Euclidean.SignedDist

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 : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ dist (↑((orthogonalProjection s) p)) p = ‖p -ᵥ ↑((orthogonalProjection s) p)‖

Tactic:
dist_eq_norm_vsub'

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ ‖p -ᵥ ↑((orthogonalProjection s) p)‖ = ‖p -ᵥ ↑((orthogonalProjection s) p)‖
Module: Mathlib.Geometry.Euclidean.SignedDist

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)
p : P
h : p ∈ affineSpan ℝ (Set.range s.points)
⊢ p ∈ affineSpan ℝ (insert (s.points i) ↑(affineSpan ℝ (s.points '' {i}ᶜ)))

Tactic:
rw [affineSpan_insert_affineSpan]

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)
p : P
h : p ∈ affineSpan ℝ (Set.range s.points)
⊢ p ∈ affineSpan ℝ (insert (s.points i) (s.points '' {i}ᶜ))