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

Goal state before:
pp: case h₂
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
heJ : M.closure {e} ⊆ M.closure J
⊢ M.closure {e} ∩ R ⊆ M.closure (J ∩ R) ∩ R ∪ R \ M.E

Tactic:
refine (inter_subset_inter_left _ ?_).trans subset_union_left

Goal state after:
case h₂
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
heJ : M.closure {e} ⊆ M.closure J
⊢ M.closure {e} ⊆ M.closure (J ∩ R)
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
⊢ I.encard = n

Tactic:
hI.encard_eq_eRk,

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 = n
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : f ∈ M.E → f ∈ M.loops
hf : f ∈ M.E
⊢ M.loops = M.closure {f}

Tactic:
rw [← closure_loops, ← insert_eq_of_mem (h hf), closure_insert_congr_right M.closure_loops,
      insert_empty_eq]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
e : α
⊢ M.eRk (I ∪ {e}) = M.eRk (insert e X)

Tactic:
hIX.eRk_eq_eRk_union,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
e : α
⊢ M.eRk (X ∪ {e}) = M.eRk (insert e X)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
e : α
⊢ M.eRk (I ∪ {e}) = M.eRk (insert e X)

Tactic:
hIX.eRk_eq_eRk_union,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
e : α
⊢ M.eRk (X ∪ {e}) = M.eRk (insert e X)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
apply eRk_union_le_eRk_add_eRk

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

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

Tactic:
apply eRk_union_le_eRk_add_eRk

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.eRank ≠ ⊤ ↔ M.RankFinite

Tactic:
by
  obtain ⟨B, hB⟩ := M.exists_isBase
  rw [← hB.encard_eq_eRank, encard_ne_top_iff]
  exact ⟨fun h ↦ hB.rankFinite_of_finite h, fun h ↦ hB.finite⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
⊢ M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B

Tactic:
← dual_isLoop_iff_isColoop,

Goal state after:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
⊢ M✶.IsLoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hX : M.IsRkFinite I
h : I.encard ≤ M.eRk I
⊢ M.Indep I

Tactic:
indep_iff_eRk_eq_encard_of_finite _

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hX : M.IsRkFinite I
h : I.encard ≤ M.eRk I
⊢ M.eRk I = I.encard

α : Type u_1
M : Matroid α
I : Set α
hX : M.IsRkFinite I
h : I.encard ≤ M.eRk I
⊢ I.Finite
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α✝ α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
⊢ M.IsColoop e ↔ ¬M.Coindep (M.E \ (M.E \ {e}))

Tactic:
← dual_isLoop_iff_isColoop,

Goal state after:
α✝ α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
⊢ M✶.IsLoop e ↔ ¬M.Coindep (M.E \ (M.E \ {e}))
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
⊢ M.eRk X = M.eRank

Tactic:
by
  obtain ⟨B, hB⟩ := M.exists_isBasis X
  exact (M.eRk_le_eRank X).antisymm <| by
    rw [← hB.encard_eq_eRk, ← (hB.isBase_of_spanning hX).encard_eq_eRank]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
h : M.closure (M.E \ {e}) = M.E
⊢ e ∈ M.closure (M.E \ {e})

Tactic:
by rwa [h]

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

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

Tactic:
(hI.map hf).eRk_eq_encard,

Goal state after:
α : Type u_1
X : Set α
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
⊢ (f '' I).encard = I.encard
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
g : R ≃ₐ[R] ↥(supported R ∅) := (Algebra.botEquivOfInjective ⋯).symm.trans ((supported R ∅).equivOfEq ⊥ ⋯).symm
⊢ Transcendental R ((Polynomial.aeval (X i)) f)

Tactic:
rwa [Transcendental, ← isAlgebraic_ringHom_iff_of_comp_eq g (RingHom.id (MvPolynomial σ R))
    Function.injective_id (by ext1; rfl), RingHom.id_apply, ← Transcendental]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I = {e}

