awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h : EffectiveEpi g
hp :
  (EffectiveEpiFamily.{v_1, u_1, 0} (C := C) (B := Y) (fun (x : PUnit.{1}) ↦ Z) fun (x : PUnit.{1}) ↦ g) →
    ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
      EffectiveEpiFamily X₂ π₂ ∧ ∃ (ι : (b : β) → X₂ b ⟶ Z), ∀ (b : β), ι b ≫ g = π₂ b ≫ f
⊢ EffectiveEpi g →
    ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
      EffectiveEpiFamily X₂ π₂ ∧ ∃ (ι : (b : β) → X₂ b ⟶ Z), ∀ (b : β), ι b ≫ g = π₂ b ≫ f

Tactic:
rw [← effectiveEpi_iff_effectiveEpiFamily g] at hp

Premises used: CategoryTheory.effectiveEpi_iff_effectiveEpiFamily
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h : EffectiveEpi g
hp :
  EffectiveEpi g →
    ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
      EffectiveEpiFamily X₂ π₂ ∧ ∃ (ι : (b : β) → X₂ b ⟶ Z), ∀ (b : β), ι b ≫ g = π₂ b ≫ f
obtain :
  ∀ (β : Type),
    Finite β →
      ∀ (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X) (h : EffectiveEpiFamily X₂ π₂) (ι : (b : β) → X₂ b ⟶ Z)
        (hι : ∀ (b : β), ι b ≫ g = π₂ b ≫ f), ∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f
⊢ ∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f

Tactic:
obtain ⟨β, _, X₂, π₂, h, ι, hι⟩ := hp inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h_1 : EffectiveEpi g
hp :
  EffectiveEpi g →
    ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
      EffectiveEpiFamily X₂ π₂ ∧ ∃ (ι : (b : β) → X₂ b ⟶ Z), ∀ (b : β), ι b ≫ g = π₂ b ≫ f
β : Type
w : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ X
h : EffectiveEpiFamily X₂ π₂
ι : (b : β) → X₂ b ⟶ Z
hι : ∀ (b : β), ι b ≫ g = π₂ b ≫ f
⊢ ∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f

Tactic:
⟨∐ X₂, Sigma.desc π₂, inferInstance, Sigma.desc ι, ?_⟩

Premises used: inferInstance, Exists.intro, CategoryTheory.Limits.Sigma.desc, CategoryTheory.Limits.sigmaObj
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h_1 : EffectiveEpi g
hp :
  EffectiveEpi g →
    ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
      EffectiveEpiFamily X₂ π₂ ∧ ∃ (ι : (b : β) → X₂ b ⟶ Z), ∀ (b : β), ι b ≫ g = π₂ b ≫ f
β : Type
w : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ X
h : EffectiveEpiFamily X₂ π₂
ι : (b : β) → X₂ b ⟶ Z
hι : ∀ (b : β), ι b ≫ g = π₂ b ≫ f
refine : Eq (α := sigmaObj.{0, v_1, u_1} X₂ ⟶ Y) (Sigma.desc ι ≫ g) (Sigma.desc π₂ ≫ f)
⊢ ∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f

Tactic:
refine ⟨∐ X₂, Sigma.desc π₂, inferInstance, Sigma.desc ι, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h_1 : EffectiveEpi g
hp :
  EffectiveEpi g →
    ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
      EffectiveEpiFamily X₂ π₂ ∧ ∃ (ι : (b : β) → X₂ b ⟶ Z), ∀ (b : β), ι b ≫ g = π₂ b ≫ f
β : Type
w : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ X
h : EffectiveEpiFamily X₂ π₂
ι : (b : β) → X₂ b ⟶ Z
hι : ∀ (b : β), ι b ≫ g = π₂ b ≫ f
h₁ :
  ∀ (b : β),
    CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} X₂) (Sigma.ι X₂ b) (Sigma.desc ι ≫ g) =
      CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} X₂) (Sigma.ι X₂ b) (Sigma.desc π₂ ≫ f)
⊢ Eq (α := sigmaObj.{0, v_1, u_1} X₂ ⟶ Y) (Sigma.desc ι ≫ g) (Sigma.desc π₂ ≫ f)

Tactic:
ext b
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Precoherent.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : Z ⟶ Y
h_1 : EffectiveEpi g
hp :
  EffectiveEpi g →
    ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ X),
      EffectiveEpiFamily X₂ π₂ ∧ ∃ (ι : (b : β) → X₂ b ⟶ Z), ∀ (b : β), ι b ≫ g = π₂ b ≫ f
