α : Type u_1
d : DynkinSystem α
C : Set (Set α)
s : Set α
⊢ GenerateHas C (sᶜ) → GenerateHas C s
α : Type u_1
d : DynkinSystem α
C : Set (Set α)
s : Set α
⊢ GenerateHas C (sᶜ) ↔ GenerateHas C s
refine' ⟨_, GenerateHas.compl⟩
α : Type u_1
d : DynkinSystem α
C : Set (Set α)
s : Set α
h : GenerateHas C (sᶜ)
⊢ GenerateHas C s
α : Type u_1
d : DynkinSystem α
C : Set (Set α)
s : Set α
⊢ GenerateHas C (sᶜ) → GenerateHas C s
intro h
case h.e'_3
α : Type u_1
d : DynkinSystem α
C : Set (Set α)
s : Set α
h : GenerateHas C (sᶜ)
⊢ s = sᶜᶜ
α : Type u_1
d : DynkinSystem α
C : Set (Set α)
s : Set α
h : GenerateHas C (sᶜ)
⊢ GenerateHas C s
convert GenerateHas.compl h
no goals
case h.e'_3
α : Type u_1
d : DynkinSystem α
C : Set (Set α)
s : Set α
h : GenerateHas C (sᶜ)
⊢ s = sᶜᶜ
simp