-- Mathlib/Topology/Category/CompHausLike/Basic.lean
theorem mono_iff_injective {X Y : CompHausLike.{u} P} (f : X ⟶ Y) :
    Mono f ↔ Function.Injective f

Proof state:
case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : ↑X.toTop
h : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) x₂
⊢ x₁ = x₂

Tactic:
let g₁ : X ⟶ X := ofHom _ ⟨fun _ => x₁, continuous_const⟩

Result:
case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : ↑X.toTop
h : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) x₂
g₁ : X ⟶ X := ofHom P { toFun := fun x => x₁, continuous_toFun := ⋯ }
⊢ x₁ = x₂

Proof state:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
constructor

Result:
case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Mono f → Function.Injective ⇑(ConcreteCategory.hom f)

case mpr
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Function.Injective ⇑(ConcreteCategory.hom f) → Mono f

Proof state:
case mpr
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Function.Injective ⇑(ConcreteCategory.hom f) → Mono f

Tactic:
rw [← CategoryTheory.mono_iff_injective]

Result:
case mpr
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Mono ⇑(ConcreteCategory.hom f) → Mono f

Proof state:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : ↑X.toTop
h : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) x₂
g₁ : X ⟶ X := ofHom P { toFun := fun x => x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun x => x₂, continuous_toFun := ⋯ }
⊢ g₁ ≫ f = g₂ ≫ f

Tactic:
ext

Result:
case h.h
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : ↑X.toTop
h : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) x₂
g₁ : X ⟶ X := ofHom P { toFun := fun x => x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun x => x₂, continuous_toFun := ⋯ }
a✝ : ↑X.toTop
⊢ (ConcreteCategory.hom (g₁ ≫ f)) a✝ = (ConcreteCategory.hom (g₂ ≫ f)) a✝

Proof state:
case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : ↑X.toTop
h : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) x₂
g₁ : X ⟶ X := ofHom P { toFun := fun x => x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun x => x₂, continuous_toFun := ⋯ }
⊢ x₁ = x₂

Tactic:
have : g₁ ≫ f = g₂ ≫ f := by ext; exact h

Result:
case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : ↑X.toTop
h : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) x₂
g₁ : X ⟶ X := ofHom P { toFun := fun x => x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun x => x₂, continuous_toFun := ⋯ }
this : g₁ ≫ f = g₂ ≫ f
⊢ x₁ = x₂

Proof state:
case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : ↑X.toTop
h : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) x₂
g₁ : X ⟶ X := ofHom P { toFun := fun x => x₁, continuous_toFun := ⋯ }
⊢ x₁ = x₂

Tactic:
let g₂ : X ⟶ X := ofHom _ ⟨fun _ => x₂, continuous_const⟩

Result:
case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : ↑X.toTop
h : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) x₂
g₁ : X ⟶ X := ofHom P { toFun := fun x => x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun x => x₂, continuous_toFun := ⋯ }
⊢ x₁ = x₂

Proof state:
case mpr
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Mono ⇑(ConcreteCategory.hom f) → Mono f

Tactic:
apply (forget (CompHausLike P)).mono_of_mono_map

Result:
no goals

Proof state:
case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Mono f → Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
intro hf x₁ x₂ h

Result:
case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : ↑X.toTop
h : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) x₂
⊢ x₁ = x₂

Proof state:
case h.h
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : ↑X.toTop
h : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) x₂
g₁ : X ⟶ X := ofHom P { toFun := fun x => x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun x => x₂, continuous_toFun := ⋯ }
a✝ : ↑X.toTop
⊢ (ConcreteCategory.hom (g₁ ≫ f)) a✝ = (ConcreteCategory.hom (g₂ ≫ f)) a✝

Tactic:
exact h

Result:
no goals

Proof state:
case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : ↑X.toTop
h : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) x₂
g₁ : X ⟶ X := ofHom P { toFun := fun x => x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun x => x₂, continuous_toFun := ⋯ }
this : g₁ ≫ f = g₂ ≫ f
⊢ x₁ = x₂

Tactic:
exact CategoryTheory.congr_fun ((cancel_mono _).mp this) x₁

Result:
no goals