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

Proof state:
case mk.mk.mk.mk
α : Type u_2
β : Type u_3
r : α → β → Prop
t₁ : Set β
closure_fst✝¹ closure_fst✝ : intentClosure r (extentClosure r t₁, t₁).1 = (extentClosure r t₁, t₁).2
⊢ { toProd := (extentClosure r t₁, t₁), closure_fst := closure_fst✝¹, closure_snd := ⋯ } =
    { toProd := (extentClosure r t₁, t₁), closure_fst := closure_fst✝, 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 β
closure_fst✝ : intentClosure r (s₁, t₁).1 = (s₁, t₁).2
h₁ : extentClosure r (s₁, t₁).2 = (s₁, t₁).1
h : { toProd := (s₁, t₁), closure_fst := closure_fst✝, closure_snd := h₁ }.toProd.2 = d.toProd.2
⊢ { toProd := (s₁, t₁), closure_fst := closure_fst✝, closure_snd := h₁ } = 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 β
closure_fst✝¹ : intentClosure r (s₁, t₁).1 = (s₁, t₁).2
h₁ : extentClosure r (s₁, t₁).2 = (s₁, t₁).1
s₂ : Set α
t₂ : Set β
closure_fst✝ : intentClosure r (s₂, t₂).1 = (s₂, t₂).2
h₂ : extentClosure r (s₂, t₂).2 = (s₂, t₂).1
h :
  { toProd := (s₁, t₁), closure_fst := closure_fst✝¹, closure_snd := h₁ }.toProd.2 =
    { toProd := (s₂, t₂), closure_fst := closure_fst✝, closure_snd := h₂ }.toProd.2
⊢ { toProd := (s₁, t₁), closure_fst := closure_fst✝¹, closure_snd := h₁ } =
    { toProd := (s₂, t₂), closure_fst := closure_fst✝, closure_snd := h₂ }

Proof state:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
h : c.toProd.2 = d.toProd.2
⊢ 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 β
closure_fst✝ : intentClosure r (s₁, t₁).1 = (s₁, t₁).2
h₁ : extentClosure r (s₁, t₁).2 = (s₁, t₁).1
h : { toProd := (s₁, t₁), closure_fst := closure_fst✝, closure_snd := h₁ }.toProd.2 = d.toProd.2
⊢ { toProd := (s₁, t₁), closure_fst := closure_fst✝, closure_snd := h₁ } = d

Proof state:
case mk.mk.mk.mk
α : Type u_2
β : Type u_3
r : α → β → Prop
s₁ : Set α
t₁ : Set β
closure_fst✝¹ : intentClosure r (s₁, t₁).1 = (s₁, t₁).2
h₁ : extentClosure r t₁ = s₁
s₂ : Set α
t₂ : Set β
closure_fst✝ : intentClosure r (s₂, t₂).1 = (s₂, t₂).2
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₂ }

Tactic:
substs h h₁ h₂

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

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

Tactic:
dsimp at h₁ h₂ h

Result:
case mk.mk.mk.mk
α : Type u_2
β : Type u_3
r : α → β → Prop
s₁ : Set α
t₁ : Set β
closure_fst✝¹ : intentClosure r (s₁, t₁).1 = (s₁, t₁).2
h₁ : extentClosure r t₁ = s₁
s₂ : Set α
t₂ : Set β
closure_fst✝ : intentClosure r (s₂, t₂).1 = (s₂, t₂).2
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₂ }