mathlib-initiative/mathlib-tactics huggingface dataset:
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:
simpa using

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 ⇑(LinearMap.lTensor (Dual R M) (LinearMap.lTensor M f))
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case refine_1
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
x✝ : IsNormalClosure F K L
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
h : ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L) = ⊤
⊢ normalClosure F K L = ⊤

Tactic:
simpa using

Goal state after:
case refine_1
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
x✝ : IsNormalClosure F K L
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
h : ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L) = ⊤
⊢ ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L) = ⊤
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case refine_2
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
x✝ : (∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) ∧ normalClosure F K L = ⊤
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
h : normalClosure F K L = ⊤
⊢ ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L) = ⊤

Tactic:
simpa using

Goal state after:
case refine_2
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
x✝ : (∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) ∧ normalClosure F K L = ⊤
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
h : normalClosure F K L = ⊤
⊢ ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L) = ⊤
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
x✝ : Free R M
a✝ : Nontrivial R
e : M ≃ₗ[R] Free.ChooseBasisIndex R M →₀ R
this : Fintype.card (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) = Fintype.card Unit
⊢ Fintype.card (Free.ChooseBasisIndex R M) = 1

Tactic:
simpa using

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
x✝ : Free R M
a✝ : Nontrivial R
e : M ≃ₗ[R] Free.ChooseBasisIndex R M →₀ R
this : Fintype.card (Free.ChooseBasisIndex R M × Free.ChooseBasisIndex R M) = Fintype.card Unit
⊢ Fintype.card (Free.ChooseBasisIndex R M) = 1
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
this :
  ⇑(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
⊢ Function.Bijective ⇑(toModuleEnd R M)

Tactic:
simpa using

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
this :
  ⇑(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
⊢ Function.Bijective MulOpposite.op
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:
simpa using

Goal state after:
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
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:
simpa using

Goal state after:
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 ⇑f
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case refine_1
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
S : Finset (Dual R M × M)
hS : (linearEquiv R M).symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ Ideal.span ↑(Finset.image (fun i ↦ i.1 i.2) S) = ⊤

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
S : Finset (Dual R M × M)
hS : (linearEquiv R M).symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ ∑ i ∈ S, i.1 i.2 ∈ Ideal.span ((fun i ↦ i.1 i.2) '' ↑S)
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
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯

Tactic:
obtain ⟨c, hc⟩ := primitive_element_inf_aux_exists_c (ιEE'.comp ιFE) (ιEE' α) (ιEE' β) f g

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
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯
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:
simpa using

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
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
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case refine_1
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₂
h : ∀ (f : ↥K₁ →ₐ[F] L), f.fieldRange ≤ K₂
⊢ K₁ ≤ K₂

Tactic:
simpa using

Goal state after:
case refine_1
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₂
h : ∀ (f : ↥K₁ →ₐ[F] L), f.fieldRange ≤ K₂
⊢ K₁ ≤ K₂
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
p q : MvPolynomial ι' R
⊢ (aeval (x ∘ f)) p = (aeval (x ∘ f)) q → p = q

Tactic:
simpa using

Goal state after:
ι : 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
p q : MvPolynomial ι' R
⊢ (aeval (x ∘ f)) p = (aeval (x ∘ f)) q → p = q
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:
simpa using

Goal state after:
ι : 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
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
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
x : (Polynomial.map ιFE g).SplittingField
hx : x ∈ (Polynomial.map ιEE' h).roots
⊢ x = ιEE' β

Tactic:
mem_roots_map h_ne_zero

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 • β
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
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
x : (Polynomial.map ιFE g).SplittingField
hx : eval₂ ιEE' x h = 0
⊢ x = ιEE' β
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B₁ B₂ : Set α
e : α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
hxB₁ : e ∈ B₁
hxB₂ : e ∉ B₂
⊢ ∃ y, (y ∈ B₂ ∧ y ∉ B₁) ∧ M.IsBase (insert y (B₁ \ {e}))

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
e : α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
hxB₁ : e ∈ B₁
hxB₂ : e ∉ B₂
⊢ ∃ y, (y ∈ B₂ ∧ y ∉ B₁) ∧ M.IsBase (insert y (B₁ \ {e}))
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hfB : f ∈ B'
h : B \ B' = {e}
hx : B' \ B = {f}
⊢ M.IsBase (B' \ B ∪ B ⊓ B')

Tactic:
inf_eq_inter,

Goal state after:
case inr
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hfB : f ∈ B'
h : B \ B' = {e}
hx : B' \ B = {f}
⊢ M.IsBase (B' \ B ∪ B ∩ B')
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.IsBase (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ M.IsBase (insert f I)

Tactic:
simpa using

Goal state after:
case inr
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.IsBase (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ M.IsBase (insert f I)
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hf : f ∈ B' \ (B \ {e})
hfB : M.Indep (insert f (B \ {e}))
⊢ f ∈ B' \ B

Tactic:
simpa using

Goal state after:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hf : f ∈ B' \ (B \ {e})
hfB : M.Indep (insert f (B \ {e}))
⊢ f ∈ B' ∧ f ∉ B
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
x : α
hxB : x ∈ B \ insert f (B \ {e})
hind : M.Indep (insert x (insert f (B \ {e})))
⊢ ?m.264 ∧ x = e

Tactic:
simpa using

Goal state after:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hfB : M.Indep (insert f (B \ {e}))
hf : f ∈ B' \ B
hnot : ¬Maximal M.Indep (insert f (B \ {e}))
x : α
hxB : x ∈ B \ insert f (B \ {e})
hind : M.Indep (insert x (insert f (B \ {e})))
⊢ ?m.264 ∧ x = e
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h✝ : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
⊢ R ∙ ↑(e 1) * ↑(e' 1) = 1

Tactic:
simpa using

Goal state after:
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h✝ : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
⊢ R ∙ ↑(e 1) * ↑(e' 1) = 1
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
x✝¹ : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) Is
x✝ : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : α → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun x ↦ x ∈ J) j → f x ⊆ f j → f j ⊆ f x
y : α
hyJ : y ∈ J
⊢ y ∈ f x

Tactic:
obtain (hle | hle) := hchain.total (hf _ hxJ).1 (hf _ hyJ).1

Goal state after:
case inl
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
x✝¹ : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) Is
x✝ : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : α → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun x ↦ x ∈ J) j → f x ⊆ f j → f j ⊆ f x
y : α
hyJ : y ∈ J
hle : f x ⊆ f y
⊢ y ∈ f x

case inr
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
x✝¹ : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) Is
x✝ : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : α → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun x ↦ x ∈ J) j → f x ⊆ f j → f j ⊆ f x
y : α
hyJ : y ∈ J
hle : f y ⊆ f x
⊢ y ∈ f x
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h✝ : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
⊢ R ∙ ↑(e' 1) * ↑(e 1) = 1

Tactic:
simpa using

Goal state after:
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h✝ : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
⊢ R ∙ ↑(e' 1) * ↑(e 1) = 1
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Finite F
α : ↥K
h : F⟮α⟯ = ⊤
⊢ F⟮↑α⟯ = K

Tactic:
simpa using

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Finite F
α : ↥K
h : F⟮α⟯ = ⊤
⊢ F⟮↑α⟯ = K
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
h : ∃ α, F⟮α⟯ = ⊤
⊢ FiniteDimensional F E

Tactic:
obtain ⟨α, hprim⟩ := h

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
α : E
hprim : F⟮α⟯ = ⊤
⊢ FiniteDimensional F E
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
h : ∃ α, F⟮α⟯ = ⊤
this : FiniteDimensional F E
⊢ Finite (IntermediateField F E)

Tactic:
obtain ⟨α, hprim⟩ := h

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
⊢ Finite (IntermediateField F E)
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x : Aˣ
x✝¹ x✝ : R
eq : (LinearMap.toSpanSingleton R A ↑x) x✝¹ = (LinearMap.toSpanSingleton R A ↑x) x✝
⊢ (fun r ↦ r • 1) x✝¹ = (fun r ↦ r • 1) x✝

Tactic:
simpa using

Goal state after:
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x : Aˣ
x✝¹ x✝ : R
eq : (LinearMap.toSpanSingleton R A ↑x) x✝¹ = (LinearMap.toSpanSingleton R A ↑x) x✝
⊢ x✝¹ • 1 = x✝ • 1
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
g : IntermediateField F E → G := fun K ↦ ⟨Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α), ⋯⟩
K K' : IntermediateField F E
heq :
  adjoin F ↑(Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)).coeffs =
    adjoin F ↑(Polynomial.map (algebraMap (↥K') E) (minpoly (↥K') α)).coeffs
⊢ K = K'

Tactic:
simpa using

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : F⟮α⟯ = ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
g : IntermediateField F E → G := fun K ↦ ⟨Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α), ⋯⟩
K K' : IntermediateField F E
heq :
  adjoin F ↑(Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)).coeffs =
    adjoin F ↑(Polynomial.map (algebraMap (↥K') E) (minpoly (↥K') α)).coeffs
⊢ K = K'
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
A : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
⊢ Function.Injective ⇑(toAlgebra e)

Tactic:
simpa using

Goal state after:
R : Type u
M : Type v
A : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
⊢ Function.Injective ⇑(LinearMap.rTensor M (Algebra.ofId R A).toLinearMap)
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_3
E : Type u_4
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
inst✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits
α : E
φ : E →ₐ[F] A
⊢ F⟮α⟯ = ⊤ ↔ ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ

Tactic:
by
  refine ⟨fun h ψ hψ ↦ (Field.primitive_element_iff_algHom_eq_of_eval' F A hA α).mp h hψ,
    fun h ↦ eq_of_le_of_finrank_eq' le_top ?_⟩
  let : Algebra F⟮α⟯ A := (φ.comp F⟮α⟯.val).toAlgebra
  rw [IntermediateField.finrank_top, ← AlgHom.card_of_splits _ _ A, Fintype.card_eq_one_iff]
  · exact ⟨{ __ := φ, commutes' := fun _ ↦ rfl }, fun ψ ↦ AlgHom.restrictScalars_injective F <|
      Eq.symm <| h _ (ψ.commutes <| AdjoinSimple.gen F α).symm⟩
  · exact fun x ↦ (IsIntegral.of_finite F x).minpoly_splits_tower_top (hA x)

Goal state after: