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

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : M.Spanning S
⊢ M.Coindep (M.E \ S)

Tactic:
rwa [← spanning_iff_compl_coindep]

Goal state after:
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.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I) ↔
      f x ∈ M.E ∧ (M.Indep (insert (f x) (f '' I)) → ∃ x_1 ∈ I, f x_1 = f x)

Tactic:
and_congr_right_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 ↔
        M.Indep (insert (f x) (f '' I)) → ∃ x_1 ∈ I, f x_1 = f x)
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: case refine_1
R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ u ⊆ t}
chainc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcn : c.Nonempty
⊢ AlgebraicIndependent R Subtype.val

pp: case refine_2
R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ u ⊆ t}
chainc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcn : c.Nonempty
⊢ ⋃₀ c ⊆ t

Tactic:
· exact algebraicIndependent_sUnion_of_directed hcn chainc.directedOn (fun x hxc ↦ (hc hxc).1)

Goal state after:
case refine_2
R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
c : Set (Set A)
hc : c ⊆ {u | AlgebraicIndependent R Subtype.val ∧ u ⊆ t}
chainc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcn : c.Nonempty
⊢ ⋃₀ c ⊆ t
Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
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 S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i ↦ x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝³ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝³ : IsScalarTower (↥Rt) (↥St) A
this✝² : NoZeroDivisors ↥St
this✝¹ : NoZeroDivisors ↥Rt
x✝² : ↥St
y : A
hy : y ∈ St
this✝ : Nontrivial R
this : Nontrivial A
z : S
x✝¹ x✝ : R
eq : (algebraMap R ↥Rt) x✝¹ = (algebraMap R ↥Rt) x✝
⊢ x✝¹ = x✝

Tactic:
by
        exact hx.algebraMap_injective congr($eq.1)

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

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
p : ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
i' : AlgebraicIndepOn R _root_.id w
h : range x ⊆ w
⊢ (Subtype.val ∘ fun i ↦ ⟨x i, ⋯⟩) = x

Tactic:
by ext; simp

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
x : ι → A
y : ι' → A
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✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : Maximal (AlgebraicIndepOn R _root_.id) B
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
⊢ Maximal (AlgebraicIndepOn R _root_.id) I

Tactic:
← isTranscendenceBasis_iff_maximal

Goal state after:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : IsTranscendenceBasis R Subtype.val
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
⊢ IsTranscendenceBasis R Subtype.val
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ trdeg R R[X] = 1

Tactic:
simpa using (IsTranscendenceBasis.polynomial Unit R).lift_cardinalMk_eq_trdeg.symm

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

Goal state before:
pp: 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✝³ : Nontrivial R
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)

Tactic:
have ⟨s, hs⟩ := exists_isTranscendenceBasis R S

Goal state after:
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✝³ : Nontrivial R
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis R Subtype.val
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ (algebraMap F E).comp ↑(RingEquiv.refl F) = (↑topEquiv.toRingEquiv).comp (algebraMap F ↥⊤)

Tactic:
by ext; simp

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

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

Tactic:
convert!
      H₁.comp_equiv <|
        .symm <|
          ((Equiv.swap j i).image s).trans <|
            .setCongr <| Equiv.image_swap_of_mem_of_notMem hj hi with
      ⟨x, rfl | hxi, hxj⟩

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

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

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ Disjoint (f.aroots (AlgebraicClosure F)).toFinset (g.aroots (AlgebraicClosure F)).toFinset ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
Finset.disjoint_iff_ne,

Goal state after:
case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (∀ a ∈ (f.aroots (AlgebraicClosure F)).toFinset, ∀ b ∈ (g.aroots (AlgebraicClosure F)).toFinset, a ≠ b) ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g
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 F E

Tactic:
by
  rw [← isGalois_iff_isGalois_bot, ← h]
  exact IsGalois.of_fixed_field E (⊤ : Subgroup Gal(E/F))

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

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
x : G
memW : x ∈ W
⊢ ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ W

