-- Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
theorem EqualizerCondition.mk (P : Cᵒᵖ ⥤ Type*)
    (hP : ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [HasPullback π π], Function.Bijective
    (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π)
    pullback.condition)) : EqualizerCondition P

Proof state:
case intro.intro
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP :
  ∀ (b : ↑{x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}),
    ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = b
b : P.obj (op X)
hb : P.map c.fst.op b = P.map c.snd.op b
h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π
hb' : P.map (pullback.fst π π).op b = P.map (pullback.snd π π).op b
a : P.obj (op B)
ha₁ : MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb'⟩
ha₂ : ∀ (y : P.obj (op B)), (fun a => MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb'⟩) y → y = a
⊢ ∃! x, P.map π.op x = b

Tactic:
refine ⟨a, ?_, ?_⟩

Result:
case intro.intro.refine_1
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP :
  ∀ (b : ↑{x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}),
    ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = b
b : P.obj (op X)
hb : P.map c.fst.op b = P.map c.snd.op b
h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π
hb' : P.map (pullback.fst π π).op b = P.map (pullback.snd π π).op b
a : P.obj (op B)
ha₁ : MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb'⟩
ha₂ : ∀ (y : P.obj (op B)), (fun a => MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb'⟩) y → y = a
⊢ (fun x => P.map π.op x = b) a

case intro.intro.refine_2
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP :
  ∀ (b : ↑{x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}),
    ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = b
b : P.obj (op X)
hb : P.map c.fst.op b = P.map c.snd.op b
h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π
hb' : P.map (pullback.fst π π).op b = P.map (pullback.snd π π).op b
a : P.obj (op B)
ha₁ : MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb'⟩
ha₂ : ∀ (y : P.obj (op B)), (fun a => MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb'⟩) y → y = a
⊢ ∀ (y : P.obj (op B)), (fun x => P.map π.op x = b) y → y = a

Proof state:
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP :
  ∀ (b : ↑{x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}),
    ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = b
b : P.obj (op X)
hb : P.map c.fst.op b = P.map c.snd.op b
⊢ ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP :
  ∀ (X B : C) (π : X ⟶ B) [inst : EffectiveEpi π] [inst : HasPullback π π],
    Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)
⊢ EqualizerCondition P

Tactic:
intro X B π _ c hc

Result:
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP :
  ∀ (X B : C) (π : X ⟶ B) [inst : EffectiveEpi π] [inst : HasPullback π π],
    Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ Nonempty (IsLimit (Fork.ofι (P.map π.op) ⋯))

Proof state:
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP :
  ∀ (X B : C) (π : X ⟶ B) [inst : EffectiveEpi π] [inst : HasPullback π π],
    Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ Nonempty (IsLimit (Fork.ofι (P.map π.op) ⋯))

Tactic:
have : HasPullback π π := ⟨c, hc⟩

Result:
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP :
  ∀ (X B : C) (π : X ⟶ B) [inst : EffectiveEpi π] [inst : HasPullback π π],
    Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
⊢ Nonempty (IsLimit (Fork.ofι (P.map π.op) ⋯))

Proof state:
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP :
  ∀ (b : ↑{x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}),
    ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = b
b : P.obj (op X)
hb : P.map c.fst.op b = P.map c.snd.op b
h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π
⊢ ∃! x, P.map π.op x = b

Tactic:
have hb' : P.map (pullback.fst π π).op b = P.map (pullback.snd _ _).op b := by
  rw [← h₁, op_comp, FunctorToTypes.map_comp_apply, hb]
  simp [← FunctorToTypes.map_comp_apply, ← op_comp]

Result:
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP :
  ∀ (b : ↑{x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}),
    ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = b
b : P.obj (op X)
hb : P.map c.fst.op b = P.map c.snd.op b
h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π
hb' : P.map (pullback.fst π π).op b = P.map (pullback.snd π π).op b
⊢ ∃! x, P.map π.op x = b

Proof state:
case intro.intro.refine_1
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP :
  ∀ (b : ↑{x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}),
    ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = b
b : P.obj (op X)
hb : P.map c.fst.op b = P.map c.snd.op b
h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π
hb' : P.map (pullback.fst π π).op b = P.map (pullback.snd π π).op b
a : P.obj (op B)
ha₁ : MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb'⟩
ha₂ : ∀ (y : P.obj (op B)), (fun a => MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb'⟩) y → y = a
⊢ (fun x => P.map π.op x = b) a

Tactic:
simpa [MapToEqualizer] using ha₁

Result:
no goals

Proof state:
case intro.intro.refine_2
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP :
  ∀ (b : ↑{x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}),
    ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = b
b : P.obj (op X)
hb : P.map c.fst.op b = P.map c.snd.op b
h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π
hb' : P.map (pullback.fst π π).op b = P.map (pullback.snd π π).op b
a : P.obj (op B)
ha₁ : MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb'⟩
ha₂ : ∀ (y : P.obj (op B)), (fun a => MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb'⟩) y → y = a
⊢ ∀ (y : P.obj (op B)), (fun x => P.map π.op x = b) y → y = a

Tactic:
simpa [MapToEqualizer] using ha₂

Result:
no goals