-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Precoverage (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Membership.mem (γ := Set (Presieve.{v, u} (X i))) (J.coverings (X i)) (Presieve.ofArrows (Y i) (g i))
ι' : Type (max u v) := (↑(Presieve.ofArrows X f).uncurry : Type (max u v))
σ' : (i : ι') → Type (max u v) :=
  fun (i : ι') ↦
    (↑(Presieve.uncurry (Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯)))) :
      Type (max u v))
α : Type (max u v) :=
  (↑(Presieve.uncurry
        (Presieve.ofArrows
          (fun (p : (i : ι) × σ i) ↦ Y (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
          fun (x : (i : ι) × σ i) ↦
          g (x.fst (β := fun (i : ι) ↦ σ i)) (x.snd (β := fun (i : ι) ↦ σ i)) ≫ f (x.fst (β := fun (i : ι) ↦ σ i)))) :
    Type (max u v))
τ' : (a : α) → Type (max u v) :=
  fun (a : α) ↦
    (↑(Presieve.uncurry
          (Presieve.ofArrows (Y ((Presieve.ofArrows.idx ⋯).fst (β := fun (i : ι) ↦ σ i)))
            (g ((Presieve.ofArrows.idx ⋯).fst (β := fun (i : ι) ↦ σ i))))) :
      Type (max u v))
fib : (i : ι' ⊕ α) → Type (max u v) := fun (i : ι' ⊕ α) ↦ Sum.elim (fun (i : ι') ↦ σ' i) (fun (i : α) ↦ Unit ⊕ τ' i) i
incl : (p : ι' ⊕ α) → ι :=
  fun (p : ι' ⊕ α) ↦
    Sum.elim (fun (i : ι') ↦ Presieve.ofArrows.idx ⋯)
      (fun (i : α) ↦ (Presieve.ofArrows.idx ⋯).fst (β := fun (i : ι) ↦ σ i)) p
fibincl : (i : ι' ⊕ α) → (j : fib i) → σ (incl i) :=
  fun (i : ι' ⊕ α) (j : fib i) ↦
    match (motive := (i : ι' ⊕ α) → (j : fib i) → σ (incl i)) i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j =>
      Sum.elim (fun (x : Unit) ↦ (Presieve.ofArrows.idx ⋯).snd (β := fun (i : ι) ↦ σ i))
        (fun (i_1 : τ' i) ↦ Presieve.ofArrows.idx ⋯) j
⊢ Eq (α := Presieve.{v, u} S)
    (Presieve.ofArrows (fun (p : (i : ι) × σ i) ↦ Y (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
      fun (x : (i : ι) × σ i) ↦
      g (x.fst (β := fun (i : ι) ↦ σ i)) (x.snd (β := fun (i : ι) ↦ σ i)) ≫ f (x.fst (β := fun (i : ι) ↦ σ i)))
    (Presieve.ofArrows
      (fun (p : (i : ι' ⊕ α) × fib i) ↦
        Y (incl (p.fst (β := fun (i : ι' ⊕ α) ↦ fib i)))
          (fibincl (p.fst (β := fun (i : ι' ⊕ α) ↦ fib i)) (p.snd (β := fun (i : ι' ⊕ α) ↦ fib i))))
      fun (p : (i : ι' ⊕ α) × fib i) ↦
      g (incl (p.fst (β := fun (i : ι' ⊕ α) ↦ fib i)))
          (fibincl (p.fst (β := fun (i : ι' ⊕ α) ↦ fib i)) (p.snd (β := fun (i : ι' ⊕ α) ↦ fib i))) ≫
        f (incl (p.fst (β := fun (i : ι' ⊕ α) ↦ fib i))))
have h : ∀ (T : C) (u : T ⟶ S)
  (hu :
    Presieve.ofArrows (fun (p : (i : ι) × σ i) ↦ Y (p.fst (β := fun (i : ι) ↦ σ i)) (p.snd (β := fun (i : ι) ↦ σ i)))
      (fun (x : (i : ι) × σ i) ↦
        g (x.fst (β := fun (i : ι) ↦ σ i)) (x.snd (β := fun (i : ι) ↦ σ i)) ≫ f (x.fst (β := fun (i : ι) ↦ σ i)))
      u),
  Presieve.ofArrows
    (fun (p : (i : ι' ⊕ α) × fib i) ↦
      Y (incl (p.fst (β := fun (i : ι' ⊕ α) ↦ fib i)))
        (fibincl (p.fst (β := fun (i : ι' ⊕ α) ↦ fib i)) (p.snd (β := fun (i : ι' ⊕ α) ↦ fib i))))
    (fun (p : (i : ι' ⊕ α) × fib i) ↦
      g (incl (p.fst (β := fun (i : ι' ⊕ α) ↦ fib i)))
          (fibincl (p.fst (β := fun (i : ι' ⊕ α) ↦ fib i)) (p.snd (β := fun (i : ι' ⊕ α) ↦ fib i))) ≫
        f (incl (p.fst (β := fun (i : ι' ⊕ α) ↦ fib i))))
    u
Tactic: refine le_antisymm (fun T u hu ↦ ?_) fun T u ⟨p⟩ ↦ .mk (Sigma.mk (incl p.1) (fibincl p.1 p.2))