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
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.{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)))
    ⊤
⊢ 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:
rw [← Set.range_comp, show Ideal.Quotient.mk pS ∘ b' = ⇑b from funext hb']

Premises used: Set.range_comp
-- 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))
⊢ 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:
b.span_eq

Premises used: Module.Basis.span_eq
-- 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))
⊢ 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:
exact b.span_eq

Premises used: Module.Basis.span_eq
-- 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
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
a₁ 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))
⊢ 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

Premises used: Set.range_comp, le_antisymm, Module.finrank_eq_card_chooseBasisIndex, IsLocalRing.quotient_span_eq_top_iff_span_eq_top, finrank_le_of_span_eq_top, Iff.mp
-- 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
ι : Type u_3
inst_6 : Fintype ι
b : Basis ι R S
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))))
⊢ 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))))

Tactic:
rw [Set.range_comp]

Premises used: Set.range_comp
-- 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
ι : 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.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:
((quotient_span_eq_top_iff_span_eq_top _).mpr b.span_eq).ge

Premises used: Iff.mpr, Eq.ge, Set.Mem, setOf, IsLocalRing.quotient_span_eq_top_iff_span_eq_top, Module.Basis.span_eq
-- 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
ι : 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.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:
exact ((quotient_span_eq_top_iff_span_eq_top _).mpr b.span_eq).ge

Premises used: Iff.mpr, Eq.ge, IsLocalRing.quotient_span_eq_top_iff_span_eq_top, Module.Basis.span_eq
-- 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
ι : Type u_3
inst_6 : Fintype ι
b : Basis ι R S
rw : Fintype.card ι = finrank R S
rw₁ rw₂ : Fintype.card ι = Fintype.card ι
⊢ 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))

Tactic:
rw [finrank_quotient_map, finrank_eq_card_basis b]

Premises used: IsLocalRing.finrank_quotient_map, Module.finrank_eq_card_basis
-- 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
ι : 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))
rw₁ 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))
⊢ 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))

Tactic:
rw [coe_basisOfTopLeSpanOfCardEqFinrank, Function.comp_apply]

Premises used: coe_basisOfTopLeSpanOfCardEqFinrank, Function.comp_apply
-- 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
ι : 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))

Tactic:
congr_fun (g := Ideal.Quotient.mk p ∘ b.repr x) ?_ i

Premises used: congr_fun
-- 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
ι : Type u_4
inst_6 : Fintype ι
b : Basis ι R S
x : S
i : ι
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))
⊢ 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))

Tactic:
refine congr_fun (g := Ideal.Quotient.mk p ∘ b.repr x) ?_ i
-- 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
ι : Type u_4
inst_6 : Fintype ι
b : Basis ι R S
x : S
i : ι
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))
⊢ 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:
apply (Finsupp.linearEquivFunOnFinite (R ⧸ p) _ _).symm.injective
-- 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
ι : Type u_4
inst_6 : Fintype ι
b : Basis ι R S
x : S
i : ι
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))
⊢ 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 (basisQuotient b).repr.symm.injective

Premises used: LinearEquiv.symm, Module.Basis.repr, LinearEquiv.injective, IsLocalRing.basisQuotient