-- Mathlib/LinearAlgebra/Dual.lean
lemma equiv (e : M ≃ₗ[R] N) : IsReflexive R N where
  bijective_dual_eval'

Proof state:
case h.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
m : N
f : Dual R N
⊢ ((Dual.eval R N) m) f = ((↑ed.symm ∘ₗ Dual.eval R M ∘ₗ ↑e.symm) m) f

Tactic:
exact DFunLike.congr_arg f (e.apply_symm_apply m).symm

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
⊢ Bijective ⇑(Dual.eval R N)

Tactic:
have : Dual.eval R N = ed.symm.comp ((Dual.eval R M).comp e.symm.toLinearMap) := by
  ext m f
  exact DFunLike.congr_arg f (e.apply_symm_apply m).symm

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
this : Dual.eval R N = ↑ed.symm ∘ₗ Dual.eval R M ∘ₗ ↑e.symm
⊢ Bijective ⇑(Dual.eval R N)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
this : Dual.eval R N = ↑ed.symm ∘ₗ Dual.eval R M ∘ₗ ↑e.symm
⊢ Bijective ⇑(Dual.eval R N)

Tactic:
simp only [this, LinearEquiv.trans_symm, LinearEquiv.symm_symm, LinearEquiv.dualMap_symm,
  coe_comp, LinearEquiv.coe_coe, EquivLike.comp_bijective]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
this : Dual.eval R N = ↑ed.symm ∘ₗ Dual.eval R M ∘ₗ ↑e.symm
⊢ Bijective (⇑(Dual.eval R M) ∘ ⇑e.symm)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
this : Dual.eval R N = ↑ed.symm ∘ₗ Dual.eval R M ∘ₗ ↑e.symm
⊢ Bijective (⇑(Dual.eval R M) ∘ ⇑e.symm)

Tactic:
exact Bijective.comp (bijective_dual_eval R M) (LinearEquiv.bijective _)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
⊢ Dual.eval R N = ↑ed.symm ∘ₗ Dual.eval R M ∘ₗ ↑e.symm

Tactic:
ext m f

Result:
case h.h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
m : N
f : Dual R N
⊢ ((Dual.eval R N) m) f = ((↑ed.symm ∘ₗ Dual.eval R M ∘ₗ ↑e.symm) m) f

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
⊢ Bijective ⇑(Dual.eval R N)

Tactic:
let ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
⊢ Bijective ⇑(Dual.eval R N)