-- Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
L : Type u_3
inst_4 : Field L
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra C L
inst_10 : IsIntegralClosure C A L
inst_11 : Algebra A C
inst_12 : IsScalarTower A C L
inst_13 : FiniteDimensional K L
inst_14 : IsDomain A
inst_15 : Algebra.IsSeparable K L
inst_16 : IsIntegrallyClosed A
inst_17 : IsNoetherianRing A
this_1 : DecidableEq L
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral A (A := L) ((b : (a : ↥s) → L) x : L)
b' : Basis (↥s) K L := LinearMap.BilinForm.dualBasis.{u_3, u_2, u_3} (V := L) (K := K) (ι := ↥s) (traceForm K L) ⋯ b
this : IsNoetherian.{u_1, u_3} A ↥(Submodule.span A (Set.range (ι := ↥s) (⇑b' : (a : ↥s) → L))) := ⋯
f : LinearMap.{u_1, u_1, u_4, u_3} (RingHom.id A) C ↥(Submodule.span A (Set.range (ι := ↥s) (⇑b' : (a : ↥s) → L))) :=
  (Submodule.inclusion ⋯ :
      ↥(LinearMap.range
            ((↑A :
                {S M : Type u_4} →
                  {M₂ : Type u_3} →
                    [inst : Semiring A] →
                      [inst_18 : Semiring S] →
                        [inst_19 : AddCommMonoid M] →
                          [inst_20 : AddCommMonoid M₂] →
                            [inst_21 : Module A M] →
                              [inst_22 : Module A M₂] →
                                [inst_23 : Module S M] →
                                  [inst_24 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
              (Algebra.linearMap C L))) →ₗ[A]
        ↥(Submodule.span A
            (Set.range (ι := ↥s)
              (⇑(LinearMap.BilinForm.dualBasis.{u_3, u_2, u_3} (V := L) (K := K) (ι := ↥s) (traceForm K L) ⋯ b :
                    Basis (↥s) K L) :
                (a : ↥s) → L)))) ∘ₗ
    (LinearMap.rangeRestrict
        ((↑A :
            {S M : Type u_4} →
              {M₂ : Type u_3} →
                [inst : Semiring A] →
                  [inst_18 : Semiring S] →
                    [inst_19 : AddCommMonoid M] →
                      [inst_20 : AddCommMonoid M₂] →
                        [inst_21 : Module A M] →
                          [inst_22 : Module A M₂] →
                            [inst_23 : Module S M] →
                              [inst_24 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
          (Algebra.linearMap C L)) :
      LinearMap.{u_1, u_1, u_4, u_3} (RingHom.id A) C
        ↥(LinearMap.range
            ((↑A :
                {S M : Type u_4} →
                  {M₂ : Type u_3} →
                    [inst : Semiring A] →
                      [inst_18 : Semiring S] →
                        [inst_19 : AddCommMonoid M] →
                          [inst_20 : AddCommMonoid M₂] →
                            [inst_21 : Module A M] →
                              [inst_22 : Module A M₂] →
                                [inst_23 : Module S M] →
                                  [inst_24 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
              (Algebra.linearMap C L))))
⊢ Eq (α := Submodule A C)
    (LinearMap.ker
      ((↑A :
          {S M : Type u_4} →
            {M₂ : Type u_3} →
              [inst : Semiring A] →
                [inst_18 : Semiring S] →
                  [inst_19 : AddCommMonoid M] →
                    [inst_20 : AddCommMonoid M₂] →
                      [inst_21 : Module A M] →
                        [inst_22 : Module A M₂] →
                          [inst_23 : Module S M] →
                            [inst_24 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
        (Algebra.linearMap C L)))
    ⊥

Tactic:
LinearMap.ker_eq_bot_of_injective (IsIntegralClosure.algebraMap_injective C A L)

Premises used: IsIntegralClosure.algebraMap_injective, LinearMap.ker_eq_bot_of_injective