awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁
α β : Type u_4
h : α ≃ β
hyp :
  ∀ (W : α → Subspace K V₁),
    Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : α), W i)) (⨆ (i : α), dualAnnihilator (W i))
W : β → Subspace K V₁
of_equiv :
  Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (x : α), W ((h : (a : α) → β) x)))
    (⨆ (i : β), dualAnnihilator (W i))
of_equiv₁ :
  Eq (α := Submodule K (Dual K V₁)) (⨆ (i : α), dualAnnihilator (W ((h : (a : α) → β) i)))
    (⨆ (i : β), dualAnnihilator (W i))
of_equiv₂ of_equiv₃ :
  Eq (α := Submodule K (Dual K V₁)) (⨆ (i : α), dualAnnihilator (W ((h : (a : α) → β) i)))
    (⨆ (x : α), dualAnnihilator (W ((h : (a : α) → β) x)))
⊢ Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : β), W i)) (⨆ (i : β), dualAnnihilator (W i))

Tactic:
rw [← h.iInf_comp, hyp _, ← h.iSup_comp]

Premises used: Equiv.iSup_comp, Equiv.iInf_comp
-- 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 : PEmpty.{u_4 + 1} → Subspace K V₁
h_empty : Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : PEmpty.{u_4 + 1}), W i)) (sSup ∅)
h_empty₁ : Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (sInf ∅)) (sSup ∅)
h_empty₂ : Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator ⊤) (sSup ∅)
h_empty₃ : Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator ⊤) ⊥
h_empty₄ h_empty₅ : Eq (α := Submodule K (Dual K V₁)) ⊥ ⊥
⊢ Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : PEmpty.{u_4 + 1}), W i))
    (⨆ (i : PEmpty.{u_4 + 1}), dualAnnihilator (W i))

Tactic:
rw [iSup_of_empty', iInf_of_isEmpty, sInf_empty, sSup_empty, dualAnnihilator_top]

Premises used: sSup_empty, Submodule.dualAnnihilator_top, sInf_empty, iInf_of_isEmpty, iSup_of_empty'
-- 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₁
α : Type u_4
h_option :
  ∀ [Fintype α],
    (∀ (W : α → Subspace K V₁),
        Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : α), W i)) (⨆ (i : α), dualAnnihilator (W i))) →
      ∀ (W : Option α → Subspace K V₁),
        Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : Option α), W i))
          (⨆ (i : Option α), dualAnnihilator (W i))
⊢ ∀ [Fintype α],
    (∀ (W : α → Subspace K V₁),
        Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : α), W i)) (⨆ (i : α), dualAnnihilator (W i))) →
      ∀ (W : Option α → Subspace K V₁),
        Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : Option α), W i))
          (⨆ (i : Option α), dualAnnihilator (W i))

Tactic:
_
-- 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₁
α : Type u_4
inst_3 : Fintype α
h :
  ∀ (W : α → Subspace K V₁),
    Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : α), W i)) (⨆ (i : α), dualAnnihilator (W i))
W : Option α → Subspace K V₁
h_option : dualAnnihilator (W none ⊓ ⨅ (b : α), W (some b)) = ⨆ (i : Option α), dualAnnihilator (W i)
h_option₁ :
  dualAnnihilator (W none ⊓ ⨅ (b : α), W (some b)) = dualAnnihilator (W none) ⊔ ⨆ (b : α), dualAnnihilator (W (some b))
h_option₂ :
  dualAnnihilator (W none) ⊔ dualAnnihilator (⨅ (b : α), W (some b)) =
    dualAnnihilator (W none) ⊔ ⨆ (b : α), dualAnnihilator (W (some b))
h_option₃ h_option₄ :
  dualAnnihilator (W none) ⊔ ⨆ (i : α), dualAnnihilator (W (some i)) =
    dualAnnihilator (W none) ⊔ ⨆ (b : α), dualAnnihilator (W (some b))
⊢ Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : Option α), W i)) (⨆ (i : Option α), dualAnnihilator (W i))

Tactic:
rw [iInf_option, iSup_option, dualAnnihilator_inf_eq, h]

Premises used: iInf_option, iSup_option, Subspace.dualAnnihilator_inf_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 W' : Subspace K V₁
h : IsCompl W W'
rw :
  ∀ (h : W ⊓ W' = ⊥ ∧ W ⊔ W' = ⊤),
    dualAnnihilator W ⊓ dualAnnihilator W' = ⊥ ∧ dualAnnihilator W ⊔ dualAnnihilator W' = ⊤
⊢ IsCompl (dualAnnihilator W) (dualAnnihilator W')

Tactic:
rw [isCompl_iff, disjoint_iff, codisjoint_iff] at h ⊢

Premises used: codisjoint_iff, disjoint_iff, isCompl_iff
-- 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₁
h : W ⊓ W' = ⊥ ∧ W ⊔ W' = ⊤
rw : Eq (α := Submodule K (Dual K V₁)) ⊥ ⊥ ∧ Eq (α := Submodule K (Dual K V₁)) ⊤ ⊤
⊢ dualAnnihilator W ⊓ dualAnnihilator W' = ⊥ ∧ dualAnnihilator W ⊔ dualAnnihilator W' = ⊤

Tactic:
rw [← dualAnnihilator_inf_eq, ← dualAnnihilator_sup_eq, h.1, h.2, dualAnnihilator_top,
    dualAnnihilator_bot]

Premises used: Submodule.dualAnnihilator_sup_eq, And.right, And.left, Submodule.dualAnnihilator_top, Submodule.dualAnnihilator_bot, Subspace.dualAnnihilator_inf_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 W' : Subspace K V₁
h : W ⊓ W' = ⊥ ∧ W ⊔ W' = ⊤
⊢ Eq (α := Submodule K (Dual K V₁)) ⊥ ⊥ ∧ Eq (α := Submodule K (Dual K V₁)) ⊤ ⊤

Tactic:
⟨rfl, rfl⟩

Premises used: And.intro, 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 W' : Subspace K V₁
h : W ⊓ W' = ⊥ ∧ W ⊔ W' = ⊤
⊢ Eq (α := Submodule K (Dual K V₁)) ⊥ ⊥ ∧ Eq (α := Submodule K (Dual K V₁)) ⊤ ⊤

Tactic:
exact ⟨rfl, rfl⟩
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ f = f.range.subtype ∘ₗ f.rangeRestrict

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V₁ →ₗ[K] V₂
rw :
  Function.Injective (α := Dual.{u_1, u_3} K ↥f.range) (β := Dual K V₁)
    (⇑(dualMap f.rangeRestrict) : (a : Dual K ↥f.range) → Dual K V₁)
⊢ finrank K ↥f.dualMap.range = finrank.{u_1, u_3} K ↥f.range

Tactic:
rw [congr_arg dualMap (show f = (range f).subtype.comp f.rangeRestrict by rfl),
    ← dualMap_comp_dualMap, range_comp,
    range_eq_top.mpr (dualMap_surjective_of_injective (range f).injective_subtype),
    Submodule.map_top, finrank_range_of_inj, Subspace.dual_finrank_eq]

Premises used: Iff.mpr, LinearMap.dualMap_surjective_of_injective, Submodule.map_top, LinearMap.finrank_range_of_inj, LinearMap.range_comp, LinearMap.range, Subspace.dual_finrank_eq, LinearMap.range_eq_top, Submodule.injective_subtype, congr_arg, LinearMap.dualMap_comp_dualMap, LinearMap.dualMap
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Injective (α := Dual.{u_1, u_3} K ↥f.range) (β := Dual K V₁)
    (⇑(dualMap f.rangeRestrict) : (a : Dual K ↥f.range) → Dual K V₁)

Tactic:
dualMap_injective_of_surjective (range_eq_top.mp f.range_rangeRestrict)

Premises used: LinearMap.range_rangeRestrict, LinearMap.dualMap_injective_of_surjective, LinearMap.range_eq_top, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Injective (α := Dual.{u_1, u_3} K ↥f.range) (β := Dual K V₁)
    (⇑(dualMap f.rangeRestrict) : (a : Dual K ↥f.range) → Dual K V₁)

Tactic:
exact dualMap_injective_of_surjective (range_eq_top.mp f.range_rangeRestrict)

Premises used: LinearMap.range_rangeRestrict, LinearMap.dualMap_injective_of_surjective, LinearMap.range_eq_top, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Injective (α := Dual K V₂) (β := Dual K V₁) (⇑f.dualMap : (a : Dual K V₂) → Dual K V₁) ↔
    Function.Surjective.{u_2 + 1, u_3 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)

Tactic:
⟨Function.mtr fun not_surj inj ↦ ?_, dualMap_injective_of_surjective⟩

Premises used: LinearMap.dualMap_injective_of_surjective, Function.mtr, Iff.intro
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V₁ →ₗ[K] V₂
refine :
  ∀ (not_surj : ¬Function.Surjective.{u_2 + 1, u_3 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂))
    (inj : Function.Injective (α := Dual K V₂) (β := Dual K V₁) (⇑f.dualMap : (a : Dual K V₂) → Dual K V₁)), False
⊢ Function.Injective (α := Dual K V₂) (β := Dual K V₁) (⇑f.dualMap : (a : Dual K V₂) → Dual K V₁) ↔
    Function.Surjective.{u_2 + 1, u_3 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)

Tactic:
refine ⟨Function.mtr fun not_surj inj ↦ ?_, dualMap_injective_of_surjective⟩
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V₁ →ₗ[K] V₂
not_surj : ¬Function.Surjective.{u_2 + 1, u_3 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)
inj : Function.Injective (α := Dual K V₂) (β := Dual K V₁) (⇑f.dualMap : (a : Dual K V₂) → Dual K V₁)
⊢ f.range < ⊤

Tactic:
rw [← range_eq_top, ← Ne, ← lt_top_iff_ne_top] at not_surj

Premises used: Ne, lt_top_iff_ne_top, LinearMap.range_eq_top
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V₁ →ₗ[K] V₂
not_surj : ¬Function.Surjective.{u_2 + 1, u_3 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)
inj : Function.Injective (α := Dual K V₂) (β := Dual K V₁) (⇑f.dualMap : (a : Dual K V₂) → Dual K V₁)
not_surj₁ : f.range < ⊤
⊢ Function.Injective (α := Dual K V₂) (β := Dual K V₁) (⇑f.dualMap : (a : Dual K V₂) → Dual K V₁)

Tactic:
rw [← range_eq_top, ← Ne, ← lt_top_iff_ne_top] at not_surj

Premises used: Ne, lt_top_iff_ne_top, LinearMap.range_eq_top
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V₁ →ₗ[K] V₂
not_surj : f.range < ⊤
inj : Function.Injective (α := Dual K V₂) (β := Dual K V₁) (⇑f.dualMap : (a : Dual K V₂) → Dual K V₁)
obtain : ∀ (φ : V₂ →ₗ[K] K) (φ0 : φ ≠ 0) (range_le_ker : f.range ≤ φ.ker), False
⊢ False

Tactic:
obtain ⟨φ, φ0, range_le_ker⟩ := (range f).exists_le_ker_of_lt_top not_surj

Premises used: Submodule.exists_le_ker_of_lt_top, LinearMap.range
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V₁ →ₗ[K] V₂
not_surj : f.range < ⊤
inj : Function.Injective (α := Dual K V₂) (β := Dual K V₁) (⇑f.dualMap : (a : Dual K V₂) → Dual K V₁)
φ : V₂ →ₗ[K] K
φ0 : φ ≠ 0
range_le_ker : f.range ≤ φ.ker
⊢ False

Tactic:
φ0 (inj <| ext fun x ↦ range_le_ker ⟨x, rfl⟩)

Premises used: LinearMap.ext, Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V₁ →ₗ[K] V₂
not_surj : f.range < ⊤
inj : Function.Injective (α := Dual K V₂) (β := Dual K V₁) (⇑f.dualMap : (a : Dual K V₂) → Dual K V₁)
φ : V₂ →ₗ[K] K
φ0 : φ ≠ 0
range_le_ker : f.range ≤ φ.ker
⊢ False

Tactic:
exact φ0 (inj <| ext fun x ↦ range_le_ker ⟨x, rfl⟩)

Premises used: LinearMap.ext, Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
f : V₁ →ₗ[K] V₂
simp_rw :
  Function.Injective (α := Dual K V₂) (β := Dual K V₁) (⇑f.dualMap : (a : Dual K V₂) → Dual K V₁) ∧
      Function.Surjective (α := Dual K V₂) (β := Dual K V₁) (⇑f.dualMap : (a : Dual K V₂) → Dual K V₁) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂) ∧
      Function.Surjective.{u_2 + 1, u_3 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)
