Theorem: basisQuotientOfLocalRing_apply (FltRegular/NumberTheory/QuotientTrace.lean)

State before:
R : Type u_3
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : LocalRing R
inst✝⁴ : Module.Free R S
inst✝³ : Module.Finite R S
p : Ideal R
inst✝² : p.IsMaximal
inst✝¹ : LocalRing R
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
i : ι
⊢ (basisQuotientOfLocalRing b) i = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b i)
Tactic:
delta basisQuotientOfLocalRing
State after:
R : Type u_3
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : LocalRing R
inst✝⁴ : Module.Free R S
inst✝³ : Module.Finite R S
p : Ideal R
inst✝² : p.IsMaximal
inst✝¹ : LocalRing R
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
i : ι
⊢ (basisOfTopLeSpanOfCardEqFinrank (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) ∘ ⇑b) ⋯ ⋯) i =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b i)

State before:
R : Type u_3
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : LocalRing R
inst✝⁴ : Module.Free R S
inst✝³ : Module.Finite R S
p : Ideal R
inst✝² : p.IsMaximal
inst✝¹ : LocalRing R
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
i : ι
⊢ (basisOfTopLeSpanOfCardEqFinrank (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) ∘ ⇑b) ⋯ ⋯) i =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b i)
Tactic:
rw [coe_basisOfTopLeSpanOfCardEqFinrank, Function.comp_apply]
State after:
no goals