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

Goal state before:
pp: case refine_2
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
x✝ : P.IsMaximal
Rp : Type u := Localization P.primeCompl
e✝ : LocalizedModule P.primeCompl M ≃ₗ[Rp] Rp
e : LocalizedModule P.primeCompl M ≃ₗ[R] Rp
x y : LocalizedModule P.primeCompl M
⊢ e y ⊗ₜ[Rp] e x = e x ⊗ₜ[Rp] e y

Tactic:
conv_lhs => rw [← mul_one (e y), ← smul_eq_mul, smul_tmul, smul_eq_mul,
    mul_comm, ← smul_eq_mul, ← smul_tmul, smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯

Tactic:
let f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯

Goal state after:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯
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
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
hm : m = 0
⊢ IsAlgebraic F α

Tactic:
rw [hm] at heq hmn

Goal state after:
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
heq : F⟮α ^ 0⟯ = F⟮α ^ n⟯
hmn : 0 < n
hm : m = 0
⊢ IsAlgebraic F α
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R

Tactic:
h_eq,

Goal state after:
α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
B : Set α
hI' : M✶.IsBasis (M.E \ (B ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
hss : M.E \ (B' ∪ R ∩ M.E) ⊆ M.E \ (B ∪ R ∩ M.E)
hi : M✶.Indep (M.E \ (B ∪ R ∩ M.E))
h_eq : M.E \ (B' ∪ R ∩ M.E) = M.E \ (B ∪ R ∩ M.E)
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M M' : Matroid α
X : Set α
⊢ M ↾ X = M' ↾ X ↔ ∀ I ⊆ X, M.Indep I ↔ M'.Indep I

Tactic:
by
  refine ⟨fun h I hIX ↦ ?_, fun h ↦ ext_indep rfl fun I (hI : I ⊆ X) ↦ ?_⟩
  · rw [← and_iff_left (a := (M.Indep I)) hIX, ← and_iff_left (a := (M'.Indep I)) hIX,
      ← restrict_indep_iff, h, restrict_indep_iff]
  rw [restrict_indep_iff, and_iff_left hI, restrict_indep_iff, and_iff_left hI, h _ hI]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
inst✝ : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
⊢ M.IsRkFinite (⋃ i, Xs i)

Tactic:
have hfin : (⋃ i, Is i).Finite := finite_iUnion <| fun i ↦ (h i).finite_of_isBasis' (hIs i)

Goal state after:
α : Type u_1
M : Matroid α
ι : Type u_2
inst✝ : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
hfin : (⋃ i, Is i).Finite
⊢ M.IsRkFinite (⋃ i, Xs i)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C X : Set α
hC : M.IsCircuit C
hXC : X ⊂ C
⊢ M.Indep X

Tactic:
← not_dep_iff (hXC.subset.trans hC.subset_ground)

Goal state after:
α : Type u_1
M : Matroid α
C X : Set α
hC : M.IsCircuit C
hXC : X ⊂ C
⊢ ¬M.Dep X
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
⊢ M.IsBasis I X

Tactic:
have hss := (hf.image_subset_image_iff hI hX).1 h.subset

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
hss : I ⊆ X
⊢ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
⊢ [M.IsLoop e, e ∈ M.closure ∅, M.IsCircuit {e}, M.Dep {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B].TFAE

Tactic:
tfae_have 2 ↔ 4 := by simp [M.empty_indep.mem_closure_iff_of_notMem (notMem_empty e)]

Goal state after:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsLoop e ↔ e ∈ M.closure ∅
tfae_2_iff_3 : e ∈ M.closure ∅ ↔ M.IsCircuit {e}
tfae_2_iff_4 : e ∈ M.closure ∅ ↔ M.Dep {e}
⊢ [M.IsLoop e, e ∈ M.closure ∅, M.IsCircuit {e}, M.Dep {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B].TFAE
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
⊢ M.IsCircuit {e, f}

Tactic:
have hf := he.isNonloop_of_mem_closure (by rw [← h]; exact M.mem_closure_self e)

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ≠ f
h : M.closure {e} = M.closure {f}
hf : M.IsNonloop f
⊢ M.IsCircuit {e, f}
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_2
⊢ (emptyOn α).eRank = 0

Tactic:
eRank_eq_zero_iff,

Goal state after:
α : Type u_2
⊢ emptyOn α = loopyOn (emptyOn α).E
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.Indep M.coloops

Tactic:
rw [← empty_union M.coloops, union_coloops_indep_iff]
  exact M.empty_indep

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

Goal state before:
pp: α : Type u
M : Matroid α
X : Set α
κ : Cardinal.{u}
⊢ M.cRk X ≤ κ ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #↑I ≤ κ

Tactic:
cRk,

Goal state after:
α : Type u
M : Matroid α
X : Set α
κ : Cardinal.{u}
⊢ (M ↾ X).cRank ≤ κ ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #↑I ≤ κ
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
⊢ M.cRk M.E = M.cRank

Tactic:
cRk,

Goal state after:
α : Type u
M : Matroid α
⊢ (M ↾ M.E).cRank = M.cRank
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
⊢ lift.{u, v} ((M.map f hf).cRk (f '' X)) = lift.{v, u} (M.cRk X)

Tactic:
cRk,

Goal state after:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
⊢ lift.{u, v} (M.map f hf ↾ f '' X).cRank = lift.{v, u} (M.cRk X)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
⊢ ⨆ i, lift.{u, v} #↑↑i ≤ lift.{v, u} (M.cRk X) ∧ lift.{v, u} (M.cRk X) ≤ lift.{u, v} (⨆ B, #↑↑B)

Tactic:
cRk,

Goal state after:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
⊢ ⨆ i, lift.{u, v} #↑↑i ≤ lift.{v, u} (M ↾ X).cRank ∧ lift.{v, u} (M.cRk X) ≤ lift.{u, v} (⨆ B, #↑↑B)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
⊢ ⨆ i, lift.{u, v} #↑↑i ≤ lift.{v, u} (⨆ B, #↑↑B) ∧ lift.{v, u} (M.cRk X) ≤ lift.{u, v} (⨆ B, #↑↑B)

Tactic:
cRk,

Goal state after:
α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
⊢ ⨆ i, lift.{u, v} #↑↑i ≤ lift.{v, u} (⨆ B, #↑↑B) ∧ lift.{v, u} (M ↾ X).cRank ≤ lift.{u, v} (⨆ B, #↑↑B)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ lift.{v, u} ((M.comap f).cRk X) = lift.{u, v} (M.cRk (f '' X))

Tactic:
cRk,

Goal state after:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ lift.{v, u} (M.comap f ↾ X).cRank = lift.{u, v} (M.cRk (f '' X))
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ ⨆ i, lift.{v, u} #↑↑i ≤ lift.{u, v} (M.cRk (f '' X)) ∧ lift.{u, v} (M.cRk (f '' X)) ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
cRk,

Goal state after:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ ⨆ i, lift.{v, u} #↑↑i ≤ lift.{u, v} (M ↾ f '' X).cRank ∧ lift.{u, v} (M.cRk (f '' X)) ≤ lift.{v, u} (⨆ B, #↑↑B)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ ⨆ i, lift.{v, u} #↑↑i ≤ lift.{u, v} (⨆ B, #↑↑B) ∧ lift.{u, v} (M.cRk (f '' X)) ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
cRk,

Goal state after:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ ⨆ i, lift.{v, u} #↑↑i ≤ lift.{u, v} (⨆ B, #↑↑B) ∧ lift.{u, v} (M ↾ f '' X).cRank ≤ lift.{v, u} (⨆ B, #↑↑B)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
I X : Set α
inst✝ : M.InvariantCardinalRank
hIX : M.IsBasis' I X
⊢ #↑I = M.cRk X

Tactic:
cRk,

Goal state after:
α : Type u
M : Matroid α
I X : Set α
inst✝ : M.InvariantCardinalRank
hIX : M.IsBasis' I X
⊢ #↑I = (M ↾ X).cRank
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
ι : Sort u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ i, Is i)
⊢ M.closure (⋂ i, Is i) = ⋂ i, M.closure (Is i)

Tactic:
convert!
    h.closure_sInter_eq_biInter_closure_of_forall_subset (range_nonempty Is)
      (by simp [subset_iUnion])
  simp

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

Goal state before:
pp: α : Type u
M : Matroid α
X : Set α
⊢ toENat (M.cRk X) = M.eRk X

Tactic:
cRk,

Goal state after:
α : Type u
M : Matroid α
X : Set α
⊢ toENat (M ↾ X).cRank = M.eRk X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBasis B S
⊢ M.Spanning B

Tactic:
h.spanning_iff_spanning

Goal state after:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBasis B S
⊢ M.Spanning S
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g : G
⊢ a ∈ fixedBy α g⁻¹ ↔ a ∈ fixedBy α g⁻¹

Tactic:
fixedBy_inv

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g : G
⊢ a ∈ fixedBy α g ↔ a ∈ fixedBy α g
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

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

Tactic:
refine isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic.2 ⟨algebraicIndependent_X .., ?_⟩
  rw [adjoin_range_X]
  set A := MvPolynomial ι R
  have := Algebra.isIntegral_of_surjective (R := (⊤ : Subalgebra R A)) (B := A) (⟨⟨·, ⟨⟩⟩, rfl⟩)
  infer_instance

Goal state after:
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
⊢ natSepDegree 0 = natSepDegree 0 + g.natSepDegree ↔ 0 = 0 ∧ g = 0 ∨ IsCoprime 0 g

Tactic:
natSepDegree_zero,

Goal state after:
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ 0 = 0 + g.natSepDegree ↔ 0 = 0 ∧ g = 0 ∨ IsCoprime 0 g
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_2
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
x✝ : ∃ n y, f = (expand F (q ^ n)) (X - C y)
n : ℕ
y : F
h : f = (expand F (q ^ n)) (X - C y)
⊢ f.natSepDegree = 1

Tactic:
rw [h, natSepDegree_expand _ q, natSepDegree_X_sub_C]

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ (𝓝 x₀).HasBasis (fun V ↦ V ∈ B) fun V ↦ (fun y ↦ x₀ * y) '' V

Tactic:
rw [B.nhds_eq]
  apply B.hasBasis

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
⊢ IsTopologicalRing R

Tactic:
let B' := B.toAddGroupFilterBasis

Goal state after:
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := B.toAddGroupFilterBasis
⊢ IsTopologicalRing R
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: case mp
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h : IsGalois (↥⊥) E
⊢ IsGalois F E

Tactic:
exact IsGalois.tower_top_of_isGalois (⊥ : IntermediateField F E) F E

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

Goal state before:
pp: case mpr
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois F E → IsGalois (↥⊥) E

Tactic:
· intro h; infer_instance

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

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

Tactic:
rw [h, natSepDegree_expand _ q, natSepDegree_X_sub_C]

Goal state after:
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.EssFiniteType F E
⊢ ∃ s,
    MaximalFor (fun t ↦ IsTranscendenceBasis F Subtype.val)
      (fun t ↦ restrictScalars F (separableClosure (↥(adjoin F t)) E)) ↑s

Tactic:
by
  let d (s : Finset E) := Field.finInsepDegree (adjoin F (s : Set E)) E
  have Hexists : {s : Finset E | IsTranscendenceBasis F ((↑) : s → E)}.Nonempty := by
    have ⟨s, hs⟩ := IntermediateField.fg_top F E
    have : Algebra.IsAlgebraic (Algebra.adjoin F (s : Set E)) E := by
      rw [← isAlgebraic_adjoin_iff_top, hs, Algebra.isAlgebraic_iff_isIntegral]
      refine Algebra.isIntegral_of_surjective topEquiv.surjective
    have ⟨t, hts, ht⟩ := exists_isTranscendenceBasis_subset (R := F) (s : Set E)
    lift t to Finset E using s.finite_toSet.subset hts
    exact ⟨t, ht⟩
  let s := d.argminOn _ Hexists
  have hs := d.argminOn_mem _ Hexists
  refine ⟨s, hs, fun t ht ↦ not_lt_iff_le_imp_ge.mp fun H ↦ ?_⟩
  have : t.Finite := by
    simp [Set.Finite, ← Cardinal.mk_lt_aleph0_iff, ht.cardinalMk_eq hs, Cardinal.natCast_lt_aleph0]
  lift t to Finset E using this
  have : Module.Finite (adjoin F (s : Set E)) E := by
    apply +allowSynthFailures Algebra.finite_of_essFiniteType_of_isAlgebraic
    · exact .of_comp F _ _
    · convert! hs.isAlgebraic_field <;> simp [s]
  have : Module.Finite ((separableClosure (adjoin F (s : Set E)) E).restrictScalars F) E :=
    inferInstanceAs <| Module.Finite (separableClosure (adjoin F (s : Set E)) E) E
  exact d.not_lt_argminOn _ ht (by apply finrank_lt_of_gt H)

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : IsTopologicalRing R
⊢ ContinuousSMul R M

Tactic:
let B' := B.toAddGroupFilterBasis

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : ModuleFilterBasis R M
inst✝ : IsTopologicalRing R
B' : AddGroupFilterBasis M := B.toAddGroupFilterBasis
⊢ ContinuousSMul R M
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✝ : FiniteDimensional K L
⊢ DiscreteTopology Gal(L/K)

Tactic:
rw [discreteTopology_iff_isOpen_singleton_one]
  change IsOpen ((⊥ : Subgroup Gal(L/K)) : Set Gal(L/K))
  rw [← IntermediateField.fixingSubgroup_top]
  exact IntermediateField.fixingSubgroup_isOpen ⊤

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

Goal state before:
pp: case mp
F : Type u_1
E : Type u_2
E' : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E
inst✝³ : Algebra F E'
inst✝² : Algebra E E'
inst✝¹ : IsScalarTower F E E'
L : IntermediateField F E
inst✝ : Normal F E
f : Gal(E'/F)
h : ∀ x ∈ map (IsScalarTower.toAlgHom F E E') L, f x = x
x : E
hx : x ∈ L
⊢ (f.restrictNormal E) x = x

Tactic:
apply_fun _ using (algebraMap E E').injective

Goal state after:
case mp
F : Type u_1
E : Type u_2
E' : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E
inst✝³ : Algebra F E'
inst✝² : Algebra E E'
inst✝¹ : IsScalarTower F E E'
L : IntermediateField F E
inst✝ : Normal F E
f : Gal(E'/F)
h : ∀ x ∈ map (IsScalarTower.toAlgHom F E E') L, f x = x
x : E
hx : x ∈ L
⊢ (algebraMap E E') ((f.restrictNormal E) x) = (algebraMap E E') x
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
E : Type u_2
E' : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E
inst✝³ : Algebra F E'
inst✝² : Algebra E E'
inst✝¹ : IsScalarTower F E E'
L : IntermediateField F E
inst✝ : Normal F E
⊢ (map (IsScalarTower.toAlgHom F E E') L).fixingSubgroup = Subgroup.comap (restrictNormalHom E) L.fixingSubgroup

Tactic:
ext f
  simp only [Subgroup.mem_comap, mem_fixingSubgroup_iff]
  constructor
  · rintro h x hx
    change f.restrictNormal E x = x
    apply_fun _ using (algebraMap E E').injective
    rw [AlgEquiv.restrictNormal_commutes]
    exact h _ ⟨x, hx, rfl⟩
  · rintro h _ ⟨x, hx, rfl⟩
    replace h := congr(algebraMap E E' $(show f.restrictNormal E x = x from h x hx))
    rwa [AlgEquiv.restrictNormal_commutes] at h

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

Goal state before:
pp: case «2»
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
h : Nat.card Gal(K/F) = 2
this : 2 ≤ 2
⊢ IsCyclic Gal(K/F)

Tactic:
· exact isCyclic_of_prime_card h

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

Goal state before:
pp: case refine_1
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
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
x✝ : C p.leadingCoeff ∣ p
q : R[X]
hMul : p = C p.leadingCoeff * q
⊢ q.Monic

Tactic:
have := hMul ▸ leadingCoeff_mul .. |>.symm

Goal state after:
case refine_1
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
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
x✝ : C p.leadingCoeff ∣ p
q : R[X]
hMul : p = C p.leadingCoeff * q
this : (C p.leadingCoeff).leadingCoeff * q.leadingCoeff = p.leadingCoeff
⊢ q.Monic
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
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
⊢ False

Tactic:
have : (restrictNormalHom L') σ ∈ (Subgroup.map (restrictNormalHom L') H.1) := by
    rw [← IntermediateField.fixingSubgroup_fixedField (Subgroup.map (restrictNormalHom L') H.1)]
    apply (mem_fixingSubgroup_iff (L' ≃ₐ[k] L')).mpr
    intro y hy
    apply Subtype.val_injective
    simp only [AlgEquiv.smul_def, restrictNormalHom_apply L'.1 σ y,
      fix y.1 ((IntermediateField.mem_lift y).mpr hy)]

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this✝ : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
this : (restrictNormalHom ↥L'.toIntermediateField) σ ∈ Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H
⊢ False
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case heval.h
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
this : Function.Injective fun σ ↦ σ x
σ : L →ₐ[K] E
⊢ ¬(aeval x) (derivative (minpoly K x)) = 0

Tactic:
exact (IsSeparable.isSeparable _ _).aeval_derivative_ne_zero (minpoly.aeval _ _)

Goal state after:
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: case intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
x : T
this✝ : DecidableEq ι
this : DecidableEq κ
val✝¹ : Fintype ι
val✝ : Fintype κ
i : ι
x✝ : i ∈ Finset.univ
⊢ ((leftMulMatrix b) (∑ i, ((leftMulMatrix c) x).diag i)).diag i = ∑ y, ((leftMulMatrix (b.smulTower c)) x).diag (i, y)

Tactic:
simp only [map_sum, smulTower_leftMulMatrix, Finset.sum_apply, Matrix.diag,
    Finset.sum_apply i (Finset.univ : Finset κ) fun y => leftMulMatrix b (leftMulMatrix c x y y)]

Goal state after:
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
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
⊢ x ∈ (algebraMap F E).range

Tactic:
have := finSepDegree_mul_finSepDegree_of_isAlgebraic F F⟮x⟯ E

Goal state after:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
this : finSepDegree F ↥F⟮x⟯ * finSepDegree (↥F⟮x⟯) E = finSepDegree F E
⊢ x ∈ (algebraMap F E).range