-- Mathlib/Order/Concept.lean
theorem ext (h : c.fst = d.fst) : c = d

Proof state:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.toProd.1 = d.toProd.1
⊢ c = d

Tactic:
obtain ⟨⟨s₁, t₁⟩, h₁, _⟩ := c

Result:
case mk.mk
α : Type u_2
β : Type u_3
r : α → β → Prop
d : Concept α β r
s₁ : Set α
t₁ : Set β
h₁ : intentClosure r (s₁, t₁).1 = (s₁, t₁).2
closure_snd✝ : extentClosure r (s₁, t₁).2 = (s₁, t₁).1
h : { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝ }.toProd.1 = d.toProd.1
⊢ { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝ } = d

Proof state:
case mk.mk.mk.mk
α : Type u_2
β : Type u_3
r : α → β → Prop
s₁ : Set α
t₁ : Set β
h₁ : intentClosure r (s₁, t₁).1 = (s₁, t₁).2
closure_snd✝¹ : extentClosure r (s₁, t₁).2 = (s₁, t₁).1
s₂ : Set α
t₂ : Set β
h₂ : intentClosure r (s₂, t₂).1 = (s₂, t₂).2
closure_snd✝ : extentClosure r (s₂, t₂).2 = (s₂, t₂).1
h :
  { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝¹ }.toProd.1 =
    { toProd := (s₂, t₂), closure_fst := h₂, closure_snd := closure_snd✝ }.toProd.1
⊢ { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝¹ } =
    { toProd := (s₂, t₂), closure_fst := h₂, closure_snd := closure_snd✝ }

Tactic:
dsimp at h₁ h₂ h

Result:
case mk.mk.mk.mk
α : Type u_2
β : Type u_3
r : α → β → Prop
s₁ : Set α
t₁ : Set β
h₁ : intentClosure r s₁ = t₁
closure_snd✝¹ : extentClosure r (s₁, t₁).2 = (s₁, t₁).1
s₂ : Set α
t₂ : Set β
h₂ : intentClosure r s₂ = t₂
closure_snd✝ : extentClosure r (s₂, t₂).2 = (s₂, t₂).1
h : s₁ = s₂
⊢ { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝¹ } =
    { toProd := (s₂, t₂), closure_fst := h₂, closure_snd := closure_snd✝ }

Proof state:
case mk.mk.mk.mk
α : Type u_2
β : Type u_3
r : α → β → Prop
s₁ : Set α
t₁ : Set β
h₁ : intentClosure r s₁ = t₁
closure_snd✝¹ : extentClosure r (s₁, t₁).2 = (s₁, t₁).1
s₂ : Set α
t₂ : Set β
h₂ : intentClosure r s₂ = t₂
closure_snd✝ : extentClosure r (s₂, t₂).2 = (s₂, t₂).1
h : s₁ = s₂
⊢ { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝¹ } =
    { toProd := (s₂, t₂), closure_fst := h₂, closure_snd := closure_snd✝ }

Tactic:
substs h h₁ h₂

Result:
case mk.mk.mk.mk
α : Type u_2
β : Type u_3
r : α → β → Prop
s₁ : Set α
closure_snd✝¹ closure_snd✝ : extentClosure r (s₁, intentClosure r s₁).2 = (s₁, intentClosure r s₁).1
⊢ { toProd := (s₁, intentClosure r s₁), closure_fst := ⋯, closure_snd := closure_snd✝¹ } =
    { toProd := (s₁, intentClosure r s₁), closure_fst := ⋯, closure_snd := closure_snd✝ }

Proof state:
case mk.mk.mk.mk
α : Type u_2
β : Type u_3
r : α → β → Prop
s₁ : Set α
closure_snd✝¹ closure_snd✝ : extentClosure r (s₁, intentClosure r s₁).2 = (s₁, intentClosure r s₁).1
⊢ { toProd := (s₁, intentClosure r s₁), closure_fst := ⋯, closure_snd := closure_snd✝¹ } =
    { toProd := (s₁, intentClosure r s₁), closure_fst := ⋯, closure_snd := closure_snd✝ }

Tactic:
rfl

Result:
no goals

Proof state:
case mk.mk
α : Type u_2
β : Type u_3
r : α → β → Prop
d : Concept α β r
s₁ : Set α
t₁ : Set β
h₁ : intentClosure r (s₁, t₁).1 = (s₁, t₁).2
closure_snd✝ : extentClosure r (s₁, t₁).2 = (s₁, t₁).1
h : { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝ }.toProd.1 = d.toProd.1
⊢ { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝ } = d

Tactic:
obtain ⟨⟨s₂, t₂⟩, h₂, _⟩ := d

Result:
case mk.mk.mk.mk
α : Type u_2
β : Type u_3
r : α → β → Prop
s₁ : Set α
t₁ : Set β
h₁ : intentClosure r (s₁, t₁).1 = (s₁, t₁).2
closure_snd✝¹ : extentClosure r (s₁, t₁).2 = (s₁, t₁).1
s₂ : Set α
t₂ : Set β
h₂ : intentClosure r (s₂, t₂).1 = (s₂, t₂).2
closure_snd✝ : extentClosure r (s₂, t₂).2 = (s₂, t₂).1
h :
  { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝¹ }.toProd.1 =
    { toProd := (s₂, t₂), closure_fst := h₂, closure_snd := closure_snd✝ }.toProd.1
⊢ { toProd := (s₁, t₁), closure_fst := h₁, closure_snd := closure_snd✝¹ } =
    { toProd := (s₂, t₂), closure_fst := h₂, closure_snd := closure_snd✝ }