-- Mathlib/LinearAlgebra/Dual.lean
theorem finite_dual_iff [Free K V] : Module.Finite K (Dual K V) ↔ Module.Finite K V

Proof state:
case mk.intro
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
ι : Type uV
b : Basis ι K V
a✝ : Nontrivial K
s : Finset (Dual K V)
span_s : span K ↑s = ⊤
⊢ Module.Finite K V

Tactic:
haveI := (b.linearIndependent.map' _ b.toDual_ker).finite_of_le_span_finite _ s ?_

Result:
case mk.intro.refine_2
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
ι : Type uV
b : Basis ι K V
a✝ : Nontrivial K
s : Finset (Dual K V)
span_s : span K ↑s = ⊤
this : Finite ι
⊢ Module.Finite K V

case mk.intro.refine_1
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
ι : Type uV
b : Basis ι K V
a✝ : Nontrivial K
s : Finset (Dual K V)
span_s : span K ↑s = ⊤
⊢ Set.range (⇑b.toDual ∘ ⇑b) ≤ ↑(span K ↑s)

Proof state:
case mk.intro.refine_2
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
ι : Type uV
b : Basis ι K V
a✝ : Nontrivial K
s : Finset (Dual K V)
span_s : span K ↑s = ⊤
this : Finite ι
⊢ Module.Finite K V

Tactic:
exact Finite.of_basis b

Result:
no goals

Proof state:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ Module.Finite K (Dual K V) ↔ Module.Finite K V

Tactic:
constructor <;> intro h

Result:
case mp
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : Module.Finite K (Dual K V)
⊢ Module.Finite K V

case mpr
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : Module.Finite K V
⊢ Module.Finite K (Dual K V)

Proof state:
case mpr
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : Module.Finite K V
⊢ Module.Finite K (Dual K V)

Tactic:
infer_instance

Result:
no goals

Proof state:
case mk.intro.refine_1
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
ι : Type uV
b : Basis ι K V
a✝ : Nontrivial K
s : Finset (Dual K V)
span_s : span K ↑s = ⊤
⊢ Set.range (⇑b.toDual ∘ ⇑b) ≤ ↑⊤

Tactic:
apply le_top

Result:
no goals

Proof state:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
a✝ : Nontrivial K
⊢ Module.Finite K V

Tactic:
obtain ⟨⟨s, span_s⟩⟩ := h

Result:
case mk.intro
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
ι : Type uV
b : Basis ι K V
a✝ : Nontrivial K
s : Finset (Dual K V)
span_s : span K ↑s = ⊤
⊢ Module.Finite K V

Proof state:
case mp
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : Module.Finite K (Dual K V)
⊢ Module.Finite K V

Tactic:
obtain ⟨⟨ι, b⟩⟩ := Free.exists_basis (R := K) (M := V)

Result:
case mp.intro.mk
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
⊢ Module.Finite K V

Proof state:
case mp.intro.mk
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
⊢ Module.Finite K V

Tactic:
nontriviality K

Result:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : Module.Finite K (Dual K V)
ι : Type uV
b : Basis ι K V
a✝ : Nontrivial K
⊢ Module.Finite K V

Proof state:
case mk.intro.refine_1
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
ι : Type uV
b : Basis ι K V
a✝ : Nontrivial K
s : Finset (Dual K V)
span_s : span K ↑s = ⊤
⊢ Set.range (⇑b.toDual ∘ ⇑b) ≤ ↑(span K ↑s)

Tactic:
rw [span_s]

Result:
case mk.intro.refine_1
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
ι : Type uV
b : Basis ι K V
a✝ : Nontrivial K
s : Finset (Dual K V)
span_s : span K ↑s = ⊤
⊢ Set.range (⇑b.toDual ∘ ⇑b) ≤ ↑⊤