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

Goal state before:
pp: case pos
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
hmn : 0 < n
hm : m = 0
heq : ⊥ = F⟮α ^ n⟯
y : F
h : (algebraMap F E) y = α ^ n
⊢ (aeval α) (X ^ n - C y) = 0

Tactic:
simp only [map_sub, map_pow, aeval_X, aeval_C, h, sub_self]

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

Goal state before:
pp: case inr
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
x✝¹ : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) Is
x✝ : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : α → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun x ↦ x ∈ J) j → f x ⊆ f j → f j ⊆ f x
y : α
hyJ : y ∈ J
hle : f y ⊆ f x
⊢ y ∈ f x

Tactic:
exact hle (hf _ hyJ).2

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Finite F
α : ↥K
h : F⟮α⟯ = ⊤
⊢ F⟮↑α⟯ = K

Tactic:
simpa only [lift_adjoin_simple, lift_top] using congr_arg lift h

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X B : Set α
hB : M.IsBase B
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
B'' : Set α
hB'' : M.IsBase B''
hIE : B''ᶜ ∩ M.E ⊆ M.E
hIB : Disjoint (B''ᶜ ∩ M.E) B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E)
hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))
hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ
⊢ False

Tactic:
apply hI

Goal state after:
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X B : Set α
hB : M.IsBase B
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := ⋯
hB' : M.IsBase B'
hX : B' = M.E \ X
B'' : Set α
hB'' : M.IsBase B''
hIE : B''ᶜ ∩ M.E ⊆ M.E
hIB : Disjoint (B''ᶜ ∩ M.E) B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E)
hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))
hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ
⊢ M.IsBase (M.E \ (B''ᶜ ∩ M.E))
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
⊢ ∃ I J, M.IsBasis I X ∧ M.IsBasis (I ∪ J) Y ∧ Disjoint X J

