awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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 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: 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
ι : Type u_3
inst_6 : Fintype ι
b : Basis ι R S
⊢ LE.le.{u_2} (α :=
    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.{u_2, u_3 + 1} (ι := ι)
        (Function.comp (β := S) (⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS)
          (⇑b : (a : ι) → S))))
have rw : LE.le.{u_2} (α :=
  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.image (α := S) (⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS)
      (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑b : (a : ι) → S))))
Tactic: rw [Set.range_comp]
-- 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
ι : Type u_3
inst_6 : Fintype ι
b : Basis ι R S
⊢ Fintype.card ι =
    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 ι = finrank R S
Tactic: rw [finrank_quotient_map, finrank_eq_card_basis 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
ι : Type u_3
inst_6 : Fintype ι
b : Basis ι R S
rw : Fintype.card ι = finrank R S
⊢ Fintype.card ι =
    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 ι = Fintype.card ι
Tactic: rw [finrank_quotient_map, finrank_eq_card_basis 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
ι : Type u_3
inst_6 : Fintype ι
b : Basis ι R S
i : ι
⊢ Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((basisOfTopLeSpanOfCardEqFinrank
            (Function.comp (β := S)
              (⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS)
              (⇑b : (a : ι) → S))
            ⋯ ⋯ :
          (a : ι) → S ⧸ pS)
        i :
      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 : (a : ι) → S) i) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
have rw : Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
  (Function.comp (β := S) (⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS)
      (⇑b : (a : ι) → S) i :
    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 : (a : ι) → S) i) :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
Tactic: rw [coe_basisOfTopLeSpanOfCardEqFinrank, Function.comp_apply]
-- 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
ι : Type u_3
inst_6 : Fintype ι
b : Basis ι R S
i : ι
rw :
  Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    (Function.comp (β := S) (⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS)
        (⇑b : (a : ι) → S) i :
      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 : (a : ι) → S) i) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
⊢ Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((basisOfTopLeSpanOfCardEqFinrank
            (Function.comp (β := S)
              (⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS)
              (⇑b : (a : ι) → S))
            ⋯ ⋯ :
          (a : ι) → S ⧸ pS)
        i :
      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 : (a : ι) → S) i) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
have rw₁ : Eq.{u_2 + 1} (α := 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 : (a : ι) → S) i) :
    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 : (a : ι) → S) i) :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