Tactic:
rw [subset_antisymm_iff, subset_inter_iff, singleton_subset_iff, and_iff_right
    (mem_fundCocircuit _ _ _), singleton_subset_iff, and_iff_left heI,
    ← M.fundCocircuit_inter_eq (hIB heI)]

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I ⊆ M.fundCocircuit e B ∩ B
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
E X : Set α
⊢ (freeOn E).closure X = X ∩ E

Tactic:
simp +contextual [← closure_inter_ground _ X, Set.ext_iff, and_comm,
    insert_subset_iff, freeOn_indep_iff, (freeOn_indep inter_subset_right).mem_closure_iff']

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

Goal state before:
pp: ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝¹ : Nontrivial S
this✝ : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this : Algebra.IsAlgebraic (↥Sy) A
i : ι'
⊢ y i ∈ ↑(Subalgebra.restrictScalars (↥Rx) Sy)

Tactic:
exact subset_adjoin (s := range y) ⟨i, rfl⟩

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

Tactic:
classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add]
  exact Finset.card_union_le _ _

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

Tactic:
zero_add,

Goal state after:
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ 0 = g.natSepDegree ↔ 0 = 0 ∧ g = 0 ∨ IsCoprime 0 g
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
B' : AddGroupFilterBasis M := B.toAddGroupFilterBasis
x✝¹ : TopologicalSpace M := B'.topology
x✝ : Set M
⊢ x✝ ∈ B' → ∃ V ∈ 𝓝 0, ∃ j ∈ B', V • id j ⊆ id x✝

Tactic:
by simpa using! B.smul

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
B' : AddGroupFilterBasis M := B.toAddGroupFilterBasis
x✝ : TopologicalSpace M := B'.topology
⊢ ContinuousSMul R M

Tactic:
exact ContinuousSMul.of_basis_zero B'.nhds_zero_hasBasis
      (fun {_} => by simpa using! B.smul)
      (by simpa using! B.smul_left) B.smul_right

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

Goal state before:
pp: case h_sep
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
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this✝ : ∀ (f : K →ₐ[F] E), Finite (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
f : K →ₐ[F] E
a✝ : f ∈ Finset.univ
⊢ IsSeparable K x

Tactic:
exact Polynomial.Separable.of_dvd ((Polynomial.separable_map (algebraMap F K)).mpr hp) h2

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case pos
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst : Field E] [inst_1 : Algebra F E] [Algebra.IsSeparable F E],
    FiniteDimensional F E → finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
L : IntermediateField F E
h : FiniteDimensional F ↥L
h' : finSepDegree F E < finrank F ↥L
hd : finrank F ↥L * finSepDegree (↥L) E = finSepDegree F E
hd' : finSepDegree (↥L) E = 0
⊢ finSepDegree F E = 0

