-- Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
theorem equalizerCondition_iff_isIso_lift (P : Cᵒᵖ ⥤ Type*) : EqualizerCondition P ↔
    ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [HasPullback π π],
      IsIso (equalizer.lift (P.map π.op) (equalizerCondition_w' P π))

Proof state:
case mpr
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 π π], IsIso (equalizer.lift (P.map π.op) ⋯)
⊢ EqualizerCondition P

Tactic:
apply EqualizerCondition.mk

Result:
case mpr.hP
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 π π], IsIso (equalizer.lift (P.map π.op) ⋯)
⊢ ∀ (X B : C) (π : X ⟶ B) [inst : EffectiveEpi π] [inst : HasPullback π π],
    Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)

Proof state:
case mp
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 π π
h : Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)
⊢ IsIso (equalizer.lift (P.map π.op) ⋯)

Tactic:
rw [← isIso_iff_bijective, mapToEqualizer_eq_comp] at h

Result:
case mp
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 π π
h :
  IsIso
    (equalizer.lift (P.map π.op) ⋯ ≫
      (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).hom)
⊢ IsIso (equalizer.lift (P.map π.op) ⋯)

Proof state:
case mpr.hP
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 π π], IsIso (equalizer.lift (P.map π.op) ⋯)
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
⊢ IsIso
    (equalizer.lift (P.map π.op) ⋯ ≫
      (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).hom)

Tactic:
infer_instance

Result:
no goals

Proof state:
case mpr.hP
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 π π], IsIso (equalizer.lift (P.map π.op) ⋯)
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
⊢ Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)

Tactic:
rw [mapToEqualizer_eq_comp, ← isIso_iff_bijective]

Result:
case mpr.hP
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 π π], IsIso (equalizer.lift (P.map π.op) ⋯)
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
⊢ IsIso
    (equalizer.lift (P.map π.op) ⋯ ≫
      (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).hom)

Proof state:
case mpr
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 π π], IsIso (equalizer.lift (P.map π.op) ⋯)) →
    EqualizerCondition P

Tactic:
intro hP

Result:
case mpr
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 π π], IsIso (equalizer.lift (P.map π.op) ⋯)
⊢ EqualizerCondition P

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
⊢ EqualizerCondition P →
    ∀ (X B : C) (π : X ⟶ B) [inst : EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)

Tactic:
intro hP X B π _ _

Result:
case mp
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 π π
⊢ IsIso (equalizer.lift (P.map π.op) ⋯)

Proof state:
case mp
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 π π
⊢ IsIso (equalizer.lift (P.map π.op) ⋯)

Tactic:
have h := hP.bijective_mapToEqualizer_pullback _ X B π

Result:
case mp
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 π π
h : Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)
⊢ IsIso (equalizer.lift (P.map π.op) ⋯)

Proof state:
case mp
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 π π
h :
  IsIso
    (equalizer.lift (P.map π.op) ⋯ ≫
      (Types.equalizerIso (P.map (pullback.fst π π).op) (P.map (pullback.snd π π).op)).hom)
⊢ IsIso (equalizer.lift (P.map π.op) ⋯)

Tactic:
exact IsIso.of_isIso_comp_right (equalizer.lift (P.map π.op)
  (equalizerCondition_w' P π))
  (Types.equalizerIso _ _).hom

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
⊢ EqualizerCondition P ↔
    ∀ (X B : C) (π : X ⟶ B) [inst : EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
⊢ EqualizerCondition P →
    ∀ (X B : C) (π : X ⟶ B) [inst : EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)

case mpr
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 π π], IsIso (equalizer.lift (P.map π.op) ⋯)) →
    EqualizerCondition P

Proof state:
case mpr.hP
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 π π], IsIso (equalizer.lift (P.map π.op) ⋯)
⊢ ∀ (X B : C) (π : X ⟶ B) [inst : EffectiveEpi π] [inst : HasPullback π π],
    Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)

Tactic:
intro X B π _ _

Result:
case mpr.hP
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 π π], IsIso (equalizer.lift (P.map π.op) ⋯)
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
⊢ Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)