Tactic: rw [coe_basisOfTopLeSpanOfCardEqFinrank, Function.comp_apply]
-- 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
ι : Type u_4
inst_6 : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) p)
    ((((Basis.repr (basisQuotient b) : (a : S ⧸ pS) → ι →₀ R ⧸ p)
              ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
            Finsupp.{u_4, u_1} ι (HasQuotient.Quotient R (B := Ideal R) p)) :
          (a : ι) → R ⧸ p)
        i :
      HasQuotient.Quotient R (B := Ideal R) p)
    ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) ((((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i) :
      HasQuotient.Quotient R (B := Ideal R) (p : Ideal R))
have refine : Eq (α := (x : ι) → HasQuotient.Quotient R (B := Ideal R) (p : Ideal R))
  (⇑((Basis.repr (basisQuotient b) : (a : S ⧸ pS) → ι →₀ R ⧸ p)
          ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
        Finsupp.{u_4, u_1} ι (HasQuotient.Quotient R (B := Ideal R) p)) :
    (a : ι) → R ⧸ p)
  (Function.comp (β := R) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)
    (⇑((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R))
Tactic: refine congr_fun (g := Ideal.Quotient.mk p ∘ b.repr x) ?_ 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
ι : Type u_4
inst_6 : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ Eq (α := (x : ι) → HasQuotient.Quotient R (B := Ideal R) (p : Ideal R))
    (⇑((Basis.repr (basisQuotient b) : (a : S ⧸ pS) → ι →₀ R ⧸ p)
            ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
          Finsupp.{u_4, u_1} ι (HasQuotient.Quotient R (B := Ideal R) p)) :
      (a : ι) → R ⧸ p)
    (Function.comp (β := R) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)
      (⇑((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R))
have a : Eq (α := Finsupp.{u_4, u_1} ι (HasQuotient.Quotient R (B := Ideal R) p))
  ((LinearEquiv.symm
          (Finsupp.linearEquivFunOnFinite (HasQuotient.Quotient R (B := Ideal R) p)
            (HasQuotient.Quotient R (B := Ideal R) p) ι) :
        (a : ι → R ⧸ p) → ι →₀ R ⧸ p)
      (⇑((Basis.repr (basisQuotient b) : (a : S ⧸ pS) → ι →₀ R ⧸ p)
              ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
            Finsupp.{u_4, u_1} ι (HasQuotient.Quotient R (B := Ideal R) p)) :
        (a : ι) → R ⧸ p) :
    Finsupp.{u_4, u_1} ι (HasQuotient.Quotient R (B := Ideal R) p))
  ((LinearEquiv.symm
          (Finsupp.linearEquivFunOnFinite (HasQuotient.Quotient R (B := Ideal R) p)
            (HasQuotient.Quotient R (B := Ideal R) p) ι) :
        (a : ι → R ⧸ p) → ι →₀ R ⧸ p)
      (Function.comp (β := R) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)
        (⇑((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)) :
    Finsupp.{u_4, u_1} ι (HasQuotient.Quotient R (B := Ideal R) p))
Tactic: apply (Finsupp.linearEquivFunOnFinite (R ⧸ p) _ _).symm.injective
-- 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
ι : Type u_4
inst_6 : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ Eq (α := Finsupp.{u_4, u_1} ι (HasQuotient.Quotient R (B := Ideal R) p))
    ((LinearEquiv.symm
            (Finsupp.linearEquivFunOnFinite (HasQuotient.Quotient R (B := Ideal R) p)
              (HasQuotient.Quotient R (B := Ideal R) p) ι) :
          (a : ι → R ⧸ p) → ι →₀ R ⧸ p)
        (⇑((Basis.repr (basisQuotient b) : (a : S ⧸ pS) → ι →₀ R ⧸ p)
                ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
              Finsupp.{u_4, u_1} ι (HasQuotient.Quotient R (B := Ideal R) p)) :
          (a : ι) → R ⧸ p) :
      Finsupp.{u_4, u_1} ι (HasQuotient.Quotient R (B := Ideal R) p))
    ((LinearEquiv.symm
            (Finsupp.linearEquivFunOnFinite (HasQuotient.Quotient R (B := Ideal R) p)
              (HasQuotient.Quotient R (B := Ideal R) p) ι) :
          (a : ι → R ⧸ p) → ι →₀ R ⧸ p)
        (Function.comp (β := R) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)
          (⇑((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)) :
      Finsupp.{u_4, u_1} ι (HasQuotient.Quotient R (B := Ideal R) p))
have a : Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
  ((LinearEquiv.symm (Basis.repr (basisQuotient b)) : (a : ι →₀ R ⧸ p) → S ⧸ pS)
      ((LinearEquiv.symm
            (Finsupp.linearEquivFunOnFinite (HasQuotient.Quotient R (B := Ideal R) p)
              (HasQuotient.Quotient R (B := Ideal R) p) ι) :
          (a : ι → R ⧸ p) → ι →₀ R ⧸ p)
        (⇑((Basis.repr (basisQuotient b) : (a : S ⧸ pS) → ι →₀ R ⧸ p)
                ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
              Finsupp.{u_4, u_1} ι (HasQuotient.Quotient R (B := Ideal R) p)) :
          (a : ι) → R ⧸ p)) :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
  ((LinearEquiv.symm (Basis.repr (basisQuotient b)) : (a : ι →₀ R ⧸ p) → S ⧸ pS)
      ((LinearEquiv.symm
            (Finsupp.linearEquivFunOnFinite (HasQuotient.Quotient R (B := Ideal R) p)
              (HasQuotient.Quotient R (B := Ideal R) p) ι) :
          (a : ι → R ⧸ p) → ι →₀ R ⧸ p)
        (Function.comp (β := R) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)
          (⇑((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R))) :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
Tactic: apply (basisQuotient b).repr.symm.injective
-- 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
ι : Type u_4
inst_6 : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((LinearEquiv.symm (Basis.repr (basisQuotient b)) : (a : ι →₀ R ⧸ p) → S ⧸ pS)
        ((LinearEquiv.symm
              (Finsupp.linearEquivFunOnFinite (HasQuotient.Quotient R (B := Ideal R) p)
                (HasQuotient.Quotient R (B := Ideal R) p) ι) :
            (a : ι → R ⧸ p) → ι →₀ R ⧸ p)
          (⇑((Basis.repr (basisQuotient b) : (a : S ⧸ pS) → ι →₀ R ⧸ p)
                  ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
                Finsupp.{u_4, u_1} ι (HasQuotient.Quotient R (B := Ideal R) p)) :
            (a : ι) → R ⧸ p)) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((LinearEquiv.symm (Basis.repr (basisQuotient b)) : (a : ι →₀ R ⧸ p) → S ⧸ pS)
        ((LinearEquiv.symm
              (Finsupp.linearEquivFunOnFinite (HasQuotient.Quotient R (B := Ideal R) p)
                (HasQuotient.Quotient R (B := Ideal R) p) ι) :
            (a : ι → R ⧸ p) → ι →₀ R ⧸ p)
          (Function.comp (β := R) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)
            (⇑((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R))) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
have a : 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) x :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
  ((Finsupp.linearCombination (HasQuotient.Quotient R (B := Ideal R) p) (⇑(basisQuotient b) : (a : ι) → S ⧸ pS) :
        (a : ι →₀ R ⧸ p) → S ⧸ pS)
      ((LinearEquiv.symm
            (Finsupp.linearEquivFunOnFinite (HasQuotient.Quotient R (B := Ideal R) p)
              (HasQuotient.Quotient R (B := Ideal R) p) ι) :
          (a : ι → R ⧸ p) → ι →₀ R ⧸ p)
        (Function.comp (β := R) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)
          (⇑((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R))) :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
Tactic: simp only [Finsupp.linearEquivFunOnFinite_symm_coe, LinearEquiv.symm_apply_apply,
    Basis.repr_symm_apply]
-- 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
ι : Type u_4
inst_6 : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ 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) x :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((Finsupp.linearCombination (HasQuotient.Quotient R (B := Ideal R) p) (⇑(basisQuotient b) : (a : ι) → S ⧸ pS) :
          (a : ι →₀ R ⧸ p) → S ⧸ pS)
        ((LinearEquiv.symm
              (Finsupp.linearEquivFunOnFinite (HasQuotient.Quotient R (B := Ideal R) p)
                (HasQuotient.Quotient R (B := Ideal R) p) ι) :
            (a : ι → R ⧸ p) → ι →₀ R ⧸ p)
          (Function.comp (β := R) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)
            (⇑((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R))) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
have a : 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) x :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
  (∑ i : ι,
      HSMul.hSMul.{u_1, u_2, u_2} (α := HasQuotient.Quotient R (B := Ideal R) p) (β :=
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
        (Function.comp (β := R) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)
          (⇑((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i)
        ((basisQuotient b : (a : ι) → S ⧸ pS) i :
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
Tactic: rw [Finsupp.linearCombination_eq_fintype_linearCombination_apply (R ⧸ p),
    Fintype.linearCombination_apply]
-- 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
ι : Type u_4
inst_6 : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ 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) x :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    (∑ i : ι,
        HSMul.hSMul.{u_1, u_2, u_2} (α := HasQuotient.Quotient R (B := Ideal R) p) (β :=
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
          (Function.comp (β := R) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)
            (⇑((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i)
          ((basisQuotient b : (a : ι) → S ⧸ pS) i :
            HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
have a : 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) x :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
  (∑ x_1 : ι,
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
          ((((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R) ((b : (a : ι) → S) x_1 : S)) :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
Tactic: simp only [Function.comp_apply, basisQuotient_apply,
    Ideal.Quotient.mk_smul_mk_quotient_map_quotient, ← Algebra.smul_def]
-- 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
ι : Type u_4
inst_6 : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ 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) x :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    (∑ x_1 : ι,
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R) ((b : (a : ι) → S) x_1 : S)) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
have a : 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) x :
    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)
      (∑ x_1 : ι,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
          ((b : (a : ι) → S) x_1 : S)) :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
Tactic: rw [← map_sum, Basis.sum_repr b x]