mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

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

Tactic:
by obtain ⟨M, rfl, rfl⟩ := hex; exact fun I ↦ Indep.subset_ground

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✝ N : Matroid β
inst✝ : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
⊢ (N.comap f).Indep I

Tactic:
comap_indep_iff,

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
inst✝ : N.Finitary
f : α → β
I : Set α
hI : ∀ J ⊆ I, J.Finite → (N.comap f).Indep J
⊢ N.Indep (f '' I) ∧ InjOn f I
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ M.IsRkFinite ((X ∪ Y) ∩ M.E)

Tactic:
refine (M.isRkFinite_of_finite (hIfin.union hJfin)).closure.subset ?_

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ (X ∪ Y) ∩ M.E ⊆ M.closure (I ∪ J)
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
⊢ M.IsRkFinite (X ∪ Y \ X) ↔ M.IsRkFinite Y

Tactic:
union_sdiff_self,

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
⊢ M.IsRkFinite (X ∪ Y) ↔ M.IsRkFinite Y
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Set α
f : α → β
hf : InjOn f (freeOn E).E
⊢ (freeOn E).map f hf = freeOn (f '' E)

Tactic:
← dual_inj

Goal state after:
α : Type u_1
β : Type u_2
E : Set α
f : α → β
hf : InjOn f (freeOn E).E
⊢ ((freeOn E).map f hf)✶ = (freeOn (f '' E))✶
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ M.eRk (X ∩ M.E) = M.eRk I

Tactic:
hI.isBasis_inter_ground.eRk_eq_eRk

Goal state after:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ M.eRk (X ∩ M.E) = M.eRk (X ∩ M.E)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
by
  nth_rw 1 [← inter_union_sdiff X Y]; apply eRk_union_le_eRk_add_eRk

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α
M : Matroid β
f : α → β
⊢ (M.comap f).Indep {e} ↔ M.IsNonloop (f e)

Tactic:
comap_indep_iff,

Goal state after:
α : Type u_1
β : Type u_2
e : α
M : Matroid β
f : α → β
⊢ M.Indep (f '' {e}) ∧ InjOn f {e} ↔ M.IsNonloop (f e)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk M.E ≤ M.eRk ((X ∪ M.E \ X) ∩ M.E)

Tactic:
union_sdiff_self,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk M.E ≤ M.eRk ((X ∪ M.E) ∩ M.E)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
J : Set α
hJ : M.IsBasis' J I
⊢ I.encard ≤ J.encard

Tactic:
← h,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hI : I.Finite
h : M.eRk I = I.encard
J : Set α
hJ : M.IsBasis' J I
⊢ M.eRk I ≤ J.encard
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
X : Set α
⊢ (loopyOn X).eRk (loopyOn X).E = 0

Tactic:
eRk_loopyOn

Goal state after:
α : Type u_1
X : Set α
⊢ 0 = 0
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
h : B = ∅
hB : M.IsBase B
⊢ M.closure ∅ = M.E

Tactic:
← h,

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
h : B = ∅
hB : M.IsBase B
⊢ M.closure B = M.E
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inr.refine_1
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.closure (M.fundCircuit x B \ {x})
⊢ M.fundCircuit x B \ {x} ⊆ B

pp: case inr.refine_2
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.closure (M.fundCircuit x B \ {x})
⊢ e ∉ M.fundCircuit x B \ {x}

Tactic:
· simpa using fundCircuit_subset_insert ..

Goal state after:
case inr.refine_2
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.closure (M.fundCircuit x B \ {x})
⊢ e ∉ M.fundCircuit x B \ {x}
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure X ∩ K = X ∩ K

Tactic:
nth_rw 1 [← inter_eq_self_of_subset_right hK]

