-- Mathlib/RingTheory/LocalRing/Quotient.lean
lemma basisQuotient_repr {ι} [Fintype ι] (b : Basis ι R S) (x) (i) :
    (basisQuotient b).repr (Ideal.Quotient.mk pS x) i =
    Ideal.Quotient.mk p (b.repr x i)

Proof state:
case a.a
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : Free R S
ι : Type u_4
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (basisQuotient b).repr.symm
      ((Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm ⇑((basisQuotient b).repr ((Ideal.Quotient.mk pS) x))) =
    (basisQuotient b).repr.symm
      ((Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)))

Tactic:
simp only [Finsupp.linearEquivFunOnFinite_symm_coe, LinearEquiv.symm_apply_apply,
  Basis.repr_symm_apply]

Result:
case a.a
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : Free R S
ι : Type u_4
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Ideal.Quotient.mk pS) x =
    (Finsupp.linearCombination (R ⧸ p) ⇑(basisQuotient b))
      ((Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)))

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : Free R S
ι : Type u_4
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm ⇑((basisQuotient b).repr ((Ideal.Quotient.mk pS) x)) =
    (Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x))

Tactic:
apply (basisQuotient b).repr.symm.injective

Result:
case a.a
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : Free R S
ι : Type u_4
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (basisQuotient b).repr.symm
      ((Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm ⇑((basisQuotient b).repr ((Ideal.Quotient.mk pS) x))) =
    (basisQuotient b).repr.symm
      ((Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)))

Proof state:
case a.a
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : Free R S
ι : Type u_4
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Ideal.Quotient.mk pS) x = ∑ x_1 : ι, (Ideal.Quotient.mk pS) ((b.repr x) x_1 • b x_1)

Tactic:
rw [← map_sum, Basis.sum_repr b x]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : Free R S
ι : Type u_4
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ ((basisQuotient b).repr ((Ideal.Quotient.mk pS) x)) i = (Ideal.Quotient.mk p) ((b.repr x) i)

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

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : Free R S
ι : Type u_4
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ ⇑((basisQuotient b).repr ((Ideal.Quotient.mk pS) x)) = ⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : Free R S
ι : Type u_4
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ ⇑((basisQuotient b).repr ((Ideal.Quotient.mk pS) x)) = ⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)

Tactic:
apply (Finsupp.linearEquivFunOnFinite (R ⧸ p) _ _).symm.injective

Result:
case a
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : Free R S
ι : Type u_4
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm ⇑((basisQuotient b).repr ((Ideal.Quotient.mk pS) x)) =
    (Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x))

Proof state:
case a.a
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : Free R S
ι : Type u_4
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Ideal.Quotient.mk pS) x =
    (Finsupp.linearCombination (R ⧸ p) ⇑(basisQuotient b))
      ((Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)))

Tactic:
rw [Finsupp.linearCombination_eq_fintype_linearCombination_apply _ (R ⧸ p),
  Fintype.linearCombination_apply]

Result:
case a.a
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : Free R S
ι : Type u_4
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Ideal.Quotient.mk pS) x = ∑ i : ι, (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)) i • (basisQuotient b) i

Proof state:
case a.a
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : Free R S
ι : Type u_4
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Ideal.Quotient.mk pS) x = ∑ i : ι, (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)) i • (basisQuotient b) i

Tactic:
simp only [Function.comp_apply, basisQuotient_apply,
  Ideal.Quotient.mk_smul_mk_quotient_map_quotient, ← Algebra.smul_def]

Result:
case a.a
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : Free R S
ι : Type u_4
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Ideal.Quotient.mk pS) x = ∑ x_1 : ι, (Ideal.Quotient.mk pS) ((b.repr x) x_1 • b x_1)