Tactic:
have : (x, 1) ∈ (fun p ↦ p.1 * p.2) ⁻¹' W := by simp [memW]

Goal state after:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
x : G
memW : x ∈ W
this : (x, 1) ∈ (fun p ↦ p.1 * p.2) ⁻¹' W
⊢ ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ W
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
⊢ ∀ {x y : Set Gal(L/K)},
    x ∈ (fun g ↦ g.carrier) '' fixedByFinite K L →
      y ∈ (fun g ↦ g.carrier) '' fixedByFinite K L → ∃ z ∈ (fun g ↦ g.carrier) '' fixedByFinite K L, z ⊆ x ∩ y

Tactic:
by
    rintro _ _ ⟨_, ⟨E1, h_E1, rfl⟩, rfl⟩ ⟨_, ⟨E2, h_E2, rfl⟩, rfl⟩
    have : FiniteDimensional K E1 := h_E1
    have : FiniteDimensional K E2 := h_E2
    refine ⟨(E1 ⊔ E2).fixingSubgroup.carrier, ⟨_, ⟨_, E1.finiteDimensional_sup E2, rfl⟩, rfl⟩, ?_⟩
    exact Set.subset_inter (E1.fixingSubgroup_le le_sup_left) (E2.fixingSubgroup_le le_sup_right)

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E✝ : Type v
inst✝⁵ : Field F
inst✝⁴ : Field E✝
inst✝³ : Algebra F E✝
E : Type v
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hfd : FiniteDimensional F E
⊢ finSepDegree F ↥⊥ = finrank F ↥⊥

Tactic:
by simp_rw [finSepDegree_bot, IntermediateField.finrank_bot]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

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

Tactic:
Associated.dvd_iff_dvd_left (show Associated (g * C g.leadingCoeff⁻¹) g from _)

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
⊢ g ∣ map (algebraMap R K) f

R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
⊢ Associated (g * C g.leadingCoeff⁻¹) g
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
⊢ eval₂ (algebraMap R T) (σ₂ x) (minpoly R x) = 0

Tactic:
← σ₂.comp_algebraMap,

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
⊢ eval₂ ((↑σ₂).comp (algebraMap R S)) (σ₂ x) (minpoly R x) = 0
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_4
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)).scaleRoots ((algebraMap R K) r)⁻¹ ∣
    (minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)).scaleRoots ((algebraMap R K) r)⁻¹

Tactic:
← scaleRoots_mul,

Goal state after:
case refine_4
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
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r * ((algebraMap R K) r)⁻¹) ∣
    (minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)).scaleRoots ((algebraMap R K) r)⁻¹
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case neg
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : ¬IsIntegral R x
⊢ natDegree 0 = (minpoly R x).natDegree - 1

Tactic:
minpoly.eq_zero hx

Goal state after:
case neg
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : ¬IsIntegral R x
⊢ natDegree 0 = natDegree 0 - 1
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
⊢ IsOpen L.fixingSubgroup.carrier ↔ FiniteDimensional k ↥L

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ IntermediateField.fixingSubgroup_isOpen L⟩
  have : (IntermediateFieldEquivClosedSubgroup.toFun L).carrier ∈ nhds 1 :=
    IsOpen.mem_nhds h (congrFun rfl)
  rw [GroupFilterBasis.nhds_one_eq] at this
  rcases this with ⟨S, ⟨gp, ⟨M, hM, eq'⟩, eq⟩, sub⟩
  rw [← eq, ← eq'] at sub
  have := hM.out
  let L' : FiniteGaloisIntermediateField k K := {
    normalClosure k M K with
    finiteDimensional := normalClosure.is_finiteDimensional k M K
    isGalois := IsGalois.normalClosure k M K }
  have : L ≤ L'.1 := by
    apply le_trans _ (IntermediateField.le_normalClosure M)
    rw [← fixedField_fixingSubgroup M, IntermediateField.le_iff_le]
    exact sub
  let _ : Algebra L L'.1 := RingHom.toAlgebra (IntermediateField.inclusion this)
  exact FiniteDimensional.left k L L'.1

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
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
q : ℕ
h2✝ : ∀ (x : K), ∃ n, x ^ q ^ n ∈ (algebraMap E K).range
h1✝ : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
h✝ : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : (algebraMap E K) y = x ^ q ^ n
m : ℕ
z : F
h1 : (algebraMap F E) z = y ^ q ^ m
⊢ (algebraMap E K) ((algebraMap F E) z) = x ^ q ^ (n + m)

Tactic:
h1,

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
q : ℕ
h2✝ : ∀ (x : K), ∃ n, x ^ q ^ n ∈ (algebraMap E K).range
h1✝ : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
h✝ : ExpChar F q
this : ExpChar E q
x : K
n : ℕ
y : E
h2 : (algebraMap E K) y = x ^ q ^ n
m : ℕ
z : F
h1 : (algebraMap F E) z = y ^ q ^ m
⊢ (algebraMap E K) (y ^ q ^ m) = x ^ q ^ (n + m)
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
i j : ι
⊢ ((traceForm R S) (b i)) (b j) = (trace R S) (b i * b j)

Tactic:
traceForm_apply

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
i j : ι
⊢ (trace R S) (b i * b j) = (trace R S) (b i * b j)
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
L : Type w
inst✝² : Field L
inst✝¹ : IsAlgClosed L
inst✝ : Nonempty (E →+* L)
h : Function.Injective fun f ↦ f.comp (algebraMap F E)
this : Algebra E L := (Classical.arbitrary (E →+* L)).toAlgebra
j : AlgebraicClosure E →ₐ[E] L := IsAlgClosed.lift
f g : Emb F E
⊢ (fun f ↦ f.comp (algebraMap F E)) (j.comp ↑f) = (fun f ↦ f.comp (algebraMap F E)) (j.comp ↑g)

Tactic:
by ext; simp

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
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : Algebra.IsAlgebraic F E
inst✝ : Algebra.IsSeparable E K
x : K
x✝¹ : x ∈ ⊤
S : IntermediateField F K := separableClosure F K
L : IntermediateField E K := adjoin E ↑S
this✝¹ : Algebra.IsSeparable (↥L) K
i : ↥S →+* ↥L := Subsemiring.inclusion ⋯
x✝ : Algebra ↥S ↥L := i.toAlgebra
this✝ : IsScalarTower (↥S) (↥L) K
this : Algebra.IsAlgebraic F K
⊢ x ∈ L

Tactic:
have : IsPurelyInseparable S K := separableClosure.isPurelyInseparable F K

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
inst✝ : Algebra.IsSeparable E K
x : K
x✝¹ : x ∈ ⊤
S : IntermediateField F K := separableClosure F K
L : IntermediateField E K := adjoin E ↑S
this✝² : Algebra.IsSeparable (↥L) K
i : ↥S →+* ↥L := Subsemiring.inclusion ⋯
x✝ : Algebra ↥S ↥L := i.toAlgebra
this✝¹ : IsScalarTower (↥S) (↥L) K
this✝ : Algebra.IsAlgebraic F K
this : IsPurelyInseparable (↥S) K
⊢ x ∈ L
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: case refine_2
A : Type u_1
K : Type u_2
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_3
inst✝¹⁰ : Field L
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsDomain A
inst✝ : Algebra.IsAlgebraic K L
this✝¹ : IsDomain C
this✝ : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥A⁰
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L) x = m • z
⊢ (algebraMap A L) ↑m * z = ↑m • z

Tactic:
smul_def

Goal state after:
case refine_2
A : Type u_1
K : Type u_2
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_3
inst✝¹⁰ : Field L
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsDomain A
inst✝ : Algebra.IsAlgebraic K L
this✝¹ : IsDomain C
this✝ : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥A⁰
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L) x = m • z
⊢ (algebraMap A L) ↑m * z = (algebraMap A L) ↑m * z
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : Fintype R
p : R[X]
hp : 0 < p.degree
a : R
x✝ : a ∈ image (fun x ↦ eval x p) univ
⊢ {a_1 | eval a_1 p = a} = (p - C a).roots.toFinset