Goal state after:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure X ∩ (M.coloops ∩ K) = X ∩ K
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
I₀ : Set α
hI₀ss : I₀ ⊆ f ⁻¹' I ∩ X
hbij : BijOn f I₀ (f '' (f ⁻¹' I ∩ X))
⊢ f '' I₀ = I

Tactic:
rw [hbij.image_eq, image_preimage_inter, inter_eq_self_of_subset_left hIX.subset]

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

Goal state before:
pp: case refine_2
α : Type u
β : Type v
M : Matroid β
f : α → β
X I₀ : Set α
hI₀X : I₀ ⊆ X
hfI₀ : InjOn f I₀
hIX : M.IsBasis' (f '' I₀) (f '' X)
⊢ lift.{u, v} #↑(f '' I₀) ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
rw [mk_image_eq_of_injOn_lift _ _ hfI₀, lift_le]

Goal state after:
case refine_2
α : Type u
β : Type v
M : Matroid β
f : α → β
X I₀ : Set α
hI₀X : I₀ ⊆ X
hfI₀ : InjOn f I₀
hIX : M.IsBasis' (f '' I₀) (f '' X)
⊢ #↑I₀ ≤ ⨆ B, #↑↑B
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ M.closure (I ∩ J) = M.closure I ∩ M.closure J

Tactic:
inter_eq_iInter,

Goal state after:
α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ M.closure (⋂ b, bif b then I else J) = M.closure I ∩ M.closure J
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 ι
⊢ Injective ⇑(aeval x) ↔ Injective ⇑(Polynomial.aeval (x default))

Tactic:
let i := uniqueAlgEquiv 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
inst✝ : Unique ι
i : MvPolynomial ι R ≃ₐ[R] Polynomial R := uniqueAlgEquiv R ι
⊢ Injective ⇑(aeval x) ↔ Injective ⇑(Polynomial.aeval (x default))
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
⊢ (I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.closure (I \ {e})) ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I

Tactic:
refine ⟨fun ⟨hIE, h⟩ e heI h_eq ↦ h e heI (h_eq.symm.subset (M.mem_closure_of_mem heI)),
    fun h ↦ ⟨fun e heI ↦ by_contra fun heE ↦ h heI ?_,fun e heI hin ↦ h heI ?_⟩⟩

Goal state after:
case refine_1
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.closure (I \ {e}) = M.closure I

case refine_2
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure I
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
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι S), (aeval (⇑g ∘ x)) p = 0 → p = 0
hf : Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
p : MvPolynomial ι R
hp : (aeval x) p = 0
this : (eval₂Hom ((↑g).comp (algebraMap R A)) fun i ↦ ↑g (x i)) p = 0
⊢ (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) p) = 0

Tactic:
← h,

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι S), (aeval (⇑g ∘ x)) p = 0 → p = 0
hf : Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
p : MvPolynomial ι R
hp : (aeval x) p = 0
this : (eval₂Hom ((algebraMap S B).comp ↑f) fun i ↦ ↑g (x i)) p = 0
⊢ (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) p) = 0
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
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι S), (aeval (⇑g ∘ x)) p = 0 → p = 0
hf : Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
p : MvPolynomial ι R
hp : (aeval x) p = 0
⊢ (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) p) = 0

Tactic:
by
    have : (g : A →+* B) _ = _ := congr(g $hp)
    rwa [map_zero, map_aeval, ← h, ← eval₂Hom_map_hom, ← aeval_eq_eval₂Hom] at this

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
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
hf : Surjective ⇑f
hg : Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : MvPolynomial ι R
hp : (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) q) = 0
⊢ (eval₂Hom ((↑g).comp (algebraMap R A)) fun i ↦ ↑g (x i)) q = 0

Tactic:
← h,

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
hf : Surjective ⇑f
hg : Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : MvPolynomial ι R
hp : (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) q) = 0
⊢ (eval₂Hom ((algebraMap S B).comp ↑f) fun i ↦ ↑g (x i)) q = 0
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: case zero
F : Type u_1
inst✝¹ : Field F
f g : F[X]
inst✝ : CharZero F
hf : HasSeparableContraction 1 f
left✝ : g.Separable
m : ℕ
hm : (expand F (1 ^ m)) g = f
⊢ g.natDegree = hf.degree

Tactic:
one_pow,

