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

Goal state before:
pp: 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

Tactic:
intro nh

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
nh : derivative p = 0
⊢ False
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝⁶ : Field k
inst✝⁵ : Finite k
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP k p
n : ℕ
inst✝² : NeZero n
l : Type u_2
inst✝¹ : Field l
inst✝ : Algebra k l
h : Module.finrank k l = n
⊢ l ≃ₐ[k] Extension k p n

Tactic:
by
  refine Nonempty.some ?_
  have : Module.Finite k l := Module.finite_of_finrank_pos <| h ▸ NeZero.pos n
  have : Finite l := Module.finite_of_finite k
  have : Fintype l := .ofFinite _
  have : IsSplittingField k l (X ^ Nat.card k ^ n - X) := by
    rw [← h, ← Module.natCard_eq_pow_finrank, ← Fintype.card_eq_nat_card]
    exact FiniteField.isSplittingField_sub l k
  refine ⟨(IsSplittingField.algEquiv _ (X ^ (Nat.card k ^ n) - X)).trans ?_⟩
  exact (IsSplittingField.algEquiv _ (X ^ (Nat.card k ^ n) - X)).symm

Goal state after:
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: case inr.inl.refine_2
k : Type u_1
inst✝ : Field k
f : k[X]
hi : Irreducible f
n : ℕ
h : f ∣ X ^ Nat.card k ^ n - X
hn : n ≠ 0
h✝ : Finite k
p : ℕ
hp : CharP k p
this✝ : Fact (Nat.Prime p)
this : NeZero n
⊢ Polynomial.map (algebraMap k (Extension k p n)) (X ^ Nat.card k ^ n - X) ≠ 0

Tactic:
· exact map_ne_zero (X_pow_card_pow_sub_X_ne_zero _ hn Finite.one_lt_card)

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

Goal state before:
pp: 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

Tactic:
intro nh

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 } := ⟨differentialFiniteDimensional F K, ⋯⟩
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
this : 0 < (minpoly F x).natDegree
nh : derivative (minpoly F x) = 0
⊢ False
Module: Mathlib.FieldTheory.IntermediateField.ExtendRight

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
F : IntermediateField K L
M : Type u_3
inst✝⁷ : Field M
inst✝⁶ : Algebra K M
inst✝⁵ : Algebra L M
inst✝⁴ : IsScalarTower K L M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra S ↥F
inst✝¹ : Algebra S M
inst✝ : IsScalarTower S (↥F) M
a : ↥(F.extendRight M)
⊢ (algebraMap (↥F) M) ((F.extendRightEquiv' M S).symm a) = ↑a

Tactic:
← algebraMap_extendRightEquiv' F M S,

Goal state after:
K : Type u_1
L : Type u_2
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
F : IntermediateField K L
M : Type u_3
inst✝⁷ : Field M
inst✝⁶ : Algebra K M
inst✝⁵ : Algebra L M
inst✝⁴ : IsScalarTower K L M
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra S ↥F
inst✝¹ : Algebra S M
inst✝ : IsScalarTower S (↥F) M
a : ↥(F.extendRight M)
⊢ (algebraMap (↥(F.extendRight M)) M) ((F.extendRightEquiv' M S) ((F.extendRightEquiv' M S).symm a)) = ↑a
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 y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 + (⇑(frobenius K p))^[x.1] (n, y).2)
    (x.1 + (n + 1, (frobenius K p) y).1,
      (frobenius K p) ((⇑(frobenius K p))^[n] x.2) + (frobenius K p) ((⇑(frobenius K p))^[x.1] y))

Tactic:
← map_add

Goal state after:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y1 y2 : ℕ × K
H : R K p y1 y2
n : ℕ
y : K
⊢ R K p (x.1 + (n, y).1, (⇑(frobenius K p))^[(n, y).1] x.2 + (⇑(frobenius K p))^[x.1] (n, y).2)
    (x.1 + (n + 1, (frobenius K p) y).1, (frobenius K p) ((⇑(frobenius K p))^[n] x.2 + (⇑(frobenius K p))^[x.1] y))
