-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
hRK : IsFractionRing R K
inst_8 : IsDomain S
inst_9 : IsDedekindDomain R
inst_10 : Algebra K L
inst_11 : Algebra R L
inst_12 : IsScalarTower R K L
inst_13 : IsScalarTower R S L
hp : p.IsMaximal
inst_14 : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
b : Basis.{v, u, v} ι (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) :=
  Free.chooseBasis (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
b' : ι → S :=
  fun (i : ι) ↦
    Exists.choose (p := fun (a : S) ↦
      Eq (α := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((Quotient.mk (map (F := R →+* S) f p) : (a : S) → S ⧸ map f p) a :
          HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p))
        ((b : (a : ι) → S ⧸ map f p) i : HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)))
      ⋯
b_eq_b' :
  Eq (α := (a : ι) → HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)) (⇑b : (a : ι) → S ⧸ map f p)
    ((⇑((↑R :
              {S M M₂ : Type v} →
                [inst : Semiring R] →
                  [inst_15 : Semiring S] →
                    [inst_16 : AddCommMonoid M] →
                      [inst_17 : AddCommMonoid M₂] →
                        [inst_18 : Module R M] →
                          [inst_19 : Module R M₂] →
                            [inst_20 : Module S M] →
                              [inst_21 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (Submodule.mkQ (map (F := R →+* S) f p))) :
        (a : S) → S ⧸ map f p) ∘
      b')
b'' : ι → L := (⇑(algebraMap S L) : (a : S) → L) ∘ b'
b''_li : LinearIndependent K b''
x : S
h : Membership.mem (γ := Submodule R S) ⊤ x
mem_span_b :
  Membership.mem (α := HasQuotient.Quotient S (B := Submodule S S) (map (F := R →+* S) f p)) (γ :=
    Submodule R (HasQuotient.Quotient S (B := Submodule S S) (map (F := R →+* S) f p)))
    (Submodule.map
      ((↑R :
          {S M M₂ : Type v} →
            [inst : Semiring R] →
              [inst_15 : Semiring S] →
                [inst_16 : AddCommMonoid M] →
                  [inst_17 : AddCommMonoid M₂] →
                    [inst_18 : Module R M] →
                      [inst_19 : Module R M₂] →
                        [inst_20 : Module S M] →
                          [inst_21 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (Submodule.mkQ (map (F := R →+* S) f p)))
      (Submodule.span R (Set.range b')))
    ((Submodule.mkQ (map (F := R →+* S) f p) : (a : S) → S ⧸ map f p) x :
      HasQuotient.Quotient S (B := Submodule S S) (map (F := R →+* S) f p))
y : S
y_mem : Membership.mem (γ := Submodule R S) (Submodule.span R (Set.range b')) y
y_eq :
  Eq (α := HasQuotient.Quotient S (B := Submodule S S) (map (F := R →+* S) f p))
    (((↑R :
              {S M M₂ : Type v} →
                [inst : Semiring R] →
                  [inst_15 : Semiring S] →
                    [inst_16 : AddCommMonoid M] →
                      [inst_17 : AddCommMonoid M₂] →
                        [inst_18 : Module R M] →
                          [inst_19 : Module R M₂] →
                            [inst_20 : Module S M] →
                              [inst_21 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (Submodule.mkQ (map (F := R →+* S) f p)) :
          (a : S) → S ⧸ map f p)
        y :
      HasQuotient.Quotient S (B := Submodule S S) (map (F := R →+* S) f p))
    ((Submodule.mkQ (map (F := R →+* S) f p) : (a : S) → S ⧸ map f p) x :
      HasQuotient.Quotient S (B := Submodule S S) (map (F := R →+* S) f p))
⊢ Membership.mem (γ := Submodule S S) (map (F := R →+* S) f p) (y - x)

Tactic:
rw [LinearMap.restrictScalars_apply, Submodule.mkQ_apply, Submodule.mkQ_apply,
        Submodule.Quotient.eq] at y_eq

Premises used: Submodule.Quotient.eq, LinearMap.restrictScalars_apply, Submodule.mkQ_apply