Goal state after:
case zero
F : Type u_1
inst✝¹ : Field F
f g : F[X]
inst✝ : CharZero F
hf : HasSeparableContraction 1 f
left✝ : g.Separable
m : ℕ
hm : (expand F 1) g = f
⊢ g.natDegree = hf.degree
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ ∀ (x : α),
    f x ∈ M.E ∧ ((M.comap f).Indep (insert x I) → x ∈ I) ↔ f x ∈ M.E ∧ (M.Indep (insert (f x) (f '' I)) → f x ∈ f '' I)

Tactic:
comap_indep_iff,

Goal state after:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ ∀ (x : α),
    f x ∈ M.E ∧ (M.Indep (f '' insert x I) ∧ InjOn f (insert x I) → x ∈ I) ↔
      f x ∈ M.E ∧ (M.Indep (insert (f x) (f '' I)) → f x ∈ f '' I)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
x✝ : ∃ x, C x = g
x : F
h : C x = g
hx : x = 0
⊢ g = 0

Tactic:
← h,

Goal state after:
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
x✝ : ∃ x, C x = g
x : F
h : C x = g
hx : x = 0
⊢ C x = 0
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case zero
F : Type u
inst✝² : Field F
f : F[X]
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
inst✝¹ : CharZero F
inst✝ : ExpChar F 1
hf : f = X ^ 1 ^ n - C y
⊢ ∃ n y, (n = 0 ∨ y ∉ (frobenius F 1).range) ∧ f = X ^ 1 ^ n - C y

Tactic:
one_pow,

Goal state after:
case zero
F : Type u
inst✝² : Field F
f : F[X]
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
inst✝¹ : CharZero F
inst✝ : ExpChar F 1
hf : f = X ^ 1 - C y
⊢ ∃ n y, (n = 0 ∨ y ∉ (frobenius F 1).range) ∧ f = X ^ 1 - C y
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
i : E →ₐ[F] K
⊢ comap i (separableClosure F K) = separableClosure F E

Tactic:
ext x
  exact map_mem_separableClosure_iff i

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case convert_2.refine_1
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
h : (minpoly F x).natSepDegree = 1
⊢ ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0

Tactic:
obtain ⟨n, y, hx⟩ := (minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C q).1 h

Goal state after:
case convert_2.refine_1
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
h : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
hx : minpoly F x = X ^ q ^ n - C y
⊢ ∃ n y, (Polynomial.aeval x) (X ^ q ^ n - C y) = 0
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ Module.rank (↥⊤) F = 1

Tactic:
IntermediateField.rank_top

Goal state after:
F : Type u
inst✝ : Field F
⊢ 1 = 1
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).natDegree ≠ 0

Tactic:
← Nat.one_le_iff_ne_zero

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).natDegree
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
inst✝ : FiniteDimensional F E
h : Nat.card Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ finrank F E = 1 * finrank (↥(fixedField ⊤)) E

Tactic:
← h,

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Nat.card Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ Nat.card Gal(E/F) = 1 * finrank (↥(fixedField ⊤)) E
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
⊢ Module.rank (↥⊤) E = 1

Tactic:
IntermediateField.rank_top

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
⊢ 1 = 1
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
K L : IntermediateField F E
inst✝ : Normal F ↥K
h : K ⊔ L = ⊤
φ : Gal(E/↥L)
hφ : (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E) φ = 1
⊢ (MulSemiringAction.toAlgAut Gal(E/↥L) F E) φ ∈ ⊤.fixingSubgroup

Tactic:
← h,

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
K L : IntermediateField F E
inst✝ : Normal F ↥K
h : K ⊔ L = ⊤
φ : Gal(E/↥L)
hφ : (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E) φ = 1
⊢ (MulSemiringAction.toAlgAut Gal(E/↥L) F E) φ ∈ (K ⊔ L).fixingSubgroup
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case pos
R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
h : σ x = y
⊢ eval₂ σ y (minpolyDiv R x) = σ ((aeval x) (derivative (minpoly R x)))

Tactic:
← h,

Goal state after:
case pos
R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
h : σ x = y
⊢ eval₂ σ (σ x) (minpolyDiv R x) = σ ((aeval x) (derivative (minpoly R x)))
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
x : S
hx : IsIntegral R x
a b : R[X]
h : (Polynomial.aeval x) a * (Polynomial.aeval x) b = 0
h' : ¬(Polynomial.aeval x) a = 0
⊢ (Polynomial.aeval x) b = 0

