awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.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 p₁ ∈ J.coverings Y
have h₁ : Presieve.ofArrows P p₁ =
  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)
Tactic: convert_to Presieve.ofArrows (P ∘ a) (fun i ↦ p₁ (a i)) ∈ _
-- 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.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 P p₁ =
    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)
⊢ Presieve.ofArrows P p₁ ∈ J.coverings Y
have convert_4 : (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: convert_to Presieve.ofArrows (P ∘ a) (fun i ↦ p₁ (a i)) ∈ _
-- 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.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 p₁ =
    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)
have h₁ : ∀ (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: refine le_antisymm (fun Z g hg ↦ ?_) fun Z g ⟨i⟩ ↦ ⟨a i⟩
-- 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.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
have 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
Tactic: refine IsStableUnderBaseChange.mem_coverings_of_isPullback (fun i ↦ f (a i)) ?_ g _
      (fun i ↦ p₂ (a i)) fun i ↦ h _
-- 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.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)) ∈
    J.coverings S
have 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
Tactic: convert! hR
-- 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.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
have 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
Tactic: refine le_antisymm (fun Z g ⟨i⟩ ↦ .mk _) fun Z g hg ↦ ?_
-- 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
⊢ (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
have 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))))
Tactic: convert_to Presieve.ofArrows _
      (fun p : Σ (i : ι' ⊕ α), fib i ↦ g (incl p.1) (fibincl _ p.2) ≫ f (incl p.1)) ∈ J.coverings S
-- 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
⊢ (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
have refine_1 : (Presieve.ofArrows (fun (i : ι' ⊕ α) ↦ X (incl i)) fun (i : ι' ⊕ α) ↦ f (incl 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 ↦ ?_
-- 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
refine_1 : (Presieve.ofArrows (fun (i : ι' ⊕ α) ↦ X (incl i)) fun (i : ι' ⊕ α) ↦ f (incl i)) ∈ J.coverings S
⊢ (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
have 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))
Tactic: refine IsStableUnderComposition.comp_mem_coverings (f := fun i ↦ f (incl i))
        (g := fun i j ↦ g (incl i) (fibincl i j)) ?_ fun i ↦ ?_
-- 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
⊢ (Presieve.ofArrows (fun (i : ι' ⊕ α) ↦ X (incl i)) fun (i : ι' ⊕ α) ↦ f (incl i)) ∈ J.coverings S
have h : (Presieve.ofArrows (fun (i : ι' ⊕ α) ↦ X (incl i)) fun (i : ι' ⊕ α) ↦ f (incl i)) = Presieve.ofArrows X f
Tactic: convert! hf
-- 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
⊢ (Presieve.ofArrows (fun (i : ι' ⊕ α) ↦ X (incl i)) fun (i : ι' ⊕ α) ↦ f (incl i)) = Presieve.ofArrows X f
have 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
Tactic: refine le_antisymm (fun T u ⟨p⟩ ↦ .mk _) fun T u hu ↦ ?_