β : Type
w : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ X
h : EffectiveEpiFamily X₂ π₂
ι : (b : β) → X₂ b ⟶ Z
hι : ∀ (b : β), ι b ≫ g = π₂ b ≫ f
b : β
⊢ CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} X₂) (Sigma.ι X₂ b) (Sigma.desc ι ≫ g) =
    CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} X₂) (Sigma.ι X₂ b) (Sigma.desc π₂ ≫ f)

Tactic:
simpa using hι b
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
⊢ ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ B₂),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : β → α) (ι : (b : β) → X₂ b ⟶ X₁ (i b)), ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f

Tactic:
⟨α, inferInstance, ?_⟩

Premises used: inferInstance, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
refine :
  ∃ (X₂ : α → C) (π₂ : (b : α) → X₂ b ⟶ B₂),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : α → α) (ι : (b : α) → X₂ b ⟶ X₁ (i b)), ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f
⊢ ∃ (β : Type) (_ : Finite β) (X₂ : β → C) (π₂ : (b : β) → X₂ b ⟶ B₂),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : β → α) (ι : (b : β) → X₂ b ⟶ X₁ (i b)), ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f

Tactic:
refine ⟨α, inferInstance, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
obtain :
  ∀ (Y : C) (g : Y ⟶ B₂),
    EffectiveEpi g →
      ∀ (g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁) (hg : g' ≫ Sigma.desc π₁ = g ≫ f),
        ∃ (X₂ : α → C) (π₂ : (b : α) → X₂ b ⟶ B₂),
          EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : α → α) (ι : (b : α) → X₂ b ⟶ X₁ (i b)), ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f
⊢ ∃ (X₂ : α → C) (π₂ : (b : α) → X₂ b ⟶ B₂),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : α → α) (ι : (b : α) → X₂ b ⟶ X₁ (i b)), ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f

Tactic:
obtain ⟨Y, g, _, g', hg⟩ := Preregular.exists_fac f (Sigma.desc π₁)

Premises used: CategoryTheory.Preregular.exists_fac, CategoryTheory.Limits.Sigma.desc
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
⊢ IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))

Tactic:
have _ := FinitaryPreExtensive.isIso_sigmaDesc_fst (fun a ↦ Sigma.ι X₁ a) g' inferInstance
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
⊢ ∃ (X₂ : α → C) (π₂ : (b : α) → X₂ b ⟶ B₂),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : α → α) (ι : (b : α) → X₂ b ⟶ X₁ (i b)), ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f

Tactic:
⟨X₂, π₂, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
refine_1 : EffectiveEpiFamily X₂ π₂
refine_2 : ∃ (i : α → α) (ι : (b : α) → X₂ b ⟶ X₁ (i b)), ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f
⊢ ∃ (X₂ : α → C) (π₂ : (b : α) → X₂ b ⟶ B₂),
    EffectiveEpiFamily X₂ π₂ ∧ ∃ (i : α → α) (ι : (b : α) → X₂ b ⟶ X₁ (i b)), ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f

Tactic:
refine ⟨X₂, π₂, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
h₁ :
  ∀ (b : α),
    CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b))
        (Sigma.ι.{0, v_1, u_1} (C := C) (fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b)) b) (Sigma.desc π' ≫ g) =
      CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b))
        (Sigma.ι.{0, v_1, u_1} (C := C) (fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b)) b) (Sigma.desc π₂)
⊢ Eq (α := (sigmaObj.{0, v_1, u_1} fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b)) ⟶ B₂) (Sigma.desc π' ≫ g)
    (Sigma.desc π₂)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
b : α
⊢ CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b))
      (Sigma.ι.{0, v_1, u_1} (C := C) (fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b)) b) (Sigma.desc π' ≫ g) =
    CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b))
      (Sigma.ι.{0, v_1, u_1} (C := C) (fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b)) b) (Sigma.desc π₂)

