mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ finrank R M = 1

Tactic:
by

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
⊢ ⇑(toModuleEnd R M) =
    ⇑(lid R M).conj ∘
      ⇑(rTensorEquiv R R (TensorProduct.comm R M (Dual R M) ≪≫ₗ linearEquiv R M)) ∘
        ⇑(RingEquiv.moduleEndSelf R) ∘ ⇑MulOpposite.opEquiv

Tactic:
by

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
⊢ Function.Bijective ⇑(toModuleEnd R M)

Tactic:
by

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
f : R →ₗ[R] M
hf : Function.Surjective ⇑f
r₁ r₂ : R
eq : f r₁ = f r₂
m : M
⊢ (fun x1 x2 ↦ x1 • x2) r₁ m = (fun x1 x2 ↦ x1 • x2) r₂ m

Tactic:
by

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
⊢ IsNormalClosure F K ↥(normalClosure F K L)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

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

Tactic:
by

Goal state after:
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
⊢ ∃ α, F⟮α⟯ = ⊤

Tactic:
by

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
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✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Module.Invertible R A
inv : A →ₗ[R] R :=
  ↑(linearEquiv R A) ∘ₗ LinearMap.lTensor (Dual R A) (LinearMap.mul' R A) ∘ₗ ↑(leftCancelEquiv A (linearEquiv R A)).symm
s : Finset (Dual R A × A)
hs : (linearEquiv R A).symm 1 = ∑ i ∈ s, i.1 ⊗ₜ[R] i.2
⊢ (inv ∘ₗ Algebra.linearMap R A) 1 = LinearMap.id 1

Tactic:
by

Goal state after:
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
⊢ ∃ p, IsSplittingField F K p

Tactic:
by

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
⊢ L →ₐ[F] L'

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
⊢ ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c

Tactic:
by

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
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
⊢ IsNormalClosure F K ↥(normalClosure F K L)

Tactic:
by

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
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
⊢ normalClosure F K L = ⨆ x, adjoin F ((minpoly F x).rootSet L)

Tactic:
by

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
⊢ ∃ s, Ideal.span ↑s = ⊤ ∧ ∀ r ∈ s, Free (Localization.Away r) (LocalizedModule.Away r M)

Tactic:
by

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 : Normal F L
⊢ Normal F ↥(normalClosure F K L)

Tactic:
by

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✝ : FiniteDimensional F K
⊢ FiniteDimensional F ↥(normalClosure F K L)

Tactic:
by

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 K L
inst✝ : IsScalarTower F K L
⊢ IsScalarTower F K ↥(normalClosure F K L)

Tactic:
by

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
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
sf : Type (max 0 u) := (n : ℕ) × ModuleCon R (Fin n → R)
c₁ c₂ : sf
⊢ c₁ = c₂ → ModuleCon.Quotient (Fin c₁.fst → R) c₁.snd ≃ₗ[R] ModuleCon.Quotient (Fin c₂.fst → R) c₂.snd

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : 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:
by

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
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✝ : (Skeleton (SemimoduleCat R))ˣ
M N : Skeleton (SemimoduleCat R)
⊢ M = N → ↑(Quotient.out M) ≃ₗ[R] ↑(Quotient.out N)

Tactic:
by

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
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 : (Skeleton (SemimoduleCat R))ˣ
this : {M N : Skeleton (SemimoduleCat R)} → M = N → ↑(Quotient.out M) ≃ₗ[R] ↑(Quotient.out N)
⊢ ↑((equivShrink (Skeleton (SemimoduleCat R))ˣ).symm (id ((equivShrink (Skeleton (SemimoduleCat R))ˣ) M))) = ↑M

Tactic:
by

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
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
⊢ ⟦SemimoduleCat.of R M'⟧ * ⟦SemimoduleCat.of R (Dual R M')⟧ = 1

Tactic:
by

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
h : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
L' : Type u_4
inst✝¹ : Field L'
inst✝ : Algebra F L'
⊢ Nonempty (↥(⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L')) →ₐ[F] L)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : Pic R
⊢ M = N ↔ Nonempty (M.AsModule ≃ₗ[R] N.AsModule)

Tactic:
by

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
⊢ Pic.mk R M = 1 ↔ Nonempty (M ≃ₗ[R] R)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : 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⟮α, β⟯ = F⟮γ⟯

Tactic:
by

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
h✝ : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
L' : Type u_4
inst✝¹ : Field L'
inst✝ : Algebra F L'
φ : ↥(⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L')) →ₐ[F] L := ⋯.some
φ' : ↥(normalClosure F K L') →ₐ[F] L := φ.comp (inclusion ⋯)
x✝¹ x✝ : K →ₐ[F] L'
h : (φ'.comp ∘ ⇑(normalClosure.algHomEquiv F K L').symm) x✝¹ = (φ'.comp ∘ ⇑(normalClosure.algHomEquiv F K L').symm) x✝
⊢ (normalClosure.algHomEquiv F K L').symm x✝¹ = (normalClosure.algHomEquiv F K L').symm x✝

Tactic:
by

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

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F ↥K
⊢ normalClosure F (↥K) L = K

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : 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 • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
p_linear : Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)
⊢ β = (algebraMap (↥F⟮γ⟯) E) (-p.coeff 0 / p.coeff 1)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F L
⊢ normalClosure F (↥K) L = ⨆ f, map f K

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Invertible R M
inst✝ : Module.Invertible R N
⊢ ↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (M ⊗[R] N))⟧
        ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (M ⊗[R] N)))⟧ ⋯) =
    ↑((equivShrink (Skeleton (SemimoduleCat R))ˣ).symm.toFun (Pic.mk R M) *
        (equivShrink (Skeleton (SemimoduleCat R))ˣ).symm.toFun (Pic.mk R N))

Tactic:
by

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

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K : IntermediateField F L
inst✝ : Normal F L
⊢ normalClosure F (↥K) L = ⨆ f, map (↑f) K

Tactic:
by

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

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K K' : IntermediateField F L
inst✝ : Normal F L
h : K ≤ K'
⊢ normalClosure F (↥K) L ≤ normalClosure F (↥K') L

Tactic:
by

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
⊢ ↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (Dual R M))⟧
        ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (Dual R M)))⟧ ⋯) =
    ↑((equivShrink (Skeleton (SemimoduleCat R))ˣ).symm.toFun (Pic.mk R M))⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M : Pic R
⊢ M⁻¹ = Pic.mk R (Dual R M.AsModule)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : Pic R
⊢ M * N = Pic.mk R (M.AsModule ⊗[R] N.AsModule)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
⊢ Normal F ↥K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
h : ∀ (a : Type u) (b : AddCommMonoid a) (c : Module R a) (d : Module.Invertible R a), Pic.mk R a = 1
M N : Pic R
⊢ M = N

Tactic:
by

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

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
⊢ Normal F ↥K ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : 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 • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
p_linear : Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)
⊢ β ∈ F⟮γ⟯

Tactic:
by

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
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
inst✝ : IsLocalRing R
M : Type u
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Invertible R M
S : Finset (Dual R M × M)
hS : (Invertible.linearEquiv R M).symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ 1 = ∑ i ∈ S, i.1 i.2

Tactic:
by

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

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
⊢ Normal F ↥K ↔ ∀ (σ : Gal(L/F)), map (↑σ) K ≤ K

Tactic:
by

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
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
inst✝ : IsLocalRing R
M : Type u
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Invertible R M
⊢ Free R M

Tactic:
by

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

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
σ✝ : L →ₐ[F] L
σ : Gal(L/F)
⊢ normalClosure F (↥(map (↑σ) K)) L = normalClosure F (↥K) L

Tactic:
by

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

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
σ : L →ₐ[F] L
⊢ normalClosure F (↥(map σ K)) L = normalClosure F (↥K) L

Tactic:
by

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
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
A : Type u_5
B : Type u_6
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : Algebra R A
x✝¹ x✝ : Pic R
⊢ Pic.mk A (A ⊗[R] (x✝¹ * x✝).AsModule) = Pic.mk A (A ⊗[R] x✝¹.AsModule) * Pic.mk A (A ⊗[R] x✝.AsModule)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
A : Type u_5
B : Type u_6
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
⊢ (mapAlgebra A B).comp (mapAlgebra R A) = mapAlgebra R B

Tactic:
by

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

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
⊢ normalClosure F (↥K₁) L ≤ K₂ ↔ K₁ ≤ K₂

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ mapAlgebra R R = MonoidHom.id (Pic R)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ mapRingHom (algebraMap R A) = mapAlgebra R A

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type u_7
T : Type u_8
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* S
g : S →+* T
⊢ (mapRingHom g).comp (mapRingHom f) = mapRingHom (g.comp f)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ mapRingHom (RingHom.id R) = MonoidHom.id (Pic R)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (⇑f ∘ x)
⊢ aeval (⇑f ∘ x) = f.comp (aeval x)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (⇑f ∘ x)
⊢ AlgebraicIndependent R x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
f : ι' → ι
hf : Injective f
⊢ AlgebraicIndependent R (x ∘ f)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
⊢ AlgebraicIndependent R Subtype.val

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s t : Set ι
H : AlgebraicIndepOn R x t
hst : s ⊆ t
⊢ AlgebraicIndepOn R x s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
K : Type u_4
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
hx✝ : AlgebraicIndependent R x
s : Set ι
hx : AlgebraicIndepOn R x s
⊢ (range fun i ↦ x ↑i) = x '' s

Tactic:
by

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

Goal state before:
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
⊢ Normal F E

Tactic:
by

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

Goal state before:
pp: R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
⊢ IsTranscendenceBasis R Subtype.val ↔ Maximal (AlgebraicIndepOn R _root_.id) s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
e : ι ≃ ι'
f : ι' → A
⊢ IsTranscendenceBasis R (f ∘ ⇑e) ↔ IsTranscendenceBasis R f

Tactic:
by

Goal state after: