awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type uR
M : Type uM
K : Type uK
V : Type uV
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Projective R M
⊢ Projective R (Dual R M)

Tactic:
have ⟨_, f, g, _, _, hfg⟩ := Finite.exists_comp_eq_id_of_projective R M
  .of_split f.dualMap g.dualMap (congr_arg dualMap hfg)

Premises used: Module.Projective, congr_arg, Module.Finite.exists_comp_eq_id_of_projective, Module.Projective.of_split, _private.0.Module.dual_projective.match_1, LinearMap.dualMap, Module.Dual
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type uR
M : Type uM
K : Type uK
V : Type uV
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Projective R M
⊢ Module.Finite R (Dual R M)

Tactic:
have ⟨n, f, g, _, _, hfg⟩ := Finite.exists_comp_eq_id_of_projective R M
  have := Finite.of_basis (Free.chooseBasis R <| Fin n → R).dualBasis
  .of_surjective _ (surjective_of_comp_eq_id f.dualMap g.dualMap <| congr_arg dualMap hfg)

Premises used: Module.Finite.of_surjective, _private.0.Module.dual_finite.match_1, congr_arg, LinearMap.surjective_of_comp_eq_id, Module.Finite.exists_comp_eq_id_of_projective, Module.Basis.dualBasis, Module.Finite, Module.Finite.of_basis, LinearMap.dualMap, Module.Dual, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
⊢ Function.Injective (α := V) (β := Dual K (Dual K V)) (⇑(eval K V) : (a : V) → Dual K (Dual K V))

Tactic:
have ⟨s, hs⟩ := Module.projective_def'.mp ‹Projective K V›
  .of_comp (f := s.dualMap.dualMap)
    (Finsupp.basisSingleOne.eval_injective.comp <| injective_of_comp_eq_id s _ hs)

Premises used: Finsupp.basisSingleOne, id, LinearMap.injective_of_comp_eq_id, Module.Basis.eval_injective, Function.Injective.comp, Module.projective_def', Iff.mp, _private.0.Module.eval_apply_injective.match_1, Function.Injective, Finsupp.linearCombination, DFunLike.coe, Module.Dual.eval, Function.Injective.of_comp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
⊢ Eq (α := Submodule K V) (ker (eval K V)) ⊥

Tactic:
ker_eq_bot_of_injective (eval_apply_injective K)

Premises used: Module.eval_apply_injective, LinearMap.ker_eq_bot_of_injective
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
⊢ Function.Injective (α := Submodule K V) (Submodule.map (eval K V))

Tactic:
Submodule.map_injective_of_injective (eval_apply_injective K)

Premises used: Module.eval_apply_injective, Submodule.map_injective_of_injective
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
⊢ Function.Surjective (α := Submodule K (Dual K (Dual K V))) (comap (eval K V))

Tactic:
Submodule.comap_surjective_of_injective (eval_apply_injective K)

Premises used: Module.eval_apply_injective, Submodule.comap_surjective_of_injective
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
v : V
⊢ Eq (α := Dual K (Dual K V)) ((eval K V : (a : V) → Dual K (Dual K V)) v : Dual K (Dual K V)) (0 : Dual K (Dual K V)) ↔
    v = 0

Tactic:
SetLike.ext_iff.mp (eval_ker K V) v

Premises used: Set.Mem, setOf, SetLike.ext_iff, Module.eval_ker, Set.preimage, Set.singleton, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
V : Type uV
inst : AddCommMonoid V
R : Type u_1
inst_1 : Semiring R
inst_2 : Module R V
inst_3 : Projective R V
x : V
hx : x ≠ 0
⊢ ∃ (f : Dual R V), Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (0 : R)

Tactic:
have ⟨M, _, _, _, ⟨i, s, his⟩⟩ := Projective.iff_split.mp ‹Projective R V›
  let b := Free.chooseBasis R M
  have : i x ≠ 0 := i.map_eq_zero_iff (injective_of_comp_eq_id i s his) |>.not.mpr hx
  have ⟨j, hj⟩ := not_forall.mp fun h ↦ b.repr.map_ne_zero_iff.mpr this <| Finsupp.ext h
  ⟨b.coord j ∘ₗ i, hj⟩

Premises used: Iff.mpr, Finsupp.ext, Module.Basis.coord, Exists, Iff.not, Ne, LinearMap.injective_of_comp_eq_id, Module.Basis.repr, _private.0.Module.Projective.exists_dual_ne_zero.match_1, LinearMap.comp, _private.0.Module.Projective.exists_dual_ne_zero.match_2, Exists.intro, Iff.mp, LinearEquiv.map_ne_zero_iff, Module.Projective.iff_split, OfNat.ofNat, Classical.not_forall, DFunLike.coe, LinearMap.map_eq_zero_iff, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
V : Type uV
inst : AddCommMonoid V
R : Type u_1
inst_1 : Semiring R
inst_2 : Module R V
inst_3 : Projective R V
v : V
hv : v = 0
⊢ ∀ (φ : Dual R V), Eq.{u_1 + 1} (α := R) ((φ : (a : V) → R) v : R) (0 : R)

Tactic:
simp [hv]
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
V : Type uV
inst : AddCommMonoid V
R : Type u_1
inst_1 : Semiring R
inst_2 : Module R V
inst_3 : Projective R V
v : V
refine : ∀ (h : ∀ (φ : Dual R V), Eq.{u_1 + 1} (α := R) ((φ : (a : V) → R) v : R) (0 : R)), v = 0
⊢ (∀ (φ : Dual R V), Eq.{u_1 + 1} (α := R) ((φ : (a : V) → R) v : R) (0 : R)) ↔ v = 0

Tactic:
refine ⟨fun h ↦ ?_, fun hv ↦ by simp [hv]⟩
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
V : Type uV
inst : AddCommMonoid V
R : Type u_1
inst_1 : Semiring R
inst_2 : Module R V
inst_3 : Projective R V
v : V
h : ∀ (φ : Dual R V), Eq.{u_1 + 1} (α := R) ((φ : (a : V) → R) v : R) (0 : R)
contrapose! : ∀ (h : v ≠ 0), ∃ (φ : Dual R V), Ne.{u_1 + 1} (α := R) ((φ : (a : V) → R) v : R) (0 : R)
⊢ v = 0

Tactic:
contrapose! h
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
V : Type uV
inst : AddCommMonoid V
R : Type u_1
inst_1 : Semiring R
inst_2 : Module R V
inst_3 : Projective R V
v : V
h : v ≠ 0
⊢ ∃ (φ : Dual R V), Ne.{u_1 + 1} (α := R) ((φ : (a : V) → R) v : R) (0 : R)

Tactic:
Projective.exists_dual_ne_zero R h

Premises used: Module.Projective.exists_dual_ne_zero
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
V : Type uV
inst : AddCommMonoid V
R : Type u_1
inst_1 : Semiring R
inst_2 : Module R V
inst_3 : Projective R V
v : V
h : v ≠ 0
⊢ ∃ (φ : Dual R V), Ne.{u_1 + 1} (α := R) ((φ : (a : V) → R) v : R) (0 : R)

Tactic:
exact Projective.exists_dual_ne_zero R h

Premises used: Module.Projective.exists_dual_ne_zero
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
V : Type uV
inst : AddCommMonoid V
K : Type u_1
inst_1 : Semifield K
inst_2 : Module K V
inst_3 : Projective K V
x : V
hx : x ≠ 0
⊢ ∃ (f : Dual K V), Eq.{u_1 + 1} (α := K) ((f : (a : V) → K) x : K) (1 : K)

Tactic:
have ⟨f, hf⟩ := exists_dual_ne_zero K hx
  ⟨(f x)⁻¹ • f, inv_mul_cancel₀ hf⟩

