Understanding Girard's Paradox

Stream: mathlib4

[Devon Andrews]

I am trying to understand the following formalization of Girard's Paradox from mathlib4:

theorem girard.{u} (pi : (Type u → Type u) → Type u)
    (lam : ∀ {A : Type u → Type u}, (∀ x, A x) → pi A) (app : ∀ {A}, pi A → ∀ x, A x)
    (beta : ∀ {A : Type u → Type u} (f : ∀ x, A x) (x), app (lam f) x = f x) : False :=
  let F (X) := (Set (Set X) → X) → Set (Set X)
  let U := pi F
  let G (T : Set (Set U)) (X) : F X := fun f => {p | {x : U | f (app x X f) ∈ p} ∈ T}
  let τ (T : Set (Set U)) : U := lam (G T)
  let σ (S : U) : Set (Set U) := app S U τ
  have στ : ∀ {s S}, s ∈ σ (τ S) ↔ {x | τ (σ x) ∈ s} ∈ S := fun {s S} =>
    iff_of_eq (congr_arg (fun f : F U => s ∈ f τ) (beta (G S) U) :)
  let ω : Set (Set U) := {p | ∀ x, p ∈ σ x → x ∈ p}
  let δ (S : Set (Set U)) := ∀ p, p ∈ S → τ S ∈ p
  have : δ ω := fun _p d => d (τ ω) <| στ.2 fun x h => d (τ (σ x)) (στ.2 h)
  this {y | ¬δ (σ y)} (fun _x e f => f _ e fun _p h => f _ (στ.1 h)) fun _p h => this _ (στ.1 h)

I understand every line syntactically except for the last two lines. I would appreciate if someone could provide me with an explanation or a syntactically easier version of the last two lines, even if the proof ends up much longer

[Aaron Liu]

Does it help if I write it out like this?

  have this : δ ω := by
    intro _ d
    apply d (τ ω)
    rw [στ]
    intro x h
    apply d (τ (σ x))
    rw [στ]
    exact h
  by
    refine this {y | ¬δ (σ y)} ?_ ?_
    · intro _ e f
      apply f _ e
      intro _ h
      exact f _ (στ.mp h)
    · intro _ h
      exact this _ (στ.mp h)

[Ruben Van de Velde]

That's uh... Write-only code

[Kevin Buzzard]

yeah this was just Mario demonstrating how few lines he could get it into.