Module: Mathlib.FieldTheory.PerfectClosure

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

Tactic:
apply Quot.sound

Goal state after:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
x : K
m : ℕ
ih : mk K p (n, x) = mk K p (m + n, (⇑(frobenius K p))^[m] x)
⊢ R K p (m + n, (⇑(frobenius K p))^[m] x) ((m + n).succ, (⇑(frobenius K p) ∘ (⇑(frobenius K p))^[m]) x)
Module: Mathlib.FieldTheory.PerfectClosure

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

Tactic:
add_comm z

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

Goal state before:
pp: case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
⊢ mk K p (n, ↑x) = mk K p (n + 1, ↑x)

Tactic:
apply Quot.sound

Goal state after:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
⊢ R K p (n, ↑x) (n + 1, ↑x)
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd ↑n
⊢ Odd n

Tactic:
by simpa using hk

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd (-↑n)
⊢ Odd ?m.72

Tactic:
by simpa using hk

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : ↑n ≠ 0
⊢ n ≠ 0

Tactic:
by simpa using hk

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : -↑n ≠ 0
⊢ ?m.78 ≠ 0

Tactic:
by simpa using hk

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
e : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
H : mk K p (m, x) ≠ 0
this : ¬(⇑(frobenius K p))^[(0, 0).1] (m, x).2 = (⇑(frobenius K p))^[(m, x).1] (0, 0).2
⊢ mk K p
      ((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
        (⇑(frobenius K p))^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
          (⇑(frobenius K p))^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2) =
    1

Tactic:
refine (eq_iff K p _ _).2 ?_

Goal state after:
K : Type u
inst✝² : Field K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
e : PerfectClosure K p
x✝ : ℕ × K
m : ℕ
x : K
H : mk K p (m, x) ≠ 0
this : ¬(⇑(frobenius K p))^[(0, 0).1] (m, x).2 = (⇑(frobenius K p))^[(m, x).1] (0, 0).2
⊢ (⇑(frobenius K p))^[(0, 1).1]
      ((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
          (⇑(frobenius K p))^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
            (⇑(frobenius K p))^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2).2 =
    (⇑(frobenius K
            p))^[((m, x).1 + ((m, x).1, (m, x).2⁻¹).1,
            (⇑(frobenius K p))^[((m, x).1, (m, x).2⁻¹).1] (m, x).2 *
              (⇑(frobenius K p))^[(m, x).1] ((m, x).1, (m, x).2⁻¹).2).1]
      (0, 1).2
Module: Mathlib.GroupTheory.CosetCover

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

Tactic:
intro i hi j hj h' c hi' hj' x hx

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
hind : H.index = s.card
this✝ : Fintype (G ⧸ H)
this : Function.Bijective fun x ↦ ↑(g ↑x)
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
h' : i ≠ j
c : Set G
hi' : c ⊆ (fun x ↦ g x • ↑H) i
hj' : c ⊆ (fun x ↦ g x • ↑H) j
x : G
hx : x ∈ c
⊢ x ∈ ⊥
Module: Mathlib.GroupTheory.CosetCover

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
j : ι
hcovers : (⋃ x ∈ {x ∈ s | H x = H j}, g x • ↑(H x)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • ↑(H x) = Set.univ
hj : j ∈ s
hcovers' : ⋃ i ∈ {x ∈ s | H x = H j}, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun x_1 ↦
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k ↦ H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
y : G
hy✝ : y ∈ ⋃ x ∈ {x ∈ s | H x = H j}, g x • ↑(H x)
k : ι
hk : k ∈ {x ∈ s | H x = H j}
hy : y ∈ g k • ↑(H k)
⊢ ?m.560 ∧ H k = H j

Tactic:
by simpa using hk

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

Tactic:
sub_self,

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)
hm : (aeval i) p = (aeval i) 0
j : F
hj : j ∈ s.erase i
this : i ∈ s.erase j
⊢ m j * ((∏ x ∈ (s.erase j).erase i, (i - x)) * 0) = 0
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
this : NeZero (finrank K L)
⊢ [IsGalois K L ∧ IsCyclic Gal(L/K),
      ∃ a, Irreducible (X ^ finrank K L - C a) ∧ IsSplittingField K L (X ^ finrank K L - C a),
      ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤].TFAE

Tactic:
tfae_have 1 → 3
  | ⟨inst₁, inst₂⟩ => exists_root_adjoin_eq_top_of_isCyclic K L hK

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
this : NeZero (finrank K L)
tfae_1_to_3 : IsGalois K L ∧ IsCyclic Gal(L/K) → ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤
⊢ [IsGalois K L ∧ IsCyclic Gal(L/K),
      ∃ a, Irreducible (X ^ finrank K L - C a) ∧ IsSplittingField K L (X ^ finrank K L - C a),
      ∃ α, α ^ finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤].TFAE
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R ↥B
x : ↥B
⊢ (Algebra.leftMulMatrix (H.basisOfBasisRight H' b)) ((algebraMap (↥B) S) x) =
    (algebraMap R ↥A).mapMatrix ((Algebra.leftMulMatrix b) x)

Tactic:
ext
  simp [Algebra.leftMulMatrix_eq_repr_mul, ← H.algebraMap_basisOfBasisRight_repr_apply H']

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

Goal state before:
pp: case zero
K : Type u_2
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsPurelyInseparable K L
a : L
n : ℕ
h : a ^ ringExpChar K ^ n ∈ (algebraMap K L).range
inst✝ : CharZero K
h✝ : ExpChar K 1
⊢ elemExponent K a ≤ n

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

Tactic:
· exact elemExponent_eq_zero_of_charZero K a ▸ Nat.zero_le _

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

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

Tactic:
have hf₁ : f.aeval a = 0 := by rwa [map_sub, aeval_C, aeval_X_pow, sub_eq_zero, eq_comm]

Goal state after:
case prime
K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
n : ℕ
h : a ^ ringExpChar K ^ n ∈ (algebraMap K L).range
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
y : K
hy : (algebraMap K L) y = a ^ ringExpChar K ^ n
f : K[X] := X ^ ringExpChar K ^ n - C y
hf₁ : (aeval a) f = 0
⊢ elemExponent K a ≤ n
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:
(minpoly F a).natDegree_map_eq_of_injective (iterateFrobenius F q n).injective,

Goal state after:
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)
⊢ (minpoly F a).natDegree ≤ (minpoly F ((iterateFrobenius E q n) a)).natDegree
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
⊢ Module.finrank (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree

Tactic:
by
  by_cases hf : ∃ c, f = C c
  · obtain ⟨c, rfl⟩ := hf
    rw [adjoin_simple_eq_bot_iff.mpr (show C c ∈ ⊥ from ⟨c, rfl⟩), finrank_bot',
      Module.finrank_of_not_finite fun H ↦ Algebra.transcendental_iff_not_isAlgebraic.mp
      transcendental <| Algebra.IsAlgebraic.of_finite K K⟮X⟯]
    simp
  rw [← (IntermediateField.adjoinXEquiv K⟮f⟯).toLinearEquiv.finrank_eq,
    adjoin.finrank (f.isAlgebraic_adjoin_simple_X hf).isIntegral,
    ← minpoly.eq_of_irreducible (f.irreducible_minpolyX hf) f.minpolyX_aeval_X, mul_comm,
    natDegree_C_mul <| inv_ne_zero <| leadingCoeff_ne_zero.mpr fun H ↦
    hf ((minpolyX_eq_zero_iff f).mp H), natDegree_minpolyX]

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
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
⊢ Irreducible (Polynomial.map (algebraMap F E) f)

Tactic:
have ha : Associated f (minpoly F x) := by
    have := isUnit_C.2 (leadingCoeff_ne_zero.2 hirr.ne_zero).isUnit.inv
    exact ⟨this.unit, by rw [IsUnit.unit_spec, minpoly.eq_of_irreducible hirr hx]⟩

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
hsep : f.Separable
hirr : Irreducible f
inst✝ : IsPurelyInseparable F E
K : Type v := AlgebraicClosure E
x : K
hx : (aeval x) f = 0
ha : Associated f (minpoly F x)
⊢ Irreducible (Polynomial.map (algebraMap F E) f)
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
x y : M
a b : R
hF : F.IsFaceOf C
hx : x ∈ C
hy : y ∈ C
ha : 0 < a
hb : 0 < b
h : a • x + b • y ∈ F
⊢ b • y + a • x ∈ F

Tactic:
rwa [add_comm]

Goal state after:
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 : y + x ∈ F
⊢ y ∈ F

Tactic:
exact mem_of_add_mem_left hF hy hx hxy

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

Goal state before:
pp: case hb
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.map (algebraMap (↥E) K⟮X⟯) (q E) ≠ 0

Tactic:
exact Polynomial.map_ne_zero (q_ne_zero h)

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
C F : PointedCone R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
hF : F.IsFaceOf C
a : R
x : M
hx : x ∈ ↑C
y : M
hy : y ∈ ↑C
ha : 0 < a
z : M
hz₁ : z ∈ ↑F
hz₂ : f z = f (a • x) + f y
⊢ (↑{ c // 0 ≤ c } f) x ∈ map f F

Tactic:
← map_add

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
C F : PointedCone R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
hF : F.IsFaceOf C
a : R
x : M
hx : x ∈ ↑C
y : M
hy : y ∈ ↑C
ha : 0 < a
z : M
hz₁ : z ∈ ↑F
hz₂ : f z = f (a • x + y)
⊢ (↑{ c // 0 ≤ c } f) x ∈ map f F
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 (Q₁ h)).natDegree + (Bivariate.swap (Φ E)).natDegree = (Bivariate.swap (θ E)).natDegree
⊢ (Bivariate.swap (θ E)).natDegree ≤ m E

Tactic:
rw [swap_θ, natDegree_neg]

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
this : (Bivariate.swap (Q₁ h)).natDegree + (Bivariate.swap (Φ E)).natDegree = (Bivariate.swap (θ E)).natDegree
⊢ (θ E).natDegree ≤ m E
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 x : P
hx : x ∈ s
⊢ ↑((orthogonalProjection s) p) = ↑(s.direction.orthogonalProjectionOnto (p -ᵥ x)) +ᵥ x

Tactic:
orthogonalProjection_apply,

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 x : P
hx : x ∈ s
⊢ ↑(s.direction.orthogonalProjectionOnto (p -ᵥ ↑(Classical.arbitrary ↥s)) +ᵥ Classical.arbitrary ↥s) =
    ↑(s.direction.orthogonalProjectionOnto (p -ᵥ x)) +ᵥ x
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
⊢ ↑((orthogonalProjection s) p) -ᵥ p ∈ s.directionᗮ

Tactic:
orthogonalProjection_apply,

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
⊢ ↑(s.direction.orthogonalProjectionOnto (p -ᵥ ↑(Classical.arbitrary ↥s)) +ᵥ Classical.arbitrary ↥s) -ᵥ p ∈ s.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
p : P
⊢ IsCompl s.direction (mk' p s.directionᗮ).direction

Tactic:
rw [direction_mk' p s.directionᗮ]
      exact s.direction.isCompl_orthogonal

Goal state after:
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)
hf : Function.Injective ⇑f.linear
⊢ (Submodule.map f.linear (vectorSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ vectorSpan ℝ (⇑f.toAffineMap '' Set.range s.points) =
    (Submodule.map f.linear (vectorSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓
      (Submodule.map f.linear ⊤ ⊓ Submodule.map f.linear (vectorSpan ℝ (Set.range s.points)))

Tactic:
← Submodule.map_inf _ hf,

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
⊢ (Submodule.map f.linear (vectorSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓ vectorSpan ℝ (⇑f.toAffineMap '' Set.range s.points) =
    (Submodule.map f.linear (vectorSpan ℝ (s.points '' {i}ᶜ)))ᗮ ⊓
      Submodule.map f.linear (⊤ ⊓ vectorSpan ℝ (Set.range s.points))