-- Mathlib/RingTheory/LocalRing/Quotient.lean
theorem finrank_quotient_map :
    finrank (R ⧸ p) (S ⧸ pS) = finrank R S

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
⊢ finrank (R ⧸ p) (S ⧸ pS) ≤ finrank R S

Tactic:
let b := Module.Free.chooseBasis R S

Result:
case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ finrank (R ⧸ p) (S ⧸ pS) ≤ finrank R S

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ finrank (R ⧸ p) (S ⧸ pS) ≤ Fintype.card (Free.ChooseBasisIndex R S)

Tactic:
apply finrank_le_of_span_eq_top

Result:
case a.hv
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ span (R ⧸ p) (Set.range ?a.v✝) = ⊤

case a.v
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ Free.ChooseBasisIndex R S → S ⧸ pS

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
⊢ finrank (R ⧸ p) (S ⧸ pS) = finrank R S

Tactic:
apply le_antisymm

Result:
case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
⊢ finrank (R ⧸ p) (S ⧸ pS) ≤ finrank R S

case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ pS)

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ pS)

Tactic:
let b := Module.Free.chooseBasis (R ⧸ p) (S ⧸ pS)

Result:
case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) (R ⧸ p) (S ⧸ pS) := Free.chooseBasis (R ⧸ p) (S ⧸ pS)
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ pS)

Proof state:
case a.hv
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ span (R ⧸ p) (Set.range ?a.v✝) = ⊤

case a.v
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ Free.ChooseBasisIndex R S → S ⧸ pS

Tactic:
rw [Set.range_comp]

Result:
case a.hv
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ span (R ⧸ p) (?a.hv.g✝ '' Set.range ?a.hv.f✝) = ⊤

case a.hv.g
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ ?m.57615 → S ⧸ pS

case a.hv.f
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ Free.ChooseBasisIndex R S → ?m.57615

R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ Type ?u.57614

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) (R ⧸ p) (S ⧸ pS) := Free.chooseBasis (R ⧸ p) (S ⧸ pS)
b' : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS) → S
hb' : ∀ (i : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)), (Ideal.Quotient.mk pS) (b' i) = b i
⊢ span R (Set.range b') = ⊤

Tactic:
apply (quotient_span_eq_top_iff_span_eq_top _).mp

Result:
case a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this✝ : Module.Finite R (S ⧸ pS)
this : Module.Finite (R ⧸ p) (S ⧸ pS)
b : Basis (Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) (R ⧸ p) (S ⧸ pS) := Free.chooseBasis (R ⧸ p) (S ⧸ pS)
b' : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS) → S
hb' : ∀ (i : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)), (Ideal.Quotient.mk pS) (b' i) = b i
⊢ span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' Set.range b') = ⊤

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
⊢ finrank (R ⧸ p) (S ⧸ pS) = finrank R S

Tactic:
have : Module.Finite R (S ⧸ pS) := Module.Finite.of_surjective
  (IsScalarTower.toAlgHom R S (S ⧸ pS)).toLinearMap (Ideal.Quotient.mk_surjective (I := pS))

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R S
inst✝ : Free R S
this : Module.Finite R (S ⧸ pS)
⊢ finrank (R ⧸ p) (S ⧸ pS) = finrank R S