Tactic:
rw [← hd, hd', mul_zero]

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

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
⊢ 1 ∈ ⋃ n, V ^ (n + 1)

Tactic:
by
      apply mem_iUnion.mpr
      use 0
      simp [mem_of_mem_nhds hV.nhds]

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

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
x✝ : G
ha : x✝ ∈ ⋃ n, V ^ (n + 1)
⊢ x✝⁻¹ ∈ ⋃ n, V ^ (n + 1)

Tactic:
rcases mem_iUnion.mp ha with ⟨k, hk⟩
      apply mem_iUnion.mpr
      use k
      rw [← hV.inv]
      simpa only [inv_pow, Set.mem_inv, inv_inv] using hk

Goal state after:
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
h : (MulSemiringAction.toAlgAut Gal(E/↥L) F E) φ = 1
⊢ φ = 1

Tactic:
AlgEquiv.ext_iff

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
h : ∀ (a : E), ((MulSemiringAction.toAlgAut Gal(E/↥L) F E) φ) a = 1 a
⊢ ∀ (a : E), φ a = 1 a
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
inst✝ : IsGalois F E'
L : IntermediateField F E'
hnfd : FiniteDimensional F ↥L
E : IntermediateField F E' := normalClosure F (↥L) E'
hle : L ≤ E
L' : IntermediateField F ↥E := restrict hle
⊢ finrank F ↥L = L.fixingSubgroup.index

Tactic:
have h := Module.finrank_mul_finrank F ↥L' ↥E

Goal state after:
F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
inst✝ : IsGalois F E'
L : IntermediateField F E'
hnfd : FiniteDimensional F ↥L
E : IntermediateField F E' := normalClosure F (↥L) E'
hle : L ≤ E
L' : IntermediateField F ↥E := restrict hle
h : finrank F ↥L' * finrank ↥L' ↥E = finrank F ↥E
⊢ finrank F ↥L = L.fixingSubgroup.index
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
K : Type u_3
L : Type u_4
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : CommRing L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R K L
inst✝² : IsScalarTower R S L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsDomain S
s : S
hs : IsIntegral R s
⊢ minpoly K ((algebraMap S L) s) = map (algebraMap R K) (minpoly R s)

Tactic:
refine (eq_of_irreducible_of_monic ?_ ?_ ?_).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
K : Type u_3
L : Type u_4
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : CommRing L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R K L
inst✝² : IsScalarTower R S L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsDomain S
s : S
hs : IsIntegral R s
⊢ Irreducible (map (algebraMap R K) (minpoly R s))

case refine_2
R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : IsDomain R
inst✝¹² : Algebra R S
K : Type u_3
L : Type u_4
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : CommRing L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R K L
inst✝² : IsScalarTower R S L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsDomain S
s : S
hs : IsIntegral R s
⊢ (Polynomial.aeval ((algebraMap S L) s)) (map (algebraMap R K) (minpoly R s)) = 0

case refine_3
R : Type u_1
S : Type u_2
inst✝¹⁵ : CommRing R
inst✝¹⁴ : CommRing S
inst✝¹³ : IsDomain R
inst✝¹² : Algebra R S
K : Type u_3
L : Type u_4
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : CommRing L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R K L
inst✝² : IsScalarTower R S L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsDomain S
s : S
hs : IsIntegral R s
⊢ (map (algebraMap R K) (minpoly R s)).Monic
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
K : Type u_3
L : Type u_4
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : CommRing L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra K L
inst✝³ : IsScalarTower R K L
inst✝² : IsScalarTower R S L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsDomain S
s : S
hs : IsIntegral R s
⊢ Irreducible (map (algebraMap R K) (minpoly R s))

Tactic:
exact ((monic hs).irreducible_iff_irreducible_map_fraction_map).1 (irreducible hs)

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
⊢ IsGalois ↥L ↥(adjoin ↥L {x}).toIntermediateField

Tactic:
by infer_instance

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

Goal state before:
pp: case refine_1
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
h : x ∈ ↑(fixedField H ⊓ L)
⊢ x ∈ ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))

Tactic:
have xL := h.out.2

Goal state after:
case refine_1
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
h : x ∈ ↑(fixedField H ⊓ L)
xL : x ∈ (fun x ↦ ↑x) L
⊢ x ∈ ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_3
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 : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → q.degree ≤ Q.degree

Tactic:
· exact (hMul ▸ degree_C_mul <| by simp [h₀]) ▸ pmin

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: case inr
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
hd : 0 < p.degree
z : k
hz : p.IsRoot z
⊢ p = C (p.coeff 0)

Tactic:
rw [← mem_roots (ne_zero_of_degree_gt hd), h] at hz

Goal state after:
case inr
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
p : k[X]
hsep : p.Separable
h : p.roots = 0
hd : 0 < p.degree
z : k
hz : z ∈ 0
⊢ p = C (p.coeff 0)
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
⊢ IsPurelyInseparable F E ↔ ∀ (x : E), (minpoly F x).natSepDegree = 1

Tactic:
obtain ⟨q, _⟩ := ExpChar.exists F
  simp_rw [isPurelyInseparable_iff_pow_mem F q, minpoly.natSepDegree_eq_one_iff_pow_mem q]

