awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
x_1 : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi (φ := fun (a : ι) ↦ 𝕜) L
p : Submodule 𝕜 E := ⨅ (i : ι), (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : FiniteDimensional.{u_4, u_5} 𝕜 (E ⧸ p)
L' : (i : ι) → LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := fun (i : ι) ↦ p.liftQ (L i) ⋯
K' : LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := p.liftQ K h
this : ⨅ (i : ι), (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
x : E
⊢ Eq.{u_4 + 1} (α := 𝕜) ((∑ i : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ : (a : E) → 𝕜) x : 𝕜)
    ((∑ i : ι, c i • L' i : (a : E ⧸ p) → 𝕜) ((p.mkQ : (a : E) → E ⧸ p) x : E ⧸ p) : 𝕜)

Tactic:
simp only [L', LinearMap.coe_sum, Finset.sum_apply, smul_apply, coe_comp, Function.comp_apply,
    smul_eq_mul]

Premises used: LinearMap.smul_apply, Finset.sum_apply, LinearMap.coe_sum, LinearMap.coe_comp, Function.comp_apply, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
⊢ (dualAnnihilator W).dualCoannihilator = W

Tactic:
le_antisymm (fun v ↦ Function.mtr ?_) (le_dualAnnihilator_dualCoannihilator _)

Premises used: Submodule.le_dualAnnihilator_dualCoannihilator, le_antisymm, Function.mtr
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
refine : ∀ v ∉ W, v ∉ (dualAnnihilator W).dualCoannihilator
⊢ (dualAnnihilator W).dualCoannihilator = W

Tactic:
refine le_antisymm (fun v ↦ Function.mtr ?_) (le_dualAnnihilator_dualCoannihilator _)

Premises used: Submodule.le_dualAnnihilator_dualCoannihilator, le_antisymm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
simp :
  v ∉ W →
    ¬∀ (φ : Dual K V),
        (∀ w ∈ W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) w : K) (0 : K)) →
          Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)
⊢ v ∉ W → v ∉ (dualAnnihilator W).dualCoannihilator

Tactic:
simp only [mem_dualAnnihilator, mem_dualCoannihilator]

Premises used: Submodule.mem_dualAnnihilator, Submodule.mem_dualCoannihilator
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
rw :
  (¬∀ (φ : Dual.{u_1, u_2} K (V ⧸ W)),
        Eq.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)) →
    ¬∀ (φ : Dual K V),
        (∀ w ∈ W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) w : K) (0 : K)) →
          Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)
⊢ v ∉ W →
    ¬∀ (φ : Dual K V),
        (∀ w ∈ W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) w : K) (0 : K)) →
          Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)

Tactic:
rw [← Quotient.mk_eq_zero W, ← Module.forall_dual_apply_eq_zero_iff K]

Premises used: Module.forall_dual_apply_eq_zero_iff, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
push :
  (∃ (φ : Dual.{u_1, u_2} K (V ⧸ W)),
      Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)) →
    ∃ (φ : Dual K V),
      (∀ w ∈ W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) w : K) (0 : K)) ∧
        Ne.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)
⊢ (¬∀ (φ : Dual.{u_1, u_2} K (V ⧸ W)),
        Eq.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)) →
    ¬∀ (φ : Dual K V),
        (∀ w ∈ W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) w : K) (0 : K)) →
          Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
⊢ (∃ (φ : Dual.{u_1, u_2} K (V ⧸ W)),
      Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)) →
    ∃ (φ : Dual K V),
      (∀ w ∈ W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) w : K) (0 : K)) ∧
        Ne.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)

Tactic:
fun ⟨φ, hφ⟩ ↦ ⟨φ.comp W.mkQ, fun w hw ↦ ?_, hφ⟩

Premises used: Exists, Ne, LinearMap.comp, And, And.intro, Exists.intro, Submodule.mkQ, OfNat.ofNat, DFunLike.coe, _private.0.Subspace.dualAnnihilator_dualCoannihilator_eq.match_2
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
refine :
  (∃ (φ : Dual.{u_1, u_2} K (V ⧸ W)),
      Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)) →
    ∀ (φ : Dual.{u_1, u_2} K (V ⧸ W))
      (hφ : Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)) (w : V) (hw : w ∈ W),
      Eq.{u_1 + 1} (α := K) ((φ ∘ₗ mkQ W : (a : V) → K) w : K) (0 : K)
⊢ (∃ (φ : Dual.{u_1, u_2} K (V ⧸ W)),
      Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)) →
    ∃ (φ : Dual K V),
      (∀ w ∈ W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) w : K) (0 : K)) ∧
        Ne.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)

Tactic:
refine fun ⟨φ, hφ⟩ ↦ ⟨φ.comp W.mkQ, fun w hw ↦ ?_, hφ⟩
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
h :
  ∃ (φ : Dual.{u_1, u_2} K (V ⧸ W)), Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)
φ : Dual.{u_1, u_2} K (V ⧸ W)
hφ : Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)
w : V
hw : w ∈ W
rw : Eq.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) ((mkQ W : (a : V) → V ⧸ W) w : V ⧸ W) : K) (0 : K)
rw₁ : Eq.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk w) : K) (0 : K)
rw₂ : Eq.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) 0 : K) (0 : K)
rw₃ rw₄ : Eq.{u_1 + 1} (α := K) 0 0
⊢ Eq.{u_1 + 1} (α := K) ((φ ∘ₗ mkQ W : (a : V) → K) w : K) (0 : K)

Tactic:
rw [comp_apply, mkQ_apply, (Quotient.mk_eq_zero W).mpr hw, φ.map_zero]

Premises used: Iff.mpr, LinearMap.comp_apply, LinearMap.map_zero, Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
rw :
  (∀ φ ∈ dualAnnihilator W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)) ↔
    v ∈ (dualAnnihilator W).dualCoannihilator
rw₁ rw₂ :
  (∀ φ ∈ dualAnnihilator W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)) ↔
    ∀ φ ∈ dualAnnihilator W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)
⊢ (∀ φ ∈ dualAnnihilator W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)) ↔ v ∈ W

Tactic:
rw [← SetLike.ext_iff.mp dualAnnihilator_dualCoannihilator_eq v, mem_dualCoannihilator]

Premises used: SetLike.ext_iff, Submodule.mem_dualCoannihilator, Iff.mp, Subspace.dualAnnihilator_dualCoannihilator_eq
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
h : ∀ (x : V), x ∈ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator ↔ x ∈ W
⊢ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator = W

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
x : V
h :
  (∀ φ ∈ dualAnnihilator W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) x : K) (0 : K)) ↔
    x ∈ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator
⊢ x ∈ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator ↔ x ∈ W

Tactic:
rw [Iff.comm, ← forall_mem_dualAnnihilator_apply_eq_zero_iff]

Premises used: Subspace.forall_mem_dualAnnihilator_apply_eq_zero_iff, Iff.comm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
x : V
⊢ (∀ φ ∈ dualAnnihilator W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) x : K) (0 : K)) ↔
    x ∈ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
⊢ map (σ₁₂ := RingHom.id K) (Dual.eval K V) W ≤ (dualAnnihilator W).dualAnnihilator

Tactic:
map_le_iff_le_comap.mpr (comap_dualAnnihilator_dualAnnihilator W).ge

Premises used: Iff.mpr, Eq.ge, Submodule.map_le_iff_le_comap, Subspace.comap_dualAnnihilator_dualAnnihilator
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W W' : Subspace K V
⊢ dualAnnihilator W ≤ dualAnnihilator W' ↔ W' ≤ W

Tactic:
(dualAnnihilatorGci K V).l_le_l_iff

Premises used: GaloisCoinsertion.l_le_l_iff, Set.Mem, Subspace.dualAnnihilatorGci
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W W' : Subspace K V
⊢ dualAnnihilator W = dualAnnihilator W' ↔ W = W'

Tactic:
⟨fun h ↦ (dualAnnihilatorGci K V).l_injective h, congr_arg _⟩

Premises used: GaloisCoinsertion.l_injective, Subspace.dualAnnihilatorGci, congr_arg, Iff.intro
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
φ : Dual.{u_1, u_2} K ↥W
w : ↥W
⊢ Eq.{u_1 + 1} (α := K) ((((W.dualLift : (a : Dual K ↥W) → Dual K V) φ : Dual K V) : (a : V) → K) (↑w : V) : K)
    ((φ : (a : ↥W) → K) w : K)

Tactic:
congr_arg φ <| LinearMap.leftInverse_apply_of_inj W.ker_subtype _

Premises used: Submodule.ker_subtype, congr_arg, LinearMap.leftInverse_apply_of_inj, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
φ : Dual.{u_1, u_2} K ↥W
w : V
hw : w ∈ W
⊢ Eq.{u_1 + 1} (α := K) ((((W.dualLift : (a : Dual K ↥W) → Dual K V) φ : Dual K V) : (a : V) → K) w : K)
    ((φ : (a : ↥W) → K) (Subtype.mk (p := fun (x : V) ↦ x ∈ W) w hw) : K)

