awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine_1 : (Presieve.ofArrows (fun (i : ι' ⊕ α) ↦ X (incl i)) fun (i : ι' ⊕ α) ↦ f (incl i)) ∈ J.coverings S
refine_2 :
  ∀ (i : ι' ⊕ α),
    Membership.mem (γ := Set (Presieve.{v, u} (X (incl i)))) (J.coverings (X (incl i)))
      (Presieve.ofArrows (fun (j : fib i) ↦ Y (incl i) (fibincl i j))
        ((fun (i : ι' ⊕ α) (j : fib i) ↦ g (incl i) (fibincl i j)) 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)))) ∈
    J.coverings S

Tactic:
refine IsStableUnderComposition.comp_mem_coverings (f := fun i ↦ f (incl i))
        (g := fun i j ↦ g (incl i) (fibincl i j)) ?_ fun i ↦ ?_

Premises used: CategoryTheory.Precoverage.IsStableUnderComposition.comp_mem_coverings
-- 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
⊢ Presieve.ofArrows X f ∈ J.coverings S

Tactic:
hf
-- 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 : (Presieve.ofArrows (fun (i : ι' ⊕ α) ↦ X (incl i)) fun (i : ι' ⊕ α) ↦ f (incl i)) = Presieve.ofArrows X f
⊢ (Presieve.ofArrows (fun (i : ι' ⊕ α) ↦ X (incl i)) fun (i : ι' ⊕ α) ↦ f (incl i)) ∈ J.coverings S

Tactic:
convert! hf
-- 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
⊢ (Presieve.ofArrows (fun (i : ι' ⊕ α) ↦ X (incl i)) fun (i : ι' ⊕ α) ↦ f (incl i)) = Presieve.ofArrows X f

Tactic:
le_antisymm (fun T u ⟨p⟩ ↦ .mk _) fun T u hu ↦ ?_

Premises used: le_antisymm
-- 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 :
  ∀ (T : C) (u : T ⟶ S) (hu : Presieve.ofArrows X f u),
    Presieve.ofArrows (fun (i : ι' ⊕ α) ↦ X (incl i)) (fun (i : ι' ⊕ α) ↦ f (incl i)) u
⊢ (Presieve.ofArrows (fun (i : ι' ⊕ α) ↦ X (incl i)) fun (i : ι' ⊕ α) ↦ f (incl i)) = Presieve.ofArrows X f

Tactic:
refine le_antisymm (fun T u ⟨p⟩ ↦ .mk _) fun T u hu ↦ ?_

Premises used: le_antisymm
-- 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
T : C
u : T ⟶ S
hu : Presieve.ofArrows X f u
⊢ Presieve.ofArrows (fun (i : ι' ⊕ α) ↦ X (incl i)) (fun (i : ι' ⊕ α) ↦ f (incl i)) u

Tactic:
exact .mk' (Sum.inl ⟨⟨_, _⟩, hu⟩) (by cat_disch) (by cat_disch)
-- 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
i : ι' ⊕ α
⊢ Membership.mem (γ := Set (Presieve.{v, u} (X (incl i)))) (J.coverings (X (incl i)))
    (Presieve.ofArrows (Y (incl i)) (g (incl i)))

Tactic:
hg (incl i)
-- 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
i : ι' ⊕ α
h :
  Eq (α := Presieve.{v, u} (X (incl i)))
    (Presieve.ofArrows (fun (j : fib i) ↦ Y (incl i) (fibincl i j))
      ((fun (i : ι' ⊕ α) (j : fib i) ↦ g (incl i) (fibincl i j)) i))
    (Presieve.ofArrows (Y (incl i)) (g (incl i)))
⊢ Membership.mem (γ := Set (Presieve.{v, u} (X (incl i)))) (J.coverings (X (incl i)))
    (Presieve.ofArrows (fun (j : fib i) ↦ Y (incl i) (fibincl i j))
      ((fun (i : ι' ⊕ α) (j : fib i) ↦ g (incl i) (fibincl i j)) i))

Tactic:
convert! hg (incl i)
-- 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
i : ι' ⊕ α
⊢ Eq (α := Presieve.{v, u} (X (incl i)))
    (Presieve.ofArrows (fun (j : fib i) ↦ Y (incl i) (fibincl i j))
      ((fun (i : ι' ⊕ α) (j : fib i) ↦ g (incl i) (fibincl i j)) i))
    (Presieve.ofArrows (Y (incl i)) (g (incl i)))

Tactic:
le_antisymm (fun T u ⟨p⟩ ↦ .mk _) fun T u hu ↦ ?_

Premises used: le_antisymm
-- 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
i : ι' ⊕ α
h :
  ∀ (T : C) (u : T ⟶ X (incl i)) (hu : Presieve.ofArrows (Y (incl i)) (g (incl i)) u),
    Presieve.ofArrows (fun (j : fib i) ↦ Y (incl i) (fibincl i j))
      ((fun (i : ι' ⊕ α) (j : fib i) ↦ g (incl i) (fibincl i j)) i) u
⊢ Eq (α := Presieve.{v, u} (X (incl i)))
    (Presieve.ofArrows (fun (j : fib i) ↦ Y (incl i) (fibincl i j))
      ((fun (i : ι' ⊕ α) (j : fib i) ↦ g (incl i) (fibincl i j)) i))
    (Presieve.ofArrows (Y (incl i)) (g (incl i)))

Tactic:
refine le_antisymm (fun T u ⟨p⟩ ↦ .mk _) fun T u hu ↦ ?_

Premises used: le_antisymm