Tactic:
simp [Finset.ext_iff, ← mem_roots_sub_C hp]

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
E : Type u_5
inst✝³ : Field E
inst✝² : Algebra K E
inst✝¹ : Algebra E L
inst✝ : IsScalarTower K E L
⊢ IsGaloisGroup (↥(fixingSubgroup G ↑(IsScalarTower.toAlgHom K E L).fieldRange)) E L

Tactic:
refine IsGaloisGroup.of_ringEquiv _ _ _ L
    (AlgHom.equivFieldRange (IsScalarTower.toAlgHom K E L)).toRingEquiv.symm fun ⟨_, ⟨x, rfl⟩⟩ ↦ ?_

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
E : Type u_5
inst✝³ : Field E
inst✝² : Algebra K E
inst✝¹ : Algebra E L
inst✝ : IsScalarTower K E L
x✝ : ↥(IsScalarTower.toAlgHom K E L).fieldRange
x : E
⊢ (algebraMap E L)
      ((IsScalarTower.toAlgHom K E L).equivFieldRange.toRingEquiv.symm
        ⟨(IsScalarTower.toAlgHom K E L).toRingHom x, ⋯⟩) =
    (algebraMap (↥(IsScalarTower.toAlgHom K E L).fieldRange) L) ⟨(IsScalarTower.toAlgHom K E L).toRingHom x, ⋯⟩
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : DecidableEq K
i : ℕ
⊢ ∑ x, ↑x ^ i = if q - 1 ∣ i then -1 else 0

Tactic:
by
  let φ : Kˣ →* K :=
    { toFun := fun x => x ^ i
      map_one' := by simp
      map_mul' := by simp [mul_pow] }
  have : Decidable (φ = 1) := by classical infer_instance
  calc (∑ x : Kˣ, φ x) = if φ = 1 then Fintype.card Kˣ else 0 := sum_hom_units φ
      _ = if q - 1 ∣ i then -1 else 0 := by
        suffices q - 1 ∣ i ↔ φ = 1 by
          simp only [this]
          split_ifs; swap
          · exact Nat.cast_zero
          · rw [Fintype.card_units, Nat.cast_sub,
              cast_card_eq_zero, Nat.cast_one, zero_sub]
            show 1 ≤ q; exact Fintype.card_pos_iff.mpr ⟨0⟩
        rw [← forall_pow_eq_one_iff, DFunLike.ext_iff]
        apply forall_congr'; intro x; simp [φ, Units.ext_iff]

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

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun x ↦ ↑x, inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ ∑ x, x ^ i = 0

Tactic:
calc
      ∑ x : K, x ^ i = ∑ x ∈ univ \ {(0 : K)}, x ^ i := by
        rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton, zero_pow hi, add_zero]
      _ = ∑ x : Kˣ, (x ^ i : K) := by simp [φ, ← this, univ.sum_map φ]
      _ = 0 := by rw [sum_pow_units K i, if_neg]; exact hiq

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

Goal state before:
pp: n : ℕ
⊢ (↑(quotientSpanNatEquivZMod n).symm).comp (castRingHom (ZMod n)) = Ideal.Quotient.mk (Ideal.span {↑n})

Tactic:
by ext; simp

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

Goal state before:
pp: n : ℤ
⊢ (↑n.quotientSpanEquivZMod.symm).comp (castRingHom (ZMod n.natAbs)) = Ideal.Quotient.mk (Ideal.span {n})

Tactic:
by ext; simp

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

Goal state before:
pp: F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
x✝ : Fintype ↥⊥ := fintypeBot F p
⊢ univ.val.card = (X ^ p - X).natDegree

Tactic:
← Finset.card_def,

Goal state after:
F : Type u_3
inst✝² : Field F
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP F p
x✝ : Fintype ↥⊥ := fintypeBot F p
⊢ #univ = (X ^ p - X).natDegree