Theorem: DividedPowerAlgebra.dividedPowerAlgebra_exponentialModule_equiv_symm_apply (DividedPowers/DPAlgebra/Exponential.lean)

State before:
R : Type u_1
inst✝⁸ : CommRing R
A : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
β : M →ₗ[R] ↥(ExponentialModule S)
n : ℕ
m : M
⊢ ((dividedPowerAlgebra_exponentialModule_equiv R M S).symm β) (dp R n m) = (coeff S n) ↑(β m)
Tactic:
unfold dividedPowerAlgebra_exponentialModule_equiv
State after:
R : Type u_1
inst✝⁸ : CommRing R
A : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
β : M →ₗ[R] ↥(ExponentialModule S)
n : ℕ
m : M
⊢ ({ toFun := fun α => linearMap α ∘ₗ exp_LinearMap R M,
            invFun := fun β =>
              lift'
                (fun x =>
                  match x with
                  | (n, m) => (coeff S n) ↑(β m))
                ⋯ ⋯ ⋯ ⋯,
            left_inv := ⋯, right_inv := ⋯ }.symm
        β)
      (dp R n m) =
    (coeff S n) ↑(β m)

State before:
R : Type u_1
inst✝⁸ : CommRing R
A : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
β : M →ₗ[R] ↥(ExponentialModule S)
n : ℕ
m : M
⊢ ({ toFun := fun α => linearMap α ∘ₗ exp_LinearMap R M,
            invFun := fun β =>
              lift'
                (fun x =>
                  match x with
                  | (n, m) => (coeff S n) ↑(β m))
                ⋯ ⋯ ⋯ ⋯,
            left_inv := ⋯, right_inv := ⋯ }.symm
        β)
      (dp R n m) =
    (coeff S n) ↑(β m)
Tactic:
simp only [Equiv.coe_fn_symm_mk, lift'AlgHom_apply_dp]
State after:
no goals