awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M₁ →ₗ[R] M₂
x : Dual R M₂
h :
  Eq (α := Dual R M₁) ((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) (0 : Dual R M₁) ↔
    x ∈ f.range.dualAnnihilator
h₁ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    x ∈ f.range.dualAnnihilator
h₂ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    ∀ w ∈ f.range, Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) w : R) (0 : R)
h₃ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    ∀ w ∈ (↑f.range : Set M₂), Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) w : R) (0 : R)
⊢ x ∈ f.dualMap.ker ↔ x ∈ f.range.dualAnnihilator
have h₄ : (∀ (x_1 : M₁),
    Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
      ((0 : (a : M₁) → R) x_1 : R)) ↔
  ∀ (w : M₂),
    Membership.mem (γ := Set M₂) (Set.range.{u_3, u_2 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) w →
      Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) w : R) (0 : R)
Tactic: simp_rw [mem_ker, LinearMap.ext_iff, Submodule.mem_dualAnnihilator,
    ← SetLike.mem_coe, coe_range, Set.forall_mem_range, dualMap_apply, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M₁ →ₗ[R] M₂
x : Dual R M₂
h :
  Eq (α := Dual R M₁) ((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) (0 : Dual R M₁) ↔
    x ∈ f.range.dualAnnihilator
h₁ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    x ∈ f.range.dualAnnihilator
h₂ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    ∀ w ∈ f.range, Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) w : R) (0 : R)
h₃ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    ∀ w ∈ (↑f.range : Set M₂), Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) w : R) (0 : R)
h₄ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    ∀ (w : M₂),
      Membership.mem (γ := Set M₂) (Set.range.{u_3, u_2 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) w →
        Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) w : R) (0 : R)
⊢ x ∈ f.dualMap.ker ↔ x ∈ f.range.dualAnnihilator
have h₅ : (∀ (x_1 : M₁),
    Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
      ((0 : (a : M₁) → R) x_1 : R)) ↔
  ∀ (i : M₁), Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) ((f : (a : M₁) → M₂) i : M₂) : R) (0 : R)
Tactic: simp_rw [mem_ker, LinearMap.ext_iff, Submodule.mem_dualAnnihilator,
    ← SetLike.mem_coe, coe_range, Set.forall_mem_range, dualMap_apply, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M₁ →ₗ[R] M₂
x : Dual R M₂
h :
  Eq (α := Dual R M₁) ((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) (0 : Dual R M₁) ↔
    x ∈ f.range.dualAnnihilator
h₁ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    x ∈ f.range.dualAnnihilator
h₂ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    ∀ w ∈ f.range, Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) w : R) (0 : R)
h₃ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    ∀ w ∈ (↑f.range : Set M₂), Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) w : R) (0 : R)
h₄ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    ∀ (w : M₂),
      Membership.mem (γ := Set M₂) (Set.range.{u_3, u_2 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) w →
        Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) w : R) (0 : R)
h₅ :
  (∀ (x_1 : M₁),
      Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
        ((0 : (a : M₁) → R) x_1 : R)) ↔
    ∀ (i : M₁), Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) ((f : (a : M₁) → M₂) i : M₂) : R) (0 : R)
⊢ x ∈ f.dualMap.ker ↔ x ∈ f.range.dualAnnihilator
have h₆ : (∀ (x_1 : M₁),
    Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) ((f : (a : M₁) → M₂) x_1 : M₂) : R) ((0 : (a : M₁) → R) x_1 : R)) ↔
  ∀ (i : M₁), Eq.{u_1 + 1} (α := R) ((x : (a : M₂) → R) ((f : (a : M₁) → M₂) i : M₂) : R) (0 : R)
Tactic: simp_rw [mem_ker, LinearMap.ext_iff, Submodule.mem_dualAnnihilator,
    ← SetLike.mem_coe, coe_range, Set.forall_mem_range, dualMap_apply, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
⊢ f.dualMap.ker = (Dual.eval R M' ∘ₗ f).range.dualCoannihilator
have h : ∀ (x : Dual R M'), x ∈ f.dualMap.ker ↔ x ∈ (Dual.eval R M' ∘ₗ f).range.dualCoannihilator
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B : M →ₗ[R] M' →ₗ[R] R
⊢ B.range.dualCoannihilator = B.flip.ker
have h : ∀ (x : M'), x ∈ B.range.dualCoannihilator ↔ x ∈ B.flip.ker
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type uK
V : Type uV
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
⊢ Nonempty (V ≃ₗ[K] Dual K V) ↔ FiniteDimensional K V
have refine : Nonempty (V ≃ₗ[K] Dual K V) → ∀ (e : V ≃ₗ[K] Dual K V), FiniteDimensional K V
Tactic: refine ⟨fun ⟨e⟩ ↦ ?_, fun h ↦ ⟨(Module.Free.chooseBasis K V).toDualEquiv⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type uK
V : Type uV
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
⊢ FiniteDimensional K V
have rw : Module.rank K V < ℵ₀
Tactic: rw [FiniteDimensional, ← Module.rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type uK
V : Type uV
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
⊢ Module.rank K V < ℵ₀
have by_contra! : ∀ (this : ℵ₀ ≤ Module.rank K V), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type uK
V : Type uV
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this : ℵ₀ ≤ Module.rank K V
⊢ False
have apply : lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)
Tactic: apply (lift_rank_lt_rank_dual this).ne
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
Goal:
K : Type uK
V : Type uV
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this : ℵ₀ ≤ Module.rank K V
⊢ lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)
have this₁ : lift.{max uK uV, uV} (Module.rank K V) = lift.{uV, max uK uV} (Module.rank K (Dual K V))
Tactic: have := e.lift_rank_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type uK
V : Type uV
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this_1 : ℵ₀ ≤ Module.rank K V
this : lift.{max uK uV, uV} (Module.rank K V) = lift.{uV, max uK uV} (Module.rank K (Dual K V))
⊢ lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)
have rwa : ∀ (this : lift.{uK, uV} (Module.rank K V) = lift.{uV, max uK uV} (Module.rank K (Dual K V))),
  lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)
Tactic: rwa [lift_umax, lift_id'.{uV}] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type uK
V : Type uV
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this_1 : ℵ₀ ≤ Module.rank K V
this : lift.{max uK uV, uV} (Module.rank K V) = lift.{uV, max uK uV} (Module.rank K (Dual K V))
rwa :
  ∀ (this : lift.{uK, uV} (Module.rank K V) = lift.{uV, max uK uV} (Module.rank K (Dual K V))),
    lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)
⊢ lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)
have rwa₁ : ∀ (this : lift.{uK, uV} (Module.rank K V) = Module.rank K (Dual K V)),
  lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)
