awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
⊢ finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) =
    finrank R S
have this : Module.Finite.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
  (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
Tactic: have : Module.Finite (R ⧸ p) (S ⧸ pS) := Module.Finite.of_restrictScalars_finite R _ _
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
this :
  Module.Finite.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
⊢ finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) =
    finrank R S
have a : finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) ≤
  finrank R S
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
this :
  Module.Finite.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
a :
  finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) ≤
    finrank R S
⊢ finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) =
    finrank R S
have a₁ : finrank R S ≤
  finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
this :
  Module.Finite.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
| finrank R S
have rw : Fintype.card.{u_2} (Free.ChooseBasisIndex R S)
Tactic: rw [finrank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
this :
  Module.Finite.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) ≤
    finrank R S
have a : finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) ≤
  Fintype.card.{u_2} (Free.ChooseBasisIndex R S)
Tactic: conv_rhs => rw [finrank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
this :
  Module.Finite.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) ≤
    Fintype.card.{u_2} (Free.ChooseBasisIndex R S)
have a : Eq.{u_2 + 1} (α :=
  Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
  (span (HasQuotient.Quotient R (B := Ideal R) p)
    (Set.range (ι := Free.ChooseBasisIndex R S)
      (Function.comp (β := S) (⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS)
        (⇑b : (a : Free.ChooseBasisIndex R S) → S))))
  ⊤
Tactic: apply finrank_le_of_span_eq_top
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
this :
  Module.Finite.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
a :
  Eq.{u_2 + 1} (α :=
    Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      (Set.range (ι := Free.ChooseBasisIndex R S)
        (Function.comp (β := S) (⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS)
          (⇑b : (a : Free.ChooseBasisIndex R S) → S))))
    ⊤
⊢ finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) ≤
    Fintype.card.{u_2} (Free.ChooseBasisIndex R S)
have a₁ : Free.ChooseBasisIndex R S → HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)
Tactic: apply finrank_le_of_span_eq_top
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
this :
  Module.Finite.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
