-- Mathlib/Order/Category/NonemptyFinLinOrd.lean
theorem mono_iff_injective {A B : NonemptyFinLinOrd.{u}} (f : A ⟶ B) :
    Mono f ↔ Function.Injective f

Proof state:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
x✝² x✝¹ : ULift.{u, 0} (Fin 1)
x✝ : x✝² ≤ x✝¹
⊢ (fun x => a₁) x✝² ≤ (fun x => a₁) x✝¹

Tactic:
rfl

Result:
no goals

Proof state:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
⊢ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
intro a₁ a₂ h

Result:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
⊢ a₁ = a₂

Proof state:
A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Mono f → Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
intro

Result:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
⊢ Function.Injective ⇑(ConcreteCategory.hom f)

Proof state:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{?u.28183, 0} (Fin 1))
⊢ a₁ = a₂

Tactic:
let g₁ : X ⟶ A := ofHom ⟨fun _ => a₁, fun _ _ _ => by rfl⟩

Result:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x => a₁, monotone' := ⋯ }
⊢ a₁ = a₂

Proof state:
A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
refine ⟨?_, ConcreteCategory.mono_of_injective f⟩

Result:
A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Mono f → Function.Injective ⇑(ConcreteCategory.hom f)

Proof state:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x => a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x => a₂, monotone' := ⋯ }
⊢ a₁ = a₂

Tactic:
change g₁ (ULift.up (0 : Fin 1)) = g₂ (ULift.up (0 : Fin 1))

Result:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x => a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x => a₂, monotone' := ⋯ }
⊢ (ConcreteCategory.hom g₁) { down := 0 } = (ConcreteCategory.hom g₂) { down := 0 }

Proof state:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x => a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x => a₂, monotone' := ⋯ }
⊢ (ConcreteCategory.hom g₁) { down := 0 } = (ConcreteCategory.hom g₂) { down := 0 }

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

Result:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x => a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x => a₂, monotone' := ⋯ }
eq : g₁ ≫ f = g₂ ≫ f
⊢ (ConcreteCategory.hom g₁) { down := 0 } = (ConcreteCategory.hom g₂) { down := 0 }

Proof state:
case hf.h.h
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x => a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x => a₂, monotone' := ⋯ }
x✝ : ↑X.toLinOrd
⊢ (LinOrd.Hom.hom (g₁ ≫ f)) x✝ = (LinOrd.Hom.hom (g₂ ≫ f)) x✝

Tactic:
exact h

Result:
no goals

Proof state:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x => a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x => a₂, monotone' := ⋯ }
eq : g₁ ≫ f = g₂ ≫ f
⊢ (ConcreteCategory.hom g₁) { down := 0 } = (ConcreteCategory.hom g₂) { down := 0 }

Tactic:
rw [cancel_mono] at eq

Result:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x => a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x => a₂, monotone' := ⋯ }
eq : g₁ = g₂
⊢ (ConcreteCategory.hom g₁) { down := 0 } = (ConcreteCategory.hom g₂) { down := 0 }

Proof state:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x => a₁, monotone' := ⋯ }
x✝² x✝¹ : ULift.{u, 0} (Fin 1)
x✝ : x✝² ≤ x✝¹
⊢ (fun x => a₂) x✝² ≤ (fun x => a₂) x✝¹

Tactic:
rfl

Result:
no goals

Proof state:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x => a₁, monotone' := ⋯ }
⊢ a₁ = a₂

Tactic:
let g₂ : X ⟶ A := ofHom ⟨fun _ => a₂, fun _ _ _ => by rfl⟩

Result:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x => a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x => a₂, monotone' := ⋯ }
⊢ a₁ = a₂

Proof state:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
⊢ a₁ = a₂

Tactic:
let X := of (ULift (Fin 1))

Result:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{?u.28183, 0} (Fin 1))
⊢ a₁ = a₂

Proof state:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x => a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x => a₂, monotone' := ⋯ }
eq : g₁ = g₂
⊢ (ConcreteCategory.hom g₁) { down := 0 } = (ConcreteCategory.hom g₂) { down := 0 }

Tactic:
rw [eq]

Result:
no goals

Proof state:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x => a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x => a₂, monotone' := ⋯ }
⊢ g₁ ≫ f = g₂ ≫ f

Tactic:
ext

Result:
case hf.h.h
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x => a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x => a₂, monotone' := ⋯ }
x✝ : ↑X.toLinOrd
⊢ (LinOrd.Hom.hom (g₁ ≫ f)) x✝ = (LinOrd.Hom.hom (g₂ ≫ f)) x✝