mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ IsAlgebraic (↥Rt) y

Tactic:
have := Algebra.IsAlgebraic.nontrivial R S

Goal state after:
ι : 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
⊢ IsAlgebraic (↥Rt) y
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : 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
H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i s \ {j})))) (v j)
this : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
have := (adjoin R (v '' (insert i s \ {j}))).subtype_injective.nontrivial

Goal state after:
ι : 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
H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i s \ {j})))) (v j)
this✝ : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this : Nontrivial S
⊢ IsTranscendenceBasis R fun x ↦ v ↑x
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m

Tactic:
have h1 := hs.eq_prod_roots_of_monic hm

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
h1 : f = (Multiset.map (fun x ↦ X - C x) f.roots).prod
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m
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
H : Subgroup Gal(E/F)
K : IntermediateField F E
x : ↥K
y : ↥(fixedField K.fixingSubgroup)
ϕ : ↥K.fixingSubgroup
⊢ ϕ • (↑x * ↑y) = ↑x * ↑y

Tactic:
by
    rw [smul_mul', show ϕ • (x : E) = ↑x from ϕ.2 x, show ϕ • (y : E) = ↑y from y.2 ϕ]

Goal state after:
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
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
⊢ finrank (↥K) E = finrank (↥(fixedField K.fixingSubgroup)) E

Tactic:
rw [IntermediateField.finrank_fixedField_eq_card,
    Nat.card_congr (IntermediateField.fixingSubgroupEquiv K).toEquiv]

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
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
⊢ finrank (↥K) E = Nat.card Gal(E/↥K)
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ insepDegree F ↥⊥ = 1

Tactic:
by
  have := lift_insepDegree_eq_of_equiv _ _ _ (botEquiv F E)
  rwa [insepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{v, u}, Cardinal.lift_inj] at this

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:
by
      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.Topology.Algebra.Group.ClosedSubgroup

Goal state before:
pp: G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : SeparatelyContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h : T1Space (G ⧸ H)
⊢ IsOpen ↑H

Tactic:
rw [← QuotientGroup.discreteTopology_iff]

Goal state after:
G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : SeparatelyContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h : T1Space (G ⧸ H)
⊢ DiscreteTopology (G ⧸ H)
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: case right
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K L : IntermediateField F E
inst✝¹ : IsGalois F ↥K
inst✝ : FiniteDimensional F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : (Polynomial.map (algebraMap F ↥K) T).Splits ∧ adjoin F (T.rootSet E) = lift ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
h' : T'.rootSet E = T.rootSet E
⊢ L ⊔ adjoin F (T.rootSet E) = ⊤

Tactic:
hT₂.2,

Goal state after:
case right
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
K L : IntermediateField F E
inst✝¹ : IsGalois F ↥K
inst✝ : FiniteDimensional F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : (Polynomial.map (algebraMap F ↥K) T).Splits ∧ adjoin F (T.rootSet E) = lift ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
h' : T'.rootSet E = T.rootSet E
⊢ L ⊔ lift ⊤ = ⊤
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
z : M
⊢ z ∈ ↑N → (B ↑x) z = (B ↑y) z

Tactic:
hz

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
hz : z ∈ ↑N
⊢ (B ↑x) z = (B ↑y) z
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
hs : IsIntegral R s
p : R[X]
⊢ p ∈ RingHom.ker (Polynomial.aeval s).toRingHom ↔ p ∈ Ideal.span {minpoly R s}

Tactic:
simp_rw [RingHom.mem_ker, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
    isIntegrallyClosed_dvd_iff hs, ← Ideal.mem_span_singleton]

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✝ : IsPurelyInseparable F K
⊢ IsPurelyInseparable F E

Tactic:
refine ⟨⟨fun x ↦ (isIntegral' F (algebraMap E K x)).tower_bot_of_field⟩, fun x h ↦ ?_⟩
  rw [IsSeparable, ← minpoly.algebraMap_eq (algebraMap E K).injective] at h
  obtain ⟨y, h⟩ := inseparable F _ h
  exact ⟨y, (algebraMap E K).injective (h.symm ▸ (IsScalarTower.algebraMap_apply F E K y).symm)⟩

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 : ℕ
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
d : ℕ
hd : finrank F E = d
⊢ ∃ n, d = q ^ n

Tactic:
induction d using Nat.strongRecOn generalizing F with

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: case refine_1
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
x : A
hx : x ∈ ↑A⁰
⊢ ↑⟨(algebraMap A C) x, ⋯⟩ ≠ 0

Tactic:
Subtype.coe_mk,

Goal state after:
case refine_1
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
x : A
hx : x ∈ ↑A⁰
⊢ (algebraMap A C) x ≠ 0
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
⊢ z * (algebraMap C L) ↑(x, ⟨(algebraMap A C) ↑m, ⋯⟩).2 = (algebraMap C L) (x, ⟨(algebraMap A C) ↑m, ⋯⟩).1

Tactic:
Subtype.coe_mk,

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
⊢ z * (algebraMap C L) ((algebraMap A C) ↑m) = (algebraMap C L) (x, ⟨(algebraMap A C) ↑m, ⋯⟩).1
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: 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✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
this✝ : DecidableEq L
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral A (b x)
b' : Basis (↥s) K L := (traceForm K L).dualBasis ⋯ b
this : IsNoetherian A ↥(Submodule.span A (Set.range ⇑b')) := isNoetherian_span_of_finite A (Set.finite_range ⇑b')
f : C →ₗ[A] ↥(Submodule.span A (Set.range ⇑b')) := Submodule.inclusion ⋯ ∘ₗ (↑A (Algebra.linearMap C L)).rangeRestrict
⊢ f.ker = ⊥

Tactic:
rw [LinearMap.ker_comp, Submodule.ker_inclusion, Submodule.comap_bot, LinearMap.ker_codRestrict]

Goal state after:
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✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsNoetherianRing A
this✝ : DecidableEq L
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral A (b x)
b' : Basis (↥s) K L := (traceForm K L).dualBasis ⋯ b
this : IsNoetherian A ↥(Submodule.span A (Set.range ⇑b')) := isNoetherian_span_of_finite A (Set.finite_range ⇑b')
f : C →ₗ[A] ↥(Submodule.span A (Set.range ⇑b')) := Submodule.inclusion ⋯ ∘ₗ (↑A (Algebra.linearMap C L)).rangeRestrict
⊢ (↑A (Algebra.linearMap C L)).ker = ⊥
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case neg.succ
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
⊢ ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff = 0 x

Tactic:
nextCoeff,

Goal state after:
case neg.succ
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : (expand K (p ^ (n + 1))) g = minpoly K x
⊢ (↑(finrank (↥K⟮x⟯) L) *
      -if (minpoly K x).natDegree = 0 then 0 else (minpoly K x).coeff ((minpoly K x).natDegree - 1)) =
    0 x
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: case refine_1
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
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup (↥H) (↥F) L
x : L
hx : x ∈ FixedPoints.intermediateField ↥H
⊢ x ∈ F

pp: case refine_2
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
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup (↥H) (↥F) L
x : L
hx : x ∈ F
⊢ x ∈ FixedPoints.intermediateField ↥H

Tactic:
· obtain ⟨a, rfl⟩ := hHFL.isInvariant.isInvariant x hx
    exact a.prop

Goal state after:
case refine_2
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
H : Subgroup G
F : IntermediateField K L
hGKL : IsGaloisGroup G K L
hHFL : IsGaloisGroup (↥H) (↥F) L
x : L
hx : x ∈ F
⊢ x ∈ FixedPoints.intermediateField ↥H
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✝ : SMulCommClass G K L
⊢ FixedPoints.intermediateField ↥⊥ = ⊤

Tactic:
by
  simp [IntermediateField.ext_iff]

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
⊢ Function.Surjective ⇑(trace K L)

Tactic:
rw [← LinearMap.range_eq_top]
  apply (IsSimpleOrder.eq_bot_or_eq_top (α := Ideal K) _).resolve_left
  rw [LinearMap.range_eq_bot]
  exact Algebra.trace_ne_zero K L

Goal state after:
Module: Mathlib.Data.Int.Associated

Goal state before:
pp: a b : ℤ
⊢ a.natAbs = b.natAbs ↔ Associated a b

Tactic:
by
  refine Int.natAbs_eq_natAbs_iff.trans ?_
  constructor
  · rintro (rfl | rfl)
    · rfl
    · exact ⟨-1, by simp⟩
  · rintro ⟨u, rfl⟩
    obtain rfl | rfl := Int.units_eq_one_or u
    · exact Or.inl (by simp)
    · exact Or.inr (by simp)

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹⁷ : Group G
inst✝¹⁶ : Group G'
A : Type u_5
B : Type u_6
C : Type u_7
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : CommRing C
inst✝¹² : IsDomain C
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra A C
inst✝⁹ : Algebra B C
inst✝⁸ : FaithfulSMul A B
inst✝⁷ : FaithfulSMul B C
inst✝⁶ : IsScalarTower A B C
inst✝⁵ : Finite G
inst✝⁴ : Finite G'
inst✝³ : MulSemiringAction G C
inst✝² : IsGaloisGroup G A C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
g : G
x : B
this✝³ : IsDomain B
this✝² : IsDomain A
this✝¹ : FaithfulSMul A C
this✝ : MulSemiringAction G (FractionRing C) := IsFractionRing.mulSemiringAction G C (FractionRing C)
this : MulSemiringAction G' (FractionRing B) := IsFractionRing.mulSemiringAction G' B (FractionRing B)
⊢ (algebraMap B (FractionRing C)) ((restrictHom G G' A B C) g • x) =
    (algebraMap C (FractionRing C)) (g • (algebraMap B C) x)

Tactic:
IsScalarTower.algebraMap_apply B (FractionRing B) (FractionRing C)

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹⁷ : Group G
inst✝¹⁶ : Group G'
A : Type u_5
B : Type u_6
C : Type u_7
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : CommRing C
inst✝¹² : IsDomain C
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra A C
inst✝⁹ : Algebra B C
inst✝⁸ : FaithfulSMul A B
inst✝⁷ : FaithfulSMul B C
inst✝⁶ : IsScalarTower A B C
inst✝⁵ : Finite G
inst✝⁴ : Finite G'
inst✝³ : MulSemiringAction G C
inst✝² : IsGaloisGroup G A C
inst✝¹ : MulSemiringAction G' B
inst✝ : IsGaloisGroup G' A B
g : G
x : B
this✝³ : IsDomain B
this✝² : IsDomain A
this✝¹ : FaithfulSMul A C
this✝ : MulSemiringAction G (FractionRing C) := IsFractionRing.mulSemiringAction G C (FractionRing C)
this : MulSemiringAction G' (FractionRing B) := IsFractionRing.mulSemiringAction G' B (FractionRing B)
⊢ (algebraMap (FractionRing B) (FractionRing C)) ((algebraMap B (FractionRing B)) ((restrictHom G G' A B C) g • x)) =
    (algebraMap C (FractionRing C)) (g • (algebraMap B C) x)
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
| 1 x

Tactic:
RingHom.one_def,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : Fintype K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
hcard : q = p ^ n
x : K
| (RingHom.id K) x
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
f : K[X]
⊢ (expand K q) f = f ^ q

Tactic:
obtain ⟨p, hp⟩ := CharP.exists K

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
f : K[X]
p : ℕ
hp : CharP K p
⊢ (expand K q) f = f ^ q
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
f : K[X]
p : ℕ
hp✝ : CharP K p
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ n
this : Fact (Nat.Prime p)
⊢ (expand K (p ^ n)) f = Polynomial.map 1 ((expand K (p ^ n)) f)

Tactic:
RingHom.one_def,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
f : K[X]
p : ℕ
hp✝ : CharP K p
n : ℕ
npos : 0 < n
hp : Nat.Prime p
hn : q = p ^ n
this : Fact (Nat.Prime p)
⊢ (expand K (p ^ n)) f = Polynomial.map (RingHom.id K) ((expand K (p ^ n)) f)
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ invFun p (toFun p (Quotient.mk x')) = Quotient.mk x'

Tactic:
dsimp only [toFun, invFun]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ (piQuotientLift p (pi Set.univ p) (single R Ms) ⋯) ((quotientPiLift p (fun i ↦ (p i).mkQ) ⋯) (Quotient.mk x')) =
    Quotient.mk x'
Module: Mathlib.LinearAlgebra.Quotient.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ Function.RightInverse (invFun p) (toFun p)

Tactic:
dsimp only [toFun, invFun]

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ Function.RightInverse ⇑(piQuotientLift p (pi Set.univ p) (single R Ms) ⋯) ⇑(quotientPiLift p (fun i ↦ (p i).mkQ) ⋯)
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: case pos
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : P.LiesOver p
⊢ finrank (R ⧸ p) (S ⧸ comap e P) = p.inertiaDeg' P

Tactic:
inertiaDeg'_algebraMap

Goal state after:
case pos
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
S₁ : Type u_1
inst✝¹ : CommRing S₁
inst✝ : Algebra R S₁
e : S ≃ₐ[R] S₁
P : Ideal S₁
he : comap f (comap e P) = p ↔ comap (algebraMap R S₁) P = p
h : P.LiesOver p
⊢ finrank (R ⧸ p) (S ⧸ comap e P) = finrank (R ⧸ p) (S₁ ⧸ P)
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommRing R
S : Type v
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Module.Finite R T
Q : Ideal T
inst✝² : P.LiesOver p
inst✝¹ : Q.LiesOver P
inst✝ : p.IsPrime
this : Q.LiesOver p
⊢ finrank (S ⧸ P) (T ⧸ Q) ≤ p.inertiaDeg' Q

Tactic:
inertiaDeg'_algebraMap

Goal state after:
R : Type u
inst✝¹⁰ : CommRing R
S : Type v
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
p : Ideal R
P : Ideal S
T : Type u_2
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Module.Finite R T
Q : Ideal T
inst✝² : P.LiesOver p
inst✝¹ : Q.LiesOver P
inst✝ : p.IsPrime
this : Q.LiesOver p
⊢ finrank (S ⧸ P) (T ⧸ Q) ≤ finrank (R ⧸ p) (T ⧸ Q)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a d d' e e' : S
a_notMem : a ∉ P ^ (i + 1)
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)
⊢ d - d' ∈ P

Tactic:
have h' : a * (d - d') ∈ P ^ (i + 1) := by
    convert! Ideal.add_mem _ h (Ideal.sub_mem _ e'_mem e_mem) using 1
    ring

Goal state after:
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a d d' e e' : S
a_notMem : a ∉ P ^ (i + 1)
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)
h' : a * (d - d') ∈ P ^ (i + 1)
⊢ d - d' ∈ P