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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FinTrdeg K L
s : Set L
hs : IsTranscendenceBasis K Subtype.val
⊢ ∃ s, IsTranscendenceBasis K Subtype.val

Tactic:
obtain ⟨s, rfl⟩ := Finset.mem_range_coe_iff.2
    (Set.finite_coe_iff.1 (finite_of_isTranscendenceBasis hs))

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FinTrdeg K L
s : Finset L
hs : IsTranscendenceBasis K Subtype.val
⊢ ∃ s, IsTranscendenceBasis K Subtype.val
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
q : F[X]
this : 0 < p.natDegree
⊢ ¬p ∣ derivative p

Tactic:
apply not_dvd_of_natDegree_lt

Goal state after:
case h.h0
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
q : F[X]
this : 0 < p.natDegree
⊢ derivative p ≠ 0

case hl
R : Type u_1
inst✝⁶ : Field R
inst✝⁵ : Differential R
a b : R
F : Type u_2
inst✝⁴ : Field F
inst✝³ : Differential F
inst✝² : CharZero F
p : F[X]
inst✝¹ : Fact (Irreducible p)
inst✝ : Fact p.Monic
q : F[X]
this : 0 < p.natDegree
⊢ (derivative p).natDegree < p.natDegree
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: case inj
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⟨differentialFiniteDimensional F K, ⋯⟩
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < (minpoly F x).natDegree
⊢ ¬minpoly F x ∣ derivative (minpoly F x)

Tactic:
apply not_dvd_of_natDegree_lt

Goal state after:
case inj.h0
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⋯
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < (minpoly F x).natDegree
⊢ derivative (minpoly F x) ≠ 0

case hl
R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⋯
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < (minpoly F x).natDegree
⊢ (derivative (minpoly F x)).natDegree < (minpoly F x).natDegree
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Finite K
this : Fintype K
x : L
hx :
  (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
        ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x)).ker =
    Module.annihilator K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
⊢ LinearIndependent K fun σ ↦ σ x

Tactic:
← span_minpoly_eq_annihilator,

Goal state after:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this✝ : Finite K
this : Fintype K
x : L
hx :
  (toSpanSingleton K[X] (AEval' (frobeniusAlgHom K L).toLinearMap)
        ((AEval'.of (frobeniusAlgHom K L).toLinearMap) x)).ker =
    Ideal.span {minpoly K (frobeniusAlgHom K L).toLinearMap}
⊢ LinearIndependent K fun σ ↦ σ x
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ adjoin F (⇑b ∘ φ '' Iio i) = adjoin F (⇑b '' Iio (φ i))

Tactic:
refine le_antisymm (adjoin.mono _ _ _ ?_) (adjoin_le_iff.mpr ?_)

Goal state after:
case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ ⇑b ∘ φ '' Iio i ⊆ ⇑b '' Iio (φ i)

case refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ ⇑b '' Iio (φ i) ⊆ ↑(adjoin F (⇑b ∘ φ '' Iio i))
Module: Mathlib.FieldTheory.Galois.Profinite

Goal state before:
pp: k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L : FiniteGaloisIntermediateField k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : ↥L.toIntermediateField
L' : FiniteGaloisIntermediateField k K
h : L ≤ L'
⊢ ↑(((proj L) g) x) = ↑(((proj L') g) ⟨↑x, ⋯⟩)

Tactic:
by
  induction L with | _ L => ?_
  induction L' with | _ L' => ?_
  let : Algebra L L' := RingHom.toAlgebra (Subsemiring.inclusion h)
  let : IsScalarTower k L L' := IsScalarTower.of_algebraMap_eq (congrFun rfl)
  rw [← finGaloisGroupFunctor_map_proj_eq_proj g h.hom]
  change (algebraMap L' K (algebraMap L L' (AlgEquiv.restrictNormal (proj (mk L') g) L x))) = _
  rw [AlgEquiv.restrictNormal_commutes (proj (mk L') g) L]
  rfl

Goal state after:
Module: Mathlib.RingTheory.Algebraic.LinearIndependent

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : ∑ x_1 ∈ s, m x_1 • (b * (x - (algebraMap F E) x_1)⁻¹) = 0
⊢ m i = 0

Tactic:
Finset.sum_congr rfl h1

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
hm : ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j) = 0
⊢ m i = 0
Module: Mathlib.RingTheory.MvPolynomial

Goal state before:
pp: K : Type v
inst✝¹ : CommRing K
inst✝ : Nontrivial K
σ : Type v
⊢ Module.rank K (MvPolynomial σ K) = #(σ →₀ ℕ)

Tactic:
by
  rw [← Cardinal.lift_inj, ← (basisMonomials σ K).mk_eq_rank]

Goal state after:
Module: Mathlib.FieldTheory.MvRatFunc.Rank

Goal state before:
pp: case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : lift.{v, u} (max #σ ℵ₀) ≤ Module.rank F K
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
lift_max,

Goal state after:
case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max v u) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : max (lift.{v, u} #σ) (lift.{v, u} ℵ₀) ≤ Module.rank F K
⊢ max (max (lift.{u, v} #F) (lift.{v, u} #σ)) ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
⊢ lift.{v, max u w} (max (max (lift.{w, u} #F) (lift.{u, w} #ι)) ℵ₀) * lift.{max u w, v} (Module.rank (↥K) E) =
    max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀

Tactic:
lift_max,

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
⊢ max (lift.{v, max u w} (max (lift.{w, u} #F) (lift.{u, w} #ι))) (lift.{v, max u w} ℵ₀) *
      lift.{max u w, v} (Module.rank (↥K) E) =
    max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
⊢ max (lift.{v, max u w} (max (lift.{w, u} #F) (lift.{u, w} #ι))) (lift.{v, max u w} ℵ₀) *
      lift.{max u w, v} (Module.rank (↥K) E) =
    max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀

Tactic:
lift_max,

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : IntermediateField F E := IntermediateField.adjoin F (range x)
this : Algebra.IsAlgebraic (↥K) E
⊢ max (max (lift.{v, max u w} (lift.{w, u} #F)) (lift.{v, max u w} (lift.{u, w} #ι))) (lift.{v, max u w} ℵ₀) *
      lift.{max u w, v} (Module.rank (↥K) E) =
    max (max (lift.{max v w, u} #F) (lift.{max u v, w} #ι)) ℵ₀
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
hm : Irreducible (1 - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ 0 - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
⊢ False

Tactic:
← C.map_one,

Goal state after:
K : Type u
inst✝ : Field K
n : ℕ
a : K
hm : Irreducible (C 1 - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ 0 - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
⊢ False
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
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
hcovers' : ⋃ k ∈ Finset.univ, f k • ↑(K k) = Set.univ
k : κ
hkfi : (H ↑k.fst).FiniteIndex
hk : K k = D
h : ⋃ i ∈ {x | K x = K k}, f i • ↑(K i) ≠ Set.univ
i : κ
hi : K i ≠ K k ∧ (K i).FiniteIndex
⊢ False

Tactic:
by_cases hfi : (H i.1.1).FiniteIndex <;> simp [K, hfi, hkfi] at hi

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 : Subalgebra R S
H : A.LinearDisjoint A
inst✝ : Flat R ↥A
hc : ∀ (a b : ↥A), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank R ↥A = 1

Tactic:
rw [← inf_of_le_left (le_refl A)] at hc ⊢
  exact H.rank_inf_eq_one_of_commute_of_flat_left_of_inj hc hinj

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✝ : FiniteDimensional F K
a : K
h : ↑(Module.finrank (↥F⟮a⟯) K) ≠ 0
⊢ normalizedTraceAux F K a = (↑(Module.finrank F ↥F⟮a⟯))⁻¹ • (trace F ↥F⟮a⟯) (AdjoinSimple.gen F a)

Tactic:
normalizedTraceAux_def

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✝ : FiniteDimensional F K
a : K
h : ↑(Module.finrank (↥F⟮a⟯) K) ≠ 0
⊢ (↑(Module.finrank F ↥F⟮a⟯))⁻¹ • (trace F ↥F⟮a⟯) (AdjoinSimple.gen F a) =
    (↑(Module.finrank F ↥F⟮a⟯))⁻¹ • (trace F ↥F⟮a⟯) (AdjoinSimple.gen F a)
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) = ⊤
this :
  Submonoid.closure (Set.range fun x ↦ x ^ q ^ n) =
    (Submonoid.map { toFun := fun x ↦ x ^ q ^ n, map_one' := ⋯, map_mul' := ⋯ } ⊤).copy (Set.range fun x ↦ x ^ q ^ n) ⋯
⊢ Set.range (toSemifield.toDivisionSemiring.toNPow.1 (q ^ n)) ⊆
    ↑(Submodule.span F (toSemifield.toDivisionSemiring.toNPow.1 (q ^ n) '' Set.range v))

Tactic:
← Set.image_univ

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) = ⊤
this :
  Submonoid.closure (Set.range fun x ↦ x ^ q ^ n) =
    (Submonoid.map { toFun := fun x ↦ x ^ q ^ n, map_one' := ⋯, map_mul' := ⋯ } ⊤).copy (Set.range fun x ↦ x ^ q ^ n) ⋯
⊢ toSemifield.toDivisionSemiring.toNPow.1 (q ^ n) '' Set.univ ⊆
    ↑(Submodule.span F (toSemifield.toDivisionSemiring.toNPow.1 (q ^ n) '' Set.range v))
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: case hdeg
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)).natDegree ≤ (minpoly F ((iterateFrobenius E q n) a)).natDegree

Tactic:
· rw [(minpoly F a).natDegree_map_eq_of_injective (iterateFrobenius F q n).injective,
      ← IntermediateField.adjoin.finrank hai,
      IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable F E hsep q n,
      ← IntermediateField.adjoin.finrank hapi, iterateFrobenius_def]

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
⊢ x⁻¹.intDegree = -x.intDegree

Tactic:
by_cases hx : x = 0 <;> simp [hx, eq_neg_iff_add_eq_zero, ← intDegree_mul (inv_ne_zero hx) hx]

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⟯) (Φ' E).content)⁻¹ * (algebraMap K[X] K⟮X⟯) (Φ' E).content) *
      Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ' E).primPart =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

Tactic:
inv_mul_cancel₀,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C 1 * Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ' E).primPart = Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (algebraMap K[X] K⟮X⟯) (Φ' E).content ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ φ E ∣ Polynomial.map (algebraMap ↥K⟮generator E⟯ ↥E) ((generator E).minpolyX ↥K⟮generator E⟯)

Tactic:
apply minpoly.dvd

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ (aeval X) (Polynomial.map (algebraMap ↥K⟮generator E⟯ ↥E) ((generator E).minpolyX ↥K⟮generator E⟯)) = 0
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
hF : F.IsFaceOf C
x y : M
hx : x ∈ C
hy : y ∈ C
hxy : x + y ∈ F
⊢ y ∈ F

Tactic:
rw [add_comm x y] at hxy

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
hF : F.IsFaceOf C
x y : M
hx : x ∈ C
hy : y ∈ C
hxy : y + x ∈ F
⊢ y ∈ F
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ dist p ↑((orthogonalProjection s) p) = 0 ↔ p ∈ s

Tactic:
dist_comm,

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ dist (↑((orthogonalProjection s) p)) p = 0 ↔ p ∈ s
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 q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
⊢ ↑((orthogonalProjection s) p) = q

Tactic:
have hq : q ∈ mk' p s.directionᗮ := by
      rwa [mem_mk', ← neg_mem_iff, neg_vsub_eq_vsub_rev]

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 q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
hq : q ∈ mk' p s.directionᗮ
⊢ ↑((orthogonalProjection s) p) = q
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 y : V
θ : Real.Angle
⊢ (o.kahler ((o.rotation θ) x)) y = (starRingEnd ℂ) ↑θ.toCircle * (o.kahler x) y

Tactic:
simp only [o.rotation_apply, map_add, map_mul, map_smulₛₗ, RingHom.id_apply,
    LinearMap.add_apply, LinearMap.smul_apply, real_smul, kahler_rightAngleRotation_left,
    Real.Angle.coe_toCircle, Complex.conj_ofReal, conj_I]
  ring

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

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
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
⊢ ℝ ∙ (p -ᵥ s.points i) = (s.altitude i).direction

Tactic:
refine Submodule.eq_of_le_of_finrank_eq ?_ ?_

Goal state after:
case mpr.refine_1
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
⊢ ℝ ∙ (p -ᵥ s.points i) ≤ (s.altitude i).direction

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
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

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

Tactic:
intro h
    rw [o.eq_iff_oangle_eq_zero_of_norm_eq] <;> simp [h]

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 : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₃ ≠ p₂

Tactic:
rw [← @vsub_ne_zero V]; exact o.right_ne_zero_of_oangle_ne_zero h

Goal state after:
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
⊢ Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h
  rw [or_comm, ← neg_ne_zero, or_comm] at h0
  rw [sub_eq_add_neg, sin_angle_add_of_inner_eq_zero h h0, norm_neg]

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
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
⊢ ∀ (r' : ℝ), o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π

Tactic:
intro r'

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
h : ¬(o.oangle x y = 0 ∨ o.oangle x y = ↑π)
r' : ℝ
⊢ o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ ↑π
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
V' : Type u_3
P' : Type u_4
inst✝³ : NormedAddCommGroup V'
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : MetricSpace P'
inst✝ : NormedAddTorsor V' P'
f : P → P'
h : Isometry f
p₁ p₂ x : P
⊢ x ∈ f ⁻¹' ↑(perpBisector (f p₁) (f p₂)) ↔ x ∈ ↑(perpBisector p₁ p₂)

Tactic:
simp [mem_perpBisector_iff_dist_eq, h.dist_eq]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
h : dist p ↑((orthogonalProjection s₁) p) = dist p ↑((orthogonalProjection s₂) p)
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
hc : ¬Collinear ℝ {p', ↑((orthogonalProjection s₁) p), ↑((orthogonalProjection s₂) p)}
⊢ ∡ (↑((orthogonalProjection s₁) p)) p' p = ∡ p p' ↑((orthogonalProjection s₂) p)

Tactic:
rw [dist_orthogonalProjection_eq_iff_angle_eq hp'₁ hp'₂, angle_comm,
    angle_eq_iff_oangle_eq_or_wbtw hp₁ hp₂] at 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
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hne : ↑((orthogonalProjection s₁) p) ≠ ↑((orthogonalProjection s₂) p)
this✝¹ : Nonempty ↥s₁
this✝ : Nonempty ↥s₂
h :
  ∡ (↑((orthogonalProjection s₁) p)) p' p = ∡ p p' ↑((orthogonalProjection s₂) p) ∨
    Wbtw ℝ p' ↑((orthogonalProjection s₁) p) ↑((orthogonalProjection s₂) p) ∨
      Wbtw ℝ p' ↑((orthogonalProjection s₂) p) ↑((orthogonalProjection s₁) p)
this : Nonempty ↥(s₁ ⊓ s₂)
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
hc : ¬Collinear ℝ {p', ↑((orthogonalProjection s₁) p), ↑((orthogonalProjection s₂) p)}
⊢ ∡ (↑((orthogonalProjection s₁) p)) p' p = ∡ p p' ↑((orthogonalProjection s₂) p)