awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
x : Dual.{u_1, u_2} K ((V₁ ⧸ W) × V₁ ⧸ W')
⊢ ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W', y + z = (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁) x
have obtain : ∀ (a : Dual.{u_1, u_2} K (V₁ ⧸ W)) (b : Dual.{u_1, u_2} K (V₁ ⧸ W')),
  ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W',
      y + z =
        (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁)
          ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W') :
              (a : Dual K (V₁ ⧸ W) × Dual K (V₁ ⧸ W')) → Dual K ((V₁ ⧸ W) × V₁ ⧸ W'))
            (a, b))
Tactic: obtain ⟨⟨a, b⟩, rfl⟩ := (dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')).surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
a : Dual.{u_1, u_2} K (V₁ ⧸ W)
b : Dual.{u_1, u_2} K (V₁ ⧸ W')
⊢ ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W',
      y + z =
        (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁)
          ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W') :
              (a : Dual K (V₁ ⧸ W) × Dual K (V₁ ⧸ W')) → Dual K ((V₁ ⧸ W) × V₁ ⧸ W'))
            (a, b))
have obtain : ∀ (a' : ↥(dualAnnihilator W)),
  ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W',
      y + z =
        (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁)
          ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W') :
              (a : Dual K (V₁ ⧸ W) × Dual K (V₁ ⧸ W')) → Dual K ((V₁ ⧸ W) × V₁ ⧸ W'))
            (((dualQuotEquivDualAnnihilator W).symm : (a : ↥(dualAnnihilator W)) → Dual K (V₁ ⧸ W)) a', b))
Tactic: obtain ⟨a', rfl⟩ := (dualQuotEquivDualAnnihilator W).symm.surjective a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
b : Dual.{u_1, u_2} K (V₁ ⧸ W')
a' : ↥(dualAnnihilator W)
⊢ ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W',
      y + z =
        (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁)
          ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W') :
              (a : Dual K (V₁ ⧸ W) × Dual K (V₁ ⧸ W')) → Dual K ((V₁ ⧸ W) × V₁ ⧸ W'))
            (((dualQuotEquivDualAnnihilator W).symm : (a : ↥(dualAnnihilator W)) → Dual K (V₁ ⧸ W)) a', b))
have obtain : ∀ (b' : ↥(dualAnnihilator W')),
  ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W',
      y + z =
        (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁)
          ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W') :
              (a : Dual K (V₁ ⧸ W) × Dual K (V₁ ⧸ W')) → Dual K ((V₁ ⧸ W) × V₁ ⧸ W'))
            (((dualQuotEquivDualAnnihilator W).symm : (a : ↥(dualAnnihilator W)) → Dual K (V₁ ⧸ W)) a',
              ((dualQuotEquivDualAnnihilator W').symm : (a : ↥(dualAnnihilator W')) → Dual K (V₁ ⧸ W')) b'))
Tactic: obtain ⟨b', rfl⟩ := (dualQuotEquivDualAnnihilator W').symm.surjective b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : F.ker = W ⊓ W'
a' : ↥(dualAnnihilator W)
b' : ↥(dualAnnihilator W')
⊢ ∃ y ∈ dualAnnihilator W,
    ∃ z ∈ dualAnnihilator W',
      y + z =
        (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁)
          ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W') :
              (a : Dual K (V₁ ⧸ W) × Dual K (V₁ ⧸ W')) → Dual K ((V₁ ⧸ W) × V₁ ⧸ W'))
            (((dualQuotEquivDualAnnihilator W).symm : (a : ↥(dualAnnihilator W)) → Dual K (V₁ ⧸ W)) a',
              ((dualQuotEquivDualAnnihilator W').symm : (a : ↥(dualAnnihilator W')) → Dual K (V₁ ⧸ W')) b'))
have right : (↑a' : Dual K V₁) + (↑b' : Dual K V₁) =
  (F.dualMap : (a : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')) → Dual K V₁)
    ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W') :
        (a : Dual K (V₁ ⧸ W) × Dual K (V₁ ⧸ W')) → Dual K ((V₁ ⧸ W) × V₁ ⧸ W'))
      (((dualQuotEquivDualAnnihilator W).symm : (a : ↥(dualAnnihilator W)) → Dual K (V₁ ⧸ W)) a',
        ((dualQuotEquivDualAnnihilator W').symm : (a : ↥(dualAnnihilator W')) → Dual K (V₁ ⧸ W')) b'))
Tactic: use a', a'.property, b', b'.property
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
⊢ ∀ {ι : Type u_4} [Finite ι] (W : ι → Subspace K V₁),
    Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : ι), W i)) (⨆ (i : ι), dualAnnihilator (W i))
have of_equiv : ∀ {α β : Type u_4} (a : α ≃ β),
  (∀ (W : α → Subspace K V₁),
      Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : α), W i)) (⨆ (i : α), dualAnnihilator (W i))) →
    ∀ (W : β → Subspace K V₁),
      Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : β), W i)) (⨆ (i : β), dualAnnihilator (W i))
Tactic: apply Finite.induction_empty_option
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
of_equiv :
  ∀ {α β : Type u_4} (a : α ≃ β),
    (∀ (W : α → Subspace K V₁),
        Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : α), W i)) (⨆ (i : α), dualAnnihilator (W i))) →
      ∀ (W : β → Subspace K V₁),
        Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : β), W i)) (⨆ (i : β), dualAnnihilator (W i))
⊢ ∀ {ι : Type u_4} [Finite ι] (W : ι → Subspace K V₁),
    Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : ι), W i)) (⨆ (i : ι), dualAnnihilator (W i))
have h_empty : ∀ (W : PEmpty.{u_4 + 1} → Subspace 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: apply Finite.induction_empty_option
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V₁ : Type u_2
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
of_equiv :
  ∀ {α β : Type u_4} (a : α ≃ β),
    (∀ (W : α → Subspace K V₁),
        Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : α), W i)) (⨆ (i : α), dualAnnihilator (W i))) →
      ∀ (W : β → Subspace K V₁),
        Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : β), W i)) (⨆ (i : β), dualAnnihilator (W i))
h_empty :
  ∀ (W : PEmpty.{u_4 + 1} → Subspace K V₁),
    Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : PEmpty.{u_4 + 1}), W i))
      (⨆ (i : PEmpty.{u_4 + 1}), dualAnnihilator (W i))
⊢ ∀ {ι : Type u_4} [Finite ι] (W : ι → Subspace K V₁),
    Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : ι), W i)) (⨆ (i : ι), dualAnnihilator (W i))
have h_option : ∀ {α : Type u_4} [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: apply Finite.induction_empty_option
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₁
⊢ Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : β), W i)) (⨆ (i : β), dualAnnihilator (W i))
have of_equiv : Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (x : α), W ((h : (a : α) → β) x)))
  (⨆ (i : β), dualAnnihilator (W i))
Tactic: rw [← h.iInf_comp, hyp _, ← h.iSup_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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))
⊢ Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : β), W i)) (⨆ (i : β), dualAnnihilator (W i))
have of_equiv₁ : Eq (α := Submodule K (Dual K V₁)) (⨆ (i : α), dualAnnihilator (W ((h : (a : α) → β) i)))
  (⨆ (i : β), dualAnnihilator (W i))
Tactic: rw [← h.iInf_comp, hyp _, ← h.iSup_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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))
⊢ Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : β), W i)) (⨆ (i : β), dualAnnihilator (W i))
have of_equiv₂ : Eq (α := Submodule K (Dual K V₁)) (⨆ (i : α), dualAnnihilator (W ((h : (a : α) → β) i)))
  (⨆ (x : α), dualAnnihilator (W ((h : (a : α) → β) x)))
Tactic: rw [← h.iInf_comp, hyp _, ← h.iSup_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₁
⊢ Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : PEmpty.{u_4 + 1}), W i))
    (⨆ (i : PEmpty.{u_4 + 1}), dualAnnihilator (W i))
have h_empty : Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : PEmpty.{u_4 + 1}), W i)) (sSup ∅)
Tactic: rw [iSup_of_empty', iInf_of_isEmpty, sInf_empty, sSup_empty, dualAnnihilator_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 ∅)
⊢ Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : PEmpty.{u_4 + 1}), W i))
    (⨆ (i : PEmpty.{u_4 + 1}), dualAnnihilator (W i))
have h_empty₁ : Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (sInf ∅)) (sSup ∅)
Tactic: rw [iSup_of_empty', iInf_of_isEmpty, sInf_empty, sSup_empty, dualAnnihilator_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 ∅)
⊢ Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : PEmpty.{u_4 + 1}), W i))
    (⨆ (i : PEmpty.{u_4 + 1}), dualAnnihilator (W i))
have h_empty₂ : Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator ⊤) (sSup ∅)
Tactic: rw [iSup_of_empty', iInf_of_isEmpty, sInf_empty, sSup_empty, dualAnnihilator_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 ∅)
⊢ Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : PEmpty.{u_4 + 1}), W i))
    (⨆ (i : PEmpty.{u_4 + 1}), dualAnnihilator (W i))
have h_empty₃ : Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator ⊤) ⊥
Tactic: rw [iSup_of_empty', iInf_of_isEmpty, sInf_empty, sSup_empty, dualAnnihilator_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 ⊤) ⊥
⊢ Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : PEmpty.{u_4 + 1}), W i))
    (⨆ (i : PEmpty.{u_4 + 1}), dualAnnihilator (W i))
have h_empty₄ : Eq (α := Submodule K (Dual K V₁)) ⊥ ⊥
Tactic: rw [iSup_of_empty', iInf_of_isEmpty, sInf_empty, sSup_empty, dualAnnihilator_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₁
⊢ Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : Option α), W i)) (⨆ (i : Option α), dualAnnihilator (W i))
have h_option : dualAnnihilator (W none ⊓ ⨅ (b : α), W (some b)) = ⨆ (i : Option α), dualAnnihilator (W i)
Tactic: rw [iInf_option, iSup_option, dualAnnihilator_inf_eq, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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)
⊢ Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : Option α), W i)) (⨆ (i : Option α), dualAnnihilator (W i))
have h_option₁ : dualAnnihilator (W none ⊓ ⨅ (b : α), W (some b)) = dualAnnihilator (W none) ⊔ ⨆ (b : α), dualAnnihilator (W (some b))
Tactic: rw [iInf_option, iSup_option, dualAnnihilator_inf_eq, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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))
⊢ Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : Option α), W i)) (⨆ (i : Option α), dualAnnihilator (W i))
have h_option₂ : dualAnnihilator (W none) ⊔ dualAnnihilator (⨅ (b : α), W (some b)) =
  dualAnnihilator (W none) ⊔ ⨆ (b : α), dualAnnihilator (W (some b))
Tactic: rw [iInf_option, iSup_option, dualAnnihilator_inf_eq, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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))
⊢ Eq (α := Submodule K (Dual K V₁)) (dualAnnihilator (⨅ (i : Option α), W i)) (⨆ (i : Option α), dualAnnihilator (W i))
have h_option₃ : dualAnnihilator (W none) ⊔ ⨆ (i : α), dualAnnihilator (W (some i)) =
  dualAnnihilator (W none) ⊔ ⨆ (b : α), dualAnnihilator (W (some b))
Tactic: rw [iInf_option, iSup_option, dualAnnihilator_inf_eq, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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'
⊢ IsCompl (dualAnnihilator W) (dualAnnihilator W')
have rw : ∀ (h : W ⊓ W' = ⊥ ∧ W ⊔ W' = ⊤), dualAnnihilator W ⊓ dualAnnihilator W' = ⊥ ∧ dualAnnihilator W ⊔ dualAnnihilator W' = ⊤
Tactic: rw [isCompl_iff, disjoint_iff, codisjoint_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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' = ⊤
⊢ dualAnnihilator W ⊓ dualAnnihilator W' = ⊥ ∧ dualAnnihilator W ⊔ dualAnnihilator W' = ⊤
have rw : Eq (α := Submodule K (Dual K V₁)) ⊥ ⊥ ∧ Eq (α := Submodule K (Dual K V₁)) ⊤ ⊤
Tactic: rw [← dualAnnihilator_inf_eq, ← dualAnnihilator_sup_eq, h.1, h.2, dualAnnihilator_top,
    dualAnnihilator_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₂
⊢ finrank K ↥f.dualMap.range = finrank.{u_1, u_3} K ↥f.range
have 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₁)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₂)
have 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
Tactic: refine ⟨Function.mtr fun not_surj inj ↦ ?_, dualMap_injective_of_surjective⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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₁)
⊢ False
have not_surj₁ : f.range < ⊤
Tactic: rw [← range_eq_top, ← Ne, ← lt_top_iff_ne_top] at not_surj
Cleared hypotheses: not_surj, inj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₁)
⊢ False
have obtain : ∀ (φ : V₂ →ₗ[K] K) (φ0 : φ ≠ 0) (range_le_ker : f.range ≤ φ.ker), False
Tactic: obtain ⟨φ, φ0, range_le_ker⟩ := (range f).exists_le_ker_of_lt_top not_surj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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.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₂)
have 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₂)
Tactic: simp_rw [Function.Bijective, dualMap_surjective_iff, dualMap_injective_iff, and_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₂)
⊢ 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₂)
have 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₂)
Tactic: simp_rw [Function.Bijective, dualMap_surjective_iff, dualMap_injective_iff, and_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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₂)
⊢ 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₂)
have 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₂)
Tactic: simp_rw [Function.Bijective, dualMap_surjective_iff, dualMap_injective_iff, and_comm]