Premises used: _private.0.Module.Projective.exists_dual_eq_one.match_1, Exists, Inv.inv, Exists.intro, Module.Projective.exists_dual_ne_zero, HSMul.hSMul, OfNat.ofNat, Eq, DFunLike.coe, inv_mul_cancel₀
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
⊢ Subsingleton (Dual K V) ↔ Subsingleton V

Tactic:
⟨fun _ ↦ ⟨fun _ _ ↦ eval_apply_injective K (Subsingleton.elim ..)⟩, fun _ ↦ inferInstance⟩

Premises used: Module.eval_apply_injective, inferInstance, Subsingleton.intro, Iff.intro, Subsingleton.elim, DFunLike.coe, Module.Dual.eval
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
contrapose! : Subsingleton (Dual K V) ↔ Subsingleton V
⊢ Nontrivial (Dual K V) ↔ Nontrivial V

Tactic:
contrapose!
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
⊢ Subsingleton (Dual K V) ↔ Subsingleton V

Tactic:
subsingleton_dual_iff K

Premises used: Module.subsingleton_dual_iff
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
⊢ Subsingleton (Dual K V) ↔ Subsingleton V

Tactic:
exact subsingleton_dual_iff K

Premises used: Module.subsingleton_dual_iff
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : Nontrivial V
⊢ Nontrivial (Dual K V)

Tactic:
(nontrivial_dual_iff K).mpr inferInstance

Premises used: Iff.mpr, inferInstance, Module.nontrivial_dual_iff
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Free K V
⊢ Module.Finite K (Dual K V) ↔ Module.Finite K V

Tactic:
⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Free K V
refine : ∀ (h : Module.Finite K (Dual K V)), Module.Finite K V
⊢ Module.Finite K (Dual K V) ↔ Module.Finite K V

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Free K V
h : Module.Finite K (Dual K V)
have : ∀ (ι : Type uV) (b : Basis ι K V), Module.Finite K V
⊢ Module.Finite K V

Tactic:
have ⟨⟨ι, b⟩⟩ := Free.exists_basis (R := K) (M := V)
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
inl : Finite ι → Module.Finite K V
inr : Infinite ι → Module.Finite K V
⊢ Module.Finite K V

Tactic:
cases finite_or_infinite ι

Premises used: finite_or_infinite
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
h_1 : Finite ι
⊢ Module.Finite K V

Tactic:
.of_basis b

Premises used: Module.Finite.of_basis
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
h_1 : Finite ι
⊢ Module.Finite K V

Tactic:
exact .of_basis b
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
h_1 : Infinite ι
⊢ Nontrivial K

Tactic:
nontriviality K
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
h_1 : Infinite ι
h_2 : Nontrivial K
have :
  ∀ (n : ℕ)
    (hn :
      ∀ (f : Dual K V →ₗ[K] Fin n → K),
        ¬Function.Surjective (α := Dual K V) (β := Fin n → K) (⇑f : (a : Dual K V) → Fin n → K)),
    Module.Finite K V
⊢ Module.Finite K V

Tactic:
have ⟨n, hn⟩ := Module.Finite.exists_nat_not_surjective K (Dual K V)
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
h_1 : Infinite ι
h_2 : Nontrivial K
n : ℕ
hn :
  ∀ (f : Dual K V →ₗ[K] Fin n → K),
    ¬Function.Surjective (α := Dual K V) (β := Fin n → K) (⇑f : (a : Dual K V) → Fin n → K)
g : (ι → K) ≃ₗ[K] Dual K V := Finsupp.llift K K K ι ≪≫ₗ b.repr.dualMap
⊢ Module.Finite K V

Tactic:
hn (LinearMap.funLeft K K (Fin.valEmbedding.trans (Infinite.natEmbedding ι)) ∘ₗ _)
    ((Function.Embedding.injective _).surjective_comp_right.comp g.symm.surjective) |>.elim

Premises used: LinearEquiv.symm, Fin.valEmbedding, False.elim, LinearEquiv.surjective, Function.Injective.surjective_comp_right, LinearMap.comp, Function.Embedding.trans, LinearMap.funLeft, Function.Embedding.injective, Function.Surjective.comp, DFunLike.coe, Infinite.natEmbedding
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
h_1 : Infinite ι
h_2 : Nontrivial K
n : ℕ
hn :
  ∀ (f : Dual K V →ₗ[K] Fin n → K),
    ¬Function.Surjective (α := Dual K V) (β := Fin n → K) (⇑f : (a : Dual K V) → Fin n → K)
g : (ι → K) ≃ₗ[K] Dual K V := Finsupp.llift K K K ι ≪≫ₗ b.repr.dualMap
⊢ Module.Finite K V

Tactic:
exact hn (LinearMap.funLeft K K (Fin.valEmbedding.trans (Infinite.natEmbedding ι)) ∘ₗ _)
    ((Function.Embedding.injective _).surjective_comp_right.comp g.symm.surjective) |>.elim

Premises used: LinearEquiv.symm, Fin.valEmbedding, False.elim, LinearEquiv.surjective, Function.Injective.surjective_comp_right, LinearMap.comp, Function.Embedding.trans, LinearMap.funLeft, Function.Embedding.injective, Function.Surjective.comp, DFunLike.coe, Infinite.natEmbedding
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Free K V
inst_4 : Module.Finite K V
⊢ Module.rank K (Dual K V) = lift.{uK, uV} (Module.rank K V)

Tactic:
(Free.chooseBasis K V).dual_rank_eq

Premises used: Module.Basis.dual_rank_eq, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
R : Type u_1
M : Type u_2
N : Type u_3
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : IsReflexive R M
inst_10 : Module.Finite R N
inst_11 : Projective R N
⊢ IsReflexive R N

Tactic:
have ⟨_, f, hf⟩ := Finite.exists_fin' R N
  have ⟨g, H⟩ := projective_lifting_property f .id hf
  .of_split g f H

Premises used: LinearMap.id, Module.IsReflexive, _private.0.Module.instIsReflexiveOfFiniteOfProjective.match_1, Module.IsReflexive.of_split, _private.0.Module.instIsReflexiveOfFiniteOfProjective.match_2, Module.projective_lifting_property, Module.Finite.exists_fin'
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
R : Type u_1
M : Type u_2
N : Type u_3
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : IsReflexive R M
inst_10 : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  LinearEquiv.dualMap (dualProdDualEquivDual R M N) ≪≫ₗ LinearEquiv.symm (dualProdDualEquivDual R (Dual R M) (Dual R N))
hl :
  ∀ (m : M) (f : Dual R (M × N)),
    Eq.{u_1 + 1} (α := R)
      ((((Dual.eval R (M × N) ∘ₗ inl R M N : (a : M) → Dual R (Dual R (M × N))) m : Dual R (Dual R (M × N))) :
            (a : Dual R (M × N)) → R)
          f :
        R)
      ((((((↑e.symm : Dual R (Dual R M) × Dual R (Dual R N) →ₗ[R] Dual R (Dual R (M × N))) ∘ₗ
                      prodMap (Dual.eval R M) (Dual.eval R N)) ∘ₗ
                    inl R M N :
                  (a : M) → Dual R (Dual R (M × N)))
                m :
              Dual R (Dual R (M × N))) :
            (a : Dual R (M × N)) → R)
          f :
        R)
hr :
  ∀ (m : N) (f : Dual R (M × N)),
    Eq.{u_1 + 1} (α := R)
      ((((Dual.eval R (M × N) ∘ₗ inr R M N : (a : N) → Dual R (Dual R (M × N))) m : Dual R (Dual R (M × N))) :
            (a : Dual R (M × N)) → R)
          f :
        R)
      ((((((↑e.symm : Dual R (Dual R M) × Dual R (Dual R N) →ₗ[R] Dual R (Dual R (M × N))) ∘ₗ
                      prodMap (Dual.eval R M) (Dual.eval R N)) ∘ₗ
                    inr R M N :
                  (a : N) → Dual R (Dual R (M × N)))
                m :
              Dual R (Dual R (M × N))) :
            (a : Dual R (M × N)) → R)
          f :
        R)
⊢ Dual.eval R (M × N) =
    (↑e.symm : Dual R (Dual R M) × Dual R (Dual R N) →ₗ[R] Dual R (Dual R (M × N))) ∘ₗ
      prodMap (Dual.eval R M) (Dual.eval R N)

Tactic:
ext m f
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
R : Type u_1
M : Type u_2
N : Type u_3
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : IsReflexive R M
inst_10 : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  LinearEquiv.dualMap (dualProdDualEquivDual R M N) ≪≫ₗ LinearEquiv.symm (dualProdDualEquivDual R (Dual R M) (Dual R N))
m : M
f : Dual R (M × N)
⊢ Eq.{u_1 + 1} (α := R)
    ((((Dual.eval R (M × N) ∘ₗ inl R M N : (a : M) → Dual R (Dual R (M × N))) m : Dual R (Dual R (M × N))) :
          (a : Dual R (M × N)) → R)
        f :
      R)
    ((((((↑e.symm : Dual R (Dual R M) × Dual R (Dual R N) →ₗ[R] Dual R (Dual R (M × N))) ∘ₗ
                    prodMap (Dual.eval R M) (Dual.eval R N)) ∘ₗ
                  inl R M N :
                (a : M) → Dual R (Dual R (M × N)))
              m :
            Dual R (Dual R (M × N))) :
          (a : Dual R (M × N)) → R)
        f :
      R)

Tactic:
simp [e]
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
R : Type u_1
M : Type u_2
N : Type u_3
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : IsReflexive R M
inst_10 : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  LinearEquiv.dualMap (dualProdDualEquivDual R M N) ≪≫ₗ LinearEquiv.symm (dualProdDualEquivDual R (Dual R M) (Dual R N))
m : N
f : Dual R (M × N)
⊢ Eq.{u_1 + 1} (α := R)
    ((((Dual.eval R (M × N) ∘ₗ inr R M N : (a : N) → Dual R (Dual R (M × N))) m : Dual R (Dual R (M × N))) :
          (a : Dual R (M × N)) → R)
        f :
      R)
    ((((((↑e.symm : Dual R (Dual R M) × Dual R (Dual R N) →ₗ[R] Dual R (Dual R (M × N))) ∘ₗ
                    prodMap (Dual.eval R M) (Dual.eval R N)) ∘ₗ
                  inr R M N :
                (a : N) → Dual R (Dual R (M × N)))
              m :
            Dual R (Dual R (M × N))) :
          (a : Dual R (M × N)) → R)
        f :
      R)

Tactic:
simp [e]
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
R : Type u_1
M : Type u_2
N : Type u_3
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : IsReflexive R M
inst_10 : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  LinearEquiv.dualMap (dualProdDualEquivDual R M N) ≪≫ₗ LinearEquiv.symm (dualProdDualEquivDual R (Dual R M) (Dual R N))
⊢ Dual.eval R (M × N) =
    (↑e.symm : Dual R (Dual R M) × Dual R (Dual R N) →ₗ[R] Dual R (Dual R (M × N))) ∘ₗ
      prodMap (Dual.eval R M) (Dual.eval R N)

Tactic:
have : Dual.eval R (M × N) = e.symm.comp ((Dual.eval R M).prodMap (Dual.eval R N)) := by
      ext m f <;> simp [e]
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
R : Type u_1
M : Type u_2
N : Type u_3
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : IsReflexive R M
inst_10 : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  LinearEquiv.dualMap (dualProdDualEquivDual R M N) ≪≫ₗ LinearEquiv.symm (dualProdDualEquivDual R (Dual R M) (Dual R N))
this :
  Dual.eval R (M × N) =
    (↑e.symm : Dual R (Dual R M) × Dual R (Dual R N) →ₗ[R] Dual R (Dual R (M × N))) ∘ₗ
      prodMap (Dual.eval R M) (Dual.eval R N)
simp :
  Bijective (α := M × N) (β := Dual R (Dual R M) × Dual R (Dual R N))
    (⇑(prodMap (Dual.eval R M) (Dual.eval R N)) : (a : M × N) → Dual R (Dual R M) × Dual R (Dual R N))
⊢ Bijective (α := M × N) (β := Dual R (Dual R (M × N))) (⇑(Dual.eval R (M × N)) : (a : M × N) → Dual R (Dual R (M × N)))

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

Premises used: EquivLike.comp_bijective, LinearMap.coe_comp, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
R : Type u_1
M : Type u_2
N : Type u_3
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : IsReflexive R M
inst_10 : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  LinearEquiv.dualMap (dualProdDualEquivDual R M N) ≪≫ₗ LinearEquiv.symm (dualProdDualEquivDual R (Dual R M) (Dual R N))
this :
  Dual.eval R (M × N) =
    (↑e.symm : Dual R (Dual R M) × Dual R (Dual R N) →ₗ[R] Dual R (Dual R (M × N))) ∘ₗ
      prodMap (Dual.eval R M) (Dual.eval R N)
⊢ Bijective (α := M × N) (β := Dual R (Dual R M) × Dual R (Dual R N))
    (⇑(prodMap (Dual.eval R M) (Dual.eval R N)) : (a : M × N) → Dual R (Dual R M) × Dual R (Dual R N))

Tactic:
(bijective_dual_eval R M).prodMap (bijective_dual_eval R N)

Premises used: Prod.map, Module.bijective_dual_eval, Function.prod, Function.Bijective.prodMap
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
R : Type u_1
M : Type u_2
N : Type u_3
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : IsReflexive R M
inst_10 : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  LinearEquiv.dualMap (dualProdDualEquivDual R M N) ≪≫ₗ LinearEquiv.symm (dualProdDualEquivDual R (Dual R M) (Dual R N))
this :
  Dual.eval R (M × N) =
    (↑e.symm : Dual R (Dual R M) × Dual R (Dual R N) →ₗ[R] Dual R (Dual R (M × N))) ∘ₗ
      prodMap (Dual.eval R M) (Dual.eval R N)
⊢ Bijective (α := M × N) (β := Dual R (Dual R M) × Dual R (Dual R N))
    (⇑(prodMap (Dual.eval R M) (Dual.eval R N)) : (a : M × N) → Dual R (Dual R M) × Dual R (Dual R N))

Tactic:
exact (bijective_dual_eval R M).prodMap (bijective_dual_eval R N)

Premises used: Module.bijective_dual_eval, Function.Bijective.prodMap
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
R : Type u_1
M : Type u_2
N : Type u_3
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : IsReflexive R M
⊢ IsReflexive R (ULift.{w, u_2} M)

Tactic:
equiv ULift.moduleEquiv.symm

Premises used: LinearEquiv.symm, Module.equiv, ULift.moduleEquiv
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K_1 : Type uK
V_1 : Type uV
inst : CommSemiring K_1
inst_1 : AddCommMonoid V_1
inst_2 : Module K_1 V_1
inst_3 : Projective K_1 V_1
R : Type u_1
M : Type u_2
N : Type u_3
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : IsReflexive R M
K : Type u_4
V : Type u_5
inst_10 : Field K
inst_11 : AddCommGroup V
inst_12 : Module K V
inst_13 : IsReflexive K V
rw : Module.rank K V < ℵ₀
⊢ FiniteDimensional K V

Tactic:
rw [FiniteDimensional, ← rank_lt_aleph0_iff]

Premises used: Module.rank_lt_aleph0_iff, FiniteDimensional