-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem finrank_quotient_map [IsDomain S] [IsDedekindDomain R] [Algebra K L]
    [Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L]
    [hp : p.IsMaximal] [Module.Finite R S] :
    finrank (R ⧸ p) (S ⧸ map (algebraMap R S) p) = finrank K L

Proof state:
case refine_2.refine_1
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
p : Ideal R
inst✝¹² : Algebra R S
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map (algebraMap R S) p)
b : Basis ι (R ⧸ p) (S ⧸ map (algebraMap R S) p) := Free.chooseBasis (R ⧸ p) (S ⧸ map (algebraMap R S) p)
b' : ι → S := fun i => ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map (algebraMap R S) p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
x : S
a✝ : x ∈ ⊤
mem_span_b : (Submodule.mkQ (map (algebraMap R S) p)) x ∈ Submodule.span (R ⧸ p) (Set.range ⇑b)
⊢ x ∈ Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map (algebraMap R S) 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

Result:
case refine_2.refine_1
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
p : Ideal R
inst✝¹² : Algebra R S
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map (algebraMap R S) p)
b : Basis ι (R ⧸ p) (S ⧸ map (algebraMap R S) p) := Free.chooseBasis (R ⧸ p) (S ⧸ map (algebraMap R S) p)
b' : ι → S := fun i => ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map (algebraMap R S) p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
x : S
a✝ : x ∈ ⊤
mem_span_b :
  (Submodule.mkQ (map (algebraMap R S) p)) x ∈
    Submodule.map (↑R (Submodule.mkQ (map (algebraMap R S) p))) (Submodule.span R (Set.range b'))
⊢ x ∈ Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map (algebraMap R S) p)

Proof state:
case refine_2.refine_1.intro.intro
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
p : Ideal R
inst✝¹² : Algebra R S
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map (algebraMap R S) p)
b : Basis ι (R ⧸ p) (S ⧸ map (algebraMap R S) p) := Free.chooseBasis (R ⧸ p) (S ⧸ map (algebraMap R S) p)
b' : ι → S := fun i => ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map (algebraMap R S) p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
x : S
a✝ : x ∈ ⊤
mem_span_b :
  (Submodule.mkQ (map (algebraMap R S) p)) x ∈
    Submodule.map (↑R (Submodule.mkQ (map (algebraMap R S) p))) (Submodule.span R (Set.range b'))
y : S
y_mem : y ∈ Submodule.span R (Set.range b')
y_eq : (↑R (Submodule.mkQ (map (algebraMap R S) p))) y = (Submodule.mkQ (map (algebraMap R S) p)) x
⊢ x ∈ Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map (algebraMap R S) p)

Tactic:
suffices y + -(y - x) ∈ _ by simpa

Result:
case refine_2.refine_1.intro.intro
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
p : Ideal R
inst✝¹² : Algebra R S
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map (algebraMap R S) p)
b : Basis ι (R ⧸ p) (S ⧸ map (algebraMap R S) p) := Free.chooseBasis (R ⧸ p) (S ⧸ map (algebraMap R S) p)
b' : ι → S := fun i => ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map (algebraMap R S) p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
x : S
a✝ : x ∈ ⊤
mem_span_b :
  (Submodule.mkQ (map (algebraMap R S) p)) x ∈
    Submodule.map (↑R (Submodule.mkQ (map (algebraMap R S) p))) (Submodule.span R (Set.range b'))
y : S
y_mem : y ∈ Submodule.span R (Set.range b')
y_eq : (↑R (Submodule.mkQ (map (algebraMap R S) p))) y = (Submodule.mkQ (map (algebraMap R S) p)) x
⊢ y + -(y - x) ∈ Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map (algebraMap R S) p)

Proof state:
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
p : Ideal R
inst✝¹² : Algebra R S
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map (algebraMap R S) p)
b : Basis ι (R ⧸ p) (S ⧸ map (algebraMap R S) p) := Free.chooseBasis (R ⧸ p) (S ⧸ map (algebraMap R S) p)
b' : ι → S := fun i => ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map (algebraMap R S) p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
x : S
a✝ : x ∈ ⊤
mem_span_b :
  (Submodule.mkQ (map (algebraMap R S) p)) x ∈
    Submodule.map (↑R (Submodule.mkQ (map (algebraMap R S) p))) (Submodule.span R (Set.range b'))
y : S
y_mem : y ∈ Submodule.span R (Set.range b')
y_eq : (↑R (Submodule.mkQ (map (algebraMap R S) p))) y = (Submodule.mkQ (map (algebraMap R S) p)) x
this : y + -(y - x) ∈ ?m.255876
⊢ x ∈ Submodule.span R (Set.range b') ⊔ Submodule.restrictScalars R (map (algebraMap R S) p)

Tactic:
simpa

Result:
no goals