K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
⊢ ∀ {ι : Type u_1} [inst : _root_.Finite ι] (W : ι → Subspace K V₁),
    dualAnnihilator (⨅ (i : ι), W i) = ⨆ (i : ι), dualAnnihilator (W i)
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type u_1
inst✝ : _root_.Finite ι
W : ι → Subspace K V₁
⊢ dualAnnihilator (⨅ (i : ι), W i) = ⨆ (i : ι), dualAnnihilator (W i)
revert ι
case refine'_1
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
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 refine'_2
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
⊢ ∀ (W : PEmpty → Subspace K V₁), dualAnnihilator (⨅ (i : PEmpty), W i) = ⨆ (i : PEmpty), dualAnnihilator (W i)

case refine'_3
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
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 : Option α), W i) = ⨆ (i : Option α), dualAnnihilator (W i)
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
⊢ ∀ {ι : Type u_1} [inst : _root_.Finite ι] (W : ι → Subspace K V₁),
    dualAnnihilator (⨅ (i : ι), W i) = ⨆ (i : ι), dualAnnihilator (W i)
refine' @Finite.induction_empty_option _ _ _ _
case refine'_1
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
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)
case refine'_1
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
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)
intro α β h hyp W
no goals
case refine'_1
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
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)
rw [← h.iInf_comp, hyp _, ← h.iSup_comp]
case refine'_2
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : PEmpty → Subspace K V₁
⊢ dualAnnihilator (⨅ (i : PEmpty), W i) = ⨆ (i : PEmpty), dualAnnihilator (W i)
case refine'_2
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
⊢ ∀ (W : PEmpty → Subspace K V₁), dualAnnihilator (⨅ (i : PEmpty), W i) = ⨆ (i : PEmpty), dualAnnihilator (W i)
intro W
no goals
case refine'_2
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : PEmpty → Subspace K V₁
⊢ dualAnnihilator (⨅ (i : PEmpty), W i) = ⨆ (i : PEmpty), dualAnnihilator (W i)
rw [iSup_of_empty', iInf_of_empty', sInf_empty, sSup_empty, dualAnnihilator_top]
case refine'_3
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
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 : Option α), W i) = ⨆ (i : Option α), dualAnnihilator (W i)
case refine'_3
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
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 : Option α), W i) = ⨆ (i : Option α), dualAnnihilator (W i)
intro α _ h W
no goals
case refine'_3
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
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 : Option α), W i) = ⨆ (i : Option α), dualAnnihilator (W i)
rw [iInf_option, iSup_option, dualAnnihilator_inf_eq, h]