Tactic: rwa [lift_umax, lift_id'.{uV}] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
b : Basis ι R M
⊢ Module.rank R (Dual R M) = lift.{uR, uM} (Module.rank R M)
have rw : Module.rank R (Dual R M) = lift.{max uM uR, uM} (Module.rank R M)
Tactic: rw [← lift_umax.{uM, uR}, b.toDualEquiv.lift_rank_eq, lift_id'.{uM, uR}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
b : Basis ι R M
rw : Module.rank R (Dual R M) = lift.{max uM uR, uM} (Module.rank R M)
⊢ Module.rank R (Dual R M) = lift.{uR, uM} (Module.rank R M)
have rw₁ : Module.rank R (Dual R M) = lift.{uM, max uM uR} (Module.rank R (Dual R M))
Tactic: rw [← lift_umax.{uM, uR}, b.toDualEquiv.lift_rank_eq, lift_id'.{uM, uR}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
b : Basis ι R M
rw : Module.rank R (Dual R M) = lift.{max uM uR, uM} (Module.rank R M)
rw₁ : Module.rank R (Dual R M) = lift.{uM, max uM uR} (Module.rank R (Dual R M))
⊢ Module.rank R (Dual R M) = lift.{uR, uM} (Module.rank R M)
have rw₂ : Module.rank R (Dual R M) = Module.rank R (Dual R M)
Tactic: rw [← lift_umax.{uM, uR}, b.toDualEquiv.lift_rank_eq, lift_id'.{uM, uR}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
b : Basis ι R M
⊢ Module.rank R (Dual R M) = lift.{uR, uM} (Module.rank R M)
have classical : Module.rank R (Dual R M) = lift.{max uM uR, uM} (Module.rank R M)
Tactic: classical rw [← lift_umax.{uM, uR}, b.toDualEquiv.lift_rank_eq, lift_id'.{uM, uR}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
b : Basis ι R M
classical : Module.rank R (Dual R M) = lift.{max uM uR, uM} (Module.rank R M)
⊢ Module.rank R (Dual R M) = lift.{uR, uM} (Module.rank R M)
have classical₁ : Module.rank R (Dual R M) = lift.{uM, max uM uR} (Module.rank R (Dual R M))
Tactic: classical rw [← lift_umax.{uM, uR}, b.toDualEquiv.lift_rank_eq, lift_id'.{uM, uR}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
b : Basis ι R M
classical : Module.rank R (Dual R M) = lift.{max uM uR, uM} (Module.rank R M)
classical₁ : Module.rank R (Dual R M) = lift.{uM, max uM uR} (Module.rank R (Dual R M))
⊢ Module.rank R (Dual R M) = lift.{uR, uM} (Module.rank R M)
have classical₂ : Module.rank R (Dual R M) = Module.rank R (Dual R M)
Tactic: classical rw [← lift_umax.{uM, uR}, b.toDualEquiv.lift_rank_eq, lift_id'.{uM, uR}]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ (∀ (φ : Dual R V), Eq.{u_1 + 1} (α := R) ((φ : (a : V) → R) v : R) (0 : R)) ↔ v = 0
have refine : ∀ (h : ∀ (φ : 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]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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)
⊢ v = 0
have contrapose! : ∀ (h : v ≠ 0), ∃ (φ : Dual R V), Ne.{u_1 + 1} (α := R) ((φ : (a : V) → R) v : R) (0 : R)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type uK
V : Type uV
inst : CommSemiring K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
⊢ Nontrivial (Dual K V) ↔ Nontrivial V
have contrapose! : Subsingleton (Dual K V) ↔ Subsingleton V
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
have refine : ∀ (h : Module.Finite K (Dual K V)), Module.Finite K V
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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)
⊢ Module.Finite K V
have have : ∀ (ι : Type uV) (b : Basis ι K V), Module.Finite K V
Tactic: have ⟨⟨ι, b⟩⟩ := Free.exists_basis (R := K) (M := V)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ Module.Finite K V
have inl : Finite ι → Module.Finite K V
Tactic: cases finite_or_infinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ Module.Finite K V
have inr : Infinite ι → Module.Finite K V
Tactic: cases finite_or_infinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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 ι
⊢ Module.Finite K V
have a : Nontrivial K
Tactic: nontriviality K
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ Module.Finite K V
have 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
Tactic: have ⟨n, hn⟩ := Module.Finite.exists_nat_not_surjective K (Dual K V)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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)
have 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)
Tactic: ext m f
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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)
⊢ 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)
have 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)
Tactic: ext m f
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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))
⊢ Bijective (α := M × N) (β := Dual R (Dual R (M × N))) (⇑(Dual.eval R (M × N)) : (a : M × N) → Dual R (Dual R (M × N)))
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 × N))) (⇑(Dual.eval R (M × N)) : (a : M × N) → Dual R (Dual R (M × N)))
have 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))
Tactic: simp only [this,
      coe_comp, LinearEquiv.coe_coe, EquivLike.comp_bijective]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ FiniteDimensional K V
have rw : Module.rank K V < ℵ₀
Tactic: rw [FiniteDimensional, ← rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ Module.rank K V < ℵ₀
have by_contra! : ∀ (contra : ℵ₀ ≤ Module.rank K V), False
Tactic: by_contra! contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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
contra : ℵ₀ ≤ Module.rank K V
this : lift.{u_4, u_5} (Module.rank K V) < Module.rank K (Dual K (Dual K V))
⊢ False
have heq : lift.{max u_5 u_4, u_5} (Module.rank K V) = lift.{u_5, max u_5 u_4} (Module.rank K (Dual K (Dual K V)))
Tactic: have heq := lift_rank_eq_of_equiv_equiv (R := K) (R' := K) (M := V) (M' := Dual K (Dual K V))
      (ZeroHom.id K) (evalEquiv K V) bijective_id (fun r v ↦ (evalEquiv K V).map_smul _ _)