Goal state after:
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✝
q : ℕ
inst✝⁵ : ExpChar F✝ q
inst✝⁴ : IsPurelyInseparable F✝ E✝
inst✝³ : FiniteDimensional F✝ E✝
F E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ∀ (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ n, finrank F E = q ^ n

Tactic:
q

Goal state after:
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✝
F E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q : ℕ
⊢ ∀ [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ n, finrank F E = q ^ n
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✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
h_dvd : map (algebraMap R K) p ∣ map (algebraMap R K) q
⊢ p ∣ q

Tactic:
rcases h_dvd with ⟨r, hr⟩
  obtain ⟨r, rfl⟩ := (mul_map_mem_lifts_iff hp).mp ⟨q, mul_comm _ r ▸ hr⟩
  use r
  simpa [← Polynomial.map_mul, (map_injective _ (FaithfulSMul.algebraMap_injective R K)).eq_iff]
    using hr

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

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
K : Type u_4
L : Type u_5
inst✝¹⁷ : Group G
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A K
inst✝⁸ : Algebra B L
inst✝⁷ : Algebra A L
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsScalarTower A B L
inst✝² : MulSemiringAction G L
inst✝¹ : SMulDistribClass G B L
inst✝ : IsGaloisGroup G A B
b : B
hb : ∀ (g : G), g • b = b
⊢ ∃ a, (algebraMap (↥(algebraMap A B).range) B) a = b

Tactic:
by
    obtain ⟨a, ha⟩ := Algebra.IsInvariant.isInvariant (A := A) b hb
    exact ⟨⟨algebraMap A B a, ⟨a, rfl⟩⟩, ha⟩

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

Goal state before:
pp: case h
G : Type u_1
inst✝⁸ : Group G
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
inst✝³ : FaithfulSMul A B
inst✝² : MulSemiringAction G B
inst✝¹ : IsGaloisGroup G A B
inst✝ : Finite G
this✝ : IsDomain A
this : FaithfulSMul G B
φ : B ≃ₐ[A] B
g : ↥(MulAction.stabilizer G ⊥)
hg : (Ideal.Quotient.stabilizerHom ⊥ ⊥ G) g = Ideal.Quotient.algEquivOfEqMap ⊥ φ ⋯
⊢ (MulSemiringAction.toAlgAut G A B) ↑g = φ

Tactic:
AlgEquiv.ext_iff

Goal state after:
case h
G : Type u_1
inst✝⁸ : Group G
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
inst✝³ : FaithfulSMul A B
inst✝² : MulSemiringAction G B
inst✝¹ : IsGaloisGroup G A B
inst✝ : Finite G
this✝ : IsDomain A
this : FaithfulSMul G B
φ : B ≃ₐ[A] B
g : ↥(MulAction.stabilizer G ⊥)
hg : ∀ (a : B ⧸ ⊥), ((Ideal.Quotient.stabilizerHom ⊥ ⊥ G) g) a = (Ideal.Quotient.algEquivOfEqMap ⊥ φ ⋯) a
⊢ ∀ (a : B), ((MulSemiringAction.toAlgAut G A B) ↑g) a = φ a
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case pos
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
s : Finset C
b : Basis (↥s) B C
this✝ : Algebra A B := (↑e).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.symm he)
⊢ e ((leftMulMatrix (b.mapCoeffs e.symm ⋯)) x).trace = ((leftMulMatrix b) x).trace

Tactic:
AddMonoidHom.map_trace

Goal state after:
case pos
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
s : Finset C
b : Basis (↥s) B C
this✝ : Algebra A B := (↑e).toAlgebra
this : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.symm he)
⊢ (((leftMulMatrix (b.mapCoeffs e.symm ⋯)) x).map ⇑e).trace = ((leftMulMatrix b) x).trace
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case pos
n : ℕ
a : ZMod n
h2a : 2 * a.val = n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

Tactic:
rw [a.neg_eq_self_iff.2 (Or.inr h2a)]

Goal state after: