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.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g_1 : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g_1 (f i)
a : (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) →
  ι :=
  fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
    Sum.elim (fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯)
      (fun (i : (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯) i
Z : C
g : Z ⟶ Y
hg : Presieve.ofArrows P p₁ g
⊢ Presieve.ofArrows (P ∘ a)
    (fun
        (i :
          (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
      p₁ (a i))
    g

Tactic:
exact .mk' (Sum.inr ⟨⟨_, _⟩, hg⟩) (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.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
a : (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) →
  ι :=
  fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
    Sum.elim (fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯)
      (fun (i : (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯) i
⊢ (Presieve.ofArrows (P ∘ a)
      fun
        (i :
          (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
      p₁ (a i)) ∈
    J.coverings Y

Tactic:
IsStableUnderBaseChange.mem_coverings_of_isPullback (fun i ↦ f (a i)) ?_ g _
      (fun i ↦ p₂ (a i)) fun i ↦ h _

Premises used: CategoryTheory.Precoverage.IsStableUnderBaseChange.mem_coverings_of_isPullback
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
a : (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) →
  ι :=
  fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
    Sum.elim (fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯)
      (fun (i : (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯) i
convert_4 :
  (Presieve.ofArrows
      (fun
          (i :
            (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕
              (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
        X (a i))
      fun
        (i :
          (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
      f (a i)) ∈
    J.coverings S
⊢ (Presieve.ofArrows (P ∘ a)
      fun
        (i :
          (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
      p₁ (a i)) ∈
    J.coverings Y

Tactic:
refine IsStableUnderBaseChange.mem_coverings_of_isPullback (fun i ↦ f (a i)) ?_ g _
      (fun i ↦ p₂ (a i)) fun i ↦ h _

Premises used: CategoryTheory.Precoverage.IsStableUnderBaseChange.mem_coverings_of_isPullback
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
a : (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) →
  ι :=
  fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
    Sum.elim (fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯)
      (fun (i : (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯) i
⊢ Presieve.ofArrows X f ∈ J.coverings S

Tactic:
hR
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
a : (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) →
  ι :=
  fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
    Sum.elim (fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯)
      (fun (i : (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯) i
h₁ :
  (Presieve.ofArrows
      (fun
          (i :
            (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕
              (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
        X (a i))
      fun
        (i :
          (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
      f (a i)) =
    Presieve.ofArrows X f
⊢ (Presieve.ofArrows
      (fun
          (i :
            (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕
              (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
        X (a i))
      fun
        (i :
          (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
      f (a i)) ∈
    J.coverings S

Tactic:
convert! hR
-- Module: Mathlib.CategoryTheory.Sites.Precoverage
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
a : (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) →
  ι :=
  fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
    Sum.elim (fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯)
      (fun (i : (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯) i
⊢ (Presieve.ofArrows
      (fun
          (i :
            (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕
              (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
        X (a i))
      fun
        (i :
          (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
      f (a i)) =
    Presieve.ofArrows X f

Tactic:
le_antisymm (fun Z g ⟨i⟩ ↦ .mk _) fun Z g hg ↦ ?_

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.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
a : (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) →
  ι :=
  fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
    Sum.elim (fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯)
      (fun (i : (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯) i
h₁ :
  ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows X f g),
    Presieve.ofArrows
      (fun
          (i :
            (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕
              (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
        X (a i))
      (fun
          (i :
            (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕
              (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
        f (a i))
      g
⊢ (Presieve.ofArrows
      (fun
          (i :
            (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕
              (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
        X (a i))
      fun
        (i :
          (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
      f (a i)) =
    Presieve.ofArrows X f

Tactic:
refine le_antisymm (fun Z g ⟨i⟩ ↦ .mk _) fun Z g hg ↦ ?_

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.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g_1 : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g_1 (f i)
a : (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) →
  ι :=
  fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
    Sum.elim (fun (i : (↑(Presieve.ofArrows X f).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯)
      (fun (i : (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦ Presieve.ofArrows.idx ⋯) i
Z : C
g : Z ⟶ S
hg : Presieve.ofArrows X f g
⊢ Presieve.ofArrows
    (fun
        (i :
          (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
      X (a i))
    (fun
        (i :
          (↑(Presieve.ofArrows X f).uncurry : Type (max u v)) ⊕ (↑(Presieve.ofArrows P p₁).uncurry : Type (max u v))) ↦
      f (a i))
    g

Tactic:
exact .mk' (Sum.inl ⟨⟨_, _⟩, hg⟩) (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
⊢ 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))))

Tactic:
le_antisymm (fun T u hu ↦ ?_) fun T u ⟨p⟩ ↦ .mk (Sigma.mk (incl p.1) (fibincl p.1 p.2))

Premises used: CategoryTheory.Presieve.ofArrows.mk, _private.0.CategoryTheory.Precoverage.comp_mem_coverings.match_2, Sigma.fst, le_antisymm, CategoryTheory.CategoryStruct.comp, Sigma.mk, Sigma.snd, CategoryTheory.Presieve.ofArrows
-- 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 (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:
.mk' ⟨Sum.inr ⟨⟨_, _⟩, hu⟩, .inl ⟨⟩⟩ hu.obj_idx.symm hu.eq_eqToHom_comp_hom_idx

Premises used: CategoryTheory.Presieve.ofArrows.mk', Sum.inl, CategoryTheory.Presieve.ofArrows.eq_eqToHom_comp_hom_idx, Subtype.mk, Sum.inr, PUnit.unit, Sigma.mk, Eq.symm, CategoryTheory.Presieve.ofArrows.obj_idx
-- 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 (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:
exact .mk' ⟨Sum.inr ⟨⟨_, _⟩, hu⟩, .inl ⟨⟩⟩ hu.obj_idx.symm hu.eq_eqToHom_comp_hom_idx
-- 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 (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:
IsStableUnderComposition.comp_mem_coverings (f := fun i ↦ f (incl i))
        (g := fun i j ↦ g (incl i) (fibincl i j)) ?_ fun i ↦ ?_

Premises used: Set.Mem, CategoryTheory.Precoverage.IsStableUnderComposition.comp_mem_coverings