-- 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.{u, v} (R ⧸ p) (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) f p)))
    (Submodule.span (R ⧸ p) (Set.range (ι := ι) (⇑b : (a : ι) → S ⧸ map 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 (α := 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))

Tactic:
rw [← @Submodule.restrictScalars_mem R,
        Submodule.restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective, b_eq_b',
        Set.range_comp, ← Submodule.map_span] at mem_span_b

Premises used: Set.range_comp, Ideal.Quotient.mk_surjective, HasQuotient.Quotient, Submodule.restrictScalars_mem, Submodule.map_span, Submodule.restrictScalars_span