Tactic:
exact eq_zero_of_ne_zero_of_mul_left_eq_zero h' h

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

Goal state before:
pp: case a
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
⊢ Subalgebra.toSubmodule R[x] ≤ Submodule.span R (Set.range (minpolyDiv R x).coeff)

Tactic:
← Submodule.span_range_natDegree_eq_adjoin (minpoly.monic hx) (minpoly.aeval _ _),

Goal state after:
case a
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
⊢ Submodule.span R ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range (minpoly R x).natDegree)) ≤
    Submodule.span R (Set.range (minpolyDiv R x).coeff)
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
x✝ x : S
B : PowerBasis R S
hint : IsIntegral R x
hx : B.gen ∈ R[x]
⊢ PowerBasis R S

Tactic:
apply PowerBasis.ofAdjoinEqTop' hint

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
x✝ x : S
B : PowerBasis R S
hint : IsIntegral R x
hx : B.gen ∈ R[x]
⊢ R[x] = ⊤
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case pos
F✝ : Type u
E✝ : Type v
inst✝¹¹ : Field F✝
inst✝¹⁰ : Field E✝
inst✝⁹ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁸ : ExpChar F✝ q✝
inst✝⁷ : IsPurelyInseparable F✝ E✝
inst✝⁶ : FiniteDimensional F✝ E✝
E : Type v
inst✝⁵ : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_1 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E], finrank F E = m → ∃ n, m = q ^ n
F : Type v
inst✝⁴ : Field F
inst✝³ : Algebra F E
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
hd : finrank F ↥⊤ = d
h : ⊥ = ⊤
⊢ ∃ n, d = q ^ n

Tactic:
← h,

Goal state after:
case pos
F✝ : Type u
E✝ : Type v
inst✝¹¹ : Field F✝
inst✝¹⁰ : Field E✝
inst✝⁹ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁸ : ExpChar F✝ q✝
inst✝⁷ : IsPurelyInseparable F✝ E✝
inst✝⁶ : FiniteDimensional F✝ E✝
E : Type v
inst✝⁵ : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_1 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E], finrank F E = m → ∃ n, m = q ^ n
F : Type v
inst✝⁴ : Field F
inst✝³ : Algebra F E
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
hd : finrank F ↥⊥ = d
h : ⊥ = ⊤
⊢ ∃ n, d = q ^ n
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

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
S : IntermediateField E K := separableClosure E K
h : adjoin E (Subtype.val '' ↑(separableClosure F ↥S)) = S
this : IsScalarTower F (↥S) K
⊢ adjoin E ↑(separableClosure F K) = S

Tactic:
← h,

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
inst✝ : Algebra.IsAlgebraic F E
S : IntermediateField E K := separableClosure E K
h : adjoin E (Subtype.val '' ↑(separableClosure F ↥S)) = S
this : IsScalarTower F (↥S) K
⊢ adjoin E ↑(separableClosure F K) = adjoin E (Subtype.val '' ↑(separableClosure F ↥S))
Module: Mathlib.RingTheory.Trace.Basic

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

Tactic:
one_pow,

Goal state after:
case pos.succ.zero
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
H : ¬Algebra.IsSeparable K L
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
n : ℕ
inst✝ : CharZero K
this : 1 ≠ 0
hn : finrank (↥(separableClosure K L)) L = 1
⊢ (trace K ↥(separableClosure K L)) (finrank (↥(separableClosure K L)) L • x) =
    0 ((algebraMap (↥(separableClosure K L)) L) x)
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
hr✝¹ : map (algebraMap B (B ⧸ Q)) r = q
hf : eval b f = 0
hr✝ : eval b r ∈ Q
a : B := f.coeff j
ha : ∀ (g : G), g • a = a
g : G
hg : g • Q ≠ Q
hr : r = ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
⊢ eval b (∑ i ∈ Finset.range k, (monomial i) (f.coeff (i + 1 + j))) * b ∈ g • Q

Tactic:
exact Ideal.mul_mem_left (g • Q) _ (hbP g hg)

Goal state after: