-- Mathlib/LinearAlgebra/Dual.lean
theorem dualAnnihilator_iInf_eq {ι : Type*} [Finite ι] (W : ι → Subspace K V₁) :
    (⨅ i : ι, W i).dualAnnihilator = ⨆ i : ι, (W i).dualAnnihilator

Proof state:
case of_equiv
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
⊢ ∀ {α β : Type u_1},
    α ≃ β →
      (∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)) →
        ∀ (W : β → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

Tactic:
intro α β h hyp W

Result:
case of_equiv
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
α β : Type u_1
h : α ≃ β
hyp : ∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
W : β → Subspace K V₁
⊢ dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

Proof state:
case h_empty
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
⊢ ∀ (W : PEmpty.{u_1 + 1} → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

Tactic:
intro W

Result:
case h_empty
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : PEmpty.{u_1 + 1} → Subspace K V₁
⊢ dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

Proof state:
case h_option
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
⊢ ∀ {α : Type u_1} [inst : Fintype α],
    (∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)) →
      ∀ (W : Option α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

Tactic:
intro α _ h W

Result:
case h_option
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
α : Type u_1
inst✝ : Fintype α
h : ∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
W : Option α → Subspace K V₁
⊢ dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

Proof state:
case of_equiv
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
α β : Type u_1
h : α ≃ β
hyp : ∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
W : β → Subspace K V₁
⊢ dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

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

Result:
no goals

Proof state:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
ι : Type u_1
inst✝ : Finite ι
W : ι → Subspace K V₁
⊢ dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

Tactic:
revert ι

Result:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
⊢ ∀ {ι : Type u_1} [inst : Finite ι] (W : ι → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

Proof state:
case h_empty
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : PEmpty.{u_1 + 1} → Subspace K V₁
⊢ dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

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

Result:
no goals

Proof state:
case h_option
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
α : Type u_1
inst✝ : Fintype α
h : ∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
W : Option α → Subspace K V₁
⊢ dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

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

Result:
no goals

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
⊢ ∀ {ι : Type u_1} [inst : Finite ι] (W : ι → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

Tactic:
apply Finite.induction_empty_option

Result:
case of_equiv
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
⊢ ∀ {α β : Type u_1},
    α ≃ β →
      (∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)) →
        ∀ (W : β → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

case h_empty
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
⊢ ∀ (W : PEmpty.{u_1 + 1} → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

case h_option
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
⊢ ∀ {α : Type u_1} [inst : Fintype α],
    (∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)) →
      ∀ (W : Option α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)