awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) 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) '' s)))
    (map (σ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)
      (span R s))
hs : Eq (α := Submodule R S) (span R s) ⊤
mpr :
  ∀
    (H :
      Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
        (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) 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) '' s)))
        (LinearMap.range (M := S) (τ₁₂ := RingHom.id R)
          (↑(IsScalarTower.toAlgHom R S
                (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
            [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
              [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)))
    (hs : Eq (α := Submodule R S) (span R s) ⊤),
    Function.Surjective (α := S) (β :=
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
      (⇑(↑(IsScalarTower.toAlgHom R S
                (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
            [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
              [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS) :
        (a : S) → S ⧸ pS)
⊢ 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) '' s))
    ⊤

Tactic:
rwa [hs, Submodule.map_top, LinearMap.range_eq_top.mpr,
      restrictScalars_eq_top_iff] at H

Premises used: Iff.mpr, Submodule.map_top, LinearMap.range_eq_top, Submodule.restrictScalars_eq_top_iff
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) 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) '' s)))
    (LinearMap.range (M := S) (τ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS))
hs : Eq (α := Submodule R S) (span R s) ⊤
mpr :
  Function.Surjective.{u_2 + 1, u_2 + 1} (α := S) (β :=
    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)
⊢ Function.Surjective (α := S) (β :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    (⇑(↑(IsScalarTower.toAlgHom R S
              (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
          [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
            [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS) :
      (a : S) → S ⧸ pS)

Tactic:
rw [LinearMap.coe_coe, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq]

Premises used: IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq, LinearMap.coe_coe
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) 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) '' s)))
    (LinearMap.range (M := S) (τ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS))
hs : Eq (α := Submodule R S) (span R s) ⊤
⊢ Function.Surjective.{u_2 + 1, u_2 + 1} (α := S) (β :=
    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)

Tactic:
Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) 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) '' s)))
    (LinearMap.range (M := S) (τ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS))
hs : Eq (α := Submodule R S) (span R s) ⊤
⊢ Function.Surjective.{u_2 + 1, u_2 + 1} (α := S) (β :=
    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)

Tactic:
exact Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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
⊢ 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 _ _
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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
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))
⊢ 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

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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
rw : Fintype.card.{u_2} (Free.ChooseBasisIndex R S)
| finrank R S

Tactic:
rw [finrank_eq_card_chooseBasisIndex]

Premises used: Module.finrank_eq_card_chooseBasisIndex
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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 :
  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)
⊢ 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:
conv_rhs => rw [finrank_eq_card_chooseBasisIndex]

Premises used: Module.finrank_eq_card_chooseBasisIndex
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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))))
    ⊤
a₁ : Free.ChooseBasisIndex R S → 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)) ≤
    Fintype.card.{u_2} (Free.ChooseBasisIndex R S)

Tactic:
apply finrank_le_of_span_eq_top

Premises used: finrank_le_of_span_eq_top
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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))
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))
⊢ 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)

Premises used: Ideal.Quotient.mk_surjective, DFunLike.coe
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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))
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)))
| 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:
rw [finrank_eq_card_chooseBasisIndex]

Premises used: Module.finrank_eq_card_chooseBasisIndex
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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))
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)))
⊢ 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:
conv_rhs => rw [finrank_eq_card_chooseBasisIndex]

Premises used: Module.finrank_eq_card_chooseBasisIndex
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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)))

Tactic:
finrank_le_of_span_eq_top (v := b') ?_

Premises used: finrank_le_of_span_eq_top
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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))
a : Eq (α := Submodule R S) (span R (Set.range b')) ⊤
⊢ 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:
refine finrank_le_of_span_eq_top (v := b') ?_

Premises used: finrank_le_of_span_eq_top
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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))
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'))
    ⊤
⊢ Eq (α := Submodule R S) (span R (Set.range b')) ⊤

Tactic:
apply (quotient_span_eq_top_iff_span_eq_top _).mp

Premises used: IsLocalRing.quotient_span_eq_top_iff_span_eq_top, Iff.mp