A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Mono f → Function.Injective ↑f
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Mono f ↔ Function.Injective ↑f
refine' ⟨_, ConcreteCategory.mono_of_injective f⟩
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
⊢ Function.Injective ↑f
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Mono f → Function.Injective ↑f
intro
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
⊢ a₁ = a₂
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
⊢ Function.Injective ↑f
intro a₁ a₂ h
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
⊢ a₁ = a₂
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
⊢ a₁ = a₂
let X := NonemptyFinLinOrdCat.of (ULift (Fin 1))
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
⊢ a₁ = a₂
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
⊢ a₁ = a₂
let g₁ : X ⟶ A := ⟨fun _ => a₁, fun _ _  _ => by rfl⟩
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
⊢ a₁ = a₂
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
⊢ a₁ = a₂
let g₂ : X ⟶ A := ⟨fun _ => a₂, fun _ _  _ => by rfl⟩
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
⊢ ↑g₁ { down := 0 } = ↑g₂ { down := 0 }
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
⊢ a₁ = a₂
change g₁ (ULift.up (0 : Fin 1)) = g₂ (ULift.up (0 : Fin 1))
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
eq : g₁ ≫ f = g₂ ≫ f
⊢ ↑g₁ { down := 0 } = ↑g₂ { down := 0 }
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
⊢ ↑g₁ { down := 0 } = ↑g₂ { down := 0 }
have eq : g₁ ≫ f = g₂ ≫ f := by
  ext
  exact h
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
eq : g₁ = g₂
⊢ ↑g₁ { down := 0 } = ↑g₂ { down := 0 }
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
eq : g₁ ≫ f = g₂ ≫ f
⊢ ↑g₁ { down := 0 } = ↑g₂ { down := 0 }
rw [cancel_mono] at eq
no goals
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
eq : g₁ = g₂
⊢ ↑g₁ { down := 0 } = ↑g₂ { down := 0 }
rw [eq]
no goals
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
x✝² x✝¹ : ↑X
x✝ : x✝² ≤ x✝¹
⊢ (fun x => a₁) x✝² ≤ (fun x => a₁) x✝¹
rfl
no goals
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
x✝² x✝¹ : ↑X
x✝ : x✝² ≤ x✝¹
⊢ (fun x => a₂) x✝² ≤ (fun x => a₂) x✝¹
rfl
case w
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
x✝ : (forget NonemptyFinLinOrdCat).obj X
⊢ (forget NonemptyFinLinOrdCat).map (g₁ ≫ f) x✝ = (forget NonemptyFinLinOrdCat).map (g₂ ≫ f) x✝
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
⊢ g₁ ≫ f = g₂ ≫ f
ext
no goals
case w
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
x✝ : (forget NonemptyFinLinOrdCat).obj X
⊢ (forget NonemptyFinLinOrdCat).map (g₁ ≫ f) x✝ = (forget NonemptyFinLinOrdCat).map (g₂ ≫ f) x✝
exact h