mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Flat R M
inst✝⁴ : Module.Finite R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Finite R N
inst✝ : Flat R N
p : PrimeSpectrum R
e : Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N) :=
  (AlgebraTensorModule.assoc R R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal) M N).symm ≪≫ₗ
    (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal)
        (Localization.AtPrime p.asIdeal ⊗[R] M) N).symm
⊢ rankAtStalk M p * rankAtStalk N p = rankAtStalk M p * rankAtStalk N p

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Flat R M
inst✝ : Module.Finite R M
p : PrimeSpectrum R
k : Type uR := p.asIdeal.ResidueField
e : k ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] M) ≃ₗ[k] k ⊗[R] M :=
  AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) k k M
⊢ finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M) =
    finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
p : Ideal R
inst✝ : p.IsPrime
K : Type uR := FractionRing R
Rp : Type uR := Localization.AtPrime p
Mp : Type (max uR uM) := LocalizedModule.AtPrime p M
⊢ finrank R M = finrank R M

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
h : Function.Injective ⇑(LinearMap.lTensor M f)
⊢ Function.Injective
    ⇑(↑(leftCancelEquiv P (linearEquiv R M)) ∘ₗ
        LinearMap.lTensor (Dual R M) (LinearMap.lTensor M f) ∘ₗ ↑(leftCancelEquiv N (linearEquiv R M)).symm)

Tactic:
]

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
h : Function.Injective ⇑(LinearMap.lTensor M f)
⊢ Function.Injective
    ⇑(↑(leftCancelEquiv P (linearEquiv R M)) ∘ₗ
        LinearMap.lTensor (Dual R M) (LinearMap.lTensor M f) ∘ₗ ↑(leftCancelEquiv N (linearEquiv R M)).symm)
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
⊢ Function.Injective ⇑f ↔ Function.Injective ⇑f

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
h : Function.Surjective ⇑(LinearMap.lTensor M f)
⊢ Function.Surjective
    ⇑(↑(leftCancelEquiv P (linearEquiv R M)) ∘ₗ
        LinearMap.lTensor (Dual R M) (LinearMap.lTensor M f) ∘ₗ ↑(leftCancelEquiv N (linearEquiv R M)).symm)

Tactic:
]

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
h : Function.Surjective ⇑(LinearMap.lTensor M f)
⊢ Function.Surjective
    ⇑(↑(leftCancelEquiv P (linearEquiv R M)) ∘ₗ
        LinearMap.lTensor (Dual R M) (LinearMap.lTensor M f) ∘ₗ ↑(leftCancelEquiv N (linearEquiv R M)).symm)
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
f : K →ₐ[F] L
x✝¹ : L
x✝ : x✝¹ ∈ f.fieldRange
x : K
hx : f.toRingHom x = x✝¹
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
⊢ Function.Surjective ⇑f ↔ Function.Surjective ⇑f

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
⊢ (∀ (x : K), (Polynomial.map (algebraMap F ↥(normalClosure F K L)) (minpoly F x)).Splits) ∧
    normalClosure F K ↥(normalClosure F K L) = ⊤

Tactic:
]

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
⊢ (∀ (x : K), (Polynomial.map (algebraMap F ↥(normalClosure F K L)) (minpoly F x)).Splits) ∧
    normalClosure F K ↥(normalClosure F K L) = ⊤
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case left
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
⊢ ∀ (x : K),
    (Polynomial.map (algebraMap F ↥(⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L))) (minpoly F x)).Splits

Tactic:
]

Goal state after:
case left
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
⊢ ∀ (x : K),
    (Polynomial.map (algebraMap F ↥(⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L))) (minpoly F x)).Splits
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
⊢ Function.Bijective ⇑(LinearMap.lTensor M f) ↔ Function.Bijective ⇑f

Tactic:
by
  simp_rw [Function.Bijective, lTensor_injective_iff, lTensor_surjective_iff]

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module.Invertible R M
inst✝ : Free R M
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case right
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : ↥(⨆ f, f.fieldRange)
x✝ : x ∈ ⊤
⊢ (⨆ f, f.fieldRange).val x ∈ ↑(⨆ i, IntermediateField.map (⨆ f, f.fieldRange).val i.fieldRange)

Tactic:
]

Goal state after:
case right
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : ↥(⨆ f, f.fieldRange)
x✝ : x ∈ ⊤
⊢ (⨆ f, f.fieldRange).val x ∈ ↑(⨆ i, IntermediateField.map (⨆ f, f.fieldRange).val i.fieldRange)
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case right
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : ↥(⨆ f, f.fieldRange)
x✝ : x ∈ ⊤
f : K →ₐ[F] L
⊢ f.fieldRange ≤ f.fieldRange

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
⊢ ⊤ ≤ F⟮↑α⟯

Tactic:
]

Goal state after:
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
⊢ ⊤ ≤ F⟮↑α⟯
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case pos
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : x = 0
⊢ 0 ∈ F⟮↑α⟯

Tactic:
]

Goal state after:
case pos
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : x = 0
⊢ 0 ∈ F⟮↑α⟯
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
h : IsNormalClosure F K L
L' : Type ?u.22
inst✝¹ : Field L'
inst✝ : Algebra F L'
splits : ∀ (x : K), (Polynomial.map (algebraMap F L') (minpoly F x)).Splits
this : adjoin F (⨆ x, (minpoly F x).rootSet L) = ⊤
⊢ L →ₐ[F] L'

Tactic:
]

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
h : IsNormalClosure F K L
L' : Type ?u.22
inst✝¹ : Field L'
inst✝ : Algebra F L'
splits : ∀ (x : K), (Polynomial.map (algebraMap F L') (minpoly F x)).Splits
this : adjoin F (⨆ x, (minpoly F x).rootSet L) = ⊤
⊢ L →ₐ[F] L'
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case neg
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
⊢ ↑α ^ n ∈ F⟮↑α⟯

Tactic:
]

Goal state after:
case neg
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
⊢ ↑α ^ n ∈ F⟮↑α⟯
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K)) F K := Module.Basis.ofVectorSpace F K
⊢ ∀ (y : ↑(Module.Basis.ofVectorSpaceIndex F K)),
    s y ∈ ↑(Subalgebra.toSubmodule (Algebra.adjoin F ((∏ x, minpoly F (s x)).rootSet K)))

Tactic:
]

Goal state after:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K)) F K := Module.Basis.ofVectorSpace F K
⊢ ∀ (y : ↑(Module.Basis.ofVectorSpaceIndex F K)),
    s y ∈ ↑(Subalgebra.toSubmodule (Algebra.adjoin F ((∏ x, minpoly F (s x)).rootSet K)))
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case refine_2
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K)) F K := Module.Basis.ofVectorSpace F K
x : ↑(Module.Basis.ofVectorSpaceIndex F K)
⊢ ∏ x_1, (aeval (s x)) (minpoly F (s x_1)) = 0

Tactic:
]

Goal state after:
case refine_2
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K)) F K := Module.Basis.ofVectorSpace F K
x : ↑(Module.Basis.ofVectorSpaceIndex F K)
⊢ ∏ x_1, (aeval (s x)) (minpoly F (s x_1)) = 0
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case inl
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
hFEp : IsSplittingField F E 0
this : ⊥ = ⊤
⊢ Normal F E

Tactic:
]

Goal state after:
case inl
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
hFEp : IsSplittingField F E 0
this : ⊥ = ⊤
⊢ Normal F E
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
x : K
⊢ (Polynomial.map (algebraMap F L) (minpoly F (φ x))).Splits

Tactic:
]

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
x : K
⊢ (Polynomial.map (algebraMap F L) (minpoly F (φ x))).Splits
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case inr
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits ∧
    (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)).Splits
⊢ IsIntegral F x ∧ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits

pp: F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p *
      Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)).Splits
⊢ Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p ≠ 0

Tactic:
]

Goal state after:
case inr
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits ∧
    (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)).Splits
⊢ IsIntegral F x ∧ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits

F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p *
      Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)).Splits
⊢ Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p ≠ 0
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case inl
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
h : Normal F L
h✝ : IsEmpty (K →ₐ[F] L)
⊢ Normal F ↥⊥

Tactic:
]

Goal state after:
case inl
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
h : Normal F L
h✝ : IsEmpty (K →ₐ[F] L)
⊢ Normal F ↥⊥
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ {α, β} ⊆ ↑F⟮γ⟯

Tactic:
]

Goal state after:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ {α, β} ⊆ ↑F⟮γ⟯
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✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ α + c • β - c • β ∈ F⟮γ⟯

Tactic:
]

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✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ α + c • β - c • β ∈ F⟮γ⟯
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : Algebra.IsAlgebraic F K
h : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
L' : Type u_4
inst✝¹ : Field L'
inst✝ : Algebra F L'
⊢ Nonempty (↥(IntermediateField.adjoin F (⨆ x, (minpoly F x).rootSet L')) →ₐ[F] L)

Tactic:
]

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : Algebra.IsAlgebraic F K
h : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
L' : Type u_4
inst✝¹ : Field L'
inst✝ : Algebra F L'
⊢ Nonempty (↥(IntermediateField.adjoin F (⨆ x, (minpoly F x).rootSet L')) →ₐ[F] L)
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case inr
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : (Polynomial.map (↑j) (Polynomial.map (algebraMap F E) (minpoly F x))).Splits
⊢ IsIntegral F x ∧ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits

Tactic:
]

Goal state after:
case inr
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : (Polynomial.map (↑j) (Polynomial.map (algebraMap F E) (minpoly F x))).Splits
⊢ IsIntegral F x ∧ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Module.Invertible R M
inst✝ : Module.Invertible R N
M' : Type u := Finite.reprₛ R M
⊢ toSkeleton (MonoidalCategoryStruct.tensorObj (SemimoduleCat.of R (Dual R M')) (SemimoduleCat.of R M')) = 1

Tactic:
]

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Module.Invertible R M
inst✝ : Module.Invertible R N
M' : Type u := Finite.reprₛ R M
⊢ toSkeleton (MonoidalCategoryStruct.tensorObj (SemimoduleCat.of R (Dual R M')) (SemimoduleCat.of R M')) = 1
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ γ ∈ F⟮α, β⟯

Tactic:
]

Goal state after:
case a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ γ ∈ F⟮α, β⟯
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : Pic R
⊢ M = N ↔ M = N

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
⊢ Nonempty (M ≃ₗ[R] R) ↔ Nonempty (M ≃ₗ[R] R)

Tactic:
]

Goal state after: