Can this Kuratowski pair injection proof be golfed?

Stream: new members

[Dan Abramov]

Here's what I got.

import Mathlib.Tactic

def kpair (a b : Nat) : Set (Set Nat) :=
  {{a}, {a, b}}

lemma kpair_injective : ∀ a₁ b₁ a₂ b₂, kpair a₁ b₁ = kpair a₂ b₂ → a₁ = a₂ ∧ b₁ = b₂ := by
  intro a1 b1 a2 b2 h
  unfold kpair at h
  constructor
  · contrapose! h
    intro hs
    rw [Set.ext_iff] at hs
    specialize hs {a1}
    simp only [Set.mem_insert_iff, Set.mem_singleton_iff, true_or] at hs
    rw [← Set.pair_eq_singleton a1, Set.pair_eq_pair_iff] at hs
    simp_all
  contrapose! h
  intro hs
  simp only [Set.pair_eq_pair_iff] at hs
  rcases hs with (_ | ⟨h1, h2⟩)
  · aesop
  rw [← Set.pair_eq_singleton a1, Set.pair_eq_pair_iff] at h1
  rw [← Set.pair_eq_singleton a2, Set.pair_eq_pair_iff] at h2
  simp_all

This is the shortest / simplest I could make it so far. Is there any way to further golf it?

[Dan Abramov]

In particular I guess I was hoping I can somehow pattern-match on the shape of these sets.

[Aaron Liu]

I golfed it a bit

import Mathlib.Tactic

def kpair (a b : Nat) : Set (Set Nat) :=
  {{a}, {a, b}}

theorem Set.singleton_eq_pair_iff {α : Type u} {x z w : α} : ({x} : Set α) = {z, w} ↔ x = z ∧ x = w := by
  rw [← Set.pair_eq_singleton x, Set.pair_eq_pair_iff]
  tauto

theorem Set.pair_eq_singleton_iff {α : Type u} {x y z : α} : ({x, y} : Set α) = {z} ↔ x = z ∧ y = z := by
  rw [← Set.pair_eq_singleton z, Set.pair_eq_pair_iff]
  tauto

lemma kpair_injective (a₁ b₁ a₂ b₂ : Nat) (h : kpair a₁ b₁ = kpair a₂ b₂) : a₁ = a₂ ∧ b₁ = b₂ := by
  unfold kpair at h
  obtain rfl : a₁ = a₂ := by
    have hs := congr({a₁} ∈ $h)
    simp [Set.singleton_eq_pair_iff] at hs
    tauto
  refine ⟨rfl, ?_⟩
  simp [Set.pair_eq_pair_iff, Set.singleton_eq_pair_iff, Set.pair_eq_singleton_iff] at h
  rcases h with _ | ⟨_, _⟩ <;> cc

[Dan Abramov]

Ah thanks, learned a few tricks from this.

[Dan Abramov]

Can you explain what this line does?

have hs := congr({a₁} ∈ $h)

[Aaron Liu]

Did you read the docstring?

[Dan Abramov]

Ah I didn't realize $ notation is part of congr itself, makes sense