-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this_3 : IsDedekindDomain S := ⋯
s : Finset L
b_1 : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b_1 : (a : ↥s) → L) x : L)
this :
  LinearIndependent.{u_4, u_1, u_4} (ι := ↥s) R (M := L)
    (⇑(LinearMap.BilinForm.dualBasis.{u_4, u_3, u_4} (V := L) (K := K) (ι := ↥s) (Algebra.traceForm K L) ⋯ b_1 :
          Basis (↥s) K L) :
      (a : ↥s) → L)
n : ℕ
b :
  Basis.{0, u_1, u_4} (Fin n) R
    ↥(LinearMap.range
        ((↑R :
            {S M : Type u_2} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_18 : Semiring S] →
                    [inst_19 : AddCommMonoid M] →
                      [inst_20 : AddCommMonoid M₂] →
                        [inst_21 : Module R M] →
                          [inst_22 : Module R M₂] →
                            [inst_23 : Module S M] →
                              [inst_24 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Algebra.linearMap S L)))
rw : HasQuotient.Quotient S (B := Submodule R S) ⊥ ≃ₗ[R] S
⊢ HasQuotient.Quotient S (B := Submodule R S)
      (LinearMap.ker
        ((↑R :
            {S M : Type u_2} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_18 : Semiring S] →
                    [inst_19 : AddCommMonoid M] →
                      [inst_20 : AddCommMonoid M₂] →
                        [inst_21 : Module R M] →
                          [inst_22 : Module R M₂] →
                            [inst_23 : Module S M] →
                              [inst_24 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Algebra.linearMap S L))) ≃ₗ[R]
    S
have rw₁ : Function.Injective.{u_2 + 1, u_4 + 1} (α := S) (β := L)
  (⇑((↑R :
          {S M : Type u_2} →
            {M₂ : Type u_4} →
              [inst : Semiring R] →
                [inst_18 : Semiring S] →
                  [inst_19 : AddCommMonoid M] →
                    [inst_20 : AddCommMonoid M₂] →
                      [inst_21 : Module R M] →
                        [inst_22 : Module R M₂] →
                          [inst_23 : Module S M] →
                            [inst_24 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (Algebra.linearMap S L)) :
    (a : S) → L)
Tactic: rw [LinearMap.ker_eq_bot.mpr]