Tactic:
dualLift_of_subtype ⟨w, hw⟩

Premises used: Subspace.dualLift_of_subtype, Subtype.mk
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
h :
  ∀ (φ : Dual.{u_1, u_2} K ↥W) (x : ↥W),
    Eq.{u_1 + 1} (α := K)
      ((((dualRestrict W ∘ₗ W.dualLift : (a : Dual K ↥W) → Dual K ↥W) φ : Dual.{u_1, u_2} K ↥W) : (a : ↥W) → K) x : K)
      ((((1 : (a : Dual K ↥W) → Dual K ↥W) φ : Dual.{u_1, u_2} K ↥W) : (a : ↥W) → K) x : K)
⊢ dualRestrict W ∘ₗ W.dualLift = 1

Tactic:
ext φ x
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
φ : Dual.{u_1, u_2} K ↥W
x : ↥W
⊢ Eq.{u_1 + 1} (α := K)
    ((((dualRestrict W ∘ₗ W.dualLift : (a : Dual K ↥W) → Dual K ↥W) φ : Dual.{u_1, u_2} K ↥W) : (a : ↥W) → K) x : K)
    ((((1 : (a : Dual K ↥W) → Dual K ↥W) φ : Dual.{u_1, u_2} K ↥W) : (a : ↥W) → K) x : K)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
x : Dual.{u_1, u_2} K ↥W
rw : (dualRestrict W ∘ₗ W.dualLift : (a : Dual K ↥W) → Dual K ↥W) x = x
rw₁ : (1 : (a : Dual K ↥W) → Dual K ↥W) x = x
rw₂ rw₃ : x = x
⊢ (dualRestrict W : (a : Dual K V) → Dual K ↥W) ((W.dualLift : (a : Dual K ↥W) → Dual K V) x) = x

Tactic:
rw [← LinearMap.comp_apply, dualRestrict_comp_dualLift, End.one_apply]

Premises used: Subspace.dualRestrict_comp_dualLift, LinearMap.comp_apply, Module.End.one_apply
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
⊢ Function.RightInverse (α := Dual K V) (β := Dual.{u_1, u_2} K ↥W) (⇑W.dualLift : (a : Dual K ↥W) → Dual K V)
    (⇑(dualRestrict W) : (a : Dual K V) → Dual K ↥W)

Tactic:
W.dualRestrict_leftInverse

Premises used: Set.Mem, Subspace.dualRestrict_leftInverse, Function.RightInverse
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
⊢ Function.Surjective (α := Dual K V) (β := Dual.{u_1, u_2} K ↥W) (⇑(dualRestrict W) : (a : Dual K V) → Dual K ↥W)

Tactic:
W.dualLift_rightInverse.surjective

Premises used: Set.Mem, Subspace.dualLift_rightInverse, Function.RightInverse.surjective
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
⊢ Function.Injective (α := Dual.{u_1, u_2} K ↥W) (β := Dual K V) (⇑W.dualLift : (a : Dual K ↥W) → Dual K V)

Tactic:
W.dualRestrict_leftInverse.injective

Premises used: Function.LeftInverse.injective, Set.Mem, Subspace.dualRestrict_leftInverse
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
φ : Dual K V
h :
  ∀ (x : ↥W),
    Eq.{u_1 + 1} (α := K)
      ((((W.quotAnnihilatorEquiv : (a : Dual K V ⧸ dualAnnihilator W) → Dual K ↥W) (Submodule.Quotient.mk φ) :
              Dual.{u_1, u_2} K ↥W) :
            (a : ↥W) → K)
          x :
        K)
      ((((dualRestrict W : (a : Dual K V) → Dual K ↥W) φ : Dual.{u_1, u_2} K ↥W) : (a : ↥W) → K) x : K)
⊢ Eq (α := Dual.{u_1, u_2} K ↥W)
    ((W.quotAnnihilatorEquiv : (a : Dual K V ⧸ dualAnnihilator W) → Dual K ↥W) (Submodule.Quotient.mk φ) :
      Dual.{u_1, u_2} K ↥W)
    ((dualRestrict W : (a : Dual K V) → Dual K ↥W) φ : Dual.{u_1, u_2} K ↥W)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
φ : Dual K V
x : ↥W
⊢ Eq.{u_1 + 1} (α := K)
    ((((W.quotAnnihilatorEquiv : (a : Dual K V ⧸ dualAnnihilator W) → Dual K ↥W) (Submodule.Quotient.mk φ) :
            Dual.{u_1, u_2} K ↥W) :
          (a : ↥W) → K)
        x :
      K)
    ((((dualRestrict W : (a : Dual K V) → Dual K ↥W) φ : Dual.{u_1, u_2} K ↥W) : (a : ↥W) → K) x : K)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
