-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem finrank_prime_pow_ramificationIdx [IsDedekindDomain S] (hP0 : P ≠ ⊥)
    [p.IsMaximal] [P.IsPrime] (he : e ≠ 0) :
    finrank (R ⧸ p) (S ⧸ P ^ e) =
      e *
        @finrank (R ⧸ p) (S ⧸ P) _ _
          (@Algebra.toModule _ _ _ _ <|
            @Quotient.algebraQuotientOfRamificationIdxNeZero _ _ _ _ _ _ _ ⟨he⟩)

Proof state:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this : NeZero e := { out := he }
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Tactic:
letI : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P

Result:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Proof state:
case neg
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : ¬FiniteDimensional (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Tactic:
have hPe := mt (finiteDimensional_iff_of_rank_eq_nsmul he hdim).mp hP

Result:
case neg
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : ¬FiniteDimensional (R ⧸ p) (S ⧸ P)
hPe : ¬FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Proof state:
case pos
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝² : NeZero e := { out := he }
this✝¹ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP this✝ : FiniteDimensional (R ⧸ p) (S ⧸ P)
this : FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Tactic:
apply @Nat.cast_injective Cardinal

Result:
case pos.a
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝² : NeZero e := { out := he }
this✝¹ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP this✝ : FiniteDimensional (R ⧸ p) (S ⧸ P)
this : FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ ↑(finrank (R ⧸ p) (S ⧸ P ^ e)) = ↑(e * finrank (R ⧸ p) (S ⧸ P))

Proof state:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Tactic:
by_cases hP : FiniteDimensional (R ⧸ p) (S ⧸ P)

Result:
case pos
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

case neg
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : ¬FiniteDimensional (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Proof state:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Tactic:
letI : NeZero e := ⟨he⟩

Result:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this : NeZero e := { out := he }
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Proof state:
case pos
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Tactic:
haveI := hP

Result:
case pos
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP this : FiniteDimensional (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Proof state:
case pos.a
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝² : NeZero e := { out := he }
this✝¹ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP this✝ : FiniteDimensional (R ⧸ p) (S ⧸ P)
this : FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ ↑(finrank (R ⧸ p) (S ⧸ P ^ e)) = ↑(e * finrank (R ⧸ p) (S ⧸ P))

Tactic:
rw [finrank_eq_rank', Nat.cast_mul, finrank_eq_rank', hdim, nsmul_eq_mul]

Result:
no goals