R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
hP0 : P ≠ ⊥
i : ℕ
hi : i < e
this : Field (R ⧸ p) := Quotient.field p
⊢ Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } =
    Module.rank (R ⧸ p) (S ⧸ P) + Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1)) }
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
hP0 : P ≠ ⊥
i : ℕ
hi : i < e
⊢ Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } =
    Module.rank (R ⧸ p) (S ⧸ P) + Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1)) }
letI : Field (R ⧸ p) := Ideal.Quotient.field _
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
hP0 : P ≠ ⊥
i : ℕ
hi : i < e
this : Field (R ⧸ p) := Quotient.field p
⊢ Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } =
    Module.rank (R ⧸ p)
        ({ x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } ⧸ LinearMap.range (powQuotSuccInclusion f p P i)) +
      Module.rank (R ⧸ p) { x // x ∈ LinearMap.range (powQuotSuccInclusion f p P i) }
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
hP0 : P ≠ ⊥
i : ℕ
hi : i < e
this : Field (R ⧸ p) := Quotient.field p
⊢ Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } =
    Module.rank (R ⧸ p) (S ⧸ P) + Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ (i + 1)) }
rw [rank_eq_of_injective _ (powQuotSuccInclusion_injective f p P i),
  (quotientRangePowQuotSuccInclusionEquiv f p P hP0 hi).symm.rank_eq]
no goals
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝³ : IsDomain S
inst✝² : IsDedekindDomain S
inst✝¹ : IsMaximal p
inst✝ : IsPrime P
hP0 : P ≠ ⊥
i : ℕ
hi : i < e
this : Field (R ⧸ p) := Quotient.field p
⊢ Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } =
    Module.rank (R ⧸ p)
        ({ x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } ⧸ LinearMap.range (powQuotSuccInclusion f p P i)) +
      Module.rank (R ⧸ p) { x // x ∈ LinearMap.range (powQuotSuccInclusion f p P i) }
exact (rank_quotient_add_rank (LinearMap.range (powQuotSuccInclusion f p P i))).symm