Tactic:
obtain ⟨I, I', hI, hI', hII'⟩ := M.exists_isBasis_subset_isBasis hXY

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ ∃ I J, M.IsBasis I X ∧ M.IsBasis (I ∪ J) Y ∧ Disjoint X J
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R I X : Set α
⊢ X ⊆ R → (M.IsBasis' I (X ∩ R) ∧ I ⊆ R ↔ M.IsBasis I (X ∩ M.E))

Tactic:
← isBasis'_iff_isBasis_inter_ground

Goal state after:
α : Type u_1
M : Matroid α
R I X : Set α
⊢ X ⊆ R → (M.IsBasis' I (X ∩ R) ∧ I ⊆ R ↔ M.IsBasis' I X)
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R I X : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsBasis I X ↔ M.IsBasis I X ∧ X ⊆ R

Tactic:
rw [isBasis_restrict_iff', and_congr_left_iff]
  intro hXR
  rw [← isBasis'_iff_isBasis_inter_ground, isBasis'_iff_isBasis]

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

Goal state before:
pp: α : Type u_1
E I X : Set α
hX : X ⊆ E
⊢ (uniqueBaseOn I E).IsBasis (X ∩ I) X

Tactic:
rw [uniqueBaseOn_isBasis_iff hX]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R = M
⊢ R = M.E

Tactic:
← h

Goal state after:
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R = M
⊢ R = (M ↾ R).E
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
⊢ M✶.IsBase B ↔ M.IsBase (M.E \ B) ∧ B ⊆ M.E

Tactic:
by rw [dual_isBase_iff, and_iff_left 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✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
⊢ (N ↾ range f).IsBase (f '' B)

Tactic:
refine Indep.isBase_of_forall_insert (by simpa using hBmax.1.1) ?_

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
⊢ ∀ e ∈ (N ↾ range f).E \ f '' B, ¬(N ↾ range f).Indep (insert e (f '' B))
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
R : Set α
M : Matroid α
hR : R ⊂ M.E
⊢ M ↾ R <r M

Tactic:
refine (M.restrict_isRestriction R hR.subset).isStrictRestriction_of_ne (fun h ↦ ?_)
  rw [← h, restrict_ground_eq] at hR
  exact hR.ne rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
⊢ ∀ t ⊆ f ⁻¹' N.E, (∃ I₀, (N.Indep (f '' I₀) ∧ InjOn f I₀) ∧ f '' t = f '' I₀) ↔ N.Indep (f '' t)

Tactic:
exact fun I hI ↦ ⟨by grind, fun h ↦ ⟨_, ⟨h, hf.mono hI⟩, rfl⟩⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
hX : X ⊆ M.E
h : M.eRk X = n
I : Set α
hI : M.IsBasis I X
⊢ M.eRk X = n

Tactic:
← h

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
hX : X ⊆ M.E
h : M.eRk X = n
I : Set α
hI : M.IsBasis I X
⊢ M.eRk X = M.eRk X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
⊢ e ∈ M.closure {?m.32}

Tactic:
← h

Goal state after:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
⊢ e ∈ M.closure {e}
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
⊢ M.closure X = ↑(M.subtypeClosure ⟨X ∩ M.E, ⋯⟩)

Tactic:
suffices ∀ (x : α), (∀ (t : Set α), M.IsFlat t → X ∩ M.E ⊆ t → x ∈ t) ↔
    (x ∈ M.E ∧ ∀ a ⊆ M.E, X ∩ M.E ⊆ a → M.IsFlat a → x ∈ a) by
    simpa [closure, subtypeClosure, Set.ext_iff]
  exact fun x ↦ ⟨fun h ↦ ⟨h _ M.ground_isFlat inter_subset_right, fun F _ hXF hF ↦ h F hF hXF⟩,
    fun ⟨_, h⟩ F hF hXF ↦ h F hF.subset_ground hXF hF⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsColoop e
hI : M.Indep I
h : e ∈ I
⊢ M.Indep (insert e I)

Tactic:
insert_eq_of_mem h

Goal state after:
α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsColoop e
hI : M.Indep I
h : e ∈ I
⊢ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
h : M.removeLoops = M
⊢ M.Loopless

Tactic:
← h

Goal state after:
α : Type u_1
M : Matroid α
h : M.removeLoops = M
⊢ M.removeLoops.Loopless
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₀ ⊆ X, f '' I₀ = I ∧ InjOn f I₀

Tactic:
obtain ⟨I₀, hI₀ss, hbij⟩ := exists_subset_bijOn (f ⁻¹' I ∩ X) f

Goal state after:
α : 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))
⊢ ∃ I₀ ⊆ X, f '' I₀ = I ∧ InjOn f 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
inst✝ : IsEmpty ι
⊢ AlgebraicIndependent R x ↔ Injective ⇑(algebraMap R A)

Tactic:
rw [algebraicIndependent_iff_injective_aeval, MvPolynomial.aeval_injective_iff_of_isEmpty]

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

Goal state before:
pp: α : Type u
M : Matroid α
⊢ M.RankInfinite ↔ ℵ₀ ≤ M.cRank

Tactic:
by
  rw [← not_lt, ← rankFinite_iff_cRank_lt_aleph0, not_rankFinite_iff]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
h : I \ X = I
⊢ False

Tactic:
rw [sdiff_eq_left, disjoint_iff_inter_eq_empty] at h

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
h : I ∩ X = ∅
⊢ False
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hI : M.IsBasis I (X ∩ M.E)
⊢ f ∈ M.closure (insert e (X ∩ M.E))

Tactic:
rw [← hI.closure_eq_closure, hI.indep.notMem_closure_iff] at he

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
⊢ f ∈ M.closure (insert e (X ∩ M.E))
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
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : ↥(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t) → ↑s := fun x ↦ ⟨↑x, ⋯⟩
⊢ AlgebraicIndependent R Subtype.val

Tactic:
convert! AlgebraicIndependent.comp li f _

Goal state after:
R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : ↥(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t) → ↑s := fun x ↦ ⟨↑x, ⋯⟩
⊢ Injective f
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
X R : Set α
M : Matroid α
hXR : X ⊆ R
hR : R ⊆ M.E
⊢ M.closure (X ∩ R) ∩ R = M.closure X ∩ R

Tactic:
inter_eq_self_of_subset_left hXR

Goal state after:
α : Type u_2
X R : Set α
M : Matroid α
hXR : X ⊆ R
hR : R ⊆ M.E
⊢ M.closure X ∩ R = M.closure X ∩ R
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
X : Set α
⊢ M.E ⊆ M.closure X

Tactic:
← h

Goal state after:
α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
X : Set α
⊢ M.closure ∅ ⊆ M.closure X
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s B : Set A
hB : (matroid R A).IsBasis B s
⊢ ∀ (x : A),
    (True ∧ B ⊆ insert x B ∧ ∀ a ∈ insert x B, IsAlgebraic (↥(adjoin R B)) a) ↔
      x ∈ ↑(algebraicClosure (↥(adjoin R s)) A)

Tactic:
subset_insert,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s B : Set A
hB : (matroid R A).IsBasis B s
⊢ ∀ (x : A), (True ∧ True ∧ ∀ a ∈ insert x B, IsAlgebraic (↥(adjoin R B)) a) ↔ x ∈ ↑(algebraicClosure (↥(adjoin R s)) A)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ f.Separable

Tactic:
simp_rw [← card_rootSet_eq_natDegree_iff_of_splits hf (SplittingField.splits f),
    rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ (f.aroots f.SplittingField).toFinset.card = f.natDegree
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
p : F[X]
hM : p.Monic
hI : Irreducible p
hf✝ : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H✝ : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
c : F[X]
h : p.natSepDegree + c.natSepDegree = 1
hf : f = p ^ multiplicity p f * c
H : ¬p ∣ c
⊢ f = (X ^ q ^ n - C y) ^ multiplicity p f

Tactic:
hD,

Goal state after:
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
p : F[X]
hM : p.Monic
hI : Irreducible p
hf✝ : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H✝ : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
c : F[X]
h : 1 + c.natSepDegree = 1
hf : f = p ^ multiplicity p f * c
H : ¬p ∣ c
⊢ f = (X ^ q ^ n - C y) ^ multiplicity p f
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
K : IntermediateField F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
| finrank (↥K) E

Tactic:
rw [← fixedField_fixingSubgroup K, IntermediateField.finrank_fixedField_eq_card]

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K : IntermediateField F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
| Nat.card ↥K.fixingSubgroup
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 : fixedField ⊤ = ⊥
⊢ IsGalois (↥⊥) 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 : fixedField ⊤ = ⊥
⊢ IsGalois (↥(fixedField ⊤)) E
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
tfae_1_to_2 : IsGalois F E → fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Nat.card Gal(E/F) = finrank F E
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Nat.card Gal(E/F) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

Tactic:
tfae_have 1 → 4 := fun _ ↦ is_separable_splitting_field F E

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
tfae_1_to_2 : IsGalois F E → fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Nat.card Gal(E/F) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Nat.card Gal(E/F) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE
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
inst✝ : Algebra.IsIntegral K L
x : L
E : IntermediateField K L := K⟮x⟯
hL : FiniteDimensional K ↥E
⊢ MulAction.stabilizer Gal(L/K) x = E.fixingSubgroup

Tactic:
ext g

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
x : L
E : IntermediateField K L := K⟮x⟯
hL : FiniteDimensional K ↥E
g : Gal(L/K)
⊢ g ∈ MulAction.stabilizer Gal(L/K) x ↔ g ∈ E.fixingSubgroup
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
inst✝² : FiniteDimensional F ↥K
inst✝¹ : FiniteDimensional (↥L) E
inst✝ : IsGalois (↥L) E
h : K ⊓ L = ⊥
x✝ : ↥K
y : E
hy : y ∈ L
hx₁ : (algebraMap (↥L) E) ⟨y, hy⟩ ∈ K
hx₂ : ⟨(algebraMap (↥L) E) ⟨y, hy⟩, hx₁⟩ ∈ fixedField (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E).range
⊢ ⟨(algebraMap (↥L) E) ⟨y, hy⟩, hx₁⟩ ∈ ⊥

Tactic:
obtain ⟨z, rfl⟩ : y ∈ (⊥ : IntermediateField F E) := h ▸ mem_inf.mpr ⟨hx₁, hy⟩

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
inst✝² : FiniteDimensional F ↥K
inst✝¹ : FiniteDimensional (↥L) E
inst✝ : IsGalois (↥L) E
h : K ⊓ L = ⊥
x✝ : ↥K
z : F
hy : (Algebra.ofId F E).toRingHom z ∈ L
hx₁ : (algebraMap (↥L) E) ⟨(Algebra.ofId F E).toRingHom z, hy⟩ ∈ K
hx₂ :
  ⟨(algebraMap (↥L) E) ⟨(Algebra.ofId F E).toRingHom z, hy⟩, hx₁⟩ ∈
    fixedField (restrictRestrictAlgEquivMapHom F (↥K) (↥L) E).range
⊢ ⟨(algebraMap (↥L) E) ⟨(Algebra.ofId F E).toRingHom z, hy⟩, hx₁⟩ ∈ ⊥
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
hB : B.Nondegenerate
inst✝ : IsTorsionFree R S
N : Submodule R M
hN : Submodule.span S ↑N = ⊤
⊢ Function.Injective ⇑(B.dualSubmoduleToDual N)

Tactic:
intro x y e

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
hB : B.Nondegenerate
inst✝ : IsTorsionFree R S
N : Submodule R M
hN : Submodule.span S ↑N = ⊤
x y : ↥(B.dualSubmodule N)
e : (B.dualSubmoduleToDual N) x = (B.dualSubmoduleToDual N) y
⊢ x = y
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
hB : B.Nondegenerate
inst✝ : IsTorsionFree R S
N : Submodule R M
hN : Submodule.span S ↑N = ⊤
x y : ↥(B.dualSubmodule N)
e : (B.dualSubmoduleToDual N) x = (B.dualSubmoduleToDual N) y
⊢ Set.EqOn ⇑(B ↑x) ⇑(B ↑y) ↑N

Tactic:
intro z

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
hB : B.Nondegenerate
inst✝ : IsTorsionFree R S
N : Submodule R M
hN : Submodule.span S ↑N = ⊤
x y : ↥(B.dualSubmodule N)
e : (B.dualSubmoduleToDual N) x = (B.dualSubmoduleToDual N) y
z : M
⊢ z ∈ ↑N → (B ↑x) z = (B ↑y) z
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case refine_2
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
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ ¬IsUnit a'

Tactic:
by_contra h_contra
    refine hₐ ?_
    rw [← ha, ← Polynomial.coe_mapRingHom]
    exact
      IsUnit.mul (IsUnit.map _ h_contra)
        (isUnit_iff_exists_inv.mpr
          (Exists.intro (C b.leadingCoeff) <| by rw [← C_mul, this, C_1]))

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

Goal state before:
pp: G : Type u_1
inst✝⁹ : Group G
B : Type u_3
C : Type u_4
inst✝⁸ : Semiring C
inst✝⁷ : MulSemiringAction G C
N : Subgroup G
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra B C
inst✝⁴ : FaithfulSMul B C
inst✝³ : MulSemiringAction G B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
g : G
b : B
this : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
⊢ ↑g • b = g • b

Tactic:
refine (Quotient.liftOn'_mk'' (· • b) _ g).trans (FaithfulSMul.algebraMap_injective B C ?_)

Goal state after:
G : Type u_1
inst✝⁹ : Group G
B : Type u_3
C : Type u_4
inst✝⁸ : Semiring C
inst✝⁷ : MulSemiringAction G C
N : Subgroup G
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra B C
inst✝⁴ : FaithfulSMul B C
inst✝³ : MulSemiringAction G B
inst✝² : SMulDistribClass G B C
inst✝¹ : IsGaloisGroup (↥N) B C
inst✝ : N.Normal
g : G
b : B
this : MulSemiringAction G B := mulSemiringActionOfNormal G B C N
⊢ (algebraMap B C) (g • b) = (algebraMap B C) (g • b)
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = ↑x.valMinAbs.natAbs
⊢ ↑x.valMinAbs.natAbs * 2 ≤ ↑n

Tactic:
← h

Goal state after:
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = ↑x.valMinAbs.natAbs
⊢ x.valMinAbs * 2 ≤ ↑n
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = -↑x.valMinAbs.natAbs
⊢ -↑n ≤ -↑x.valMinAbs.natAbs * 2

Tactic:
← h

Goal state after:
case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.valMinAbs = -↑x.valMinAbs.natAbs
⊢ -↑n ≤ x.valMinAbs * 2
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
⊢ e ((trace A C) x) = (trace B C) x

Tactic:
by
  classical
  by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
  · obtain ⟨s, ⟨b⟩⟩ := h
    let : Algebra A B := RingHom.toAlgebra e
    let : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' he.symm
    rw [Algebra.trace_eq_matrix_trace b,
      Algebra.trace_eq_matrix_trace (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he]))]
    rw [AddMonoidHom.map_trace]
    congr
    ext i j
    simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]
  rw [trace_eq_zero_of_not_exists_basis _ h, trace_eq_zero_of_not_exists_basis,
    LinearMap.zero_apply, LinearMap.zero_apply, map_zero]
  intro ⟨s, ⟨b⟩⟩
  exact h ⟨s, ⟨b.mapCoeffs e (by simp [Algebra.smul_def, ← he])⟩⟩

Goal state after:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case succ.he
n : ℕ
a b : ZMod (n + 1)
⊢ ↑(a + b).valMinAbs = ↑(a.valMinAbs + b.valMinAbs)

Tactic:
Int.cast_add,

Goal state after:
case succ.he
n : ℕ
a b : ZMod (n + 1)
⊢ ↑(a + b).valMinAbs = ↑a.valMinAbs + ↑b.valMinAbs
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: κ : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype κ
b : κ → B
P : Matrix κ κ A
⊢ (transposeAddEquiv κ κ A) (traceMatrix A (P.map ⇑(algebraMap A B) *ᵥ b)) =
    (transposeAddEquiv κ κ A) (P * traceMatrix A b * Pᵀ)

Tactic:
rw [transposeAddEquiv_apply, transposeAddEquiv_apply, ← vecMul_transpose, ← transpose_map,
    traceMatrix_of_matrix_vecMul, transpose_transpose]

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

Goal state before:
pp: G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁶ : Group G
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : MulSemiringAction G L
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
F : IntermediateField K L
⊢ Subgroup.map (↑(mulEquivAlgEquiv G K L)) (fixingSubgroup G ↑F) = F.fixingSubgroup

Tactic:
ext g

Goal state after:
G : Type u_1
K : Type u_3
L : Type u_4
inst✝⁶ : Group G
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : MulSemiringAction G L
inst✝¹ : Finite G
inst✝ : IsGaloisGroup G K L
F : IntermediateField K L
g : Gal(L/K)
⊢ g ∈ Subgroup.map (↑(mulEquivAlgEquiv G K L)) (fixingSubgroup G ↑F) ↔ g ∈ F.fixingSubgroup