[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : c.fst = d.fst
⊢ c = d
[PROOFSTEP]
obtain ⟨⟨s₁, t₁⟩, h₁, _⟩ := c
[GOAL]
case mk.mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁✝ s₂ : Set α
t t₁✝ t₂ : Set β
d : Concept α β r
s₁ : Set α
t₁ : Set β
h₁ : intentClosure r (s₁, t₁).fst = (s₁, t₁).snd
closure_snd✝ : extentClosure r (s₁, t₁).snd = (s₁, t₁).fst
h : { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝ }.toProd.fst = d.fst
⊢ { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝ } = d
[PROOFSTEP]
obtain ⟨⟨s₂, t₂⟩, h₂, _⟩ := d
[GOAL]
case mk.mk.mk.mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁✝ s₂✝ : Set α
t t₁✝ t₂✝ : Set β
s₁ : Set α
t₁ : Set β
h₁ : intentClosure r (s₁, t₁).fst = (s₁, t₁).snd
closure_snd✝¹ : extentClosure r (s₁, t₁).snd = (s₁, t₁).fst
s₂ : Set α
t₂ : Set β
h₂ : intentClosure r (s₂, t₂).fst = (s₂, t₂).snd
closure_snd✝ : extentClosure r (s₂, t₂).snd = (s₂, t₂).fst
h :
  { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝¹ }.toProd.fst =
    { toProd := (s₂, t₂), closure_fst := h₂, closure_snd := closure_snd✝ }.toProd.fst
⊢ { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝¹ } =
    { toProd := (s₂, t₂), closure_fst := h₂, closure_snd := closure_snd✝ }
[PROOFSTEP]
dsimp at h₁ h₂ h 
[GOAL]
case mk.mk.mk.mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁✝ s₂✝ : Set α
t t₁✝ t₂✝ : Set β
s₁ : Set α
t₁ : Set β
h₁ : intentClosure r s₁ = t₁
closure_snd✝¹ : extentClosure r (s₁, t₁).snd = (s₁, t₁).fst
s₂ : Set α
t₂ : Set β
h₂ : intentClosure r s₂ = t₂
closure_snd✝ : extentClosure r (s₂, t₂).snd = (s₂, t₂).fst
h : s₁ = s₂
⊢ { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝¹ } =
    { toProd := (s₂, t₂), closure_fst := h₂, closure_snd := closure_snd✝ }
[PROOFSTEP]
substs h h₁ h₂
[GOAL]
case mk.mk.mk.mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁✝ s₂ : Set α
t t₁ t₂ : Set β
s₁ : Set α
closure_snd✝¹ closure_snd✝ : extentClosure r (s₁, intentClosure r s₁).snd = (s₁, intentClosure r s₁).fst
⊢ { toProd := (s₁, intentClosure r s₁), closure_fst := (_ : intentClosure r s₁ = intentClosure r s₁),
      closure_snd := closure_snd✝¹ } =
    { toProd := (s₁, intentClosure r s₁), closure_fst := (_ : intentClosure r s₁ = intentClosure r s₁),
      closure_snd := closure_snd✝ }
[PROOFSTEP]
rfl
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : c.snd = d.snd
⊢ c = d
[PROOFSTEP]
obtain ⟨⟨s₁, t₁⟩, _, h₁⟩ := c
[GOAL]
case mk.mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁✝ s₂ : Set α
t t₁✝ t₂ : Set β
d : Concept α β r
s₁ : Set α
t₁ : Set β
closure_fst✝ : intentClosure r (s₁, t₁).fst = (s₁, t₁).snd
h₁ : extentClosure r (s₁, t₁).snd = (s₁, t₁).fst
h : { toProd := (s₁, t₁), closure_fst := closure_fst✝, closure_snd := h₁ }.toProd.snd = d.snd
⊢ { toProd := (s₁, t₁), closure_fst := closure_fst✝, closure_snd := h₁ } = d
[PROOFSTEP]
obtain ⟨⟨s₂, t₂⟩, _, h₂⟩ := d
[GOAL]
case mk.mk.mk.mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁✝ s₂✝ : Set α
t t₁✝ t₂✝ : Set β
s₁ : Set α
t₁ : Set β
closure_fst✝¹ : intentClosure r (s₁, t₁).fst = (s₁, t₁).snd
h₁ : extentClosure r (s₁, t₁).snd = (s₁, t₁).fst
s₂ : Set α
t₂ : Set β
closure_fst✝ : intentClosure r (s₂, t₂).fst = (s₂, t₂).snd
h₂ : extentClosure r (s₂, t₂).snd = (s₂, t₂).fst
h :
  { toProd := (s₁, t₁), closure_fst := closure_fst✝¹, closure_snd := h₁ }.toProd.snd =
    { toProd := (s₂, t₂), closure_fst := closure_fst✝, closure_snd := h₂ }.toProd.snd
⊢ { toProd := (s₁, t₁), closure_fst := closure_fst✝¹, closure_snd := h₁ } =
    { toProd := (s₂, t₂), closure_fst := closure_fst✝, closure_snd := h₂ }
[PROOFSTEP]
dsimp at h₁ h₂ h 
[GOAL]
case mk.mk.mk.mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁✝ s₂✝ : Set α
t t₁✝ t₂✝ : Set β
s₁ : Set α
t₁ : Set β
closure_fst✝¹ : intentClosure r (s₁, t₁).fst = (s₁, t₁).snd
h₁ : extentClosure r t₁ = s₁
s₂ : Set α
t₂ : Set β
closure_fst✝ : intentClosure r (s₂, t₂).fst = (s₂, t₂).snd
h₂ : extentClosure r t₂ = s₂
h : t₁ = t₂
⊢ { toProd := (s₁, t₁), closure_fst := closure_fst✝¹, closure_snd := h₁ } =
    { toProd := (s₂, t₂), closure_fst := closure_fst✝, closure_snd := h₂ }
[PROOFSTEP]
substs h h₁ h₂
[GOAL]
case mk.mk.mk.mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁✝ t₂ t₁ : Set β
closure_fst✝¹ closure_fst✝ : intentClosure r (extentClosure r t₁, t₁).fst = (extentClosure r t₁, t₁).snd
⊢ { toProd := (extentClosure r t₁, t₁), closure_fst := closure_fst✝¹,
      closure_snd := (_ : extentClosure r t₁ = extentClosure r t₁) } =
    { toProd := (extentClosure r t₁, t₁), closure_fst := closure_fst✝,
      closure_snd := (_ : extentClosure r t₁ = extentClosure r t₁) }
[PROOFSTEP]
rfl
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c✝ d✝ c d : Concept α β r
⊢ intentClosure r (extentClosure r (c.snd ∩ d.snd), c.snd ∩ d.snd).fst =
    (extentClosure r (c.snd ∩ d.snd), c.snd ∩ d.snd).snd
[PROOFSTEP]
rw [← c.closure_fst, ← d.closure_fst, ← intentClosure_union, intentClosure_extentClosure_intentClosure]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c✝ d✝ c d : Concept α β r
⊢ extentClosure r (c.fst ∩ d.fst, intentClosure r (c.fst ∩ d.fst)).snd =
    (c.fst ∩ d.fst, intentClosure r (c.fst ∩ d.fst)).fst
[PROOFSTEP]
rw [← c.closure_snd, ← d.closure_snd, ← extentClosure_union, extentClosure_intentClosure_extentClosure]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
⊢ c.snd ⊆ d.snd ↔ d ≤ c
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : c.snd ⊆ d.snd
⊢ d ≤ c
[PROOFSTEP]
rw [← fst_subset_fst_iff, ← c.closure_snd, ← d.closure_snd]
[GOAL]
case refine'_1
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
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
[PROOFSTEP]
exact extentClosure_anti _ h
[GOAL]
case refine'_2
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : d ≤ c
⊢ c.snd ⊆ d.snd
[PROOFSTEP]
rw [← c.closure_fst, ← d.closure_fst]
[GOAL]
case refine'_2
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
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
[PROOFSTEP]
exact intentClosure_anti _ h
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
⊢ c.snd ⊂ d.snd ↔ d < c
[PROOFSTEP]
rw [ssubset_iff_subset_not_subset, lt_iff_le_not_le, snd_subset_snd_iff, snd_subset_snd_iff]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c✝ d✝ : Concept α β r
src✝ : SemilatticeInf (Concept α β r) := instSemilatticeInfConcept
c d e : Concept α β r
⊢ c ≤ e → d ≤ e → c ⊔ d ≤ e
[PROOFSTEP]
simp_rw [← snd_subset_snd_iff]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c✝ d✝ : Concept α β r
src✝ : SemilatticeInf (Concept α β r) := instSemilatticeInfConcept
c d e : Concept α β r
⊢ e.snd ⊆ c.snd → e.snd ⊆ d.snd → e.snd ⊆ (c ⊔ d).snd
[PROOFSTEP]
exact subset_inter
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
S : Set (Concept α β r)
⊢ intentClosure r
      (extentClosure r (⋂ (c : Concept α β r) (_ : c ∈ S), c.snd), ⋂ (c : Concept α β r) (_ : c ∈ S), c.snd).fst =
    (extentClosure r (⋂ (c : Concept α β r) (_ : c ∈ S), c.snd), ⋂ (c : Concept α β r) (_ : c ∈ S), c.snd).snd
[PROOFSTEP]
simp_rw [← closure_fst, ← intentClosure_iUnion₂, intentClosure_extentClosure_intentClosure]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
S : Set (Concept α β r)
⊢ extentClosure r
      (⋂ (c : Concept α β r) (_ : c ∈ S), c.fst, intentClosure r (⋂ (c : Concept α β r) (_ : c ∈ S), c.fst)).snd =
    (⋂ (c : Concept α β r) (_ : c ∈ S), c.fst, intentClosure r (⋂ (c : Concept α β r) (_ : c ∈ S), c.fst)).fst
[PROOFSTEP]
simp_rw [← closure_snd, ← extentClosure_Union₂, extentClosure_intentClosure_extentClosure]
