mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : AddCommMonoid Q
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I J : (Submodule R A)ˣ
⊢ Function.Injective (⇑(↑(I * J)).subtype ∘ ⇑((↑I).mulMap' ↑J))

Tactic:
convert!
    (projective_units_and_mul'_comp_lTensor_bijective J).2.1.comp
      (Flat.rTensor_preserves_injective_linearMap _ I.1.subtype_injective)

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : AddCommMonoid Q
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Module R P
inst✝³ : Module R Q
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I J : (Submodule R A)ˣ
⊢ ⇑(↑(I * J)).subtype ∘ ⇑((↑I).mulMap' ↑J) =
    ⇑(LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (↑J).subtype) ∘ ⇑(LinearMap.rTensor (↥↑J) (↑I).subtype)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ I = ⋃ i, I

Tactic:
iUnion_const

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ I = I
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.Indep (⋃ i, I)

Tactic:
iUnion_const

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B X : Set α
hX : X ⊆ M.E
hB : M.IsBase B
hBX : B ⊆ X
⊢ B ⊆ X ∧ ∀ (J : Set α), M.Indep J → B ⊆ J → J ⊆ X → B = J

Tactic:
and_iff_right hBX

Goal state after:
α : Type u_1
M : Matroid α
B X : Set α
hX : X ⊆ M.E
hB : M.IsBase B
hBX : B ⊆ X
⊢ ∀ (J : Set α), M.Indep J → B ⊆ J → J ⊆ X → B = J
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I E : Set α
⊢ (uniqueBaseOn I E)✶ = uniqueBaseOn (E \ I) E

Tactic:
rw [← uniqueBaseOn_inter_ground_eq]
  refine ext_isBase rfl (fun B (hB : B ⊆ E) ↦ ?_)
  rw [dual_isBase_iff, uniqueBaseOn_isBase_iff inter_subset_right,
    uniqueBaseOn_isBase_iff sdiff_subset, uniqueBaseOn_ground]
  exact ⟨fun h ↦ by rw [← sdiff_sdiff_cancel_left hB, h, sdiff_inter_self_eq_sdiff],
    fun h ↦ by rw [h, inter_comm I]; simp⟩

Goal state after:
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
Indep : Set α → Prop
M : Matroid α
h : ∀ (I : Set α), M.Indep I ↔ Indep I
⊢ ∃ M_1, M.E = M_1.E ∧ M_1.Indep = Indep

Tactic:
refine ⟨_, rfl, funext (by simp [h])⟩

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
I : Set β
⊢ (∃ s ⊆ M.E, M.Indep s ∧ I = f '' s) ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀

Tactic:
exact ⟨fun ⟨I₀, _, hI₀⟩ ↦ ⟨I₀, hI₀⟩, fun ⟨I₀, hI₀⟩ ↦ ⟨I₀, hI₀.1.subset_ground, hI₀⟩⟩

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
hss : M.fundCircuit e I ⊆ C
⊢ e ∈ M.closure I

Tactic:
rw [hI.mem_closure_iff]
      exact .inl (hC.dep.superset hCs (insert_subset (hC.subset_ground heC) hI.subset_ground))

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
⊢ X ∪ X \ M.E = X ∧ (M ↾ X).E = X

Tactic:
union_eq_self_of_subset_right sdiff_subset,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
⊢ X = X ∧ (M ↾ X).E = X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk (X ∪ M.closure Y) = M.eRk (X ∪ Y)

Tactic:
rw [← eRk_closure_eq, closure_union_closure_right_eq, eRk_closure_eq]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
⊢ M.IsNonloop f

Tactic:
by
  rw [isNonloop_iff, and_comm]
  by_contra! h; apply he.not_isLoop
  rw [isLoop_iff] at *; convert! hef using 1
  obtain (hf | hf) := em (f ∈ M.E)
  · rw [← closure_loops, ← insert_eq_of_mem (h hf), closure_insert_congr_right M.closure_loops,
      insert_empty_eq]
  rw [eq_comm, ← closure_inter_ground, inter_comm, inter_singleton_eq_empty.mpr hf, loops]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
e : α
M : Matroid α
X Y : Set α
⊢ M.eRk (insert e X ∩ insert e Y) + M.eRk (insert e (X ∪ Y)) ≤ M.eRk (insert e X) + M.eRk (insert e Y)

Tactic:
insert_union_distrib

Goal state after:
α : Type u_1
e : α
M : Matroid α
X Y : Set α
⊢ M.eRk (insert e X ∩ insert e Y) + M.eRk (insert e X ∪ insert e Y) ≤ M.eRk (insert e X) + M.eRk (insert e Y)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
h : M.IsLoop e
⊢ ¬M.IsColoop e

Tactic:
rw [← dual_isLoop_iff_isColoop]; rw [← dual_dual M, dual_isLoop_iff_isColoop] at h
  exact h.isNonloop.not_isLoop

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
⊢ C ∩ K ≠ ∅ → (C ∩ K).Nontrivial

Tactic:
← nonempty_iff_ne_empty

Goal state after:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
⊢ (C ∩ K).Nonempty → (C ∩ K).Nontrivial
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case neg
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite ↑(B' \ B)
S : (a : α) → a ∈ B' \ B → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite ↑(S a ha)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ a, S ↑a ⋯
hUB : B ∩ B' ∪ U ⊆ B
hBU : ¬B ⊆ B ∩ B' ∪ U
a : α
ha : a ∈ B' \ (B ∩ B' ∪ U)
ind : N.Indep (insert a (B ∩ B' ∪ U))
this : a ∈ B' \ B
⊢ S a this ⊆ U

Tactic:
exact subset_iUnion_of_subset ⟨a, this⟩ subset_rfl

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := uniqueAlgEquiv R ι
y : ι
⊢ (aeval x) (X y) = ((Polynomial.aeval (x default)).comp ↑i) (X y)

Tactic:
simp [i, Subsingleton.elim y default]

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
i : ι
hs : AlgebraicIndepOn R x s
hi : Transcendental (↥(adjoin R (x '' s))) (x i)
⊢ AlgebraicIndepOn R x (insert i s)

Tactic:
nontriviality R

Goal state after:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
i : ι
hs : AlgebraicIndepOn R x s
hi : Transcendental (↥(adjoin R (x '' s))) (x i)
a✝ : Nontrivial R
⊢ AlgebraicIndepOn R x (insert i s)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ False

Tactic:
refine (h (sdiff_singleton_ssubset.2 heI)).ne ?_

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure I
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i ↦ (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i ↦ x ↑i
i : ι
hi : i ∉ t
a✝ : ι
h : a✝ ∈ t
⊢ X a✝ ∈ X '' t

Tactic:
Set.mem_image_of_mem _ h

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
⊢ AlgebraicIndependent R Subtype.val

Tactic:
nontriviality R

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a✝ : Nontrivial R
⊢ AlgebraicIndependent R Subtype.val
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
x : ι → A
f : A →ₐ[R] A'
h : Injective ⇑f
H : IsTranscendenceBasis R (⇑f ∘ x)
s : Set A
hs : AlgebraicIndepOn R _root_.id s
hs' : range x ⊆ s
⊢ range (⇑f ∘ x) ⊆ ⇑f '' s

Tactic:
rw [Set.range_comp]

Goal state after:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
x : ι → A
f : A →ₐ[R] A'
h : Injective ⇑f
H : IsTranscendenceBasis R (⇑f ∘ x)
s : Set A
hs : AlgebraicIndepOn R _root_.id s
hs' : range x ⊆ s
⊢ ⇑f '' range x ⊆ ⇑f '' s
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Injective ⇑f
⊢ lift.{v', v} (trdeg R A) ≤ lift.{v, v'} (trdeg R A')

Tactic:
nontriviality R

Goal state after:
R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Injective ⇑f
a✝ : Nontrivial R
⊢ lift.{v', v} (trdeg R A) ≤ lift.{v, v'} (trdeg R A')
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective ⇑f
⊢ lift.{v, v'} (trdeg R A') ≤ lift.{v', v} (trdeg R A)

Tactic:
nontriviality R

Goal state after:
R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective ⇑f
a✝ : Nontrivial R
⊢ lift.{v, v'} (trdeg R A') ≤ lift.{v', v} (trdeg R A)
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_3
ι' : Type u_4
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x ↦ g (f ↑x)
⊢ AlgebraicIndependent R fun x ↦ g ↑x

Tactic:
nontriviality R

Goal state after:
R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_3
ι' : Type u_4
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x ↦ g (f ↑x)
a✝ : Nontrivial R
⊢ AlgebraicIndependent R fun x ↦ g ↑x
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nonempty ι
⊢ IsTranscendenceBasis R X

Tactic:
nontriviality R

Goal state after:
ι : Type u
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nonempty ι
a✝ : Nontrivial R
⊢ IsTranscendenceBasis R X
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
⊢ IsTranscendenceBasis R fun x ↦ Polynomial.X

Tactic:
nontriviality R

Goal state after:
ι : Type u
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
a✝ : Nontrivial R
⊢ IsTranscendenceBasis R fun x ↦ Polynomial.X
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inl
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
s t : Set A
a : A
h : (matroid R A).IsBasis s t
h✝ : Subsingleton A
⊢ IsAlgebraic (↥(adjoin R s)) a ↔ IsAlgebraic (↥(adjoin R t)) a

pp: case inr
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
s t : Set A
a : A
h : (matroid R A).IsBasis s t
h✝ : Nontrivial A
⊢ IsAlgebraic (↥(adjoin R s)) a ↔ IsAlgebraic (↥(adjoin R t)) a

Tactic:
· apply iff_of_false <;> apply is_transcendental_of_subsingleton

Goal state after:
case inr
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
s t : Set A
a : A
h : (matroid R A).IsBasis s t
h✝ : Nontrivial A
⊢ IsAlgebraic (↥(adjoin R s)) a ↔ IsAlgebraic (↥(adjoin R t)) a
Module: Mathlib.FieldTheory.SeparableDegree

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
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
⊢ Infinite (Emb F ↥(adjoin F (Set.range x)))

Tactic:
rw [← (embEquivOfEquiv _ _ _ hx.1.aevalEquivField).infinite_iff]

Goal state after:
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
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
⊢ Infinite (Emb F (FractionRing (MvPolynomial ι F)))
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inl
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
j : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial S
this✝¹ : IsDomain S
this✝ : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj✝ : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
x : ι
hxj : x ∉ {j}
hj : j ∈ insert x s
this : Nontrivial ↥(adjoin R (v '' (insert x s \ {j})))
H₂ : v j ∈ (matroid R S).closure (v '' (insert x s \ {j}))
hi : x ∉ s
eq : v x = v j
⊢ v ↑⟨x, ⋯⟩ = ((fun x ↦ v ↑x) ∘ ⇑((Equiv.image (Equiv.swap j x) s).trans (Equiv.setCongr ⋯)).symm) ⟨x, ⋯⟩

Tactic:
simp [eq]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case convert_2.refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
x✝ : ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
n : ℕ
y : F
h : (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
hnezero : X ^ q ^ n - C y ≠ 0
⊢ (minpoly F x).natSepDegree = 1

Tactic:
refine ((natSepDegree_le_of_dvd _ _ (minpoly.dvd F x h) hnezero).trans_eq <|
    natSepDegree_X_pow_char_pow_sub_C q n y).antisymm ?_

Goal state after:
case convert_2.refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
x✝ : ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
n : ℕ
y : F
h : (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
hnezero : X ^ q ^ n - C y ≠ 0
⊢ 1 ≤ (minpoly F x).natSepDegree
Module: Mathlib.FieldTheory.SeparableClosure

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
⊢ Cardinal.toNat (insepDegree F K) = finInsepDegree F K

Tactic:
← finInsepDegree_def'

Goal state after:
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
⊢ finInsepDegree F K = finInsepDegree F K
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
⊢ (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E)

Tactic:
change (K⟮x⟯ →ₐ[F] E) ≃ Σ f : K →ₐ[F] E, _

Goal state after:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
⊢ (↥K⟮x⟯ →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E)
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : FiniteDimensional K ↥E
⊢ IsOpen ↑E.fixingSubgroup

Tactic:
have h_basis : E.fixingSubgroup.carrier ∈ galGroupBasis K L :=
    ⟨E.fixingSubgroup, ⟨E, ‹_›, rfl⟩, rfl⟩
  have h_nhds := GroupFilterBasis.mem_nhds_one (galGroupBasis K L) h_basis
  exact Subgroup.isOpen_of_mem_nhds _ h_nhds

Goal state after:
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
f : Gal(↥(adjoin ↥L {x}).toIntermediateField/↥L)
a✝ : f ∈ ⊤
σ : Gal(K/↥L)
hσ : (restrictNormalHom ↥(adjoin ↥L {x}).toIntermediateField) σ = f
⊢ ↑(f ⟨x, mem⟩) = ↑⟨x, mem⟩

Tactic:
rw [← hσ, restrictNormalHom_apply (adjoin L {x}).1 σ ⟨x, mem⟩]

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
f : Gal(↥(adjoin ↥L {x}).toIntermediateField/↥L)
a✝ : f ∈ ⊤
σ : Gal(K/↥L)
hσ : (restrictNormalHom ↥(adjoin ↥L {x}).toIntermediateField) σ = f
⊢ σ ↑⟨x, mem⟩ = ↑⟨x, mem⟩
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
⊢ ∃ g', map (algebraMap R K) g' * C g.leadingCoeff = g

Tactic:
have g_ne_0 : g ≠ 0 := ne_zero_of_dvd_ne_zero (Monic.ne_zero <| hf.map (algebraMap R K)) hg
  suffices lem : ∃ g' : R[X], g'.map (algebraMap R K) = g * C g.leadingCoeff⁻¹ by
    obtain ⟨g', hg'⟩ := lem
    use g'
    rw [hg', mul_assoc, ← C_mul, inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr g_ne_0), C_1, mul_one]
  have g_mul_dvd : g * C g.leadingCoeff⁻¹ ∣ f.map (algebraMap R K) := by
    rwa [Associated.dvd_iff_dvd_left (show Associated (g * C g.leadingCoeff⁻¹) g from _)]
    rw [associated_mul_isUnit_left_iff]
    exact isUnit_C.mpr (inv_ne_zero <| leadingCoeff_ne_zero.mpr g_ne_0).isUnit
  let algeq :=
    (Subalgebra.equivOfEq _ _ <| integralClosure_eq_bot R _).trans
      (Algebra.botEquivOfInjective <| IsFractionRing.injective R <| K)
  have :
    (algebraMap R _).comp algeq.toAlgHom.toRingHom = (integralClosure R _).toSubring.subtype := by
    ext x; (conv_rhs => rw [← algeq.symm_apply_apply x]); rfl
  have H :=
    (mem_lifts _).1
      (integralClosure.mem_lifts_of_monic_of_dvd_map K hf (monic_mul_leadingCoeff_inv g_ne_0)
        g_mul_dvd)
  refine ⟨map algeq.toAlgHom.toRingHom ?_, ?_⟩
  · use! Classical.choose H
  · rw [map_map, this]
    exact Classical.choose_spec H

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
⊢ ∑ σ, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) = X ^ r

Tactic:
rw [← sub_eq_zero]

Goal state after:
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
⊢ ∑ σ, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r = 0
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
⊢ ∃ x, a * x ^ n + b * x + c = 0

Tactic:
let f : k[X] := C a * X ^ n + C b * X + C c

Goal state after:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
n : ℕ
a b c : k
hn : ↑n = 0
hn' : 2 ≤ n
hb : b ≠ 0
f : k[X] := C a * X ^ n + C b * X + C c
⊢ ∃ x, a * x ^ n + b * x + c = 0
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: K : Type v
inst✝² : Field K
k : Type u_1
inst✝¹ : CommSemiring k
inst✝ : IsSepClosed K
f : k →+* K
hf : Function.Injective ⇑f
p : k[X]
hp : p.degree ≠ 0
hsep : p.Separable
⊢ (map f p).degree ≠ 0

Tactic:
degree_map_eq_of_injective hf

Goal state after:
K : Type v
inst✝² : Field K
k : Type u_1
inst✝¹ : CommSemiring k
inst✝ : IsSepClosed K
f : k →+* K
hf : Function.Injective ⇑f
p : k[X]
hp : p.degree ≠ 0
hsep : p.Separable
⊢ p.degree ≠ 0
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : Nontrivial S
pb : PowerBasis K S
⊢ (Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff

Tactic:
have d_pos : 0 < pb.dim := PowerBasis.dim_pos pb

Goal state after:
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
⊢ (Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ x.valMinAbs = y

Tactic:
rw [← sub_eq_zero]

Goal state after:
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ x.valMinAbs - y = 0
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ x.valMinAbs - y = 0

Tactic:
apply @Int.eq_zero_of_abs_lt_dvd n

Goal state after:
case h1
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ ↑n ∣ x.valMinAbs - y

case h2
n : ℕ
inst✝ : NeZero n
x : ZMod n
y : ℤ
h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
⊢ |x.valMinAbs - y| < ↑n
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos.succ.prime
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
this : p ≠ 0
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
hn : finrank (↥(separableClosure K L)) L = p ^ (n + 1)
hprime : Nat.Prime p
hchar✝ : CharP K p
⊢ (trace K ↥(separableClosure K L)) (finrank (↥(separableClosure K L)) L • x) =
    0 ((algebraMap (↥(separableClosure K L)) L) x)

Tactic:
rw [hn, pow_succ', mul_smul, LinearMap.map_smul_of_tower, nsmul_eq_mul,
          CharP.cast_eq_zero, zero_mul, LinearMap.zero_apply]

Goal state after: