-- Mathlib/Condensed/Discrete/LocallyConstant.lean
/--
To check equality of two elements of `X(S)`, it suffices to check equality after composing with
each `X(S) → X(Sᵢ)`.
-/
lemma presheaf_ext (X : (CompHausLike.{u} P)ᵒᵖ ⥤ Type max u w)
    [PreservesFiniteProducts X] (x y : X.obj ⟨S⟩)
    [HasExplicitFiniteCoproducts.{u} P]
    (h : ∀ (a : Fiber f), X.map (sigmaIncl f a).op x = X.map (sigmaIncl f a).op y) : x = y

Proof state:
case a.a.h
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
h : X.map (sigmaIncl f a).op x = X.map (sigmaIncl f a).op y
⊢ sigmaComparison X (fun a => ↑(fiber f a).toTop) ((X.mapIso (sigmaIso f).op).hom x) a =
    sigmaComparison X (fun a => ↑(fiber f a).toTop) ((X.mapIso (sigmaIso f).op).hom y) a

Tactic:
rw [← sigmaComparison_comp_sigmaIso] at h

Result:
case a.a.h
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
h :
  ((X.mapIso (sigmaIso f).op).hom ≫ (sigmaComparison X fun a => ↑(fiber f a).toTop) ≫ fun g => g a) x =
    ((X.mapIso (sigmaIso f).op).hom ≫ (sigmaComparison X fun a => ↑(fiber f a).toTop) ≫ fun g => g a) y
⊢ sigmaComparison X (fun a => ↑(fiber f a).toTop) ((X.mapIso (sigmaIso f).op).hom x) a =
    sigmaComparison X (fun a => ↑(fiber f a).toTop) ((X.mapIso (sigmaIso f).op).hom y) a

Proof state:
case a.a
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
h : ∀ (a : Fiber ⇑f), X.map (sigmaIncl f a).op x = X.map (sigmaIncl f a).op y
⊢ sigmaComparison X (fun a => ↑(fiber f a).toTop) ((X.mapIso (sigmaIso f).op).hom x) =
    sigmaComparison X (fun a => ↑(fiber f a).toTop) ((X.mapIso (sigmaIso f).op).hom y)

Tactic:
ext a

Result:
case a.a.h
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
h : ∀ (a : Fiber ⇑f), X.map (sigmaIncl f a).op x = X.map (sigmaIncl f a).op y
a : Fiber ⇑f
⊢ sigmaComparison X (fun a => ↑(fiber f a).toTop) ((X.mapIso (sigmaIso f).op).hom x) a =
    sigmaComparison X (fun a => ↑(fiber f a).toTop) ((X.mapIso (sigmaIso f).op).hom y) a

Proof state:
case a.a.h
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
h : ∀ (a : Fiber ⇑f), X.map (sigmaIncl f a).op x = X.map (sigmaIncl f a).op y
a : Fiber ⇑f
⊢ sigmaComparison X (fun a => ↑(fiber f a).toTop) ((X.mapIso (sigmaIso f).op).hom x) a =
    sigmaComparison X (fun a => ↑(fiber f a).toTop) ((X.mapIso (sigmaIso f).op).hom y) a

Tactic:
specialize h a

Result:
case a.a.h
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
h : X.map (sigmaIncl f a).op x = X.map (sigmaIncl f a).op y
⊢ sigmaComparison X (fun a => ↑(fiber f a).toTop) ((X.mapIso (sigmaIso f).op).hom x) a =
    sigmaComparison X (fun a => ↑(fiber f a).toTop) ((X.mapIso (sigmaIso f).op).hom y) a

Proof state:
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
h : ∀ (a : Fiber ⇑f), X.map (sigmaIncl f a).op x = X.map (sigmaIncl f a).op y
⊢ x = y

Tactic:
apply injective_of_mono (X.mapIso (sigmaIso f).op).hom

Result:
case a
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
h : ∀ (a : Fiber ⇑f), X.map (sigmaIncl f a).op x = X.map (sigmaIncl f a).op y
⊢ (X.mapIso (sigmaIso f).op).hom x = (X.mapIso (sigmaIso f).op).hom y

Proof state:
case a
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
h : ∀ (a : Fiber ⇑f), X.map (sigmaIncl f a).op x = X.map (sigmaIncl f a).op y
⊢ (X.mapIso (sigmaIso f).op).hom x = (X.mapIso (sigmaIso f).op).hom y

Tactic:
apply injective_of_mono (sigmaComparison X (fun a ↦ (fiber f a).1))

Result:
case a.a
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
h : ∀ (a : Fiber ⇑f), X.map (sigmaIncl f a).op x = X.map (sigmaIncl f a).op y
⊢ sigmaComparison X (fun a => ↑(fiber f a).toTop) ((X.mapIso (sigmaIso f).op).hom x) =
    sigmaComparison X (fun a => ↑(fiber f a).toTop) ((X.mapIso (sigmaIso f).op).hom y)

Proof state:
case a.a.h
P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝¹ : PreservesFiniteProducts X
x y : X.obj (op S)
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
h :
  ((X.mapIso (sigmaIso f).op).hom ≫ (sigmaComparison X fun a => ↑(fiber f a).toTop) ≫ fun g => g a) x =
    ((X.mapIso (sigmaIso f).op).hom ≫ (sigmaComparison X fun a => ↑(fiber f a).toTop) ≫ fun g => g a) y
⊢ sigmaComparison X (fun a => ↑(fiber f a).toTop) ((X.mapIso (sigmaIso f).op).hom x) a =
    sigmaComparison X (fun a => ↑(fiber f a).toTop) ((X.mapIso (sigmaIso f).op).hom y) a

Tactic:
exact h

Result:
no goals