-- Module: Mathlib.CategoryTheory.Sites.Precoverage
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
h :
  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))))
convert_to :
  (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)))) ∈
    J.coverings 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))) ∈
    J.coverings S

Tactic:
convert_to Presieve.ofArrows _
      (fun p : Σ (i : ι' ⊕ α), fib i ↦ g (incl p.1) (fibincl _ p.2) ≫ f (incl p.1)) ∈ J.coverings S

Premises used: Sigma.fst, CategoryTheory.CategoryStruct.comp, CategoryTheory.Precoverage.coverings, Sigma.snd, CategoryTheory.Presieve.ofArrows