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