chore: golf IsSplittingField.algEquiv (#8142)

Also golfs `Normal.of_algEquiv` and `Algebra.IsIntegral.of_finite` and refactors `Algebra.IsAlgebraic.bijective_of_isScalarTower`.

Mathlib/FieldTheory/Normal.lean

@@ -110,24 +110,15 @@ theorem AlgHom.normal_bijective [h : Normal F E] (ϕ : E →ₐ[F] K) : Function
 -- Porting note: `[Field F] [Field E] [Algebra F E]` added by hand.
 variable {F E} {E' : Type*} [Field F] [Field E] [Algebra F E] [Field E'] [Algebra F E']
 
-theorem Normal.of_algEquiv [h : Normal F E] (f : E ≃ₐ[F] E') : Normal F E' :=
-  normal_iff.2 fun x => by
-    cases' h.out (f.symm x) with hx hhx
-    have H := map_isIntegral f.toAlgHom hx
-    simp [AlgEquiv.toAlgHom_eq_coe] at H
-    use H
-    apply Polynomial.splits_of_splits_of_dvd (algebraMap F E') (minpoly.ne_zero hx)
-    · rw [← AlgHom.comp_algebraMap f.toAlgHom]
-      exact Polynomial.splits_comp_of_splits (algebraMap F E) f.toAlgHom.toRingHom hhx
-    · apply minpoly.dvd _ _
-      rw [← AddEquiv.map_eq_zero_iff f.symm.toAddEquiv]
-      exact
-        Eq.trans (Polynomial.aeval_algHom_apply f.symm.toAlgHom x (minpoly F (f.symm x))).symm
-          (minpoly.aeval _ _)
+theorem Normal.of_algEquiv [h : Normal F E] (f : E ≃ₐ[F] E') : Normal F E' := by
+  rw [normal_iff] at h ⊢
+  intro x; specialize h (f.symm x)
+  rw [← f.apply_symm_apply x, minpoly.algEquiv_eq, ← f.toAlgHom.comp_algebraMap]
+  exact ⟨map_isIntegral f h.1, splits_comp_of_splits _ _ h.2⟩
 #align normal.of_alg_equiv Normal.of_algEquiv
 
 theorem AlgEquiv.transfer_normal (f : E ≃ₐ[F] E') : Normal F E ↔ Normal F E' :=
-  ⟨fun _ => Normal.of_algEquiv f, fun _ => Normal.of_algEquiv f.symm⟩
+  ⟨fun _ ↦ Normal.of_algEquiv f, fun _ ↦ Normal.of_algEquiv f.symm⟩
 #align alg_equiv.transfer_normal AlgEquiv.transfer_normal
 
 open IntermediateField

Mathlib/FieldTheory/SplittingField/Construction.lean

@@ -359,23 +359,10 @@ instance (f : K[X]) : NoZeroSMulDivisors K f.SplittingField :=
   inferInstance
 
 /-- Any splitting field is isomorphic to `SplittingFieldAux f`. -/
-def algEquiv (f : K[X]) [IsSplittingField K L f] : L ≃ₐ[K] SplittingField f := by
-  refine'
-    AlgEquiv.ofBijective (lift L f <| splits (SplittingField f) f)
-      ⟨RingHom.injective (lift L f <| splits (SplittingField f) f).toRingHom, _⟩
-  haveI := finiteDimensional (SplittingField f) f
-  haveI := finiteDimensional L f
-  have : FiniteDimensional.finrank K L = FiniteDimensional.finrank K (SplittingField f) :=
-    le_antisymm
-      (LinearMap.finrank_le_finrank_of_injective
-        (show Function.Injective (lift L f <| splits (SplittingField f) f).toLinearMap from
-          RingHom.injective (lift L f <| splits (SplittingField f) f : L →+* f.SplittingField)))
-      (LinearMap.finrank_le_finrank_of_injective
-        (show Function.Injective (lift (SplittingField f) f <| splits L f).toLinearMap from
-          RingHom.injective (lift (SplittingField f) f <| splits L f : f.SplittingField →+* L)))
-  change Function.Surjective (lift L f <| splits (SplittingField f) f).toLinearMap
-  refine' (LinearMap.injective_iff_surjective_of_finrank_eq_finrank this).1 _
-  exact RingHom.injective (lift L f <| splits (SplittingField f) f : L →+* f.SplittingField)
+def algEquiv (f : K[X]) [h : IsSplittingField K L f] : L ≃ₐ[K] SplittingField f :=
+  AlgEquiv.ofBijective (lift L f <| splits (SplittingField f) f) <|
+    have := finiteDimensional L f
+    ((Algebra.isAlgebraic_of_finite K L).algHom_bijective₂ _ <| lift _ f h.1).1
 #align polynomial.is_splitting_field.alg_equiv Polynomial.IsSplittingField.algEquiv
 
 end IsSplittingField

Mathlib/Logic/Function/Basic.lean

@@ -127,7 +127,7 @@ theorem Injective.of_comp {g : γ → α} (I : Injective (f ∘ g)) : Injective
 #align function.injective.of_comp Function.Injective.of_comp
 
 @[simp]
-theorem Injective.of_comp_iff {f : α → β} (hf : Injective f) (g : γ → α) :
+theorem Injective.of_comp_iff (hf : Injective f) (g : γ → α) :
     Injective (f ∘ g) ↔ Injective g :=
   ⟨Injective.of_comp, hf.comp⟩
 #align function.injective.of_comp_iff Function.Injective.of_comp_iff
@@ -138,6 +138,10 @@ theorem Injective.of_comp_right {g : γ → α} (I : Injective (f ∘ g)) (hg :
   obtain ⟨y, rfl⟩ := hg y
   exact congr_arg g (I h)
 
+theorem Surjective.bijective₂_of_injective {g : γ → α} (hf : Surjective f) (hg : Surjective g)
+    (I : Injective (f ∘ g)) : Bijective f ∧ Bijective g :=
+  ⟨⟨I.of_comp_right hg, hf⟩, I.of_comp, hg⟩
+
 @[simp]
 theorem Injective.of_comp_iff' (f : α → β) {g : γ → α} (hg : Bijective g) :
     Injective (f ∘ g) ↔ Injective f :=
@@ -182,6 +186,10 @@ theorem Surjective.of_comp_iff (f : α → β) {g : γ → α} (hg : Surjective
 theorem Surjective.of_comp_left {g : γ → α} (S : Surjective (f ∘ g)) (hf : Injective f) :
     Surjective g := fun a ↦ let ⟨c, hc⟩ := S (f a); ⟨c, hf hc⟩
 
+theorem Injective.bijective₂_of_surjective {g : γ → α} (hf : Injective f) (hg : Injective g)
+    (S : Surjective (f ∘ g)) : Bijective f ∧ Bijective g :=
+  ⟨⟨hf, S.of_comp⟩, hg, S.of_comp_left hf⟩
+
 @[simp]
 theorem Surjective.of_comp_iff' (hf : Bijective f) (g : γ → α) :
     Surjective (f ∘ g) ↔ Surjective g :=

Mathlib/RingTheory/Algebraic.lean

@@ -298,17 +298,20 @@ theorem Algebra.IsAlgebraic.algHom_bijective (ha : Algebra.IsAlgebraic K L) (f :
   exact ⟨a, Subtype.ext_iff.1 ha⟩
 #align algebra.is_algebraic.alg_hom_bijective Algebra.IsAlgebraic.algHom_bijective
 
+theorem Algebra.IsAlgebraic.algHom_bijective₂ [Field R] [Algebra K R]
+    (ha : Algebra.IsAlgebraic K L) (f : L →ₐ[K] R) (g : R →ₐ[K] L) :
+    Function.Bijective f ∧ Function.Bijective g :=
+  (g.injective.bijective₂_of_surjective f.injective (ha.algHom_bijective <| g.comp f).2).symm
+
 theorem Algebra.IsAlgebraic.bijective_of_isScalarTower (ha : Algebra.IsAlgebraic K L)
     [Field R] [Algebra K R] [Algebra L R] [IsScalarTower K L R] (f : R →ₐ[K] L) :
     Function.Bijective f :=
-  ⟨f.injective, Function.Surjective.of_comp <|
-    (ha.algHom_bijective <| f.comp <| IsScalarTower.toAlgHom K L R).2⟩
+  (ha.algHom_bijective₂ (IsScalarTower.toAlgHom K L R) f).2
 
 theorem Algebra.IsAlgebraic.bijective_of_isScalarTower' [Field R] [Algebra K R]
     (ha : Algebra.IsAlgebraic K R) [Algebra L R] [IsScalarTower K L R] (f : R →ₐ[K] L) :
     Function.Bijective f :=
-  ⟨f.injective, Function.Surjective.of_comp_left
-    (ha.algHom_bijective <| (IsScalarTower.toAlgHom K L R).comp f).2 (RingHom.injective _)⟩
+  (ha.algHom_bijective₂ f (IsScalarTower.toAlgHom K L R)).1
 
 theorem AlgHom.bijective [FiniteDimensional K L] (ϕ : L →ₐ[K] L) : Function.Bijective ϕ :=
   (Algebra.isAlgebraic_of_finite K L).algHom_bijective ϕ

Mathlib/RingTheory/IntegralClosure.lean

@@ -458,12 +458,8 @@ theorem Algebra.IsIntegral.finite (h : Algebra.IsIntegral R A) [h' : Algebra.Fin
   exact Algebra.smul_def _ _
 #align algebra.is_integral.finite Algebra.IsIntegral.finite
 
-theorem Algebra.IsIntegral.of_finite [h : Module.Finite R A] : Algebra.IsIntegral R A := by
-  apply RingHom.Finite.to_isIntegral
-  rw [RingHom.Finite]
-  convert h
-  ext
-  exact (Algebra.smul_def _ _).symm
+theorem Algebra.IsIntegral.of_finite [h : Module.Finite R A] : Algebra.IsIntegral R A :=
+  fun _ ↦ isIntegral_of_mem_of_FG ⊤ h.1 _ trivial
 #align algebra.is_integral.of_finite Algebra.IsIntegral.of_finite
 
 /-- finite = integral + finite type -/