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

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ i (y1 ^ p ^ n2 * y2 ^ p ^ n1) = (x1 * x2) ^ p ^ (n1 + n2)

Tactic:
map_mul,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ i (y1 ^ p ^ n2) * i (y2 ^ p ^ n1) = (x1 * x2) ^ p ^ (n1 + n2)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ (iterateFrobeniusEquiv M p (n1 + n2)).symm (j (y1 ^ p ^ n2 * y2 ^ p ^ n1)) =
    (iterateFrobeniusEquiv M p n1).symm (j y1) * (iterateFrobeniusEquiv M p n2).symm (j y2)

Tactic:
map_mul,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ (iterateFrobeniusEquiv M p (n1 + n2)).symm (j (y1 ^ p ^ n2) * j (y2 ^ p ^ n1)) =
    (iterateFrobeniusEquiv M p n1).symm (j y1) * (iterateFrobeniusEquiv M p n2).symm (j y2)
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ (iterateFrobeniusEquiv M p (n1 + n2)).symm (j y1 ^ p ^ n2 * j y2 ^ p ^ n1) =
    (iterateFrobeniusEquiv M p n1).symm (j y1) * (iterateFrobeniusEquiv M p n2).symm (j y2)

Tactic:
map_mul,

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing K
inst✝⁷ : CommRing L
inst✝⁶ : CommRing M
inst✝⁵ : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst✝⁴ : ExpChar M p
inst✝³ : ExpChar K p
inst✝² : PerfectRing M p
inst✝¹ : IsPRadical i p
inst✝ : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : i y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : i y2 = x2 ^ p ^ n2
⊢ (iterateFrobeniusEquiv M p (n1 + n2)).symm (j y1 ^ p ^ n2) *
      (iterateFrobeniusEquiv M p (n1 + n2)).symm (j y2 ^ p ^ n1) =
    (iterateFrobeniusEquiv M p n1).symm (j y1) * (iterateFrobeniusEquiv M p n2).symm (j y2)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
⊢ ↑x = ↑y ↔ ↑x = ↑y

Tactic:
constructor <;> intro H

Goal state after:
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ ↑x = ↑y

case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ ↑x = ↑y
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ ProfiniteGrp.{max v u}
cone : Limits.Cone F
m : cone.pt ⟶ (limitCone F).pt
h : ∀ (j : J), m ≫ (limitCone F).π.app j = cone.π.app j
⊢ m =
    ofHom
      (let __src :=
        TopCat.Hom.hom
          ((Profinite.limitConeIsLimit (F ⋙ forget₂ ProfiniteGrp.{max u v} Profinite)).lift
              ((forget₂ ProfiniteGrp.{max u v} Profinite).mapCone cone)).hom;
      { toFun := __src.toFun, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ })

Tactic:
apply (forget₂ ProfiniteGrp Profinite).map_injective
    simpa using! (Profinite.limitConeIsLimit (F ⋙ (forget₂ ProfiniteGrp Profinite))).uniq
      ((forget₂ ProfiniteGrp Profinite).mapCone cone) ((forget₂ ProfiniteGrp Profinite).map m)
      (fun j ↦ congrArg (forget₂ ProfiniteGrp Profinite).map (h j))

Goal state after:
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : ↑n ≠ 0
⊢ ∃ r, x = r ^ ↑n

pp: case inr
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : -↑n ≠ 0
⊢ ∃ r, x = r ^ (-↑n)

Tactic:
· simpa using exists_eq_pow_of_isSquare hx (by simpa using hk)

Goal state after:
case inr
R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : -↑n ≠ 0
⊢ ∃ r, x = r ^ (-↑n)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y : ℕ × K
H : R K p x✝ y
n : ℕ
x : K
⊢ R K p (n, x⁻¹) (n + 1, (x ^ p)⁻¹)

Tactic:
rw [← inv_pow]

Goal state after:
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y : ℕ × K
H : R K p x✝ y
n : ℕ
x : K
⊢ R K p (n, x⁻¹) (n + 1, x⁻¹ ^ p)
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ ((0, 0).1, (0, 0).2⁻¹) = (0, 0)

Tactic:
by rw [inv_zero]

Goal state after:
Module: Mathlib.FieldTheory.Laurent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
x : R[X]
hx : (taylor (-r)) x * p = 0
this : x = (taylor (r - r)) x
⊢ x = 0

Tactic:
mul_right_mem_nonZeroDivisors_eq_zero_iff hp,

Goal state after:
R : Type u
inst✝ : CommRing R
r : R
p : R[X]
hp : p ∈ R[X]⁰
x : R[X]
hx : (taylor (-r)) x = 0
this : x = (taylor (r - r)) x
⊢ x = 0
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 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j) = 0
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
⊢ ∑ x_1 ∈ s, (aeval x) (C (m x_1) * ∏ j ∈ s.erase x_1, (X - C j)) =
    ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j)

Tactic:
map_mul,

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
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
⊢ ∑ x_1 ∈ s, (aeval x) (C (m x_1)) * (aeval x) (∏ j ∈ s.erase x_1, (X - C j)) =
    ∑ x_1 ∈ s, m x_1 • ∏ j ∈ s.erase x_1, (x - (algebraMap F E) j)
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)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
hm : ∑ x ∈ s, (aeval i) (C (m x) * ∏ j ∈ s.erase x, (X - C j)) = 0
⊢ m i = 0

Tactic:
map_mul,

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)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
hm : ∑ x ∈ s, (aeval i) (C (m x)) * (aeval i) (∏ j ∈ s.erase x, (X - C j)) = 0
⊢ m i = 0
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
e : Gal(K[n√a]/K)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ (of (X ^ n - C a))
        ↑↑((rootsOfUnityEquivOfPrimitiveRoots ⋯ hζ).symm
              (rootsOfUnity.mkOfPowEq (if a = 0 then 1 else e (root (X ^ n - C a)) / root (X ^ n - C a)) ⋯)) *
      root (X ^ n - C a) =
    e (root (X ^ n - C a))

Tactic:
rootsOfUnityEquivOfPrimitiveRoots_symm_apply,

Goal state after:
K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
e : Gal(K[n√a]/K)
this✝ : Fact (Irreducible (X ^ n - C a))
this : Algebra K K[n√a] := inferInstance
⊢ ↑↑(rootsOfUnity.mkOfPowEq (if a = 0 then 1 else e (root (X ^ n - C a)) / root (X ^ n - C a)) ⋯) * root (X ^ n - C a) =
    e (root (X ^ n - C a))
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : HasExponent K L
p : ℕ
inst✝ : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
⊢ (algebraMap K L) (iterateFrobeniusAux K L p n 1) = (algebraMap K L) 1

Tactic:
rw [(algebraMap K L).map_one,
      algebraMap_iterateFrobeniusAux K p hn 1,
      one_pow]

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

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : HasExponent K L
p : ℕ
inst✝ : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
⊢ (algebraMap K L) (iterateFrobeniusAux K L p n 0) = (algebraMap K L) 0

Tactic:
rw [(algebraMap K L).map_zero,
      algebraMap_iterateFrobeniusAux K p hn 0,
      zero_pow]

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : HasExponent K L
p : ℕ
inst✝ : ExpChar K p
n : ℕ
hn : exponent K L ≤ n
⊢ p ^ n ≠ 0
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : HasExponent K L
p : ℕ
inst✝⁵ : ExpChar K p
inst✝⁴ : Field F
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
inst✝ : ExpChar F p
n : ℕ
hn : exponent K L ≤ n
r : F
a : L
⊢ (r • a) ^ p ^ n = (algebraMap F L) ((_root_.iterateFrobenius F p n) r) * a ^ p ^ n

Tactic:
iterateFrobenius_def,

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : HasExponent K L
p : ℕ
inst✝⁵ : ExpChar K p
inst✝⁴ : Field F
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
inst✝ : ExpChar F p
n : ℕ
hn : exponent K L ≤ n
r : F
a : L
⊢ (r • a) ^ p ^ n = (algebraMap F L) (r ^ p ^ n) * a ^ p ^ n
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : HasExponent K L
p : ℕ
inst✝⁵ : ExpChar K p
inst✝⁴ : Field F
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
inst✝ : ExpChar F p
n : ℕ
hn : exponent K L ≤ n
a : F
⊢ (algebraMap K L) ((iterateFrobeniusₛₗ F K L p hn) ((algebraMap F L) a)) = (algebraMap F L) a ^ p ^ n

Tactic:
algebraMap_iterateFrobeniusₛₗ F K L p hn

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : HasExponent K L
p : ℕ
inst✝⁵ : ExpChar K p
inst✝⁴ : Field F
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
inst✝ : ExpChar F p
n : ℕ
hn : exponent K L ≤ n
a : F
⊢ (algebraMap F L) a ^ p ^ n = (algebraMap F L) a ^ p ^ n
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
L1 L2 : IntermediateField F E
h1 : IsPurelyInseparable F ↥L1
h2 : IsPurelyInseparable F ↥L2
⊢ IsPurelyInseparable F ↥(L1 ⊔ L2)

Tactic:
by
  rw [← le_perfectClosure_iff] at h1 h2 ⊢
  exact sup_le h1 h2

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
⊢ Cardinal.lift.{w, v} (insepDegree F E) * Cardinal.lift.{v, w} (insepDegree E K) =
    Cardinal.lift.{v, w} (insepDegree F K)

Tactic:
by
  have h := lift_rank_mul_lift_insepDegree_of_isPurelyInseparable (separableClosure F E) E K
  rwa [← insepDegree_eq_of_isSeparable F (separableClosure F E) K] at h

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 (c E) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) = Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

Tactic:
map_mul,

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: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (Polynomial.C (c E) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)).natDegree = (φ E).natDegree

Tactic:
natDegree_mul (C_ne_zero.mpr (c_ne_zero h)) (map_ne_zero (φ_ne_zero h)),

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ (Polynomial.C (c E)).natDegree + (Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)).natDegree = (φ E).natDegree
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
H : Φ E = 0
this : (c E).num = coeff 0 (φ E).natDegree
⊢ False

Tactic:
coeff_zero

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
H : Φ E = 0
this : (c E).num = 0
⊢ False
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
x✝ : ℕ
| Polynomial.X ^ x✝ • Polynomial.map Polynomial.C ((Φ E).coeff x✝)

Tactic:
← monomial_one_right_eq_X_pow,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
x✝ : ℕ
| (monomial x✝) 1 • Polynomial.map Polynomial.C ((Φ E).coeff x✝)
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ m E ≤ (∑ x ∈ (Φ E).support, Bivariate.swap ((monomial x) ((Φ E).coeff x))).natDegree

Tactic:
conv in (fun _ ↦ _) =>
    ext
    rw [Bivariate.swap_monomial, mul_comm, ← Polynomial.smul_eq_C_mul,
      ← monomial_one_right_eq_X_pow, ← Polynomial.algebraMap_eq]

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ m E ≤ (∑ x ∈ (Φ E).support, (monomial x) 1 • Polynomial.map (algebraMap K K[X]) ((Φ E).coeff x)).natDegree
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ Bivariate.swap (Polynomial.C (g E) * Polynomial.map Polynomial.C (f E)) -
      Bivariate.swap (Polynomial.C (f E) * Polynomial.map Polynomial.C (g E)) =
    -θ E

Tactic:
map_mul,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ Bivariate.swap (Polynomial.C (g E)) * Bivariate.swap (Polynomial.map Polynomial.C (f E)) -
      Bivariate.swap (Polynomial.C (f E) * Polynomial.map Polynomial.C (g E)) =
    -θ E
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ Bivariate.swap (Polynomial.C (g E)) * Bivariate.swap (Polynomial.map Polynomial.C (f E)) -
      Bivariate.swap (Polynomial.C (f E) * Polynomial.map Polynomial.C (g E)) =
    -θ E

Tactic:
map_mul,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ Bivariate.swap (Polynomial.C (g E)) * Bivariate.swap (Polynomial.map Polynomial.C (f E)) -
      Bivariate.swap (Polynomial.C (f E)) * Bivariate.swap (Polynomial.map Polynomial.C (g E)) =
    -θ E
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  (Bivariate.swap (Polynomial.map Polynomial.C (Polynomial.C (Q₃ h)) * Φ E)).natDegree =
    (Bivariate.swap (θ E)).natDegree
⊢ (Bivariate.swap (Φ E)).natDegree = (θ E).natDegree

Tactic:
map_mul,

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this :
  (Bivariate.swap (Polynomial.map Polynomial.C (Polynomial.C (Q₃ h))) * Bivariate.swap (Φ E)).natDegree =
    (Bivariate.swap (θ E)).natDegree
⊢ (Bivariate.swap (Φ E)).natDegree = (θ E).natDegree
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✝ : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₂ : p₂ ∈ s
this : Nonempty ↥s
⊢ ↑((orthogonalProjection s) p₁) = p₂ → dist p₁ ↑((orthogonalProjection s) p₁) = dist p₁ p₂

Tactic:
intro h
    nth_rw 4 [← h]

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)
p : P
⊢ line[ℝ, p, s.points i] = s.altitude i ↔
    p ≠ s.points i ∧
      p ∈ affineSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ

Tactic:
rw [eq_iff_direction_eq_of_mem (mem_affineSpan ℝ (Set.mem_insert_of_mem _ (Set.mem_singleton _)))
      (s.mem_altitude _),
    ← vsub_right_mem_direction_iff_mem (mem_affineSpan ℝ (Set.mem_range_self i)) p,
    direction_affineSpan, direction_affineSpan, direction_affineSpan]
  constructor
  · intro h
    constructor
    · intro heq
      rw [heq, Set.pair_eq_singleton, vectorSpan_singleton] at h
      have hd : finrank ℝ (s.altitude i).direction = 0 := by rw [← h, finrank_bot]
      simp at hd
    · rw [← Submodule.mem_inf, _root_.inf_comm, ← direction_altitude, ← h]
      exact
        vsub_mem_vectorSpan ℝ (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (Set.mem_singleton _))
  · rintro ⟨hne, h⟩
    rw [← Submodule.mem_inf, _root_.inf_comm, ← direction_altitude] at h
    rw [vectorSpan_eq_span_vsub_set_left_ne ℝ (Set.mem_insert _ _),
      Set.insert_sdiff_of_mem _ (Set.mem_singleton _),
      Set.sdiff_singleton_eq_self fun h => hne (Set.mem_singleton_iff.1 h), Set.image_singleton]
    refine Submodule.eq_of_le_of_finrank_eq ?_ ?_
    · rw [Submodule.span_le]
      simpa using h
    · rw [finrank_direction_altitude, finrank_span_set_eq_card]
      · simp
      · exact .singleton <| by simpa using hne

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 : ℕ
s : Simplex ℝ P n
i j : Fin (n + 1)
h : i ≠ j
⊢ have this := ⋯;
  ⟪s.points j -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫ = 0

Tactic:
by
  have : NeZero n := by grind [neZero_iff]
  refine Submodule.inner_right_of_mem_orthogonal
    (K := vectorSpan ℝ (s.points '' {i}ᶜ))
    (vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan
      (s.mem_affineSpan_image_iff.2 h.symm)
      (Affine.Simplex.altitudeFoot_mem_affineSpan_image_compl _ _))
    ?_
  rw [← direction_affineSpan, ← Affine.Simplex.range_faceOpposite_points]
  exact vsub_orthogonalProjection_mem_direction_orthogonal _ _

Goal state after:
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
h : y = (‖y‖ / ‖x‖) • (o.rotation θ) x
⊢ ∃ r, 0 < r ∧ y = r • (o.rotation θ) x

Tactic:
exact ⟨‖y‖ / ‖x‖, div_pos (norm_pos_iff.2 hy) (norm_pos_iff.2 hx), h⟩

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ : P
h : InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₄ -ᵥ p₃) = π
left✝ : p₂ -ᵥ p₃ ≠ 0
r : ℝ
hr : r < 0
hpr : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)
⊢ -r • -(p₂ -ᵥ p₃) + 1 • -(p₂ -ᵥ p₃) = p₄ -ᵥ p₂

Tactic:
smul_neg,

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 : p₄ -ᵥ p₃ = r • (p₂ -ᵥ p₃)
⊢ -(-r • (p₂ -ᵥ p₃)) + 1 • -(p₂ -ᵥ p₃) = p₄ -ᵥ p₂
Module: Mathlib.Geometry.Euclidean.Altitude

Goal state before:
pp: case a.refine_2.refine_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hij : i ≠ j
r : ℝ
hr : r ≠ 0
h : s.points j -ᵥ s.altitudeFoot j = r • (s.points i -ᵥ s.altitudeFoot i)
hk : ∃ k, k ≠ i ∧ k ≠ j
hs :
  vectorSpan ℝ (Set.range s.points) =
    vectorSpan ℝ (Set.range (s.faceOpposite i).points) ⊔ vectorSpan ℝ (Set.range (s.faceOpposite j).points)
⊢ s.points j -ᵥ s.altitudeFoot j ∈ (vectorSpan ℝ (Set.range (s.faceOpposite j).points))ᗮ

Tactic:
rw [← direction_affineSpan]
        exact vsub_orthogonalProjection_mem_direction_orthogonal _ _

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
⊢ p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • -(r • (p₃ -ᵥ p₁))

Tactic:
smul_neg,

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

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle x z - o.oangle x y = o.oangle y z

Tactic:
by
  rw [sub_eq_iff_eq_add, o.oangle_add_swap hx hy hz]

Goal state after: