-- Mathlib/FieldTheory/PolynomialGaloisGroup.lean
theorem mapRoots_bijective [h : Fact (p.Splits (algebraMap F E))] :
    Function.Bijective (mapRoots p E)

Proof state:
case right.intro.intro
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(p.rootSet E)
key :
  (map (algebraMap F E) p).roots =
    Multiset.map (⇑↑(IsScalarTower.toAlgHom F p.SplittingField E)) (map (algebraMap F p.SplittingField) p).roots
x : p.SplittingField
hx1 : x ∈ (map (algebraMap F p.SplittingField) p).roots
hx2 : ↑(IsScalarTower.toAlgHom F p.SplittingField E) x = ↑y
⊢ ∃ a, mapRoots p E a = y

Tactic:
exact ⟨⟨x, (@Multiset.mem_toFinset _ (Classical.decEq _) _ _).mpr hx1⟩, Subtype.ext hx2⟩

Result:
no goals

Proof state:
case right
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(p.rootSet E)
key :
  (map (↑(IsScalarTower.toAlgHom F p.SplittingField E)) (map (algebraMap F p.SplittingField) p)).roots =
    Multiset.map (⇑↑(IsScalarTower.toAlgHom F p.SplittingField E)) (map (algebraMap F p.SplittingField) p).roots
⊢ ∃ a, mapRoots p E a = y

Tactic:
rw [map_map, AlgHom.comp_algebraMap] at key

Result:
case right
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(p.rootSet E)
key :
  (map (algebraMap F E) p).roots =
    Multiset.map (⇑↑(IsScalarTower.toAlgHom F p.SplittingField E)) (map (algebraMap F p.SplittingField) p).roots
⊢ ∃ a, mapRoots p E a = y

Proof state:
case right
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(p.rootSet E)
key :
  (map (algebraMap F E) p).roots =
    Multiset.map (⇑↑(IsScalarTower.toAlgHom F p.SplittingField E)) (map (algebraMap F p.SplittingField) p).roots
hy : ∃ a ∈ (map (algebraMap F p.SplittingField) p).roots, ↑(IsScalarTower.toAlgHom F p.SplittingField E) a = ↑y
⊢ ∃ a, mapRoots p E a = y

Tactic:
rcases hy with ⟨x, hx1, hx2⟩

Result:
case right.intro.intro
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(p.rootSet E)
key :
  (map (algebraMap F E) p).roots =
    Multiset.map (⇑↑(IsScalarTower.toAlgHom F p.SplittingField E)) (map (algebraMap F p.SplittingField) p).roots
x : p.SplittingField
hx1 : x ∈ (map (algebraMap F p.SplittingField) p).roots
hx2 : ↑(IsScalarTower.toAlgHom F p.SplittingField E) x = ↑y
⊢ ∃ a, mapRoots p E a = y

Proof state:
case left
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
⊢ Function.Injective (mapRoots p E)

Tactic:
exact fun _ _ h => Subtype.ext (RingHom.injective _ (Subtype.ext_iff.mp h))

Result:
no goals

Proof state:
case right
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(p.rootSet E)
key :
  (map (algebraMap F E) p).roots =
    Multiset.map (⇑↑(IsScalarTower.toAlgHom F p.SplittingField E)) (map (algebraMap F p.SplittingField) p).roots
hy : ↑y ∈ p.rootSet E
⊢ ∃ a, mapRoots p E a = y

Tactic:
simp only [rootSet, Finset.mem_coe, Multiset.mem_toFinset, key, Multiset.mem_map] at hy

Result:
case right
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(p.rootSet E)
key :
  (map (algebraMap F E) p).roots =
    Multiset.map (⇑↑(IsScalarTower.toAlgHom F p.SplittingField E)) (map (algebraMap F p.SplittingField) p).roots
hy : ∃ a ∈ (map (algebraMap F p.SplittingField) p).roots, ↑(IsScalarTower.toAlgHom F p.SplittingField E) a = ↑y
⊢ ∃ a, mapRoots p E a = y

Proof state:
case right
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(p.rootSet E)
key :
  (map (algebraMap F E) p).roots =
    Multiset.map (⇑↑(IsScalarTower.toAlgHom F p.SplittingField E)) (map (algebraMap F p.SplittingField) p).roots
⊢ ∃ a, mapRoots p E a = y

Tactic:
have hy := Subtype.mem y

Result:
case right
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(p.rootSet E)
key :
  (map (algebraMap F E) p).roots =
    Multiset.map (⇑↑(IsScalarTower.toAlgHom F p.SplittingField E)) (map (algebraMap F p.SplittingField) p).roots
hy : ↑y ∈ p.rootSet E
⊢ ∃ a, mapRoots p E a = y

Proof state:
case right
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
⊢ Function.Surjective (mapRoots p E)

Tactic:
intro y

Result:
case right
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(p.rootSet E)
⊢ ∃ a, mapRoots p E a = y

Proof state:
case right
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(p.rootSet E)
⊢ ∃ a, mapRoots p E a = y

Tactic:
have key :=
  roots_map (IsScalarTower.toAlgHom F p.SplittingField E : p.SplittingField →+* E)
    ((splits_id_iff_splits _).mpr (IsSplittingField.splits p.SplittingField p))

Result:
case right
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
y : ↑(p.rootSet E)
key :
  (map (↑(IsScalarTower.toAlgHom F p.SplittingField E)) (map (algebraMap F p.SplittingField) p)).roots =
    Multiset.map (⇑↑(IsScalarTower.toAlgHom F p.SplittingField E)) (map (algebraMap F p.SplittingField) p).roots
⊢ ∃ a, mapRoots p E a = y

Proof state:
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
⊢ Function.Bijective (mapRoots p E)

Tactic:
constructor

Result:
case left
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
⊢ Function.Injective (mapRoots p E)

case right
F : Type u_1
inst✝² : Field F
p : F[X]
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : Fact (Splits (algebraMap F E) p)
⊢ Function.Surjective (mapRoots p E)