case refine'_1
ι : Sort ?u.9043
α : Type u_2
β : Type u_1
γ : Type ?u.9052
κ : ι → Sort ?u.9057
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : c.snd ⊆ d.snd
⊢ d ≤ c

case refine'_2
ι : Sort ?u.9043
α : Type u_2
β : Type u_1
γ : Type ?u.9052
κ : ι → Sort ?u.9057
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : d ≤ c
⊢ c.snd ⊆ d.snd
ι : Sort ?u.9043
α : Type u_2
β : Type u_1
γ : Type ?u.9052
κ : ι → Sort ?u.9057
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
⊢ c.snd ⊆ d.snd ↔ d ≤ c
refine' ⟨fun h => _, fun h => _⟩
case refine'_1
ι : Sort ?u.9043
α : Type u_2
β : Type u_1
γ : Type ?u.9052
κ : ι → Sort ?u.9057
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : c.snd ⊆ d.snd
⊢ extentClosure r d.snd ⊆ extentClosure r c.snd
case refine'_1
ι : Sort ?u.9043
α : Type u_2
β : Type u_1
γ : Type ?u.9052
κ : ι → Sort ?u.9057
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : c.snd ⊆ d.snd
⊢ d ≤ c
rw [← fst_subset_fst_iff, ← c.closure_snd, ← d.closure_snd]
no goals
case refine'_1
ι : Sort ?u.9043
α : Type u_2
β : Type u_1
γ : Type ?u.9052
κ : ι → Sort ?u.9057
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : c.snd ⊆ d.snd
⊢ extentClosure r d.snd ⊆ extentClosure r c.snd
exact extentClosure_anti _ h
case refine'_2
ι : Sort ?u.9043
α : Type u_2
β : Type u_1
γ : Type ?u.9052
κ : ι → Sort ?u.9057
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : d ≤ c
⊢ intentClosure r c.fst ⊆ intentClosure r d.fst
case refine'_2
ι : Sort ?u.9043
α : Type u_2
β : Type u_1
γ : Type ?u.9052
κ : ι → Sort ?u.9057
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : d ≤ c
⊢ c.snd ⊆ d.snd
rw [← c.closure_fst, ← d.closure_fst]
no goals
case refine'_2
ι : Sort ?u.9043
α : Type u_2
β : Type u_1
γ : Type ?u.9052
κ : ι → Sort ?u.9057
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : d ≤ c
⊢ intentClosure r c.fst ⊆ intentClosure r d.fst
exact intentClosure_anti _ h