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
Q : ℕ → Prop :=
  fun i => Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
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) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
let Q : ℕ → Prop :=
  fun i => Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) }
    = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
case refine_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
Q : ℕ → Prop :=
  fun i => Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ Q j

case refine_2
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
Q : ℕ → Prop :=
  fun i => Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Q e
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
Q : ℕ → Prop :=
  fun i => Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
refine @Nat.decreasingInduction' Q i e (fun j lt_e _le_j ih => ?_) hi ?_
case refine_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
Q : ℕ → Prop :=
  fun i => Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ j) } = (e - j) • Module.rank (R ⧸ p) (S ⧸ P)
case refine_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
Q : ℕ → Prop :=
  fun i => Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ Q j
dsimp only
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
Q : ℕ → Prop :=
  fun i => Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ P ≠ ⊥
case refine_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
Q : ℕ → Prop :=
  fun i => Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ j) } = (e - j) • Module.rank (R ⧸ p) (S ⧸ P)
rw [rank_pow_quot_aux f p P _ lt_e, ih, ← succ_nsmul, Nat.sub_succ, ← Nat.succ_eq_add_one,
  Nat.succ_pred_eq_of_pos (Nat.sub_pos_of_lt lt_e)]
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
Q : ℕ → Prop :=
  fun i => Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ P ≠ ⊥
assumption
case refine_2
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
Q : ℕ → Prop :=
  fun i => Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ e) } = (e - e) • Module.rank (R ⧸ p) (S ⧸ P)
case refine_2
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
Q : ℕ → Prop :=
  fun i => Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Q e
dsimp only
case refine_2
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
Q : ℕ → Prop :=
  fun i => Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) { x // x ∈ ⊥ } = 0
case refine_2
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
Q : ℕ → Prop :=
  fun i => Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ e) } = (e - e) • Module.rank (R ⧸ p) (S ⧸ P)
rw [Nat.sub_self, zero_nsmul, map_quotient_self]
no goals
case refine_2
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
Q : ℕ → Prop :=
  fun i => Module.rank (R ⧸ p) { x // x ∈ map (Quotient.mk (P ^ e)) (P ^ i) } = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) { x // x ∈ ⊥ } = 0
exact rank_bot (R ⧸ p) (S ⧸ P ^ e)