-- Mathlib/CategoryTheory/Subpresheaf/Equalizer.lean
lemma equalizer_eq_iff :
    Subpresheaf.equalizer f g = A ↔ f = g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
this : A ≤ Subpresheaf.equalizer f g ↔ f = g
⊢ Subpresheaf.equalizer f g = A ↔ f = g

Tactic:
rw [← this]

Result:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
this : A ≤ Subpresheaf.equalizer f g ↔ f = g
⊢ Subpresheaf.equalizer f g = A ↔ A ≤ Subpresheaf.equalizer f g

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
this : A ≤ Subpresheaf.equalizer f g ↔ f = g
h : Subpresheaf.equalizer f g = A
⊢ A ≤ Subpresheaf.equalizer f g

Tactic:
rw [h]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
⊢ Subpresheaf.equalizer f g = A ↔ f = g

Tactic:
have := range_le_equalizer_iff f g (𝟙 _)

Result:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
this : range (𝟙 A.toPresheaf ≫ A.ι) ≤ Subpresheaf.equalizer f g ↔ 𝟙 A.toPresheaf ≫ f = 𝟙 A.toPresheaf ≫ g
⊢ Subpresheaf.equalizer f g = A ↔ f = g

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
this : A ≤ Subpresheaf.equalizer f g ↔ f = g
⊢ Subpresheaf.equalizer f g = A → A ≤ Subpresheaf.equalizer f g

Tactic:
intro h

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
this : A ≤ Subpresheaf.equalizer f g ↔ f = g
h : Subpresheaf.equalizer f g = A
⊢ A ≤ Subpresheaf.equalizer f g

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
this : A ≤ Subpresheaf.equalizer f g ↔ f = g
h : A ≤ Subpresheaf.equalizer f g
⊢ Subpresheaf.equalizer f g = A

Tactic:
exact le_antisymm (equalizer_le f g) h

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
this : range (𝟙 A.toPresheaf ≫ A.ι) ≤ Subpresheaf.equalizer f g ↔ 𝟙 A.toPresheaf ≫ f = 𝟙 A.toPresheaf ≫ g
⊢ Subpresheaf.equalizer f g = A ↔ f = g

Tactic:
simp only [Category.id_comp, range_ι] at this

Result:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
this : A ≤ Subpresheaf.equalizer f g ↔ f = g
⊢ Subpresheaf.equalizer f g = A ↔ f = g

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
this : A ≤ Subpresheaf.equalizer f g ↔ f = g
⊢ A ≤ Subpresheaf.equalizer f g → Subpresheaf.equalizer f g = A

Tactic:
intro h

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
this : A ≤ Subpresheaf.equalizer f g ↔ f = g
h : A ≤ Subpresheaf.equalizer f g
⊢ Subpresheaf.equalizer f g = A

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
this : A ≤ Subpresheaf.equalizer f g ↔ f = g
⊢ Subpresheaf.equalizer f g = A ↔ A ≤ Subpresheaf.equalizer f g

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
this : A ≤ Subpresheaf.equalizer f g ↔ f = g
⊢ Subpresheaf.equalizer f g = A → A ≤ Subpresheaf.equalizer f g

case mpr
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
this : A ≤ Subpresheaf.equalizer f g ↔ f = g
⊢ A ≤ Subpresheaf.equalizer f g → Subpresheaf.equalizer f g = A