case mk.mk
ι : Sort ?u.5798
α : Type u_1
β : Type u_2
γ : Type ?u.5807
κ : ι → Sort ?u.5812
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
ι : Sort ?u.5798
α : Type u_1
β : Type u_2
γ : Type ?u.5807
κ : ι → Sort ?u.5812
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
h : c.fst = d.fst
⊢ c = d
obtain ⟨⟨s₁, t₁⟩, h₁, _⟩ := c
case mk.mk.mk.mk
ι : Sort ?u.5798
α : Type u_1
β : Type u_2
γ : Type ?u.5807
κ : ι → Sort ?u.5812
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✝ }
case mk.mk
ι : Sort ?u.5798
α : Type u_1
β : Type u_2
γ : Type ?u.5807
κ : ι → Sort ?u.5812
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
obtain ⟨⟨s₂, t₂⟩, h₂, _⟩ := d
case mk.mk.mk.mk
ι : Sort ?u.5798
α : Type u_1
β : Type u_2
γ : Type ?u.5807
κ : ι → Sort ?u.5812
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✝ }
case mk.mk.mk.mk
ι : Sort ?u.5798
α : Type u_1
β : Type u_2
γ : Type ?u.5807
κ : ι → Sort ?u.5812
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✝ }
dsimp at h₁ h₂ h
case mk.mk.mk.mk
ι : Sort ?u.5798
α : Type u_1
β : Type u_2
γ : Type ?u.5807
κ : ι → Sort ?u.5812
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✝ }
case mk.mk.mk.mk
ι : Sort ?u.5798
α : Type u_1
β : Type u_2
γ : Type ?u.5807
κ : ι → Sort ?u.5812
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✝ }
substs h h₁ h₂
no goals
case mk.mk.mk.mk
ι : Sort ?u.5798
α : Type u_1
β : Type u_2
γ : Type ?u.5807
κ : ι → Sort ?u.5812
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✝ }
rfl