⊢ (↑W.dualEquivDual : Dual K ↥W →ₗ[K] ↥W.dualLift.range) = W.dualLift.rangeRestrict

Tactic:
rfl

Premises used: Set.Mem, LinearMap.codRestrict, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
φ : Dual.{u_1, u_2} K ↥W
⊢ Eq (α := ↥W.dualLift.range) ((W.dualEquivDual : (a : Dual K ↥W) → ↥W.dualLift.range) φ : ↥W.dualLift.range)
    (Subtype.mk (p := fun (x : Dual K V) ↦ x ∈ W.dualLift.range) ((W.dualLift : (a : Dual K ↥W) → Dual K V) φ) ⋯ :
      ↥W.dualLift.range)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
inst_3 : FiniteDimensional K V
⊢ FiniteDimensional K (Dual K V)

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
pos : ∀ (h : FiniteDimensional K V), finrank K (Dual K V) = finrank K V
neg : ∀ (h : ¬FiniteDimensional K V), finrank K (Dual K V) = finrank K V
⊢ finrank K (Dual K V) = finrank K V

Tactic:
by_cases h : FiniteDimensional K V

Premises used: FiniteDimensional
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : FiniteDimensional K V
⊢ finrank K (Dual K V) = finrank K V

Tactic:
LinearEquiv.finrank_eq (Basis.ofVectorSpace K V).toDualEquiv.symm

Premises used: LinearEquiv.symm, LinearEquiv.finrank_eq, Module.Basis.ofVectorSpace, Module.Basis.toDualEquiv
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : FiniteDimensional K V
⊢ finrank K (Dual K V) = finrank K V

Tactic:
exact LinearEquiv.finrank_eq (Basis.ofVectorSpace K V).toDualEquiv.symm

Premises used: LinearEquiv.symm, LinearEquiv.finrank_eq, Module.Basis.ofVectorSpace, Module.Basis.toDualEquiv
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : FiniteDimensional K V
⊢ finrank K (Dual K V) = finrank K V

Tactic:
classical exact LinearEquiv.finrank_eq (Basis.ofVectorSpace K V).toDualEquiv.symm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ¬FiniteDimensional K V
neg : ∀ (s : Finset V) (a : Basis (↑(↑s : Set V) : Type u_2) K V), False
neg₁ : ∀ (s : Finset (Dual K V)) (a : Basis (↑(↑s : Set (Dual K V)) : Type (max u_1 u_2)) K (Dual K V)), False
⊢ finrank K (Dual K V) = finrank K V

Tactic:
rw [finrank_eq_zero_of_basis_imp_false, finrank_eq_zero_of_basis_imp_false]

Premises used: finrank_eq_zero_of_basis_imp_false
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ¬FiniteDimensional K V
⊢ ∀ (s : Finset V) (a : Basis (↑(↑s : Set V) : Type u_2) K V), False

Tactic:
fun _ b ↦ h (Module.Finite.of_basis b)

Premises used: Module.Finite.of_basis
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ¬FiniteDimensional K V
⊢ ∀ (s : Finset V) (a : Basis (↑(↑s : Set V) : Type u_2) K V), False

Tactic:
exact fun _ b ↦ h (Module.Finite.of_basis b)

Premises used: Module.Finite.of_basis
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ¬FiniteDimensional K V
⊢ ∀ (s : Finset (Dual K V)) (a : Basis (↑(↑s : Set (Dual K V)) : Type (max u_1 u_2)) K (Dual K V)), False

Tactic:
fun _ b ↦ h ((Module.finite_dual_iff K).mp <| Module.Finite.of_basis b)

Premises used: Module.finite_dual_iff, Iff.mp, Module.Finite.of_basis
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ¬FiniteDimensional K V
⊢ ∀ (s : Finset (Dual K V)) (a : Basis (↑(↑s : Set (Dual K V)) : Type (max u_1 u_2)) K (Dual K V)), False

Tactic:
exact fun _ b ↦ h ((Module.finite_dual_iff K).mp <| Module.Finite.of_basis b)

Premises used: Module.finite_dual_iff, Iff.mp, Module.Finite.of_basis
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
W : Subspace K V
⊢ (dualAnnihilator W).dualCoannihilator = W

Tactic:
have : _ = W := Subspace.dualAnnihilator_dualCoannihilator_eq
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
W : Subspace K V
this : (dualAnnihilator W).dualCoannihilator = W
⊢ (OrderIso.symm (mapEvalEquiv K V) : (a : Submodule K (Dual K (Dual K V))) → Submodule K V)
      (dualAnnihilator W).dualAnnihilator =
    W

Tactic:
rw [dualCoannihilator, ← Module.mapEvalEquiv_symm_apply] at this

Premises used: Submodule.dualCoannihilator, Module.mapEvalEquiv_symm_apply
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
W : Subspace K V
this :
  (OrderIso.symm (mapEvalEquiv K V) : (a : Submodule K (Dual K (Dual K V))) → Submodule K V)
      (dualAnnihilator W).dualAnnihilator =
    W
rwa rwa₁ rwa₂ rwa₃ :
  (OrderIso.symm (mapEvalEquiv K V) : (a : Submodule K (Dual K (Dual K V))) → Submodule K V)
      (dualAnnihilator W).dualAnnihilator =
    W
⊢ (dualAnnihilator W).dualAnnihilator = (mapEvalEquiv K V : (a : Submodule K V) → Submodule K (Dual K (Dual K V))) W

Tactic:
rwa [← OrderIso.symm_apply_eq]

Premises used: OrderIso.symm_apply_eq
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
W : Subspace K V
rw : finrank.{u_1, u_2} K ↥W + finrank.{u_1, u_2} K (V ⧸ W) = finrank K V
rw₁ : finrank.{u_1, u_2} K (V ⧸ W) + finrank.{u_1, u_2} K ↥W = finrank K V
rw₂ rw₃ : finrank K V = finrank K V
⊢ finrank.{u_1, u_2} K ↥W + finrank K ↥(dualAnnihilator W) = finrank K V

Tactic:
rw [← W.quotEquivAnnihilator.finrank_eq, add_comm, Submodule.finrank_quotient_add_finrank]

Premises used: Submodule.finrank_quotient_add_finrank, LinearEquiv.finrank_eq, add_comm, Subspace.quotEquivAnnihilator
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
Φ : Subspace K (Dual K V)
⊢ finrank.{u_1, u_2} K ↥(comap (↑(evalEquiv K V) : V →ₗ[K] Dual K (Dual K V)) (dualAnnihilator Φ)) =
    finrank K ↥(dualAnnihilator Φ)

Tactic:
LinearEquiv.finrank_eq (LinearEquiv.ofSubmodule' _ _)

Premises used: LinearEquiv.finrank_eq, LinearEquiv.ofSubmodule'
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
Φ : Subspace K (Dual K V)
⊢ finrank.{u_1, u_2} K ↥(comap (↑(evalEquiv K V) : V →ₗ[K] Dual K (Dual K V)) (dualAnnihilator Φ)) =
    finrank K ↥(dualAnnihilator Φ)

Tactic:
exact LinearEquiv.finrank_eq (LinearEquiv.ofSubmodule' _ _)

Premises used: LinearEquiv.finrank_eq, LinearEquiv.ofSubmodule'
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
W : Subspace K (Dual K V)
rw : finrank K ↥W + finrank K ↥(dualAnnihilator W) = finrank K V
rw₁ : finrank K (Dual K V) = finrank K V
rw₂ rw₃ : finrank K V = finrank K V
⊢ finrank K ↥W + finrank.{u_1, u_2} K ↥(dualCoannihilator W) = finrank K V

Tactic:
rw [finrank_dualCoannihilator_eq, finrank_add_finrank_dualAnnihilator_eq, dual_finrank_eq]

Premises used: Subspace.finrank_dualCoannihilator_eq, Subspace.dual_finrank_eq, Subspace.finrank_add_finrank_dualAnnihilator_eq
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
W : Submodule R M
w : M
hw : w ∈ W
h :
  ∀ (φ : Dual R M) (hφ : φ ∈ W.dualAnnihilator),
    Eq.{u_1 + 1} (α := R)
      ((((W.dualAnnihilator.subtype.flip : (a : M) → ↥W.dualAnnihilator →ₗ[R] R) w : ↥W.dualAnnihilator →ₗ[R] R) :
            (a : ↥W.dualAnnihilator) → R)
          (Subtype.mk (p := fun (x : Dual R M) ↦ x ∈ W.dualAnnihilator) φ hφ) :
        R)
      ((0 : (a : ↥W.dualAnnihilator) → R) (Subtype.mk (p := fun (x : Dual R M) ↦ x ∈ W.dualAnnihilator) φ hφ) : R)
⊢ w ∈ W.dualAnnihilator.subtype.flip.ker

Tactic:
ext ⟨φ, hφ⟩