b : Basis.{u_2, u_1, u_2}
  (Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
  (HasQuotient.Quotient R (B := Ideal R) p)
  (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :=
  Free.chooseBasis (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
⊢ finrank R S ≤
    finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
have a : ∀
  (b' :
    (i :
        Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
          (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) →
      S)
  (hb' :
    ∀
      (i :
        Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
          (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))),
      Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) (b' i) :
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
        ((b : (a : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) → S ⧸ pS) i :
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))),
  finrank R S ≤
    finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
Tactic: choose b' hb' using fun i ↦ Ideal.Quotient.mk_surjective (b i)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
this :
  Module.Finite.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
b : Basis.{u_2, u_1, u_2}
  (Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
  (HasQuotient.Quotient R (B := Ideal R) p)
  (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :=
  Free.chooseBasis (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
b' :
  (i :
      Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) →
    S
hb' :
  ∀
    (i :
      Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))),
    Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) (b' i) :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
      ((b : (a : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) → S ⧸ pS) i :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
| finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
have rw : Fintype.card.{u_2}
  (Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
Tactic: rw [finrank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
this :
  Module.Finite.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
b : Basis.{u_2, u_1, u_2}
  (Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
  (HasQuotient.Quotient R (B := Ideal R) p)
  (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :=
  Free.chooseBasis (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
b' :
  (i :
      Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) →
    S
hb' :
  ∀
    (i :
      Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))),
    Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) (b' i) :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
      ((b : (a : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) → S ⧸ pS) i :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
⊢ finrank R S ≤
    finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
have a : finrank R S ≤
  Fintype.card.{u_2}
    (Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
Tactic: conv_rhs => rw [finrank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
this :
  Module.Finite.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
b : Basis.{u_2, u_1, u_2}
  (Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
  (HasQuotient.Quotient R (B := Ideal R) p)
  (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :=
  Free.chooseBasis (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
b' :
  (i :
      Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) →
    S
hb' :
  ∀
    (i :
      Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))),
    Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) (b' i) :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
      ((b : (a : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) → S ⧸ pS) i :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
⊢ finrank R S ≤
    Fintype.card.{u_2}
      (Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
have a : Eq (α := Submodule R S) (span R (Set.range b')) ⊤
Tactic: refine finrank_le_of_span_eq_top (v := b') ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
this :
  Module.Finite.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
b : Basis.{u_2, u_1, u_2}
  (Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
  (HasQuotient.Quotient R (B := Ideal R) p)
  (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :=
  Free.chooseBasis (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
b' :
  (i :
      Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) →
    S
hb' :
  ∀
    (i :
      Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))),
    Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) (b' i) :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
      ((b : (a : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) → S ⧸ pS) i :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
⊢ Eq (α := Submodule R S) (span R (Set.range b')) ⊤
have a : Eq (α :=
  Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
  (span (HasQuotient.Quotient R (B := Ideal R) p)
    ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' Set.range b'))
  ⊤
Tactic: apply (quotient_span_eq_top_iff_span_eq_top _).mp
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
this :
  Module.Finite.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
b : Basis.{u_2, u_1, u_2}
  (Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
  (HasQuotient.Quotient R (B := Ideal R) p)
  (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :=
  Free.chooseBasis (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
b' :
  (i :
      Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) →
    S
hb' :
  ∀
    (i :
      Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))),
    Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
      ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) (b' i) :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
      ((b : (a : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) → S ⧸ pS) i :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
⊢ Eq (α :=
    Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' Set.range b'))
    ⊤
have a : Eq.{u_2 + 1} (α :=
  Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
  (span (HasQuotient.Quotient R (B := Ideal R) p)
    (Set.range (ι :=
      Free.ChooseBasisIndex.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
      (⇑b : (a : Free.ChooseBasisIndex (R ⧸ p) (S ⧸ pS)) → S ⧸ pS)))
  ⊤
Tactic: rw [← Set.range_comp, show Ideal.Quotient.mk pS ∘ b' = ⇑b from funext hb']
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
⊢ finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) =
    finrank R S
have have : ∀
  (this :
    Module.Finite.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))),
  finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) =
    finrank R S
Tactic: classical
  have : Module.Finite (R ⧸ p) (S ⧸ pS) := Module.Finite.of_restrictScalars_finite R _ _
  apply le_antisymm
  · let b := Module.Free.chooseBasis R S
    conv_rhs => rw [finrank_eq_card_chooseBasisIndex]
    apply finrank_le_of_span_eq_top
    rw [Set.range_comp]
    apply (quotient_span_eq_top_iff_span_eq_top _).mpr b.span_eq
  · let b := Module.Free.chooseBasis (R ⧸ p) (S ⧸ pS)
    choose b' hb' using fun i ↦ Ideal.Quotient.mk_surjective (b i)
    conv_rhs => rw [finrank_eq_card_chooseBasisIndex]
    refine finrank_le_of_span_eq_top (v := b') ?_
    apply (quotient_span_eq_top_iff_span_eq_top _).mp
    rw [← Set.range_comp, show Ideal.Quotient.mk pS ∘ b' = ⇑b from funext hb']
    exact b.span_eq
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
have have₁ have₂ :
  ∀
    (this :
      Module.Finite.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))),
    finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) =
      finrank R S
⊢ finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) =
    finrank R S
have a : ∀
  (this :
    Module.Finite.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))),
  finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) ≤
    finrank R S
Tactic: classical
  have : Module.Finite (R ⧸ p) (S ⧸ pS) := Module.Finite.of_restrictScalars_finite R _ _
  apply le_antisymm
  · let b := Module.Free.chooseBasis R S
    conv_rhs => rw [finrank_eq_card_chooseBasisIndex]
    apply finrank_le_of_span_eq_top
    rw [Set.range_comp]
    apply (quotient_span_eq_top_iff_span_eq_top _).mpr b.span_eq
  · let b := Module.Free.chooseBasis (R ⧸ p) (S ⧸ pS)
    choose b' hb' using fun i ↦ Ideal.Quotient.mk_surjective (b i)
    conv_rhs => rw [finrank_eq_card_chooseBasisIndex]
    refine finrank_le_of_span_eq_top (v := b') ?_
    apply (quotient_span_eq_top_iff_span_eq_top _).mp
    rw [← Set.range_comp, show Ideal.Quotient.mk pS ∘ b' = ⇑b from funext hb']
    exact b.span_eq