-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem primesOver_finite : (primesOver p B).Finite

Proof state:
case pos
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpm : ⊥.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
hpb : p = ⊥
⊢ (⊥.primesOver B).Finite

Tactic:
haveI : IsDomain A := IsDomain.of_bot_isPrime A

Result:
case pos
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpm : ⊥.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
hpb : p = ⊥
this : IsDomain A
⊢ (⊥.primesOver B).Finite

Proof state:
case neg
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
hpb : ¬p = ⊥
⊢ (p.primesOver B).Finite

Tactic:
rw [← coe_primesOverFinset hpb B]

Result:
case neg
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
hpb : ¬p = ⊥
⊢ (↑(primesOverFinset p B)).Finite

Proof state:
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
⊢ (p.primesOver B).Finite

Tactic:
by_cases hpb : p = ⊥

Result:
case pos
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
hpb : p = ⊥
⊢ (p.primesOver B).Finite

case neg
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
hpb : ¬p = ⊥
⊢ (p.primesOver B).Finite

Proof state:
case neg
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
hpb : ¬p = ⊥
⊢ (↑(primesOverFinset p B)).Finite

Tactic:
exact (primesOverFinset p B).finite_toSet

Result:
no goals

Proof state:
case pos
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpm : ⊥.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
hpb : p = ⊥
this : IsDomain A
⊢ {⊥}.Finite

Tactic:
exact Set.finite_singleton ⊥

Result:
no goals

Proof state:
case pos
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
hpb : p = ⊥
⊢ (p.primesOver B).Finite

Tactic:
rw [hpb] at hpm ⊢

Result:
case pos
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpm : ⊥.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
hpb : p = ⊥
⊢ (⊥.primesOver B).Finite

Proof state:
case pos
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpm : ⊥.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
hpb : p = ⊥
this : IsDomain A
⊢ (⊥.primesOver B).Finite

Tactic:
rw [primesOver_bot A B]

Result:
case pos
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpm : ⊥.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
hpb : p = ⊥
this : IsDomain A
⊢ {⊥}.Finite