simp_rw₁ :
  Function.Injective (α := Dual K V₂) (β := Dual K V₁) (⇑f.dualMap : (a : Dual K V₂) → Dual K V₁) ∧
      Function.Injective.{u_2 + 1, u_3 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂) ∧
      Function.Surjective.{u_2 + 1, u_3 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)
simp_rw₂ :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂) ∧
      Function.Injective.{u_2 + 1, u_3 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂) ∧
      Function.Surjective.{u_2 + 1, u_3 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)
⊢ Function.Bijective (α := Dual K V₂) (β := Dual K V₁) (⇑f.dualMap : (a : Dual K V₂) → Dual K V₁) ↔
    Function.Bijective.{u_2 + 1, u_3 + 1} (α := V₁) (β := V₂) (⇑f : (a : V₁) → V₂)

Tactic:
simp_rw [Function.Bijective, dualMap_surjective_iff, dualMap_injective_iff, and_comm]

Premises used: LinearMap.dualMap_injective_iff, and_comm, Function.Bijective, LinearMap.dualMap_surjective_iff
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : IsReflexive K V₂
change : B.ker.dualAnnihilator = (B.dualMap ∘ₗ (↑(evalEquiv K V₂) : V₂ →ₗ[K] Dual K (Dual K V₂))).range
⊢ B.ker.dualAnnihilator = B.flip.range

Tactic:
change _ = range (B.dualMap.comp (Module.evalEquiv K V₂).toLinearMap)

Premises used: LinearMap.range, LinearMap.comp, LinearEquiv.toLinearMap, Module.evalEquiv, LinearMap.dualMap
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : IsReflexive K V₂
rw : B.dualMap.range = (B.dualMap ∘ₗ (↑(evalEquiv K V₂) : V₂ →ₗ[K] Dual K (Dual K V₂))).range
rw₁ rw₂ : B.dualMap.range = B.dualMap.range
⊢ B.ker.dualAnnihilator = (B.dualMap ∘ₗ (↑(evalEquiv K V₂) : V₂ →ₗ[K] Dual K (Dual K V₂))).range

Tactic:
rw [← range_dualMap_eq_dualAnnihilator_ker, range_comp_of_range_eq_top _ (LinearEquiv.range _)]

Premises used: LinearMap.range_comp_of_range_eq_top, LinearMap.range_dualMap_eq_dualAnnihilator_ker, LinearEquiv.range
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : FiniteDimensional K V₁
rw :
  Surjective (α := V₁) (β := Dual K V₂)
      (Function.comp (β := Dual K (Dual K V₁)) (⇑B.flip.dualMap : (a : Dual K (V₁ →ₗ[K] K)) → Dual K V₂)
        (⇑(LinearEquiv.toEquiv (evalEquiv K V₁)) : (a : V₁) → Dual K (Dual K V₁))) ↔
    Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)
⊢ Injective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)

Tactic:
rw [← dualMap_surjective_iff, ← (evalEquiv K V₁).toEquiv.surjective_comp]

Premises used: Equiv.surjective_comp, LinearEquiv.toEquiv, LinearMap.dualMap_surjective_iff, Module.evalEquiv
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : FiniteDimensional K V₁
⊢ Surjective (α := V₁) (β := Dual K V₂)
      (Function.comp (β := Dual K (Dual K V₁)) (⇑B.flip.dualMap : (a : Dual K (V₁ →ₗ[K] K)) → Dual K V₂)
        (⇑(LinearEquiv.toEquiv (evalEquiv K V₁)) : (a : V₁) → Dual K (Dual K V₁))) ↔
    Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : FiniteDimensional K V₂
rw :
  Injective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Injective (α := Dual K (V₂ →ₗ[K] K)) (β := Dual K V₁) (⇑B.dualMap : (a : Dual K (V₂ →ₗ[K] K)) → Dual K V₁)
⊢ Injective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)

Tactic:
rw [← dualMap_injective_iff]

Premises used: LinearMap.dualMap_injective_iff
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : FiniteDimensional K V₂
⊢ Injective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Injective (α := Dual K (V₂ →ₗ[K] K)) (β := Dual K V₁) (⇑B.dualMap : (a : Dual K (V₂ →ₗ[K] K)) → Dual K V₁)

Tactic:
(evalEquiv K V₂).toEquiv.injective_comp B.dualMap