Tactic:
simp [π₂, π']
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
⊢ Eq (α := (sigmaObj.{0, v_1, u_1} fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b)) ⟶ B₂) (Sigma.desc π' ≫ g)
    (Sigma.desc π₂)

Tactic:
have : (Sigma.desc π' ≫ g) = Sigma.desc π₂ := by ext; simp [π₂, π']
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
this :
  Eq (α := (sigmaObj.{0, v_1, u_1} fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b)) ⟶ B₂) (Sigma.desc π' ≫ g)
    (Sigma.desc π₂)
refine_1 : EffectiveEpi (Y := sigmaObj.{0, v_1, u_1} X₂) (Sigma.desc π' ≫ g)
⊢ EffectiveEpiFamily X₂ π₂

Tactic:
rw [← effectiveEpi_desc_iff_effectiveEpiFamily, ← this]

Premises used: CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamily
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
this :
  Eq (α := (sigmaObj.{0, v_1, u_1} fun (b : α) ↦ Limits.pullback g' (Sigma.ι X₁ b)) ⟶ B₂) (Sigma.desc π' ≫ g)
    (Sigma.desc π₂)
⊢ EffectiveEpi (Y := sigmaObj.{0, v_1, u_1} X₂) (Sigma.desc π' ≫ g)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
⊢ ∃ (i : α → α) (ι : (b : α) → X₂ b ⟶ X₁ (i b)), ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f

Tactic:
⟨id, fun b ↦ pullback.snd _ _, fun b ↦ ?_⟩

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.Sigma.ι, id, Exists.intro
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
refine_2 :
  ∀ (b : α),
    CategoryStruct.comp (Y := X₁ (id b))
        ((fun (b : α) ↦ (pullback.snd g' (Sigma.ι X₁ b) : Limits.pullback g' (Sigma.ι X₁ b) ⟶ X₁ b)) b) (π₁ (id b)) =
      π₂ b ≫ f
⊢ ∃ (i : α → α) (ι : (b : α) → X₂ b ⟶ X₁ (i b)), ∀ (b : α), ι b ≫ π₁ (i b) = π₂ b ≫ f

Tactic:
refine ⟨id, fun b ↦ pullback.snd _ _, fun b ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
b : α
refine_2 :
  Eq (α := Limits.pullback g' (Sigma.ι X₁ b) ⟶ B₁) (pullback.snd g' (Sigma.ι X₁ b) ≫ π₁ b)
    (pullback.fst g' (Sigma.ι X₁ b) ≫ g' ≫ Sigma.desc π₁)
⊢ CategoryStruct.comp (Y := X₁ (id b))
      ((fun (b : α) ↦ (pullback.snd g' (Sigma.ι X₁ b) : Limits.pullback g' (Sigma.ι X₁ b) ⟶ X₁ b)) b) (π₁ (id b)) =
    π₂ b ≫ f

Tactic:
simp only [X₂, π₂, id_eq, Category.assoc, ← hg]

Premises used: CategoryTheory.Category.assoc, id_eq
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
b : α
refine_2 :
  Eq (α := Limits.pullback g' (Sigma.ι X₁ b) ⟶ B₁) (pullback.snd g' (Sigma.ι X₁ b) ≫ π₁ b)
    (CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} X₁) (pullback.snd g' (Sigma.ι X₁ b) ≫ Sigma.ι X₁ b)
      (Sigma.desc π₁))
⊢ Eq (α := Limits.pullback g' (Sigma.ι X₁ b) ⟶ B₁) (pullback.snd g' (Sigma.ι X₁ b) ≫ π₁ b)
    (pullback.fst g' (Sigma.ι X₁ b) ≫ g' ≫ Sigma.desc π₁)

Tactic:
rw [← Category.assoc, pullback.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : FinitaryPreExtensive.{v_1, u_1} C
inst_2 : Preregular.{v_1, u_1} C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
h_1 : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w : EffectiveEpi g
g' : Y ⟶ sigmaObj.{0, v_1, u_1} X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : (a : α) → C := fun (a : α) ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun (a : α) ↦ pullback.fst g' (Sigma.ι X₁ a)
h_2 :
  IsIso.{v_1, u_1} (C := C) (X := sigmaObj.{0, v_1, u_1} fun (x : α) ↦ Limits.pullback g' (Sigma.ι X₁ x)) (Y := Y)
    (Sigma.desc fun (x : α) ↦ pullback.fst g' (Sigma.ι X₁ x))
b : α
⊢ Eq (α := Limits.pullback g' (Sigma.ι X₁ b) ⟶ B₁) (pullback.snd g' (Sigma.ι X₁ b) ≫ π₁ b)
    (CategoryStruct.comp (Y := sigmaObj.{0, v_1, u_1} X₁) (pullback.snd g' (Sigma.ι X₁ b) ≫ Sigma.ι X₁ b)
      (Sigma.desc π₁))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
h :
  ∀ (B : C) (S : Sieve.{v_1, u_1} B),
    S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B ↔
      S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B
⊢ Eq (α := GrothendieckTopology.{v_1, u_1} C) (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C))
    (coherentTopology C)

Tactic:
ext B S
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
⊢ S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B ↔
    S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preregular.{v_1, u_1} C
inst_2 : FinitaryPreExtensive.{v_1, u_1} C
B : C
S : Sieve.{v_1, u_1} B
h :
  ∀ (h : S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B),
    S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B
h₁ :
  ∀ (h : S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B),
    S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B
⊢ S ∈ (Coverage.toGrothendieck (extensiveCoverage C ⊔ regularCoverage C) : (a : C) → Set (Sieve a)) B ↔
    S ∈ (coherentTopology C : (a : C) → Set (Sieve a)) B

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