Theorem: Module.piEquiv_apply_symm (Matroid/ForMathlib/LinearAlgebra/StdBasis.lean)

State before:
α : Type u_1
R : Type u_2
η : Type u_3
ι : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype α
inst✝ : DecidableEq α
y : Dual R (α → R)
i : α
⊢ (piEquiv α R R).symm y i = y (Pi.single i 1)
Tactic:
simp only [piEquiv, Basis.constr, Pi.basisFun_apply, LinearMap.stdBasis_apply,
  LinearEquiv.coe_symm_mk]
State after:
α : Type u_1
R : Type u_2
η : Type u_3
ι : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype α
inst✝ : DecidableEq α
y : Dual R (α → R)
i : α
⊢ y (update 0 i 1) = y (Pi.single i 1)

State before:
α : Type u_1
R : Type u_2
η : Type u_3
ι : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype α
inst✝ : DecidableEq α
y : Dual R (α → R)
i : α
⊢ y (update 0 i 1) = y (Pi.single i 1)
Tactic:
rfl
State after:
no goals