Theorem: DividedPowerAlgebra.roby4.Ψ_eq (DividedPowers/DPAlgebra/Dpow.lean)

State before:
R : Type u
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra A S
I : Ideal S
hI : DividedPowers I
S₀ : Subalgebra A S
hIS₀ : IsCompl (Subalgebra.toSubmodule S₀) (Submodule.restrictScalars A I)
condTFree : CondTFree A
condD : CondD A
hM : DividedPowers (augIdeal A (↥I →₀ A))
hM_eq : ∀ (n : ℕ) (x : ↥I →₀ A), hM.dpow n ((ι A (↥I →₀ A)) x) = dp A n x
i : S
hi : i ∈ I
⊢ (Ψ A S hI S₀) (Algebra.TensorProduct.includeRight ((ι A (↥I →₀ A)) (Finsupp.single ⟨i, hi⟩ 1))) = i
Tactic:
simp [Ψ, Φ, f, Basis.constr_apply]
State after:
no goals