Premises used: Equiv.injective_comp, LinearEquiv.toEquiv, Module.evalEquiv, DFunLike.coe, LinearMap.dualMap
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : FiniteDimensional K V₂
⊢ Injective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Injective (α := Dual K (V₂ →ₗ[K] K)) (β := Dual K V₁) (⇑B.dualMap : (a : Dual K (V₂ →ₗ[K] K)) → Dual K V₁)

Tactic:
exact (evalEquiv K V₂).toEquiv.injective_comp B.dualMap

Premises used: Equiv.injective_comp, LinearEquiv.toEquiv, Module.evalEquiv, DFunLike.coe, LinearMap.dualMap
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : FiniteDimensional K V₁
⊢ Surjective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Injective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)

Tactic:
flip_injective_iff₂.symm

Premises used: LinearMap.flip_injective_iff₂, Iff.symm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : FiniteDimensional K V₂
⊢ Surjective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Injective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)

Tactic:
flip_injective_iff₁.symm

Premises used: LinearMap.flip_injective_iff₁, Iff.symm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : FiniteDimensional K V₁
simp_rw :
  Injective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ∧
      Surjective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Injective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K) ∧
      Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)
simp_rw₁ :
  Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K) ∧
      Surjective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Injective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K) ∧
      Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)
simp_rw₂ :
  Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K) ∧
      Injective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K) ↔
    Injective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K) ∧
      Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)
⊢ Bijective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Bijective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)

Tactic:
simp_rw [Bijective, flip_injective_iff₁, flip_surjective_iff₁, and_comm]

Premises used: LinearMap.flip_injective_iff₁, LinearMap.flip_surjective_iff₁, and_comm, Function.Bijective
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : FiniteDimensional K V₂
⊢ Bijective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Bijective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)

Tactic:
flip_bijective_iff₁.symm

Premises used: LinearMap.flip_bijective_iff₁, Iff.symm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_4
V : Type u_5
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K (Dual K V)
inst_3 : FiniteDimensional K ↥W
⊢ Function.Bijective (α := V ⧸ dualCoannihilator W) (β := Dual K ↥W)
    (⇑(quotDualCoannihilatorToDual W) : (a : V ⧸ dualCoannihilator W) → Dual K ↥W)

Tactic:
⟨W.quotDualCoannihilatorToDual_injective, letI : AddCommGroup W := inferInstance
    flip_injective_iff₂.mp W.flip_quotDualCoannihilatorToDual_injective⟩

Premises used: LinearMap.flip_injective_iff₂, Submodule.quotDualCoannihilatorToDual_injective, And.intro, Iff.mp, Function.Bijective, Submodule.flip_quotDualCoannihilatorToDual_injective
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_4
V : Type u_5
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K (Dual K V)
inst_3 : FiniteDimensional K ↥W
⊢ Function.Bijective (α := ↥W) (β := LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id K) (V ⧸ dualCoannihilator W) K)
    (⇑(quotDualCoannihilatorToDual W).flip : (a : ↥W) → V ⧸ dualCoannihilator W →ₗ[K] K)

Tactic:
letI : AddCommGroup W := inferInstance
  flip_bijective_iff₂.mpr W.quotDualCoannihilatorToDual_bijective

Premises used: Iff.mpr, LinearMap.flip_bijective_iff₂, Subspace.quotDualCoannihilatorToDual_bijective
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_4
V : Type u_5
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K (Dual K V)
inst_3 : FiniteDimensional K ↥W
⊢ (dualCoannihilator W).dualAnnihilator = W

Tactic:
let e := (LinearEquiv.ofBijective _ W.flip_quotDualCoannihilatorToDual_bijective).trans
    (Submodule.dualQuotEquivDualAnnihilator _)
  letI : AddCommGroup W := inferInstance
  haveI : FiniteDimensional K W.dualCoannihilator.dualAnnihilator := LinearEquiv.finiteDimensional e
  (eq_of_le_of_finrank_eq W.le_dualCoannihilator_dualAnnihilator e.finrank_eq).symm

Premises used: Submodule.dualCoannihilator, Submodule.quotDualCoannihilatorToDual, Subspace.flip_quotDualCoannihilatorToDual_bijective, LinearEquiv.finrank_eq, LinearMap.flip, Submodule.eq_of_le_of_finrank_eq, Eq.symm, LinearEquiv.trans, Submodule.dualQuotEquivDualAnnihilator, LinearEquiv.ofBijective, Submodule.le_dualCoannihilator_dualAnnihilator