[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ ↑(trans e (dualMap (symm (flip e)))) = Dual.eval R N
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
x✝¹ : N
x✝ : Dual R N
⊢ ↑(↑↑(trans e (dualMap (symm (flip e)))) x✝¹) x✝ = ↑(↑(Dual.eval R N) x✝¹) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ IsReflexive R N
[PROOFSTEP]
constructor
[GOAL]
case bijective_dual_eval'
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ Function.Bijective ↑(Dual.eval R N)
[PROOFSTEP]
rw [← trans_dualMap_symm_flip e]
[GOAL]
case bijective_dual_eval'
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
⊢ Function.Bijective ↑↑(trans e (dualMap (symm (flip e))))
[PROOFSTEP]
exact LinearEquiv.bijective _
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
h : optParam (IsReflexive R N) (_ : IsReflexive R N)
⊢ flip (flip e) = e
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
h : optParam (IsReflexive R N) (_ : IsReflexive R N)
x✝¹ : N
x✝ : M
⊢ ↑(↑(flip (flip e)) x✝¹) x✝ = ↑(↑e x✝¹) x✝
[PROOFSTEP]
rfl