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

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 π
inst✝ : HasPullback π π
hP :
  ∀ (y : P.obj (op X)),
    P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).fst.op y =
        P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).snd.op y →
      ∃! x, P.map π.op x = y
⊢ ∀ (b : ↑{x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}),
    ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = b

Tactic:
intro ⟨b, hb⟩

Result:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
hP :
  ∀ (y : P.obj (op X)),
    P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).fst.op y =
        P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).snd.op y →
      ∃! x, P.map π.op x = y
b : P.obj (op X)
hb : b ∈ {x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}
⊢ ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb⟩

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 π
inst✝ : HasPullback π π
hP :
  ∀ (y : P.obj (op X)),
    P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).fst.op y =
        P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).snd.op y →
      ∃! x, P.map π.op x = y
b : P.obj (op X)
hb : b ∈ {x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}
⊢ ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb⟩

Tactic:
obtain ⟨a, ha₁, ha₂⟩ := hP b hb

Result:
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 π
inst✝ : HasPullback π π
hP :
  ∀ (y : P.obj (op X)),
    P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).fst.op y =
        P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).snd.op y →
      ∃! x, P.map π.op x = y
b : P.obj (op X)
hb : b ∈ {x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}
a : P.obj (op B)
ha₁ : P.map π.op a = b
ha₂ : ∀ (y : P.obj (op B)), (fun x => P.map π.op x = b) y → y = a
⊢ ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb⟩

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 π
inst✝ : HasPullback π π
hP :
  ∀ (y : P.obj (op X)),
    P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).fst.op y =
        P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).snd.op y →
      ∃! x, P.map π.op x = y
b : P.obj (op X)
hb : b ∈ {x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}
a : P.obj (op B)
ha₁ : P.map π.op a = b
ha₂ : ∀ (y : P.obj (op B)), (fun x => P.map π.op x = b) y → y = a
⊢ ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb⟩

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 π
inst✝ : HasPullback π π
hP :
  ∀ (y : P.obj (op X)),
    P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).fst.op y =
        P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).snd.op y →
      ∃! x, P.map π.op x = y
b : P.obj (op X)
hb : b ∈ {x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}
a : P.obj (op B)
ha₁ : P.map π.op a = b
ha₂ : ∀ (y : P.obj (op B)), (fun x => P.map π.op x = b) y → y = a
⊢ (fun a => MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb⟩) 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 π
inst✝ : HasPullback π π
hP :
  ∀ (y : P.obj (op X)),
    P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).fst.op y =
        P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).snd.op y →
      ∃! x, P.map π.op x = y
b : P.obj (op X)
hb : b ∈ {x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}
a : P.obj (op B)
ha₁ : P.map π.op a = b
ha₂ : ∀ (y : P.obj (op B)), (fun x => P.map π.op x = b) y → y = a
⊢ ∀ (y : P.obj (op B)), (fun a => MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb⟩) y → y = a

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 π
inst✝ : HasPullback π π
hP :
  ∀ (y : P.obj (op X)),
    P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).fst.op y =
        P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).snd.op y →
      ∃! x, P.map π.op x = y
b : P.obj (op X)
hb : b ∈ {x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}
a : P.obj (op B)
ha₁ : P.map π.op a = b
ha₂ : ∀ (y : P.obj (op B)), (fun x => P.map π.op x = b) y → y = a
⊢ ∀ (y : P.obj (op B)), (fun a => MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb⟩) y → y = a

Tactic:
simpa [MapToEqualizer] using ha₂

Result:
no goals

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

Tactic:
intro X B π _ _

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

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 π
inst✝ : HasPullback π π
hP : Nonempty (IsLimit (Fork.ofι (P.map π.op) ⋯))
⊢ Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)

Tactic:
rw [Types.type_equalizer_iff_unique] at hP

Result:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
hP :
  ∀ (y : P.obj (op X)),
    P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).fst.op y =
        P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).snd.op y →
      ∃! x, P.map π.op x = y
⊢ Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)

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 π
inst✝ : HasPullback π π
hP :
  ∀ (y : P.obj (op X)),
    P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).fst.op y =
        P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).snd.op y →
      ∃! x, P.map π.op x = y
b : P.obj (op X)
hb : b ∈ {x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}
a : P.obj (op B)
ha₁ : P.map π.op a = b
ha₂ : ∀ (y : P.obj (op B)), (fun x => P.map π.op x = b) y → y = a
⊢ (fun a => MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = ⟨b, hb⟩) a

Tactic:
simpa [MapToEqualizer] using ha₁

Result:
no goals