Theorem: finrank_quotient_map_of_localRing (FltRegular/NumberTheory/QuotientTrace.lean)

State before:
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) = 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))
State after:
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) = finrank R S

State before:
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) = finrank R S
Tactic:
have : Module.Finite (R ⧸ p) (S ⧸ pS) := Module.Finite.of_restrictScalars_finite R _ _
State after:
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) = finrank R S

State before:
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) = finrank R S
Tactic:
apply le_antisymm
State after:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) ≤ finrank R S

case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)

State before:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) ≤ finrank R S
Tactic:
let b := Module.Free.chooseBasis R S
State after:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) ≤ finrank R S

State before:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) ≤ finrank R S
Tactic:
conv_rhs => rw [finrank_eq_card_chooseBasisIndex]
State after:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) ≤ Fintype.card (Module.Free.ChooseBasisIndex R S)

State before:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) ≤ Fintype.card (Module.Free.ChooseBasisIndex R S)
Tactic:
apply finrank_le_of_span_eq_top (IsScalarTower.toAlgHom R S (S ⧸ pS) ∘ b)
State after:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ Submodule.span (R ⧸ p) (Set.range (⇑(IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) ∘ ⇑b)) = ⊤

State before:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ Submodule.span (R ⧸ p) (Set.range (⇑(IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) ∘ ⇑b)) = ⊤
Tactic:
rw [Set.range_comp]
State after:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ Submodule.span (R ⧸ p) (⇑(IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) '' Set.range ⇑b) = ⊤

State before:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ Submodule.span (R ⧸ p) (⇑(IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) '' Set.range ⇑b) = ⊤
Tactic:
apply (quotient_span_eq_top_iff_span_eq_top_of_localRing _).mpr b.span_eq
State after:
no goals

State before:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
Tactic:
let b := Module.Free.chooseBasis (R ⧸ p) (S ⧸ pS)
State after:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)

State before:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
Tactic:
choose b' hb' using fun i ↦ Ideal.Quotient.mk_surjective (b i)
State after:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)

State before:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ finrank R S ≤ finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
Tactic:
conv_rhs => rw [finrank_eq_card_chooseBasisIndex]
State after:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ finrank R S ≤ Fintype.card (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p))

State before:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ finrank R S ≤ Fintype.card (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p))
Tactic:
apply finrank_le_of_span_eq_top b'
State after:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ Submodule.span R (Set.range b') = ⊤

State before:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ Submodule.span R (Set.range b') = ⊤
Tactic:
apply (quotient_span_eq_top_iff_span_eq_top_of_localRing _).mp
State after:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' Set.range b') = ⊤

State before:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' Set.range b') = ⊤
Tactic:
rw [← Set.range_comp, show Ideal.Quotient.mk pS ∘ b' = ⇑b from funext hb']
State after:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ Submodule.span (R ⧸ p) (Set.range ⇑b) = ⊤

State before:
case a
R : Type u_2
S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : LocalRing R
inst✝³ : Module.Free R S
inst✝² : Module.Finite R S
p : Ideal R
inst✝¹ : p.IsMaximal
inst✝ : LocalRing R
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)) (R ⧸ p)
  (S ⧸ Ideal.map (algebraMap R S) p) :=
  Module.Free.chooseBasis (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b' : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) → S
hb' :
  ∀ (i : Module.Free.ChooseBasisIndex (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)),
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b' i) = b i
⊢ Submodule.span (R ⧸ p) (Set.range ⇑b) = ⊤
Tactic:
exact b.span_eq
State after:
no goals